Title
A robust machine code proof framework for highly secure applications
Abstract
Security-critical applications at the highest Evaluation Assurance Levels (EAL) require formal proofs of correctness in order to achieve certification. To support secure application development at the highest EALs, we have developed techniques to largely automate the process of producing proofs of correctness of machine code. As part of the Secure, High-Assurance Development Environment program, we have produced in ACL2 an executable formal model of the Rockwell Collins AAMP7G microprocessor at the instruction set level, in order to facilitate proofs of correctness about that processor's machine code. The AAMP7G, currently in use in Rockwell Collins secure system products, supports strict time and space partitioning in hardware, and has received a U.S. National Security Agency (NSA) Multiple Independent Levels of Security (MILS) certificate based in part on a formal proof of correctness of its separation kernel microcode. Proofs of correctness of AAMP7G machine code are accomplished using the method of "compositional cutpoints", which requires neither traditional clock functions nor a Verification Condition Generator (VCG). In this paper, we will summarize the AAMP7G architecture, detail our ACL2 model of the processor, and describe our development of the compositional cutpoint method into a robust machine code proof framework.
Year
DOI
Venue
2006
10.1145/1217975.1217978
ACL
Keywords
Field
DocType
machine code,aamp7g architecture,rockwell collins secure system,robust machine code proof,formal proof,secure application,multiple independent levels,executable formal model,acl2 model,rockwell collins aamp7g microprocessor,aamp7g machine code,development environment,national security agency,certification,application development,cryptography,theorem proving
Microcode,Programming language,Cryptography,Instruction set,Computer science,Correctness,Theoretical computer science,Artificial intelligence,Formal proof,Executable,Machine code,Mathematical proof,Machine learning
Conference
ISBN
Citations 
PageRank 
0-9788493-0-2
23
2.05
References 
Authors
5
3
Name
Order
Citations
PageRank
David S. Hardin1273.90
Eric W. Smith2232.05
William D. Young333166.64