SHF: Small: End-to-End Formal Verification of Concurrent C Programs

University Of Illinois At Chicago, Chicago IL

Investigators

Abstract

The C programming language is widely used in both the basic software that makes computers work, and in high-performance applications that need to perform many computations at the same time (concurrently). Unfortunately, C code is highly error-prone, and concurrent C code is even more so. The goal of this project is to guarantee that concurrent C programs always run correctly by developing tools for mathematically proving the correctness of those programs. The project’s novelties are the development of an end-to-end toolchain for concurrent C programs, with interactive and automatic proof tools at the top, a precise model of the behavior of concurrent C programs (including the latest high-performance concurrency features) in the middle, and a formal connection to the code that the computer actually executes at the bottom. The project’s impacts are more reliable software and a reduction in software failures, including those that lead to lost productivity, privacy and security breaches, and even physical safety incidents (for instance, due to bugs in car software). The project builds on the newest version of the Verified Software Toolchain (VST), a tool for proving that C programs meet specifications written in separation logic. Notably, VST is formally connected to the CompCert verified compiler, so that programs verified in VST are mathematically guaranteed to compile to assembly code with the desired behavior. The project extends VST in two directions. First, it integrates RefinedC, an annotation-based verifier for C based on the Iris separation logic framework; the newest version of VST also rests on Iris foundations, so the investigator will reimplement RefinedC’s annotations in VST and extend them to more features of the C language, yielding a semi-automatic end-to-end verification system for C programs. Second, the project extends VST’s logic and foundational guarantees to concurrent programs, including those that use the atomic operations introduced in the C11 standard. This includes both sequentially consistent operations (where each memory address appears to contain a single value) and, ultimately, weak-memory operations (where different threads may see different values at the same address). The end result is a complete toolchain for guaranteeing that high-performance concurrent C programs meet their specifications when compiled and run. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.