Data61’s Trustworthy Systems Research Group aims to achieve fundamental, game-changing improvements in the design, implementation, and verification of software systems scaling from the embedded to the enterprise space. We will apply rigorous techniques at various abstraction levels of software systems, to achieve solid and practically meaningful guarantees, for provable security, safety, and reliability properties of critical systems.
Using Rump kernels to run unmodified NetBSD drivers on seL4
Limited support is now available for running unmodified NetBSD drivers on seL4 using rump kernels. We have modified the Rumprun unikernel to use seL4 as a supported platform on ia32 and x86_64. This makes it possible to run unmodified POSIX applications on Rumprun on seL4. The Rumprun unikernel uses NetBSD rump kernels to provide operating […]
seL4 on the Raspberry Pi 3
seL4 on the Raspberry Pi 3 The seL4 kernel is a burgeoning project that’s been creating a buzz in the security world for its uncompromising capability-based security model that comes with end-to-end proofs of conformance to its formal specification. It’s a microkernel, and it’s the fastest of its ilk. It says, “Security is no excuse […]
Introducing Device Untyped Memory in seL4
Device Untyped Memory Modelling the hardware more closely to improve robustness of configuring device driver access to the machine. User-level driver Background The L4 family of microkernels have a long history of running device drivers as user-level processes. The microkernel itself only has the bare minimum of drivers to initialise the CPU and manage time […]