Research Team Status
- Jonathan Aldrich, Professor, School of Computer Science
- Joshua Sunshine, Assistant Professor, School of Computer Science
- Long Nguyen, Ph.D. student, School of Computer Science
- Ian McCormack, Ph.D. student, School of Computer Science
We are also collaborating with Jenna DiVincenzo at Purdue University, who pioneered gradual verification in her thesis work with Jonathan and Joshua.
Project Goals
Following the research program outlined in our technical proposal, we are working on the following goals:
- We are refining and evaluating the Continuous Assurance system developed in year 1 of the proposal. This system support incremental progress in writing and evolving proofs about code by integrating static and dynamic verification in the context of continuous integration. We are currently designing user studies that will help us refine the design of the system and evaluate whether it helps developers more easily create and evolve correctness proofs about code.
- We are also beginning to work on the proof maintenance and repair system that will provide automated support for bringing proofs that have been broken as a result of software evolution into compliance. We expect to have an initial prototype of the system in the next quarter, but we anticipate ongoing refinement and extensions to cover more cases of code and specification evolution over the rest of the grant period of performance.
Our main continuous assurance system is focused on functional correctness and security properties in C0 an education subset of C used in teaching at CMU. However, we are also exploring continuous assurance through hybrid static/dynamic verification techniques in Rust, with initial results as reported below.
Accomplishments
We met our first milestone: defining the first version of our Continuous Assurance system. This system is embodied in a IntelliJ Plugin for gvc0, our gradual verification system. The plugin is available at:
https://github.com/advancingdragon/c0
and the README.md file there has instructions on how to install it. Our system allows developers to write, edit, and check proofs about their code. It also implements a novel proof debugger that helps developers understand the symbolic state of the verifier at every program point. This debugger allows developers to quickly understand and fix problems with their proofs. We believe the debugger will significantly increase the usability of the continuous assurance, automatic proof repair, and proof generation tools in our continuous reasoning for gradual verification project; our formative evaluation (currently under way) will provide a preliminary assessment of this and guide the future refinement of the system.
We also developed a continuous assurance system for security-relevant memory safety properties in Rust. Rust enforces memory safety statically for the safe part of Rust, but in practice, essentially all Rust code relies on code written in C for functionality that cannot be or has not yet been written in Rust. That C code must also follow Rust's rules for pointers that are shared with Rust, but previously, there has been no way to enforce this. Our approach, to appear in ICSE 2025, combines an existing tool for checking unsafe Rust with the LLVM interpreter executing linked C code in order to check C's use of Rust pointers. Our study of open-source Rust crates identified 47 instances of undefined or undesired behavior in 37 libraries. Three bugs were found in libraries that had more than 10,000 daily downloads on average during our observation period, and one was found in a library maintained by the Rust Project. We are working with developers in the Rust project to make this a production-ready tool, with the goal of eventually deploying continuous assurance across the Rust ecosystem.
Continuous assurance is a new, foundational area of cybersecurity research that was an explicit part of the Science of Security vision and the main focus of our proposal. The continuous assurance prototypes above make an initial contribution to this area, but more refinement will be necessary to realize the potential impact of this idea.
Publications and presentations
Ian McCormack, Jonathan Aldrich, and Joshua Sunshine. A Study of Undefined Behavior Across Foreign Function Boundaries in Rust Libraries. To appear in Proc. International Conference on Software Engineering, 2025.