High-Assurance Synthesis and Analysis Techniques for Memory-Safe Programming Languages     

Memory-safe programming languages have garnered significant interest in recent years, with memory-safe language initiatives issuing from NSA, as well as the White House Office of Science and Technology Policy.  The Rust language has attracted particular attention, due to its unique memory ownership model and efficient compiler, capable of producing code that is competitive in efficiency with C/C++ compilers.

Google  and Amazon are major Rust adopters, and Rust development support is being added to the Linux kernel.  Additionally, after spending decades dealing with a never-ending parade of security vulnerabilities due to C/C++, which continue to manifest at a high rate despite the use of sophisticated analysis tools, Microsoft announced at its BlueHat 2023 developer conference that is was beginning to rewrite core Windows libraries in Rust.

For formal methods practitioners, Rust and other memory-safe languages present opportunities for high-assurance synthesis, as well as formal analysis.

The goal in  formal synthesis is to extract code in a given implementation language from a formal (or semi-formal) specification.  The code extraction process may be conducted via a mathematically proven set of transformations, as in the HOL4-hosted CakeML compiler (which provides a verified compilation process all the way to binary); or it may take the form of a semi-formal "pretty-printing" process, as in the extraction of OCaml code from Coq specifications.  In order to interoperate with mainstream development methods, extraction is often made to C/C++.

But, with the increasing use of memory-safe languages such as Rust, formal methods toolsmiths have an opportunity to produce extraction and transpilation tools from formal/semi-formal specifications that can produce higher-quality, analyzable code by targeting a  memory-safe language.  In this talk, we will describe new efforts by our research team to perform high-assurance formal synthesis to the Rust programming language.

One of the advantages of the memory-safe languages is the capability to reason about application code written in the imperative style favored by industry, but without the snarls of the unrestricted pointers of C/C++.  Much progress has been made to this end in recent years, and developers can now verify the correctness of common open-source algorithm and data structure code that utilizes common idioms such as records, loops, modular integers, and the like, and verified compilers can guarantee that such code is compiled correctly to binary.  Many open-source verification tools have emerged to reason about code written in memory-safe languages, such as the Verus verification tool for Rust programs developed by our teammates at Carnegie-Mellon University, the Kani model checker for Rust developed by Amazon, etc.  We will provide an overview of our use of formal verification tools for memory-safe languages in this talk.

Part of our interest in Rust stems from its potential as a hardware/software co-assurance language. This interest is motivated in part by emerging application areas, such as autonomous and semi-autonomous platforms for land, sea, air, and space, that require sophisticated algorithms and data structures, are subject to stringent accreditation/certification, and encourage hardware/software co-design approaches.  In this talk, we will update our progress on the use of Rust as a High-Level Synthesis (HLS) language.

HLS developers specify the high-level abstract behavior of a digital system in a manner that omits hardware design details such as clocking; the HLS toolchain is then responsible for "filling in the details" to produce a Register Transfer Level (RTL) structure that can be used to realize the design in hardware. HLS development is thus closer to software development than traditional hardware design in Hardware Description Languages (HDLs) such as Verilog or VHDL.  Most incumbent HLS languages are a subset of C, e.g. Mentor Graphics' Algorithmic C, or Vivado HLS by Xilinx.  A Rust-based HLS would bring a single modern, type-safe, and memory-safe expression language for both hardware and software realizations, with very high assurance.

As a study of the suitability of Rust as an HLS, we have crafted a Rust subset, inspired by Russinoff's Restricted Algorithmic C (RAC), which we have imaginatively named Restricted Algorithmic Rust, or RAR.  In fact, in our first implementation of a RAR toolchain, we merely "transpile" (perform a source-to-source translation of) the RAR source into RAC.  By so doing, we leverage a number of existing hardware/software co-assurance tools with a minimum investment of time and effort.  By transpiling  RAR to RAC, we gain access to existing HLS compilers.  But most importantly for our research, we leverage the open-source RAC-to-ACL2 translator that Russinoff and colleagues at Arm have successfully utilized in industrial-strength floating point hardware verification. We conclude the talk by describing recent progress in the formal verification of a number of hardware/software co-assurance examples written in the RAR Rust subset, targeting both hardware and software implementation.

David S. Hardin has made contributions in the areas of formal methods, computer architecture for High Assurance systems, as well as memory-safe programming languages. He is currently Chief Technologist for Trusted Methods in the Applied Research and Technology organization at Collins Aerospace, where he has served as Principal Investigator or Researcher for several U.S. DoD Research and Development programs. He most recently contributed to the DARPA Cyber-Assured Systems Engineering program (CASE).  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. He is author or co-author of more than 75 peer-reviewed publications, and is an inventor or co-inventor on 15 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.  In 2023, he was inducted into the Woodford County (KY) Public Schools Hall of Fame.