VeriCores: Cyber-Instrumenting Devices Built from Verified Components
Presented as part of the 2018 HCSS conference.
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 Rockwell Collins, 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 60 peer-reviewed publications, and is a co-inventor on 12 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.
ABSTRACT
Experience on cyber-assurance research and development programs such as DARPA HACMS has taught us that the safety and security of systems constructed using legacy components can be significantly improved if low-overhead monitoring/attestation/cross-domain elements are introduced at critical interfaces. Such elements establish that system components achieve acceptable performance and isolate bad behavior. These subsystems must be designed to a high level of assurance and operate in a trustworthy fashion, lest their introduction increases, rather than decreases, the system's attack surface.
We are currently developing VeriCores, standardized cyber-instrumenting devices for high-assurance systems built using verified components. A VeriCore is intended to minimize "consumables", such as Size, Weight, Power, and Cost (SWaP-C). This is both a security, as well as an engineering concern, as a "bad actor" can't attack a resource that isn't present. In some designs, a VeriCore may be instantiated as a "bump-in-the-wire", drawing its power from the monitored interface, acting as a pass-through for valid transactions over that interface, and establishing execution characteristics for appraisal. In the case where a high-assurance separation kernel is already present, the VeriCore logic may be implemented solely in software, and execute in a partition of that operating system.
The basic software stack for a VeriCore consists of the seL4 verified microkernel, verified drivers for supported I/O interfaces, a verified networking stack for seL4 currently in development by Kestrel Institute under DARPA funding, and a minimal verified runtime and measurement capability derived from the CakeML verified ML compiler. The VeriCore tool suite includes tools supporting verified development and synthesis of application-specific components. The goal of VeriCore development is to produce verified applications to execute on the verified runtime environment, employing Verification-Enhanced Development principles.
Once realized, VeriCore instances can be "dropped into" critical systems designs as needed, wherever critical, provably correct basic input validation, lexing, parsing, attestation protocol handling, data transformation, cross-domain filtering, majority voting, basic secure hash, etc. functions are required in order to meet high-assurance design requirements.
In order to provide efficient implementations of high-level data structures with the high assurance needed for VeriCore deployment, we have developed a verifying compiler approach that supports the "natural" functional proof style, but yet applies to more efficient data structure implementations. Algorithms are expressed in a system-level language called DASL, employing a mostly-functional style (similar to modern programming languages, such as Swift and Rust), with additional annotations indicating maximum array sizes, etc. We base the Intermediate Verification Language for the DASL toolchain upon higher-order logic; thus, claims about program behavior, as well as source-to-source transformations of the intermediate form, can be mathematically proven. On that basis, proofs about high-level programs over high-level data structures can be carried out while a formal, proved connection to the low-level efficient implementation is automatically ensured.
DASL compiler output is source code for a choice of conventional programming languages, such as Ada, Java, VHDL, C or ML. This source is then further compiled to machine code or an FPGA bit file using conventional tools and a small set of verified runtime functions. Since we compile to an array-based implementation, supporting hardware implementations is particularly straightforward. If the user selects ML code generation, we are able to offer a complete verified toolchain and verified execution environment down to the machine code level, using technologies from the CakeML project. CakeML provides mechanisms to convert HOL4 logic formulas to a subset of Standard ML, as well as a verified compiler from that ML subset to machine code for a number of common Instruction Set Architectures. We thus can readily perform a verified translation of a DASL program to machine code, and execute that verified machine code on VeriCore hardware.
In this talk we will describe the VeriCore infrastructure, detail VeriCore application development, and discuss various applications of the technology to large, heterogeneous systems as well as autonomous systems. We will conclude with a demonstration of the VeriCore technology on representative hardware.