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 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.

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.

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 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 1 year into the project.  We do have publications in preparation & submission so we anticipate there will be more to report soon!

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 were attached to the quarterly report for Q2 2024.