Validating a High-Performance, Programmable Secure Coprocessor

This paper details our experiences with successfully validating a trusted device at FIPS 140-1 Level 4, earning the world's first certificate at this highest level. Over the last several years, our group designed and built a physically secure PCI card containing a general purpose processor with crypto support. However, for this device to function as a trusted platform for secure coprocessor applications, we needed to establish that assurance through independent validation. We chose FIPS 140-1, since discussions of secure hardware usually cite that standard, and Level 4, since the weaker levels did not provide sufficient assurance for many proposed applications.
Successful validation at Level 4 required withstanding a fairly open-ended suite of physical attacks, and preparing formal modeling and verification of the internal software-as well as meeting a number of other sizeable challenges that were not initially apparent. In some sense, our validation effort was an experiment to quantify the design and work effort necessary to achieve this previously unachieved security assurance level. Since our device is a programmable platform, we hope this work substantially lowers the barrier for others to develop, deploy, and validate secure coprocessor applications.