Document Open Access Logo

Hierarchical Stochastic SAT and Quality Assessment of Logic Locking

Authors Christoph Scholl , Tobias Seufert , Fabian Siegwolf

PDF

File

Thumbnail PDF
PDF
LIPIcs.SAT.2024.24.pdf
  • Filesize: 1.03 MB
  • 22 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic
  • Theory of computation → Automated reasoning
Keywords
  • Stochastic Boolean Satisfiability
  • Hierarchical Stochastic SAT
  • Binary Decision Diagrams
  • Decision Procedure

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

Motivated by the application of quality assessment of logic locking we introduce Hierarchical Stochastic SAT (HSSAT) which generalizes Stochastic SAT (SSAT). We look into the complexity of HSSAT and for solving HSSAT formulas we provide a prototype solver which computes exact evaluation results (i.e., without any approximation and without any imprecision caused by numerical rounding errors). Finally, we perform an intensive experimental evaluation of our HSSAT solver in the context of quality assessment of logic locking.

Cite As Get BibTex

Christoph Scholl, Tobias Seufert, and Fabian Siegwolf. Hierarchical Stochastic SAT and Quality Assessment of Logic Locking. In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 24:1-24:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024) https://doi.org/10.4230/LIPIcs.SAT.2024.24

Author Details

Christoph Scholl
  • Department of Computer Science, University of Freiburg, Germany
Tobias Seufert
  • Department of Computer Science, University of Freiburg, Germany
Fabian Siegwolf
  • Department of Computer Science, University of Freiburg, Germany

Funding

This work was supported by the German Research Foundation (DFG) within the project SUPRA (SCHO 894/7-1).

Supplementary Materials

References

  1. Alex Baumgarten, Akhilesh Tyagi, and Joseph Zambreno. Preventing IC piracy using reconfigurable logic barriers. IEEE Des. Test Comput., 27(1):66-75, 2010. URL: https://doi.org/10.1109/MDT.2010.24.
  2. Berkeley Logic Synthesis and Verification Group. ABC: A system for sequential synthesis and verification. available at https://people.eecs.berkeley.edu/~alanmi/abc/, 2019.
  3. Robert K. Brayton and Alan Mishchenko. ABC: an academic industrial-strength verification tool. In Tayssir Touili, Byron Cook, and Paul B. Jackson, editors, Computer Aided Verification, 22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, 2010. Proceedings, volume 6174 of Lecture Notes in Computer Science, pages 24-40. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-14295-6_5.
  4. Franc Brglez and Hideo Fujiwara. A neutral netlist of 10 combinational benchmark circuits and a target translator in fortran. In Proceedings of IEEE International Symposium Circuits and Systems (ISCAS 85), pages 677-692. IEEE Press, Piscataway, N.J., 1985. Google Scholar
  5. Randal E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Trans. Computers, 35(8):677-691, 1986. URL: https://doi.org/10.1109/TC.1986.1676819.
  6. Pei-Wei Chen, Yu-Ching Huang, and Jie-Hong R. Jiang. A sharp leap from quantified boolean formula to stochastic boolean satisfiability solving. In Thirty-Fifth AAAI Conference on Artificial Intelligence, AAAI 2021, Thirty-Third Conference on Innovative Applications of Artificial Intelligence, IAAI 2021, The Eleventh Symposium on Educational Advances in Artificial Intelligence, EAAI 2021, Virtual Event, February 2-9, 2021, pages 3697-3706. AAAI Press, 2021. URL: https://doi.org/10.1609/AAAI.V35I5.16486.
  7. Gustavo K. Contreras, Md. Tauhidur Rahman, and Mohammad Tehranipoor. Secure split-test for preventing IC piracy by untrusted foundry and assembly. In 2013 IEEE International Symposium on Defect and Fault Tolerance in VLSI and Nanotechnology Systems, DFTS 2013, New York City, NY, USA, October 2-4, 2013, pages 196-203. IEEE Computer Society, 2013. URL: https://doi.org/10.1109/DFT.2013.6653606.
  8. Fulvio Corno, Matteo Sonza Reorda, and Giovanni Squillero. Rt-level itc'99 benchmarks and first ATPG results. IEEE Des. Test Comput., 17(3):44-53, 2000. URL: https://doi.org/10.1109/54.867894.
  9. Sophie Dupuis, Papa-Sidi Ba, Giorgio Di Natale, Marie-Lise Flottes, and Bruno Rouzeyre. A novel hardware logic encryption technique for thwarting illegal overproduction and hardware trojans. In 2014 IEEE 20th International On-Line Testing Symposium, IOLTS 2014, Platja d'Aro, Girona, Spain, July 7-9, 2014, pages 49-54. IEEE, 2014. URL: https://doi.org/10.1109/IOLTS.2014.6873671.
  10. Yu-Wei Fan and Jie-Hong R. Jiang. Sharpssat: A witness-generating stochastic boolean satisfiability solver. In Brian Williams, Yiling Chen, and Jennifer Neville, editors, Thirty-Seventh AAAI Conference on Artificial Intelligence, AAAI 2023, Thirty-Fifth Conference on Innovative Applications of Artificial Intelligence, IAAI 2023, Thirteenth Symposium on Educational Advances in Artificial Intelligence, EAAI 2023, Washington, DC, USA, February 7-14, 2023, pages 3949-3958. AAAI Press, 2023. URL: https://doi.org/10.1609/AAAI.V37I4.25509.
  11. Yu-Wei Fan and Jie-Hong R. Jiang. Unifying decision and function queries in stochastic boolean satisfiability. In Michael J. Wooldridge, Jennifer G. Dy, and Sriraam Natarajan, editors, Thirty-Eighth AAAI Conference on Artificial Intelligence, AAAI 2024, Thirty-Sixth Conference on Innovative Applications of Artificial Intelligence, IAAI 2024, Fourteenth Symposium on Educational Advances in Artificial Intelligence, EAAI 2014, February 20-27, 2024, Vancouver, Canada, pages 7995-8003. AAAI Press, 2024. URL: https://doi.org/10.1609/AAAI.V38I8.28637.
  12. The gnu multiple precision arithmetic library. https://gmplib.org/, 2024.
  13. Markus Hecher and Johannes Fichte. Model counting competition 2023. https://mccompetition.org/, 2023.
  14. Alexander Ivrii, Sharad Malik, Kuldeep S. Meel, and Moshe Y. Vardi. On computing minimal independent support and its applications to sampling and counting. Constraints An Int. J., 21(1):41-58, 2016. URL: https://doi.org/10.1007/S10601-015-9204-Z.
  15. Tuukka Korhonen and Matti Järvisalo. Integrating tree decompositions into decision heuristics of propositional model counters (short paper). In Laurent D. Michel, editor, 27th International Conference on Principles and Practice of Constraint Programming, CP 2021, Montpellier, France (Virtual Conference), October 25-29, 2021, volume 210 of LIPIcs, pages 8:1-8:11. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPICS.CP.2021.8.
  16. Jean-Marie Lagniez, Emmanuel Lonca, and Pierre Marquis. Improving model counting by leveraging definability. In Subbarao Kambhampati, editor, Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence, IJCAI 2016, New York, NY, USA, 9-15 July 2016, pages 751-757. IJCAI/AAAI Press, 2016. URL: http://www.ijcai.org/Abstract/16/112.
  17. Jean-Marie Lagniez and Pierre Marquis. An improved decision-dnnf compiler. In Carles Sierra, editor, Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, IJCAI 2017, Melbourne, Australia, August 19-25, 2017, pages 667-673. ijcai.org, 2017. URL: https://doi.org/10.24963/IJCAI.2017/93.
  18. Stephen M. Majercik and Byron Boots. DC-SSAT: A divide-and-conquer approach to solving stochastic satisfiability problems efficiently. In Manuela M. Veloso and Subbarao Kambhampati, editors, Proceedings, The Twentieth National Conference on Artificial Intelligence and the Seventeenth Innovative Applications of Artificial Intelligence Conference, July 9-13, 2005, Pittsburgh, Pennsylvania, USA, pages 416-422. AAAI Press / The MIT Press, 2005. URL: http://www.aaai.org/Library/AAAI/2005/aaai05-066.php.
  19. Marcel Merten, Sebastian Huhn, and Rolf Drechsler. Quality assessment of rfet-based logic locking protection mechanisms using formal methods. In IEEE European Test Symposium, ETS 2022, Barcelona, Spain, May 23-27, 2022, pages 1-2. IEEE, 2022. URL: https://doi.org/10.1109/ETS54262.2022.9810459.
  20. Shipra Panda and Fabio Somenzi. Who are the variables in your neighborhood. In Richard L. Rudell, editor, Proceedings of the 1995 IEEE/ACM International Conference on Computer-Aided Design, ICCAD 1995, San Jose, California, USA, November 5-9, 1995, pages 74-77. IEEE Computer Society / ACM, 1995. URL: https://doi.org/10.1109/ICCAD.1995.479994.
  21. Jeyavijayan Rajendran, Youngok K. Pino, Ozgur Sinanoglu, and Ramesh Karri. Security analysis of logic obfuscation. In Patrick Groeneveld, Donatella Sciuto, and Soha Hassoun, editors, The 49th Annual Design Automation Conference 2012, DAC '12, San Francisco, CA, USA, June 3-7, 2012, pages 83-89. ACM, 2012. URL: https://doi.org/10.1145/2228360.2228377.
  22. Jeyavijayan Rajendran, Huan Zhang, Chi Zhang, Garrett S. Rose, Youngok K. Pino, Ozgur Sinanoglu, and Ramesh Karri. Fault analysis-based logic encryption. IEEE Trans. Computers, 64(2):410-424, 2015. URL: https://doi.org/10.1109/TC.2013.193.
  23. Jarrod A. Roy, Farinaz Koushanfar, and Igor L. Markov. EPIC: ending piracy of integrated circuits. In Donatella Sciuto, editor, Design, Automation and Test in Europe, DATE 2008, Munich, Germany, March 10-14, 2008, pages 1069-1074. ACM, 2008. URL: https://doi.org/10.1109/DATE.2008.4484823.
  24. Ricardo Salmon and Pascal Poupart. On the relationship between satisfiability and markov decision processes. In Amir Globerson and Ricardo Silva, editors, Proceedings of the Thirty-Fifth Conference on Uncertainty in Artificial Intelligence, UAI 2019, Tel Aviv, Israel, July 22-25, 2019, volume 115 of Proceedings of Machine Learning Research, pages 1105-1115. AUAI Press, 2019. URL: http://proceedings.mlr.press/v115/salmon20a.html.
  25. Christoph Scholl, Tobias Seufert, and Fabian Siegwolf. Hierarchical SSAT: Benchmarks and solver HSSATSolve. https://nc.informatik.uni-freiburg.de/index.php/s/PQ9zBAejC2ERCTD, 2024.
  26. Shubham Sharma, Subhajit Roy, Mate Soos, and Kuldeep S. Meel. GANAK: A scalable probabilistic exact model counter. In Sarit Kraus, editor, Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence, IJCAI 2019, Macao, China, August 10-16, 2019, pages 1169-1176. ijcai.org, 2019. URL: https://doi.org/10.24963/IJCAI.2019/163.
  27. Friedrich Slivovsky. Interpolation-based semantic gate extraction and its applications to QBF preprocessing. In Shuvendu K. Lahiri and Chao Wang, editors, Computer Aided Verification - 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part I, volume 12224 of Lecture Notes in Computer Science, pages 508-528. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-53288-8_24.
  28. Fabio Somenzi. Efficient manipulation of decision diagrams. Int. J. Softw. Tools Technol. Transf., 3(2):171-181, 2001. URL: https://doi.org/10.1007/S100090100042.
  29. Mate Soos and Kuldeep S. Meel. Arjun: An efficient independent support computation technique and its applications to counting and sampling. In Tulika Mitra, Evangeline F. Y. Young, and Jinjun Xiong, editors, Proceedings of the 41st IEEE/ACM International Conference on Computer-Aided Design, ICCAD 2022, San Diego, California, USA, 30 October 2022 - 3 November 2022, pages 71:1-71:9. ACM, 2022. URL: https://doi.org/10.1145/3508352.3549406.
  30. Larry J. Stockmeyer. The polynomial-time hierarchy. Theor. Comput. Sci., 3(1):1-22, 1976. URL: https://doi.org/10.1016/0304-3975(76)90061-X.
  31. Pramod Subramanyan, Sayak Ray, and Sharad Malik. Evaluating the security of logic encryption algorithms. In IEEE International Symposium on Hardware Oriented Security and Trust, HOST 2015, Washington, DC, USA, 5-7 May, 2015, pages 137-143. IEEE Computer Society, 2015. URL: https://doi.org/10.1109/HST.2015.7140252.
  32. Ryosuke Suzuki, Kenji Hashimoto, and Masahiko Sakai. Improvement of projected model-counting solver with component decomposition using SAT solving in components. Technical Report SIG-FPAI-103-B506, JSAI Technical Report, March 2017. in Japanese. Google Scholar
  33. G. S. Tseitin. On the complexity of derivation in propositional calculus. In Jörg H. Siekmann and Graham Wrightson, editors, Automation of Reasoning: 2: Classical Papers on Computational Logic 1967-1970, pages 466-483. Springer Berlin Heidelberg, 1983. Google Scholar
  34. Klaus W. Wagner. The complexity of combinatorial problems with succinct input representation. Acta Informatica, 23(3):325-356, 1986. URL: https://doi.org/10.1007/BF00289117.
  35. Hao-Ren Wang, Kuan-Hua Tu, Jie-Hong Roland Jiang, and Christoph Scholl. Quantifier elimination in stochastic boolean satisfiability. In Kuldeep S. Meel and Ofer Strichman, editors, 25th International Conference on Theory and Applications of Satisfiability Testing, SAT 2022, August 2-5, 2022, Haifa, Israel, volume 236 of LIPIcs, pages 23:1-23:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPICS.SAT.2022.23.
  36. Yang Xie and Ankur Srivastava. Mitigating SAT attack on logic locking. In Benedikt Gierlichs and Axel Y. Poschmann, editors, Cryptographic Hardware and Embedded Systems - CHES 2016 - 18th International Conference, Santa Barbara, CA, USA, August 17-19, 2016, Proceedings, volume 9813 of Lecture Notes in Computer Science, pages 127-146. Springer, 2016. URL: https://doi.org/10.1007/978-3-662-53140-2_7.
  37. Muhammad Yasin, Bodhisatwa Mazumdar, Jeyavijayan (JV) Rajendran, and Ozgur Sinanoglu. Sarlock: SAT attack resistant logic locking. In William H. Robinson, Swarup Bhunia, and Ryan Kastner, editors, 2016 IEEE International Symposium on Hardware Oriented Security and Trust, HOST 2016, McLean, VA, USA, May 3-5, 2016, pages 236-241. IEEE Computer Society, 2016. URL: https://doi.org/10.1109/HST.2016.7495588.
  38. Muhammad Yasin, Jeyavijayan (JV) Rajendran, Ozgur Sinanoglu, and Ramesh Karri. On improving the security of logic locking. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 35(9):1411-1424, 2016. URL: https://doi.org/10.1109/TCAD.2015.2511144.
  39. Muhammad Yasin, Abhrajit Sengupta, Mohammed Thari Nabeel, Mohammed Ashraf, Jeyavijayan Rajendran, and Ozgur Sinanoglu. Provably-secure logic locking: From theory to practice. In Bhavani Thuraisingham, David Evans, Tal Malkin, and Dongyan Xu, editors, Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, CCS 2017, Dallas, TX, USA, October 30 - November 03, 2017, pages 1601-1618. ACM, 2017. URL: https://doi.org/10.1145/3133956.3133985.
  40. Muhammad Yasin, Abhrajit Sengupta, Benjamin Carrión Schäfer, Yiorgos Makris, Ozgur Sinanoglu, and Jeyavijayan Rajendran. What to lock?: Functional and parametric locking. In Laleh Behjat, Jie Han, Miroslav N. Velev, and Deming Chen, editors, Proceedings of the on Great Lakes Symposium on VLSI 2017, Banff, AB, Canada, May 10-12, 2017, pages 351-356. ACM, 2017. URL: https://doi.org/10.1145/3060403.3060492.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact