Model Validation for DARPA DPRIVE
| Commodity hardware description languages (HDLs) like VHDL and Verilog present a challenge from a high assurance point of view because they lack formalized semantics: when a team of hardware engineers produce a circuit design in a commodity HDL and claims that it correctly implements a pseudocode algorithm, on what basis can that claim be evaluated? A formalized model of the circuit design may be painstakingly created (e.g., in the logic of a theorem prover), but how is the accuracy and faithfulness of that model then established? The distance between the widely adopted commodity HDLs and formal models of hardware have been a well-recognized and persistent impediment to driving formal methods into hardware development. |
This talk presents a technique developed at Two Six Technologies, called model validation, that formally connects hardware design and its formal model via a functional, high-level synthesis language called ReWire1. Model validation introduces a “model” program to bridge the gap between the hardware design and algorithm by establishing 1) the equivalence of the algorithm to the model and 2) the equivalence of the model to the circuit design. Equivalence between the algorithm and the ReWire model is verified with a ReWire semantics formalized in Isabelle. Equivalence between the ReWire model and the circuit design is established by producing binary circuits from each (using commodity synthesis tools and the ReWire compiler rwc) and then applying an automated binary equivalence checker.
This talk describes our experience applying model validation as part of the DARPA Data Protection in Virtual Environments (DPRIVE) program2. DPRIVE aims to develop a novel hardware accelerator to ease computational challenges preventing widespread use of fully homomorphic (FHE) that began with Gentry’s discovery3 and was improved upon in the PROCEED4 program. To this end DPRIVE’s purpose is to design hardware accelerators to improve upon the existing algorithmic gains to FHE. Model validation through ReWire moves formal methods into the practical world, empowering hardware designers to reason about the correctness, safety, and security properties of their designs. In addition, we expect our pipeline to protect hardware supply chains by allowing for a full formal analysis of RTL implementations before tape out.
- http://mu-chaco.github.io/ReWire/
- https://www.darpa.mil/news-events/2020-03-02
- Gentry, Craig. A fully homomorphic encryption scheme. Stanford university, 2009.
- https://www.darpa.mil/program/programming-computation-on-encrypted-data
Distribution Statement "A" (Approved for Public Release, Distribution Unlimited)
Ian Blumenfeld is the Research Director for Mathematics at Two Six Technologies. In that role, he is a principal investigator on multiple DARPA programs, spanning the areas of formal methods, modern cryptography, and applied category theory. Prior to his work at TwoSix, Ian was a formal verification engineer at Apple, where he verified cryptographic properties of the iPhone secure enclave processor. Ian has worked in roles in and around the federal research space for more than a decade, including 5 years as an applied research mathematician at the National Security Agency.
License: DARPA Public Release