nach oben

Erschienen in:

2018 | OriginalPaper | Buchkapitel

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

verfasst von : Ying Qin, Xiao Yang Shen, Zhen Yue Du

Erschienen in: Cyberspace Safety and Security

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

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!

Jetzt informieren

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!

Jetzt informieren

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!

Jetzt informieren

Vorheriges Kapitel Towards the Blockchain Technology for System Voting Process

Nächstes Kapitel 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

Titel: Privacy-Preserving SAT Solving Based on Projection-Equivalence CNF Obfuscation
verfasst von: Ying Qin
Xiao Yang Shen
Zhen Yue Du
Verlag: Springer International Publishing
Buch: Cyberspace Safety and Security
Print ISBN: 978-3-030-01688-3

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

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

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"