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

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 starting to work on formative evaluation of the continuous assurance system, and are also beginning to work on the proof maintenance system.

Accomplishments

We have now prototyped an initial integrated development environment (IDE) supporting continuous assurance in support of the first project goal.  Our current prototype allows developers to view the verification status of their code and implements an initial proof debugger that helps developers understand the symbolic state of the verifier at every program point.  This debugger will allow 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.

The prototype above meets our anticipated milestone that within 6 months we would have a first version of a continuous assurance system.  We anticipate having a complete, refined version of this by the end of the first year of the project, as envisioned in our proposal.

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 prototype above makes an initial contribution to this area, but more refinement will be necessary to realize the potential impact of this idea.

Publications and presentations

There are no publications as we are only 6 months into the project.  PI Aldrich gave a technical presentation on Continuous Reasoning with Gradual Verification at the Science of Security PI meeting held in July 2024; the slides were uploaded as part of the meeting record, and are also attached below.