First Formal Methods in the Field (FMiTF) Bootcamp

The first FMitF Bootcamp will cover two themes, "Building Verified JIT Compilers" and "Formally verifying low-level programs in F*". The exercises in the Bootcamp assume that the students have a working knowledge of formal techniques. The main focus of the Bootcamp is on applying this knowledge to some domain-specific challenge problems.

Lecturers

• Building Verified JIT Compilers
  Emina Torlak and Xi Wang
  Abstract: Modern operating systems (OSes) can be customized with user programs that implement functionality like system call whitelisting and power management. For portability and safety, such programs are written in domain-specific languages (DSLs), and the OS kernel executes them via just-in-time (JIT) compilation to native code. The correctness of these in-kernel JITs is critical for OS security because adversaries can exploit miscompilation bugs to compromise the kernel.

  The goal of this bootcamp is to build a verified JIT compiler for the Linux ePBF language, targeting RISC-V. The project will build onServal, a framework for verifying low-level systems, and Rosette, a language for building verifiers. The bootcamp will start with a tutorial on Serval, Rosette, and the verified JIT challenge. The participants will then build and verify the JIT in stages, starting with arithmetic instructions, and if the time allows, adding memory instructions and peephole optimizations. Expect to learn fast, work hard, and type a lot of parentheses!

  
  Bios: Emina Torlak, and Xi Wang are members of the UNSAT group at the University of Washington. The UNSAT group aims to develop foundational technologies for improving the correctness and performance of practical computer systems. Our research spans the areas of formal methods, programming languages, and operating systems. We build verification and synthesis tools and use these tools to build efficient, reliable, and secure systems.
• Formally verifying low-level programs in F*
  Jonathan Protzenko and Nikhil Swamy (Microsoft)
  Abstract: This three-day tutorial will teach students about the F* framework, along with its Low* subset that compiles to C. Students will get to hack on a simplified, yet representative sample application which we will provide. The application will be a pared-down messaging client between two parties. We expect that at the end of these three-days, students will be familiar with the F* universe, and will be able to head home with enough material that they can set out to verify their own applications.

  Detailed program:

  The first day will cover F* basics, starting with the functional subset of F*. Students will be tasked with filling out a partial specification of our communication protocol, implementing missing operations at the spec level. We will also review how to prove properties about specifications, using various lemmas related to our messaging protocol as examples.

  The second day will cover low-level programming, showing how to use the Low* subset of F* to author stateful programs that can be compiled and extracted to C. We will work on small examples and cover basic data structures, e.g. arrays, and our C-like memory model.

  For the final day, students will fill out larger chunks of the application code, authoring core parts of the low-level implementation. As a bonus task, students will have to opportunity to try to prove a few properties related to cryptographic security for this toy protocol.

Registration

Postponed