Allen School professors Emina Torlak and Xi Wang, co-founders of the UNSAT group, have received an Amazon Research Award for their work in automated verification for critical infrastructure software.
The award will support Torlak and Wang’s continued work in applying cutting edge verification and synthesis technology to critical infrastructure software. Their most recent project, Jitterbug, is a tool for writing and proving the correctness of just-in-time (JIT) compilers for computers using the extended Berkeley Packet Filter (eBPF) technology. It provides a formal correctness guarantee for eBPF JITs, a security-critical component of the Linux operating system, through a precise specification of JIT correctness and an automated verification strategy that scales to practical implementations.
“Compiler bugs can be very costly in this setting,” Torlak said, “so it’s important to catch them early.”
Jitterbug builds on two of UNSAT’s existing projects: Serval, a framework for creating automated verifiers for systems software, and Rosette, a solver-aided programming language for synthesis and verification. The team has used the tool to find more than 30 new bugs in a number of deployed eBPF JITs and to develop new optimizations. With support from the Amazon award, the group aims to improve the usability of Jitterbug and make the integration with development better.
The UNSAT group was formed when Torlak and Wang joined the Allen School in 2014, with Wang’s expertise in operating systems complementing Torlak’s in programming languages and automated reasoning.
“It’s hard for people to get everything right when building software systems,” Wang said. “How do you build correct systems without too much effort? We created UNSAT to pull our resources together to develop solutions that make this process easier.”
Read more about Jitterbug and explore more of the group’s research here. Learn more about the Amazon Research Award program here.
Congratulations, Emina and Xi!