This talk will introduce the Rosette system and the frameworks it supports for verifying and synthesizing critical infrastructure software.
Rosette is a programming language for rapid creation of solver-aided tools. These tools work by reducing verification and synthesis tasks to satisfiability queries, which involves compiling programs to logical constraints. To build a new tool, you write an interpreter for the tool's input language, and Rosette lifts this interpreter into a symbolic compiler. Since its first public release in 2014, Rosette has enabled a wide range of programmers, from professional developers to high school students, to create over 30 new verification and synthesis tools. Example applications include verifying radiation therapy software in current clinical use and synthesizing efficient GPU kernels.
In the past few years, the UNSAT group at the University of Washington has used Rosette to develop Serval, an automated verification framework for low-level systems software, and Jitterbug, a tool for verifying just-in-time compilers (JITs) for the extended Berkeley Packet Filter (BPF) language. We have applied Jitterbug to find 30+ new bugs in the Linux BPF JITs for the x86-32, x86-64, arm32, arm64, and riscv64 architectures, and to develop a new verified BPF JIT for riscv32, RISC-V compressed instruction support for riscv64, and new optimizations in existing JITs. All of these changes have been upstreamed to the Linux kernel.