Mechanized Certification of Secure Hardware Designs

S. Ray and W. A. Hunt, Jr.

In M. S. Abadir, L. Wang, and J. Bhadra, editors, Proceedings of the 8th International Workshop on Microprocessor Test and Verification, Common Challenges and Solutions (MTV 2007), Austin, TX, December 2007, pages 25-32. IEEE Computer Society

© 2008 IEEE. Personal use of this material is permitted. However, permission to reprint/republish this material for advertising or promotional purposes or for creating new collective works for resale or redistribution to servers or lists, or to reuse any copyrighted component of this work in other works must be obtained from the IEEE.


Abstract

We develop a framework for mechanized certification of secure hardware systems built out of commercial off-the-shelf (COTS) components purchased from untrusted vendors. Certification requires a guarantee that the fabricated system satisfies the requisite safety and security properties. Our framework facilitates this by (1) providing an unambiguous description of the requirements specification in a formal, computational logic, (2) a formalized hardware description language (HDL) to describe the implementation, and (3) mechanical tools and techniques for providing a certification of correctness and security. We illustrate the use of the framework in certifying the correctness and security properties of the netlist implementation of a voting machine using the ACL2 theorem prover.

Relevant files


BibTex

@Inproceedings{ray-certification,
  author    = "S. Ray and Hunt, Jr., W. A.",
  title     = "{Mechanized Certification of Secure Hardware Designs}",
  booktitle = "{Proceedings of the 8th International Workshop on Microprocessor Test and Verification, 
                Common Challenges and Solutions (MTV 2007)}",
  editor    = "M. S. Abadir and L. Wang and J. Bhadra",
  address   = "{Austin, TX}",
  month     = dec,
  year      = "2007",
  pages     = "25-32",
  publisher = "IEEE Computer Society"
}