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.

As part of the Sockeye project, we define formal hardware semantics for systems software to build on. Currently, we are capturing the addressing semantics on the dumpster fire that is modern hardware. By getting a grip on the addressing capabilities of the different contexts, we can determine how accessible certain devices or regions of memory are by the multitude of contexts in an SoC, and, for example, make decisions where to place kernel datastructures or how to program (IO-)MMUs.

Kirsch is our work in designing operating systems that understand the platform they run on.

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