F* PoP Up Seminar

Modular Verification of Non-Leakage for Hardware Security Modules with K2

K2 is a framework for proving that an implementation of a hardware security module (HSM) leaks nothing more than what is mandated by its functional specification. K2's proof covers the software and the hardware of an HSM, which enables it to catch all bugs above the cycle-level digital circuit abstraction, including timing side channels. K2's key contribution is a novel approach to proving non-leakage in a modular fashion, using transitive information-preserving refinement. This enables K2 to use different techniques for verifying different layers (software and hardware), reuse existing verified components, and largely automate several parts of the proof, while still providing a single top-to-bottom combined theorem. We use K2 to develop several HSMs, including an ECDSA certificate-signing HSM and a password-hashing HSM, on top of the OpenTitan Ibex and PicoRV32 processors. K2 provides a strong guarantee for these HSMs; for instance, it proves that the ECDSA-on-Ibex HSM implementation (2,300 lines of code and 13,500 lines of Verilog) leaks nothing more than what is allowed by a 50-line specification of its behavior.

Mechanised Verification of an OCaml-style Garbage Collector

Programming languages with managed runtimes often provide memory safety with the help of a garbage collector (GC). GCs are often implemented in an unsafe language like C and utilise low-level memory operations. Bugs in the GC implementation affects the memory safety guarantees of the managed language.

In this work, we present a specification and verification framework for GCs operating over OCaml-style objects. Unlike prior work, our correctness conditions are based on graph reachability, which permits evolution of the GC without having to rewrite the core safety specifications. Our framework is developed in F*, a proof-oriented solver-aided programming language, and its subset Low*, which facilitates extraction of verified C code. Using this framework, we have verified a stop-the-world mark and sweep GC which is compatible with OCaml. Our experimental results illustrates that the extracted verified code performs on par with a handwritten GC implementation.

The Lazy Professor's Route to Teaching Programming Language Semantics a.k.a. A Theorem Proving Approach to PL Semantics

The talk will unfold the story of a lazy professor who felt that using theorem provers is an "easy" shortcut to messy proofs while teaching programming languages theory. We will discuss his experience of using this methodology (and the story of distressed students) in an ACM summer school on programming languages. Once the program and its semantics are encoded in any of the different styles—operational, denotational, or axiomatic, powerful proof assistants like F* can prove exciting language features with minimal human assistance. The hope is that teaching programming languages via proof assistants will not only provide a more concrete understanding of this topic but also prepare future programming language researchers to use theorem provers as fundamental tools in their research and not as an afterthought. Well, although the methodology was born out of the professor's attempt at saving face after a heavy dose of procrastination, it opens up interesting questions on if undergraduate students are ready enough to date theorem provers.

Related paper

Securing Verified IO Programs Against Unverified Code in F*

YouTube recording of the talk, Paper, Code.