Travis Hance

Verifying Concurrent Systems Code Degree Type: CS
Advisor(s): Bryan Parno
Graduated: August 2024

Abstract:

Concurrent software is notoriously difficult to write correctly, so to increase confidence in it, it is often desirable to apply formal verification techniques. One technique that is especially promising for verifying concurrent software is concurrent separation logic (CSL), which uses reasoning principles based on resource ownership. However, even with CSL, verifying complex systems at scale (e.g., those with 1000s of lines of code) remains challenging. The reasons it remains challenging include,

1. The manual proof effort required by many existing CSL frameworks.
2. The inherent complexity of the target systems. Sophisticated systems may have custom, low-level synchronization logic, which may be deeply intertwined with domain logic, in the interest of performance.

We posit that a promising way to overcome (1) is, rather than using CSL directly, to use an ownership type system such as Rust's, taking advantage of its sophisticated but efficient type-checking algorithms. To demonstrate this, we develop a full methodology, from theory to implementation, based around this core idea, showing that we can recover the rich reasoning principles of CSL in this setting In particular, we show that this methodology is rich enough to support the verification of inherently complex systems as in (2).

Thesis Committee:
Bryan Parno (Chair)
David Andersen
Frank Pfenning
Derek Dreyer (Max Planck Institute for Software Systems)

Srinivasan Seshan, Head, Computer Science Department
Martial Hebert, Dean, School of Computer Science

Keywords:
Rust, systems, formal verification, separation logic, Iris, type systems, ownership types, semantic types