The Sockeye project is a large part of the NetOS group’s research. We (the NetOS group) are part of the Institute for Computing Platforms, informally called Systems Group.

We research better ways of building operating and other systems software for modern hardware platforms, by building secure foundations.

The Sockeye domain-specific language defines machine-readable semantics for describing the real behavior of hardware components, and security properties that should be upheld. The resulting specifications are compiled and analyzed by the Sockeye compiler, using established verification tools like Z3, Rosette, and CBMC.

We have created specifications of real-world hardware systems, from microcontrollers to server CPUs using the Sockeye DSL. We have specified security properties for correct configuration of Arm TrustZone isolation, and proven that these can be correctly established on some systems, while our analysis tools revealed hard- and software bugs in configurations for other systems that turned out to be exploitable vulnerabilities.

Kirsch is our work in designing operating systems that understand the platform they run on. To manage the complexity of modern hardware, we formally model hardware and then derive guarantees and configurations from that model.

See our publications for a more in-depth treatment of our ideas.