research • formally verified systems & capability-based operating systems
i worked on seL4, the world's first operating system kernel with a computer-checked end-to-end correctness proof, and created Robigalia, a design for a persistent capability operating system built using rust.
seL4: verified correctness
seL4 is a microkernel whose implementation has been formally verified to match its specification, and whose specification has been proven to satisfy critical security properties. this means we have mathematical proof that the kernel implementation:
- contains no buffer overflows
- has no arithmetic errors
- will never crash or hang
- correctly enforces capability-based access control
- preserves data integrity and confidentiality
this level of assurance is unprecedented in systems software. the verification was done using the Isabelle/HOL proof assistant, with around 200,000 lines of proof for 10,000 lines of C code. my work involved using seL4, understanding its capability model, and contributing to the ecosystem around it.
my work on seL4
i interned at UNSW/Data61 in 2016, learning Isabelle from some experts and LARPing as a grad student for 8 months. my main contribution was substantially overhauling their translator from Haskell to HOL specifications.
the original translator was written in Python and had a dense pile of scary regexps that, when iterated to a fixed point, would successively rewrite haskell into isabelle, respecting the weird restrictions HOL has versus haskell and patching over differences in the typeclass systems. those regexps worked in mysterious ways by basically capturing someone's interactive vim session in the misty past.
i replaced it with a proper Haskell parser off the shelf instead. i was too much of a coward but was tempted to write the translator in Haskell itself. the new approach was more maintainable and less magical, though i didn't end up finishing it before my internship concluded—the branch is locked away in their bitbucket.
robigalia: capability systems in rust
Robigalia was my vision for a persistent capability operating system built using rust on top of seL4. the core idea was to combine:
- capability-based security: all authority flows through unforgeable object references (capabilities), making security policies explicit and composable
- persistence: the entire system state persists across reboots; programs and data live in a single address space that survives power cycles
- rust's safety: leveraging rust's ownership system to enforce security properties at compile time
- seL4's verified kernel: building on a foundation with mathematical correctness guarantees
while robigalia remains aspirational, it represented important thinking about how modern language design could enhance operating system security. the capability model and rust's ownership model are philosophically aligned: both are about explicit, statically-checkable authority and access control.
capability-based security
capability systems represent a fundamentally different approach to security than traditional access control lists. in a capability system, the ability to perform an operation is represented by possession of an unforgeable token (capability). this makes security:
- compositional: you can safely combine programs because authority is explicit
- principle-of-least-privilege by construction: programs only have access to what they're given
- auditable: authority flow is traceable through capability transfers
these properties make it much easier to build secure systems. instead of fighting with permissions and ambient authority, you design programs that receive exactly the capabilities they need to do their job.
the formal methods connection
this work tied directly into my interests in formal verification and proof engineering. seL4's verification represents what's possible when we apply mathematical rigor to systems programming. the proofs guarantee properties that testing can never fully establish.
capability systems, meanwhile, make security properties more amenable to formal reasoning. the explicit nature of authority makes it possible to prove security properties about entire systems, not just individual components.
learning and influence
working with seL4 and designing robigalia taught me about:
- formal verification of systems code
- capability-based security models
- microkernel architecture and IPC performance
- persistent systems and orthogonal persistence
- how language design affects system security
these ideas influenced my thinking about software architecture and security. the capability model and verification approach represent what computing could be: systems that are secure by construction and correct by proof.