Name
Abstract | ||
|---|---|---|
Propositional satisfiability (SAT) has been widely used in hardware and software verification. Outsourcing complex SAT problem to Cloud can leverage the huge computation capability and flexibility of Cloud. But some confidential information encoded in CNF formula, such as circuit structure, may be leaked to unauthorized third party.In this paper, we propose a novel Cloud-oriented SAT solving algorithm to preserve privacy. First, an obfuscated CNF formula is generated by embedding a Husk formula into the original formula with proper rules. Second, the obfuscated formula is solved by a state-of-the-art SAT solver deployed in Cloud. Third, a simple mapping algorithm is used to map the solution of the obfuscated formula back to that of the original CNF formula.Theoretical analysis and experimental result show that our algorithms can significantly improve security of the SAT solver with linear complexity while keeping its solution space unchanged. |
Year | DOI | Venue |
|---|---|---|
2014 | 10.1007/978-3-319-11119-3_18 | WEB TECHNOLOGIES AND APPLICATIONS, APWEB 2014, PT II |
Keywords | Field | DocType |
SAT solver, CNF formula, Privacy, Obfuscating, Cloud computing | #SAT,Computer science,Boolean satisfiability problem,Satisfiability,Outsourcing,Third party,Theoretical computer science,Software verification,Cloud computing,Computation | Conference |
Volume | ISSN | Citations |
8710 | 0302-9743 | 2 |
PageRank | References | Authors |
0.36 | 12 | 4 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Ying Qin | 1 | 30 | 4.39 |
| Shengyu Shen | 2 | 83 | 10.06 |
| Jingzhu Kong | 3 | 2 | 0.36 |
| Huadong Dai | 4 | 4 | 2.77 |