Top

Published in:

2018 | OriginalPaper | Chapter

Privacy-Preserving SAT Solving Based on Projection-Equivalence CNF Obfuscation

Authors : Ying Qin, Xiao Yang Shen, Zhen Yue Du

Published in: Cyberspace Safety and Security

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

In this paper, we study the problem of privacy-preserving SAT solving in the cloud computing paradigm. we present a CNF obfuscation algorithm and its corresponding solution recovery algorithm, to prevent unauthorized third party obtaining sensitive information. By obfuscation, the CNF formula is transformed into another formula with different circuit structure and projection-equivalence over-approximated solution space. Solution of the original CNF can be extracted from the solution of obfuscated CNF by projection based solution recovery algorithm. Theoretical analysis demonstrates that, obfuscation algorithm can change the structure of CNF formula with polynomial time complexity, while solution recovery algorithm can filter out solution with linear time complexity.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

previous chapter Towards the Blockchain Technology for System Voting Process

next chapter A Fragile Watermarking and Bilinear Fuzzy Equations

Davis, M., Putnam, H.: A computing procedure for quantification theory. J. ACM 7(3), 201–215 (1960)MathSciNetCrossRef

Hachtel, G., Somenzi, F.: Logic Synthesis and Verification Algorithms, vol. I-XXIII, pp. 1–564. Springer, Heidelberg (2006)MATH

Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154–169. Springer, Heidelberg (2000). https://doi.org/10.1007/10722167_15CrossRef

Soos, M., Nohl, K., Castelluccia, C.: Extending SAT solvers to cryptographic problems. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 244–257. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-02777-2_24CrossRef

Hyvärinen, A.E.J., Junttila, T., Niemelä, I.: Grid-based SAT solving with iterative partitioning and clause learning. In: Lee, J. (ed.) CP 2011. LNCS, vol. 6876, pp. 385–399. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-23786-7_30CrossRef

Tseitin, G.: On the complexity of derivation in propositional calculus. Stud. Constr. Math. Math. Logic (1968)

Li, C.: Integrating equivalency reasoning into Davis-Putnam procedure. In: AAAI/IAAI 2000, pp. 291–296 (2000)

Ostrowski, R., Grégoire, É., Mazure, B., Saïs, L.: Recovering and exploiting structural knowledge from CNF formulas. In: Van Hentenryck, P. (ed.) CP 2002. LNCS, vol. 2470, pp. 185–199. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-46135-3_13CrossRef

Roy, J., Markov, I., Bertacco, V.: Restoring circuit structure from SAT instances. In: IWLS 2004, pp. 361–368 (2004)

10.

Fu, Z., Malik, S.: Extracting logic circuit structure from conjunctive normal form descriptions. In: VLSI Design, pp. 37–42 (2007)

11.

MiniSat-SAT Algorithms and Applications Invited talk given by Niklas Sorensson at the CADE-20 workshop ESCAR. http://minisat.se/Papers.html

12.

Balduzzi, M., Zaddach, J., Balzarotti, D., Kirda, E., Loureiro, S.: A security analysis of Amazon’s elastic compute cloud service. In: SAC 2012, pp. 1427–1434 (2012)

13.

Ristenpart, T., Tromer, E., Shacham, H., Savage, S.: Hey, you, get off of my cloud: exploring information leakage in third-party compute clouds. In: CCS 2009, pp. 199–212 (2009)

14.

Achlioptas, D., Gomes, C., Kautz, H., Selman, B.: Generating satisfiable problem instances. In: AAAI/IAAI 2000, pp. 256–261 (2000)

15.

Jarvisalo, M.: Equivalence checking hardware multiplier designs. SAT Competition 2007 Benchmark Description

16.

Pyhala, T.: Factoring Benchmark for SAT-solvers. http://www.tcs.hut.fi/Software/genfacbm/

17.

Brakerski, Z., Rothblum, G.: Black-box obfuscation for d-CNFs. In: ITCS 2014, pp. 235–250 (2014)

18.

Du, W., Goodrich, M.T.: Searching for high-value rare events with uncheatable grid computing. In: Ioannidis, J., Keromytis, A., Yung, M. (eds.) ACNS 2005. LNCS, vol. 3531, pp. 122–137. Springer, Heidelberg (2005). https://doi.org/10.1007/11496137_9CrossRef

19.

Paralleling OpenSMT Towards Cloud Computing. http://www.inf.usi.ch/urop-Tsitovich-2-127208.pdf

20.

Formal in the Cloud OneSpin: New Spin on Cloud Computing. http://www.eejournal.com/archives/articles/20130627-onespin/?printView=true

21.

Zhang, X., He, F., Zuo, W.: Theory and practice of program obfuscation. In: Crisan, M. (ed.) Convergence and Hybrid Information Technologies, p. 426. INTECH, Croatia, March 2010. ISBN 978-953-307-068-1

22.

Karypis, G., Aggarwal, R., Kumar, V., Shekhar, S.: Multilevel hypergraph partitioning: application in VLSI domain. In: DAC 1997, pp. 526–529 (1997)

23.

Shen, S.Y., Qin, Y., Li, S.K.: Minimizing counterexample with unit core extraction and incremental SAT. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 298–312. Springer, Heidelberg (2005). https://doi.org/10.1007/978-3-540-30579-8_20CrossRef

24.

Qin, Y., Shen, S., Kong, J., Dai, H.: Cloud-oriented SAT solver based on obfuscating CNF formula. In: Han, W., Huang, Z., Hu, C., Zhang, H., Guo, L. (eds.) APWeb 2014. LNCS, vol. 8710, pp. 188–199. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-11119-3_18CrossRef

25.

Qin, Y., Shen, S.Y., Jia, Y.: Structure-aware CNF obfuscation for privacy-preserving SAT solving. In: MEMOCODE 2014, pp. 84–93 (2014)

26.

Li, X., Wang, H., Ding, B., Li, X., Feng, D.: Resource allocation with multi-factor node ranking in data center networks. Futur. Gener. Comput. Syst. 32, 1–12 (2014). https://doi.org/10.1016/j.future.2013.09.028CrossRef

27.

Ren, Y., Liu, L., Zhang, Q., Wu, Q., Guan, J., Kong, J., Dai, H., Shao, L.: Shared-memory optimizations for inter-virtual-machine communication. ACM Comput. Surv. 48(4), 49:1–49:42 (2016). https://doi.org/10.1145/2847562CrossRef

Title: Privacy-Preserving SAT Solving Based on Projection-Equivalence CNF Obfuscation
Authors: Ying Qin
Xiao Yang Shen
Zhen Yue Du
Publisher: Springer International Publishing
Book: Cyberspace Safety and Security
Print ISBN: 978-3-030-01688-3

Electronic ISBN: 978-3-030-01689-0

Copyright Year: 2018
DOI: https://doi.org/10.1007/978-3-030-01689-0_18

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner