Skip to main content
SpringerLink
Log in

Survey on Applications of Formal Methods in Reverse Engineering and Intellectual Property Protection

  • Published:
Journal of Hardware and Systems Security Aims and scope Submit manuscript

Abstract

Recent years have seen a growth in the use of algorithmic techniques, and especially formal methods, in reverse engineering. Depending on the motivation and requirements of the attacker, algorithms can be used for reconstructing circuit netlists, extracting a higher-level description of a circuit from unstructured sea-of-gates, or resynthesizing the Boolean function of a logic circuit from examples. At each step of this process, formal methods can be leveraged. In this survey, we review some of the applications of formal methods in reverse engineering and in IP protection.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2
Fig. 3
Fig. 4
Fig. 5
Fig. 6

Similar content being viewed by others

Notes

  1. Counting the number of solutions to a CNF formula is known as the #SAT (sharp-SAT) problem or as model counting.

References

  1. Chipworks: circuit extraction software. http://www.chipworks.com/ko/node/298

  2. Degate. http://www.degate.org/documentation/

  3. Amir S, Shakya B, Xu X, Jin Y, Bhunia S, Tehranipoor M, Forte D (2018) Development and evaluation of hardware obfuscation benchmarks. J Hardware Syst Secur, 1–20

  4. Asadizanjani N, Tehranipoor M, Forte D (2017) PCB reverse engineering using nondestructive X-ray tomography and advanced image processing. IEEE Trans Comp Packag Manuf Technol 7(2):292–299

    Google Scholar 

  5. Baumgarten A, Tyagi A, Zambreno J (2010) Preventing IC piracy using reconfigurable logic barriers. IEEE Des Test Comput 27:1

    Article  Google Scholar 

  6. Brayton R, Mishchenko A ABC: an academic industrial-strength verification tool. In: CAV (2010). Springer, pp 24–40

  7. Chakraborty RS, Bhunia S (2009) Harpoon: an obfuscation-based soc design methodology for hardware protection. IEEE Trans Comput-Aided Des Integr Circ Syst 28(10):1493–1502

    Article  Google Scholar 

  8. Chen S, Chen J, Forte D, Di J, Tehranipoor M, Wang L (2015) Chip-level anti-reverse engineering using transformable interconnects. In: 2015 IEEE international symposium on defect and fault tolerance in VLSI and nanotechnology systems (DFTS). IEEE, pp 109–114

  9. Cocchi RP, Baukus JP, Chow LW, Wang BJ (2014) Circuit camouflage integration for hardware IP protection. In: Proceedings of the 51st annual design automation conference, DAC ’14. ACM, New York, pp 153:1–153:5

  10. Collantes MIM, El Massad M, Garg S (2016) Threshold-dependent camouflaged cells to secure circuits against reverse engineering attacks. In: 2016 IEEE computer society annual symposium on VLSI (ISVLSI). IEEE, pp 443–448

  11. Cook SA, Mitchell DG (1997) Finding hard instances of the satisfiability problem. In: Satisfiability problem: theory and applications: DIMACS workshop, vol 35, pp 1–17

  12. De Wolf P, Geva M, Hantschel T, Vandervorst W, Bylsma R (1998) Two-dimensional carrier profiling of inp structures using scanning spreading resistance microscopy. Appl Phys Lett 73(15):2155–2157

    Article  Google Scholar 

  13. Eén N, Sörensson N (2003) Temporal induction by incremental SAT solving. Electron Notes Theor Comput Sci 89(4):543–560

    Article  Google Scholar 

  14. El Massad M, Garg S, Tripunitara M (2017) Reverse engineering camouflaged sequential circuits without scan access. In: 2017 IEEE/ACM international conference on computer-aided design (ICCAD). IEEE, pp 33–40

  15. El Massad M, Garg S, Tripunitara MV (2015) Integrated circuit (IC) decamouflaging: reverse engineering camouflaged ics within minutes. In: NDSS

  16. Erbagci B, Erbagci C, Akkaya NEC, Mai K (2016) A secure camouflaged threshold voltage defined logic family. In: 2016 IEEE International symposium on hardware oriented security and trust (HOST). IEEE, pp 229–235

  17. Gascón A, Subramanyan P, Dutertre B, Tiwari A, Jovanović D, Malik S (2014) Template-based circuit understanding. In: Formal methods in computer-aided design (FMCAD), 2014. IEEE, pp 83–90

  18. Hansen MC, Yalcin H, Hayes JP (1999) Unveiling the ISCAS-85 benchmarks: a case study in reverse engineering. IEEE Des Test Comput 16(3):72–80

    Article  Google Scholar 

  19. Jha S, Gulwani S, Seshia SA, Tiwari A (2010) Oracle-guided component-based program synthesis. In: Proceedings of the 32nd ACM/IEEE international conference on software engineering, vol 1. ACM, pp 215–224

  20. Keshavarz S, Holcomb D (2017) Threshold-based obfuscated keys with quantifiable security against invasive readout. In: 2017 IEEE/ACM international conference on computer-aided design (ICCAD), pp 57–64

  21. Keshavarz S, Paar C, Holcomb D (2017) Design automation for obfuscated circuits with multiple viable functions. In: Design, automation test in Europe conference exhibition (DATE), 2017, pp 886–889

  22. Keshavarz S, Schellenberg F, Richter B, Paar C, Holcomb D (2018) SAT-based reverse engineering of gate-level schematics using fault injection and probing. In: 2018 IEEE international symposium on hardware oriented security and trust (HOST). IEEE

  23. Koren E, Rosenwaks Y, Allen J, Hemesath E, Lauhon L (2009) Nonuniform doping distribution along silicon nanowires measured by kelvin probe force microscopy and scanning photocurrent microscopy. Appl Phys Lett 95(9):092105

    Article  Google Scholar 

  24. Li M, Shamsi K, Meade T, Zhao Z, Yu B, Jin Y, Pan DZ (2017) Provably secure camouflaging strategy for IC protection. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems

  25. Li W, Gascon A, Subramanyan P, Tan WY, Tiwari A, Malik S, Shankar N, Seshia SA (2013) WordRev: finding word-level structures in a sea of bit-level gates. In: 2013 IEEE international symposium on hardware-oriented security and trust (HOST), pp 67–74

  26. Li W, Wasson Z, Seshia SA (2012) Reverse engineering circuits using behavioral pattern mining. In: 2012 IEEE international Symposium on hardware-oriented security and trust (HOST). IEEE, pp 83–88

  27. Liu D, Yu C, Zhang X, Holcomb D (2016) Oracle-guided incremental SAT solving to reverse engineer camouflaged logic circuits. In: Proceedings of the 2016 conference on design, automation & test in Europe, DATE ’16. EDA Consortium, San Jose, pp 433–438

  28. Malik S, Becker G, Paar C, Burleson W (2015) Development of a layout-level hardware obfuscation tool. In: IEEE Computer society annual symposium on VLSI, ISVLSI 2015

  29. Meade T, Zhang S, Jin Y Netlist reverse engineering for high-level functionality reconstruction. In: 2016 21st Asia and South Pacific (2016) design automation conference (ASP-DAC). IEEE, pp 655–660

  30. Nohl K, Evans D, Starbug S, Plötz H (2008) Reverse-engineering a cryptographic RFID tag. In: USENIX security symposium, vol 28

  31. Patnaik S, Ashra M, Knechtel J, Sinanoglu O (2017) Obfuscating the interconnects: low-cost and resilient full-chip layout camouflaging. In: 2017 IEEE/ACM international conference on computer-aided design (ICCAD). IEEE, pp 41–48

  32. Pilato C, Regazzoni F, Karri R, Garg S (2018) TAO: techniques for algorithmic obscuration during high-level synthesis. In: Proceedings of ACM/IEEE design automation conference (DAC 2018) to appear. ACM/IEEE

  33. Plaza SM, Markov IL (2014) Protecting integrated circuits from piracy with test-aware logic locking. In: Proceedings of the 2014 IEEE/ACM international conference on computer-aided design. IEEE Press, pp 262–269

  34. Plaza SM, Markov IL (2015) Solving the third-shift problem in IC piracy with test-aware logic locking. IEEE Trans Comput-Aided Des Integr Circ Syst 34(6):961–971

    Article  Google Scholar 

  35. Quadir SE, Chen J, Forte D, Asadizanjani N, Shahbazmohamadi S, Wang L, Chandy J, Tehranipoor M (2016) A survey on chip to system reverse engineering. ACM J Emerg Technol Comput Syst (JETC) 13(1):6

    Google Scholar 

  36. Rajendran J, Pino Y, Sinanoglu O, Karri R Security analysis of logic obfuscation. In: Proceedings of the 49th annual design automation conference (2012). ACM, pp 83–89

  37. Rajendran J, Sam M, Sinanoglu O, Karri R (2013) Security analysis of integrated circuit camouflaging. In: Proceedings of the 2013 ACM SIGSAC conference on computer & communications security. ACM, pp 709–720

  38. Rajendran J, Zhang H, Zhang C, Rose GS, Pino Y, Sinanoglu O, Karri R (2015) Fault analysis-based logic encryption. IEEE Trans Comput 64(2):410–424

    Article  MathSciNet  Google Scholar 

  39. Roy JA, Koushanfar F, Markov IL (2010) Ending piracy of integrated circuits. Computer 43(10):30–38

    Article  Google Scholar 

  40. Shamsi K, Li M, Meade T, Zhao Z, Pan DZ, Jin Y (2017) Appsat: approximately deobfuscating integrated circuits. In: 2017 IEEE international symposium on hardware oriented security and trust (HOST). IEEE, pp 95–100

  41. Shamsi K, Li M, Meade T, Zhao Z, Pan DZ, Jin Y (2017) Cyclic obfuscation for creating sat-unresolvable circuits. In: Proceedings of the on great lakes symposium on VLSI 2017. ACM, pp 173–178

  42. Shen Y, Zhou H (2017) Double dip: re-evaluating security of logic encryption algorithms. In: Proceedings of the on great lakes symposium on VLSI 2017. ACM, pp 179–184

  43. Shi Y, Gwee B. -H., Ren Y, Ting CW (2012) Extracting functional modules from flattened gate-level netlist. In: 2012 international Symposium on communications and information technologies (ISCIT). IEEE, pp 538–543

  44. Shi Y, Ting CW, Gwee BH, Ren Y (2010) A highly efficient method for extracting FSMs from flattened gate-level netlist. In: Proceedings of 2010 IEEE international symposium on circuits and systems, pp 2610–2613

  45. Subramanyan P, Ray S, Malik S (2015) Evaluating the security of logic encryption algorithms. In: 2015 IEEE international symposium on hardware oriented security and trust (HOST). IEEE, pp 137–143

  46. Subramanyan P, Tsiskaridze N, Li W, Gascón A., Tan WY, Tiwari A, Shankar N, Seshia SA, Malik S (2014) Reverse engineering digital circuits using structural and functional analyses. IEEE Trans Emerging Topics Comput 2(1):63–80

    Article  Google Scholar 

  47. Subramanyan P, Tsiskaridze N, Pasricha K, Reisman D, Susnea A, Malik S (2013) Reverse engineering digital circuits using functional analysis. In: Proceedings of the conference on design, automation and test in Europe. EDA Consortium, pp 1277–1280

  48. Tehranipoor M, Karri R, Koushanfar F, Potkonjak M (2016) Trusthub. Available on-line: https://www.trust-hub.org

  49. Thurley M (2006) sharpSAT–counting models with advanced component caching and implicit bcp. In: International conference on theory and applications of satisfiability testing. Springer, pp 424–429

  50. Torrance R, James D (2009) The state-of-the-art in IC reverse engineering. In: Cryptographic hardware and embedded systems-CHES 2009. Springer, pp 363–381

  51. Torrance R, James D (2011) The state-of-the-art in semiconductor reverse engineering. In: 2011 48th ACM/EDAC/IEEE design automation conference (DAC). IEEE, pp 333–338

  52. Wang Y, Chen P, Hu J, Li G, Rajendran J (2018) The cat and mouse in split manufacturing. IEEE Trans Very Large Scale Integr(VLSI) Syst 26(5):805–817

    Article  Google Scholar 

  53. Xie Y, Srivastava A (2016) Mitigating sat attack on logic locking. In: International conference on cryptographic hardware and embedded systems. Springer, pp 127–146

  54. Xie Y, Srivastava A (2017) Delay locking: security enhancement of logic locking against ic counterfeiting and overproduction. In: Proceedings of the 54th annual design automation conference 2017. ACM, p 9

  55. Xu X, Shakya B, Tehranipoor MM, Forte D (2017) Novel bypass attack and BDD-based tradeoff analysis against all known logic locking attacks. In: International conference on cryptographic hardware and embedded systems. Springer, pp 189–210

  56. Yang B, Wu K, Karri R (2006) Secure scan: a design-for-test architecture for crypto chips. IEEE Trans Comput-Aided Des Integr Circ Syst 25(10):2287–2293

    Article  Google Scholar 

  57. Yasin M, Mazumdar B, Rajendran J, Sinanoglu O (2016) Sarlock: sat attack resistant logic locking. In: 2016 IEEE international symposium on hardware oriented security and trust (HOST). IEEE, pp 236–241

  58. Yasin M, Mazumdar B, Sinanoglu O, Rajendran J (2016) Camoperturb: secure IC camouflaging for minterm protection. In: Proceedings of the 35th international conference on computer-aided design. ACM, p 29

  59. Yasin M, Mazumdar B, Sinanoglu O, Rajendran J (2017) Removal attacks on logic locking and camouflaging techniques. IEEE Transactions on Emerging Topics in Computing

  60. Yasin M, Saeed SM, Rajendran J, Sinanoglu O (2016) Activation of logic encrypted chips: Pre-test or post-test? In: 2016 design automation test in Europe conference exhibition (DATE), pp 139–144

  61. Yasin M, Sengupta A, Nabeel MT, Ashraf M, Rajendran J, Sinanoglu O (2017) Provably-secure logic locking: from theory to practice https://github.com/dfx-nyuad/ccs17. In: 2017 CCS. ACM, pp 1601–1618

  62. Yasin M, Sinanoglu O (2015) Transforming between logic locking and IC camouflaging. In: 2015 10th international design test symposium (IDT), pp 1–4

  63. Yasin M, Sinanoglu O, Rajendran J (2017) Testing the trustworthiness of ic testing: an oracle-less attack on ic camouflaging. IEEE Trans Inf Forens Secur 12(11):2668–2682

    Article  Google Scholar 

  64. Yu C, Zhang X, Liu D, Ciesielski M, Holcomb D (2017) Incremental SAT-based reverse engineering of camouflaged logic circuits. IEEE Trans Comput-Aided Des Integr Circ Syst 36(10):1647–1659

    Article  Google Scholar 

  65. Zhang GL, Li B, Yu B, Pan DZ, Schlichtmann U (2018) TimingCamouflage: improving circuit security against counterfeiting by unconventional timing. In: DATE 2018. IEEE

  66. Zhou H, Jiang R, Kong S (2017) CycSAT: SAT-based attack on cyclic logic encryptions. In: 2017 IEEE/ACM international conference on computer-aided design (ICCAD). IEEE, pp 49–56

Download references

Author information

Authors and Affiliations

  1. Department of Electrical and Computer Engineering, University of Massachusetts Amherst, Amherst, MA, USA

    Shahrzad Keshavarz, Samaneh Ghandali & Daniel Holcomb

  2. École Polytechnique Fédérale de Lausanne, Lausanne, Switzerland

    Cunxi Yu

  3. Department of Electrical and Computer Engineering, University of Illinois at Chicago, Chicago, IL, USA

    Xiaolin Xu

Authors
  1. Shahrzad Keshavarz
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Cunxi Yu
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Samaneh Ghandali
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Xiaolin Xu
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Daniel Holcomb
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Shahrzad Keshavarz.

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Keshavarz, S., Yu, C., Ghandali, S. et al. Survey on Applications of Formal Methods in Reverse Engineering and Intellectual Property Protection. J Hardw Syst Secur 2, 214–224 (2018). https://doi.org/10.1007/s41635-018-0044-3

Download citation

  • Received:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s41635-018-0044-3

Keywords

Search

Navigation