Mechanized Certification of Secure Hardware Designs

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 net list implementation of a voting machine using the ACL2 theorem prover.