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
• Hemant Gouni, 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:

1. 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 have designed 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, and are now piloting and running those studies.
2. 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. 

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 and also through a new foundation for hybrid static/dynamic information flow, 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, which was presented 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 (see https://borrowsanitizer.com/), with the goal of eventually deploying continuous assurance across the Rust ecosystem.

Finally, we have developed a new foundation for continuous assurance of information flow.  Existing information flow type systems have seen little adoption, likely in part due to the complexity of the specifications required.  We propose a new approach, Structural Information Flow, drawing from insights in modal and hybrid logic, We show with a range of examples that structural information flow specifications are straightforward to write and easy to visually parse. Uniquely in the structural setting, we demonstrate that declassification emerges not as an aberration to non-interference, but as a natural and unavoidable consequence of sufficiently general machinery for information flow. This flavor of declassification features excellent local reasoning and enables our approach to account for real-world information flow needs without compromising its theoretical elegance. Finally, we establish non-interference via a logical relations approach, showing off its simplicity in the face of the expressive power captured.  This work will be presented at OOPSLA 2025.

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.  Proc. International Conference on Software Engineering, 2025.  Slides for this paper presentation were presented at the July 2025 Science of Security meeting and were uploaded to the VO.
• Hemant Gouni, Frank Pfenning, and Jonathan Aldrich.  Structural Information Flow: A Fresh Look at Types for Non-Interference.  To appear in Proceedings of the ACM on Programming Languages (PACMPL), issue OOPSLA2, 2025.

The second paper has been accepted but is not yet published.  We will add it to the SoS VO when it is published, at which point we will have complete BibTeX information