#!/usr/local/bin/php ITCES Workshop 2006

Workshop on
Innovative Techniques for
Certification of Embedded Systems
April 4, 2006
San Jose, California, USA

Extended submission deadline: March 3, 2006

Satellite workshop of the

 
 
 
 
 
 

Question or Comment
Contact: Oleg Sokolsky
Last updated: March 23, 06

Using Formal Methods in a Security Certification

Matt Wilding

Rockwell Collins

In May 2005 the Rockwell Collins’ AAMP7G microprocessor was certified as capable of simultaneously processing information at all classification levels. The certification included a formal verification that the microprocessor implements secure partition separation. A formal low-level design model corresponding line-for-line with the microprocessor's microcode was proved to work properly. The AAMP7G separation correctness theorem and proof were developed using the ACL2 theorem prover, and the hundreds of pages of definitions and lemmas that lead ACL2 to accept the separation correctness proof were checked using this publically-available tool.

In this talk I will describe how we analyzed the AAMP7G, what we needed to invent to accomplish the verification, and what is needed to make formal methods based certifications of this kind more routine. (The AAMP7G's formal verification was joint work with David Greve and Ray Richards)