Skip to main content
SpringerLink
Log in

IP Trust Validation Using Proof-Carrying Hardware

  • Chapter
  • First Online:
Hardware IP Security and Trust

Abstract

The wide usage of hardware Intellectual Property (IP) cores from untrusted third-party vendors has raised security vulnerabilities at design stages of the IC design flow. Possibility of hardware Trojans and/or design backdoors in the IP cores has increased security concerns. As existing functional testing methods fall short in detecting these unspecified (often malicious) logic, formal methods provide powerful solutions in detecting malicious behaviors in hardware. Toward this direction, we will discuss theorem proving and model checking for hardware trust evaluation. Specifically, proof-carrying hardware (PCH) and its applications are introduced in detail. While PCH methods suffer from scalability issues and cannot be easily used for large-scale applications such as System-on-Chip (SoC) design, we will also discuss variants of PCH such as the Hierarchy Preserving Formal Verification framework, for alleviating the scalability challenge.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD 159.99
Price excludes VAT (USA)
  • Durable hardcover edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  1. M. Banga, M. Hsiao, Trusted RTL: Trojan detection methodology in pre-silicon designs, in IEEE International Symposium on Hardware-Oriented Security and Trust (HOST) (2010), pp. 56–59

    Google Scholar 

  2. A. Waksman, M. Suozzo, S. Sethumadhavan, FANCI: identification of stealthy malicious logic using boolean functional analysis, in Proceedings of the ACM SIGSAC Conference on Computer & Communications Security, CCS’13 (2013), pp. 697–708

    Google Scholar 

  3. D. Sullivan, J. Biggers, G. Zhu, S. Zhang, Y. Jin, FIGHT-metric: Functional identification of gate-level hardware trustworthiness, in Design Automation Conference (DAC) (2014)

    Book  Google Scholar 

  4. N. Tsoutsos, C. Konstantinou, M. Maniatakos, Advanced techniques for designing stealthy hardware trojans, in Design Automation Conference (DAC), 2014 51st ACM/EDAC/IEEE (2014)

    Google Scholar 

  5. M. Rudra, N. Daniel, V. Nagoorkar, D. Hoe, Designing stealthy trojans with sequential logic: A stream cipher case study, in Design Automation Conference (DAC), 2014 51st ACM/EDAC/IEEE (2014)

    Book  Google Scholar 

  6. S. Drzevitzky, U. Kastens, M. Platzner, Proof-carrying hardware: Towards runtime verification of reconfigurable modules, in International Conference on Reconfigurable Computing and FPGAs (2009), pp. 189–194

    Google Scholar 

  7. S. Drzevitzky, M. Platzner, Achieving hardware security for reconfigurable systems on chip by a proof-carrying code approach, in 6th International Workshop on Reconfigurable Communication-Centric Systems-on-Chip (2011), pp. 1–8

    Google Scholar 

  8. E. Love, Y. Jin, Y. Makris, Proof-carrying hardware intellectual property: a pathway to trusted module acquisition. IEEE Trans. Inf. Forensics Secur. 7 (1), 25–40 (2012)

    Article  Google Scholar 

  9. Y. Jin, B. Yang, Y. Makris, Cycle-accurate information assurance by proof-carrying based signal sensitivity tracing, in IEEE International Symposium on Hardware-Oriented Security and Trust (HOST) (2013), pp. 99–106

    Google Scholar 

  10. Y. Jin, Y. Makris, A proof-carrying based framework for trusted microprocessor IP, in 2013 IEEE/ACM International Conference on Computer-Aided Design (ICCAD) (2013), pp. 824–829

    Google Scholar 

  11. INRIA, The Coq proof assistant (2010), http://coq.inria.fr/

    Google Scholar 

  12. F. Wolff, C. Papachristou, S. Bhunia, R.S. Chakraborty, Towards Trojan-free trusted ICs: problem analysis and detection scheme, in IEEE Design Automation and Test in Europe (2008), pp. 1362–1365

    Google Scholar 

  13. M. Hicks, M. Finnicum, S.T. King, M.M.K. Martin, J.M. Smith, Overcoming an untrusted computing base: detecting and removing malicious hardware automatically, in Proceedings of IEEE Symposium on Security and Privacy (2010), pp. 159–172

    Google Scholar 

  14. C. Sturton, M. Hicks, D. Wagner, S. King, Defeating UCI: building stealthy and malicious hardware, in 2011 IEEE Symposium on Security and Privacy (SP) (2011), pp. 64–77

    Google Scholar 

  15. X. Zhang, M. Tehranipoor, Case study: detecting hardware trojans in third-party digital ip cores, in 2011 IEEE International Symposium on Hardware-Oriented Security and Trust (HOST) (2011), pp. 67–70

    Google Scholar 

  16. Y. Jin, Design-for-security vs. design-for-testability: A case study on dft chain in cryptographic circuits, in IEEE Computer Society Annual Symposium on VLSI (ISVLSI) (2014), pp. 19–24

    Google Scholar 

  17. X. Guo, R. G. Dutta, Y. Jin, F. Farahmandi, P. Mishra, Pre-silicon security verification and validation: a formal perspective, in Proceedings of the 52Nd Annual Design Automation Conference, DAC’15 (2015), pp. 145:1–145:6

    Google Scholar 

  18. F.M. De Paula, M. Gort, A.J. Hu, S.J. Wilton, J. Yang, Backspace: formal analysis for post-silicon debug, in Proceedings of the 2008 International Conference on Formal Methods in Computer-Aided Design (IEEE Press, New York, 2008), p. 5

    Google Scholar 

  19. S. Drzevitzky, Proof-carrying hardware: Runtime formal verification for secure dynamic reconfiguration, in 2010 International Conference on Field Programmable Logic and Applications (FPL) (2010), pp. 255–258

    Google Scholar 

  20. J. Rajendran, V. Vedula, R. Karri, Detecting malicious modifications of data in third-party intellectual property cores, in Proceedings of the Annual Design Automation Conference, DAC ’15 (ACM, New York, 2015), pp. 112:1–112:6

    Google Scholar 

  21. J. Harrison, Floating-point verification, in FM 2005: Formal Methods, International Symposium of Formal Methods Europe, Proceedings, ed. by J. Fitzgerald, I.J. Hayes, A. Tarlecki. Lecture Notes in Computer Science, vol. 3582 (Springer, Berlin, 2005), pp. 529–532

    Google Scholar 

  22. S. Owre, J.M. Rushby, N. Shankar, PVS: a prototype verification system, in 11th International Conference on Automated Deduction (CADE) (Saratoga, NY), ed. by D. Kapur. Lecture Notes in Artificial Intelligence, vol. 607 (Springer, Berlin, 1992), pp. 748–752

    Google Scholar 

  23. D. Russinoff, M. Kaufmann, E. Smith, R. Sumners, Formal verification of floating-point RTL at AMD using the ACL2 theorem prover, in Proceedings of the 17th IMACS World Congress on Scientific Computation, Applied Mathematics and Simulation, Paris, France (2005)

    Google Scholar 

  24. J.-D. Quesel, S. Mitsch, S. Loos, N. Aréchiga, A. Platzer, How to model and prove hybrid systems with KeYmaera: a tutorial on safety. Int. J. Softw. Tools Technol. Transfer 18, 67–91 (2016)

    Article  Google Scholar 

  25. A. Chlipala, Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant (MIT Press, Cambridge, 2013)

    MATH  Google Scholar 

  26. U. Norell, Dependently typed programming in Agda, in Advanced Functional Programming (Springer, Berlin, 2009), pp. 230–266

    Book  MATH  Google Scholar 

  27. R.L. Constable, S.F. Allen, H.M. Bromley, W.R. Cleaveland, J.F. Cremer, R.W. Harper, D.J. Howe, T.B. Knoblock, N.P. Mendler, P. Panangaden, J.T. Sasaki, S.F. Smith, Implementing Mathematics with the Nuprl Proof Development System (Prentice-Hall, Upper Saddle River, 1986)

    Google Scholar 

  28. L.C. Paulson, Isabelle: the next 700 theorem provers, in Logic and Computer Science, vol. 31 (Academic Press, London, 1990), pp. 361–386

    Google Scholar 

  29. E.M. Clarke, O. Grumberg, D. Peled, Model Checking (MIT press, Cambridge, 1999)

    Google Scholar 

  30. T.A. Henzinger, R. Jhala, R. Majumdar, G. Sutre, Software verification with blast, in Model Checking Software, (Springer, Berlin, 2003), pp. 235–239

    MATH  Google Scholar 

  31. J. O’Leary, X. Zhao, R. Gerth, C.-J.H. Seger, Formally verifying ieee compliance of floating-point hardware. Intel Technol. J. 3 (1), 1–14 (1999)

    Google Scholar 

  32. M. Srivas, M. Bickford, Formal verification of a pipelined microprocessor. IEEE Softw. 7 (5), 52–64 (1990)

    Article  Google Scholar 

  33. T. Kropf, Introduction to Formal Hardware Verification (Springer, Berlin, 2013)

    MATH  Google Scholar 

  34. G. Klein, K. Elphinstone, G. Heiser, J. Andronick, D. Cock, P. Derrin, D. Elkaduwe, K. Engelhardt, R. Kolanski, M. Norrish, T. Sewell, H. Tuch, S. Winwood, seL4: formal verification of an os kernel, in Proceedings of the ACM SIGOPS 22nd Symposium on Operating systems principles (ACM, New York, 2009), pp. 207–220

    Book  Google Scholar 

  35. S. Chaki, E.M. Clarke, A. Groce, S. Jha, H. Veith, Modular verification of software components in C. IEEE Trans. Softw. Eng. 30 (6), 388–402 (2004)

    Article  Google Scholar 

  36. H. Chen, D. Ziegler, T. Chajed, A. Chlipala, M.F. Kaashoek, N. Zeldovich, Using crash hoare logic for certifying the fscq file system, in Proceedings of the 25th Symposium on Operating Systems Principles, SOSP’15 (ACM, New York, 2015), pp. 18–37

    Book  Google Scholar 

  37. M. Vijayaraghavan, A. Chlipala, N. Dave, Modular deductive verification of multiprocessor hardware designs, in Computer Aided Verification (Springer, Cham, 2015), pp. 109–127

    Google Scholar 

  38. A.A. Mir, S. Balakrishnan, S. Tahar, Modeling and verification of embedded systems using cadence SMV, in 2000 Canadian Conference on Electrical and Computer Engineering, vol. 1 (IEEE, New York, 2000), pp. 179–183

    Google Scholar 

  39. M. Kwiatkowska, G. Norman, D. Parker, Prism: probabilistic symbolic model checker, in Computer Performance Evaluation: Modelling Techniques and Tools (Springer, Berlin, 2002), pp. 200–204

    Book  MATH  Google Scholar 

  40. G.J. Holzmann, The model checker spin. IEEE Trans. Softw. Eng. 23 (5), 279 (1997)

    Google Scholar 

  41. D. Beyer, M.E. Keremoglu, Cpachecker: a tool for configurable software verification, in Computer Aided Verification (Springer, Berlin, 2011), pp. 184–190

    Book  Google Scholar 

  42. A. David, K. G. Larsen, A. Legay, M. Mikučionis, Z. Wang, Time for statistical model checking of real-time systems, in Computer Aided Verification (Springer, Berlin, 2011), pp. 349–355

    Google Scholar 

  43. E. Clarke, O. Grumberg, S. Jha, Y. Lu, H. Veith, Counterexample-guided abstraction refinement, in Computer Aided Verification, (Springer, Berlin 2000), pp. 154–169

    MATH  Google Scholar 

  44. C. Baier, J. Katoen, Principles of Model Checking (MIT Press, Cambridge, 2008)

    MATH  Google Scholar 

  45. A. Biere, A. Cimatti, E.M. Clarke, M. Fujita, Y. Zhu, Symbolic model checking using sat procedures instead of BDDs, in Proceedings of the 36th annual ACM/IEEE Design Automation Conference (ACM, New York, 1999), pp. 317–320

    Google Scholar 

  46. R.E. Bryant, Symbolic boolean manipulation with ordered binary-decision diagrams. ACM Comput. Surv. 24 (3), 293–318 (1992)

    Article  Google Scholar 

  47. R.E. Bryant, Graph-based algorithms for boolean function manipulation. IEEE Trans. Comput. 100 (8), 677–691 (1986)

    Article  MATH  Google Scholar 

  48. A. Cimatti, E. Clarke, E. Giunchiglia, F. Giunchiglia, M. Pistore, M. Roveri, R. Sebastiani, A. Tacchella, Nusmv 2: an opensource tool for symbolic model checking, in Computer Aided Verification (Springer, Berlin, 2002), pp. 359–364

    MATH  Google Scholar 

  49. E. Clarke, A. Biere, R. Raimi, Y. Zhu, Bounded model checking using satisfiability solving. Form. Methods Syst. Des. 19 (1), 7–34 (2001)

    Article  MATH  Google Scholar 

  50. A. Biere, A. Cimatti, E.M. Clarke, O. Strichman, Y. Zhu, Bounded model checking Adv. Comput. 58, 117–148 (2003)

    Google Scholar 

  51. S. Qadeer, J. Rehof, Context-bounded model checking of concurrent software, in Tools and Algorithms for the Construction and Analysis of Systems (Springer, Berlin, 2005), pp. 93–107

    MATH  Google Scholar 

  52. G.C. Necula, Proof-carrying code, in POPL ’97: Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (1997), pp. 106–119

    Google Scholar 

  53. X. Guo, R.G. Dutta, Y. Jin, Hierarchy-preserving formal verification methods for pre-silicon security assurance, in 16th International Workshop on Microprocessor and SOC Test and Verification (MTV) (2015)

    Google Scholar 

  54. G.E. Suh, J.W. Lee, D. Zhang, S. Devadas, Secure program execution via dynamic information flow tracking, in Proceedings of the 11th International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS XI (2004), pp. 85–96

    Google Scholar 

  55. S. Chen, J. Xu, N. Nakka, Z. Kalbarczyk, R. Iyer, Defeating memory corruption attacks via pointer taintedness detection, in Proceedings. International Conference on Dependable Systems and Networks, 2005. DSN 2005 (2005), pp. 378–387

    Google Scholar 

  56. W. Shi, J. Fryman, G. Gu, H.-H. Lee, Y. Zhang, J. Yang, Infoshield: a security architecture for protecting information usage in memory, in The Twelfth International Symposium on High-Performance Computer Architecture, 2006 (2006), pp. 222–231

    Google Scholar 

  57. N. Vachharajani, M. Bridges, J. Chang, R. Rangan, G. Ottoni, J. Blome, G. Reis, M. Vachharajani, D. August, RIFLE: an architectural framework for user-centric information-flow security, in 37th International Symposium on Microarchitecture, 2004. MICRO-37 2004 (2004), pp. 243–254

    Google Scholar 

  58. Y.-Y. Chen, P. A. Jamkhedkar, R.B. Lee, A software-hardware architecture for self-protecting data, in Proceedings of the 2012 ACM Conference on Computer and Communications Security, CCS’12 (2012), pp. 14–27

    Google Scholar 

  59. Y. Jin, D. Oliveira, Extended abstract: trustworthy SoC architecture with on-demand security policies and HW-SW cooperation, in 5th Workshop on SoCs, Heterogeneous Architectures and Workloads (SHAW-5) (2014)

    Google Scholar 

  60. Y. Jin, Y. Makris, Proof carrying-based information flow tracking for data secrecy protection and hardware trust, in IEEE 30th VLSI Test Symposium (VTS) (2012), pp. 252–257

    Google Scholar 

  61. X. Guo, R.G. Dutta, P. Mishra, Y. Jin, Scalable soc trust verification using integrated theorem proving and model checking, in IEEE Symposium on Hardware Oriented Security and Trust (HOST) (2016), pp. 124–129.

    Google Scholar 

  62. S. Berezin, Model checking and theorem proving: a unified framework. Ph.D. Thesis, SRI International (2002)

    Google Scholar 

  63. P. Dybjer, Q. Haiyan, M. Takeyama, Verifying haskell programs by combining testing, model checking and interactive theorem proving. Inf. Softw. Technol. 46 (15), 1011–1025 (2004)

    Article  Google Scholar 

Download references

Acknowledgements

This work has been partially supported by the National Science Foundation (NSF-1319105), the Army Research Office (ARO W911NF-16-1-0124), and Cisco.

Author information

Authors and Affiliations

  1. University of Central Florida, Orlando, FL, 32816, USA

    Xiaolong Guo, Raj Gautam Dutta & Yier Jin

Authors
  1. Xiaolong Guo
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Raj Gautam Dutta
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Yier Jin
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Yier Jin .

Editor information

Editors and Affiliations

  1. Department of Computer and Information Science and Engineering, University of Florida , Gainesville, Florida, USA

    Prabhat Mishra

  2. Department of Electrical and Computer Engineering, University of Florida , Gainesville, Florida, USA

    Swarup Bhunia

  3. Department of Electrical and Computer Engineering, University of Florida , Gainesville, Florida, USA

    Mark Tehranipoor

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this chapter

Cite this chapter

Guo, X., Dutta, R.G., Jin, Y. (2017). IP Trust Validation Using Proof-Carrying Hardware. In: Mishra, P., Bhunia, S., Tehranipoor, M. (eds) Hardware IP Security and Trust. Springer, Cham. https://doi.org/10.1007/978-3-319-49025-0_10

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-49025-0_10

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-49024-3

  • Online ISBN: 978-3-319-49025-0

  • eBook Packages: EngineeringEngineering (R0)

Publish with us

Policies and ethics

Search

Navigation