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, our primary current project goal is developing a Continuous Assurance system.  This system will support incremental progress in writing and evolving proofs about code by integrating static and dynamic verification in the context of continuous integration.

The basic Continuous Assurance system is a first step that makes it easier to evolve proofs by providing continuous feedback about the consistency and correctness of specifications and code.  It is also a foundation for later parts of the project, including a proof maintenance system that quickly restores static and dynamic verifiability after a change to code, and a proof repair system that helps developers make more comprehensive fixes to proofs that were broken by software evolution.  Together, we believe these systems will have a substantial effect on maintaining proofs over time.

We are now working on formative evaluation of the continuous assurance system--specifically to understand whether and how it helps proof developers to construct and evolve valid proofs more effectively, and whether there are any barriers to usage that we can overcome by refining the design of the system. We are also beginning to work on the proof maintenance system that will provide automated support for bringing proofs that have been broken as a result of software evolution into compliance.

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.