Verified Hardware/Software Co-Assurance: Enhancing Safety and Security for Critical Systems
Abstract:
Experienced developers of safety-critical and security-critical systems have long emphasized the importance of applying the highest degree of scrutiny to a system's I/O boundaries. From a safety perspective, input validation is a traditional “best practice.” For security-critical architecture and design, identification of the attack surface has emerged as a primary analysis technique. One of our current research focus areas concerns the identification of and mitigation against attacks along that surface, using mathematically-based tools. We are motivated in these efforts by emerging application areas, such as assured autonomy, that feature a high degree of network connectivity, require sophisticated algorithms and data structures, are subject to stringent accreditation/certification, and encourage hardware/software co-design approaches. We have conducted several experiments employing a state-of-the-art toolchain, due to Russinoff and O'Leary, and originally designed for use in floating-point hardware verification, to determine its suitability for the creation of safety-critical/security-critical input filters. We focus first on software implementation, but extending to hardware as well as hardware/software co-designs. We have implemented a high-assurance filter for JSON-formatted data used in an Unmanned Aerial Vehicle (UAV) application. Our JSON filter is built using a table-driven lexer/parser, supported by mathematically-proven lexer and parser table generation technology, as well as verified data structures. Filter behavior is expressed in a subset of Algorithmic C, which defines a set of C++ header files providing support for hardware design, including the peculiar bit widths utilized in that discipline, and enables compilation to both hardware and software platforms. The Russinoff-O'Leary Restricted Algorithmic C (RAC) toolchain translates Algorithmic C source to the Common Lisp subset supported by the ACL2 theorem prover; once in ACL2, filter behavior can be mathematically verified. We describe how we utilize RAC to translate our JSON filter to ACL2, present proofs of correctness for its associated data types, and describe validation and performance results obtained through the use of concrete test vectors.
|
BIO Dr. David S. Hardin has made contributions in the areas of formal methods, computer architecture for High Assurance systems, as well as real-time and embedded Java. He is a Principal Research Engineer in the Advanced Technology Center at Collins Aerospace, and currently serves as a co-Principal Investigator for the DARPA CASE (Cyber Assured Systems Engineering) program. He is the editor of the book Design and Verification of Microprocessor Systems for High-Assurance Applications (Springer 2010), and a co-author of The Real-Time Specification for Java, as well as the Java 2 Micro Edition Connected Device Configuration/Foundation Profile standards. He is author or co-author of more than 70 peer-reviewed publications, and is a co-inventor on 14 U.S. patents. In 1999, Dr. Hardin co-founded aJile Systems, a startup company focused on real-time and embedded Java technology, and served as aJile's Chief Technical Officer from 1999 to 2003. |
Dr. Hardin was selected as a Rockwell Engineer of the Year for 1997 for his contributions to the development of the world's first Java microprocessor. His academic career includes BSEE and MSEE degrees from the University of Kentucky, and a Ph.D. in Electrical and Computer Engineering from Kansas State University, in 1989. Dr. Hardin is a proud native of the Commonwealth of Kentucky, and is a Kentucky Colonel.