Doctoral Thesis: Techniques for Foundational End-to-End Verification of Systems Stacks

Wednesday, August 21
3:00 pm - 4:30 pm

32-G882

Add to Calendar
FacebookTwitterLinkedInEmailShare

By: Samuel Gruetter

Details

  • Date: Wednesday, August 21
  • Time: 3:00 pm - 4:30 pm
  • Category:
  • Location: 32-G882
Additional Location Details:

Abstract: Today’s software is full of bugs and vulnerabilities. Formal verification provides a promising remedy through mathematical specifications and machine-checked proofs that the implementations conform to the specifications. However, there could still be bugs in the specifications or in the verification tools, which could lead to missed bugs in the software being verified. Therefore, this dissertation advocates for foundational end-to-end verification, a proof-based software development method that can mitigate both of these concerns:

It is end-to-end in the sense that the correctness proofs of individual components are used to discharge the assumptions of adjacent components throughout the whole stack, resulting in end-to-end theorems that only mention the top-most and bottom-most specifications, so that bugs in intermediate specifications cannot invalidate the soundness of the end-to-end statement anymore.

The method is foundational in the sense that the soundness of the proofs only relies on the foundations of mathematics and on the correctness of a small proof-checking kernel, but not on the correctness of other, domain-specific verification tools, because these tools are either proven correct once-and-for-all, or they output proofs that are checked by the kernel.

Ensuring that all the reasoning can be checked by the same small foundational kernel requires considerable effort, and the first part of this dissertation presents techniques to reduce this effort:

Omnisemantics, a new style of semantics that can be used instead of traditional small-step or big-step operational semantics, offer a smooth way of combining undefined behavior and nondeterminism, and enable forward-simulation compiler correctness proofs with nondeterministic languages, whereas previous approaches need to fall back to the much less convenient backward simulations if support for nondeterminism is needed.

Live Verification is proposed, a technique to turn an interactive proof assistant into a programming assistant that displays the symbolic state of the program as the user writes it and allows the user to tweak the symbolic state as long as the tweaks are provably sound. An additional convenience-improving feature is that instead of stating lengthy loop invariants, the user only needs to give the diff between the symbolic state before the loop and the desired loop invariant, resulting in shorter and more maintainable annotations. Finally, in order to make Live Verification practical, a number of additional proof techniques is presented.

The second part of the dissertation shows how these techniques were useful in three collaborative case studies: An embedded system running on a verified processor with an end-to-end proof where the software-hardware interface specification cancels out, a cryptographic server with an end-to-end proof going from high-level elliptic-curve math all the way down to machine code, and a trap handler to catch unsupported-instruction exceptions whose correctness proof combines program-logic proofs about C-level functions, a compiler correctness proof, and proofs about hand-written assembly.

Zoom Link:
https://mit.zoom.us/j/94297415474

Host