Scaling Formal Verification with Specification Extraction
| Abstract: Formal verification is a powerful tool for assuring software systems. By building machine-checked mathematical proofs that software meets its specifications, formal verification provides high confidence that softwareis correct and free of vulnerabilities. Unfortunately, formal verification is also difficult and expensive, specifically for programs that use and manipulate pointers. Although there are powerful separation logics for manually verifying pointer programs, they require a high degree of time and expertise to effectively use them. There are also a number of automated verification tools, based on techniques such as symbolic execution or model-checking, but these are often brittle in terms of which programs they can handle and only work for specific sorts of properties. In this talk, we will discuss a new approach called specification extraction that reduces the time and effort of verifying pointer programs, allowing it to scale up to larger and more complex systems. |
This approach extracts functional specifications that describe the behaviors of programs from which they are extracted ina logical language without pointers. Because the extracted specifications do not contain pointers, they are much easier to verify than the original programs.
Specification extraction works by type-checking the LLVM bitcode of the program being verified using a Rust-like memory-safe type system for LLVM. This allows the specification extraction system to understand how pointers flow through the program. It then uses the proofs-as-programs principle to extract functional specifications from the type-checking proofs of programs that are well-typed in this type system. Users control this process by giving Rust-like types for each of the functions in their program. For programs written in Rust, this can be done automatically by translating the Rust types of its functions to the LLVM-level type system. The benefit of using type-checking to analyze an input program as compared to other automated tools and analyses is that type-checking is a form of automated analysis that users can understand. When the analysis fails, it gives the users meaningful type errors that they can interpret and fix, either by adding type annotations or fixing bugs that those type errors have uncovered in the original program. The benefit compared to manual separation logic tools is that specification extraction performs all the pointer and separation reasoning automatically without requiring nearly the same amount of time and expertise aswriting a separation logic proof.
Specification extraction has been implemented as the Heapster extension of the Software Analysis Workbench (SAW)1, and has been described in a recent publication.2 Heapster is being used in ongoing DARPA and DoD programs to assure security-critical applications. A key area where Heapster is being applied is toverify implementations of communications and cryptographic protocols. Correct implementation of these sorts of protocols is often critical to security of a system. Verifying a protocol generally requires proving that the implementation matches a state machine, which is often written at a high level of abstraction.Specification extraction is useful in this sort of verification because it generates specifications at a higherlevel of abstraction than the original implementation, making them much closer to and easier to comparewith these state machine specifications.
1SAW with Heapster is available at https://github.com/GaloisInc/saw-script/
2 He et al., “A Type System for Extracting Functional Specifications from Memory-Safe Imperative Programs”, OOPSLA2021.
Dr Westbrook is a research lead at Galois, Inc. He develops scalable formal methods tools for real-world applications, including in the space domain. He has been the principle investigator for a number of Galois efforts on government programs for DARPA and the Space Force. He earned his doctorate in Computer Science from Washington University in Saint Louis in 2008.