Formally verified OSes have been “the future” for over 15 years, so why haven’t they been adopted more? In this talk we will explore some of the history of microkernels, RTOSes, and software platform security for ICS/CPS, both verified and un-verified. We will outline some of the key challenges we have encountered through engagements with energy suppliers and healthcare providers, and what we see as the barriers to adoption.

The context of ICS/CPS development and their certification / accreditation requirements often create challenges and restrictions not encountered elsewhere. There are many good reasons why developers can’t just add random, untrusted code to critical systems (!), but what if we could? How could we become comfortable with that — and convince an accreditor — that our untrusted code cannot negatively impact a system’s security and safety-critical functionality? To have any chance of achieving this we need cast-iron guarantees of both separation and controlled information flow, and realistically we can’t build this without provable security (i.e., formal verification). Unfortunately, this isn’t the whole story: we have the high-level safety and security claims (e.g., “the system is secure”, “the system operates safely”), and our low-level proven guarantees of isolation from the OS, but making the link between these two is often less well fleshed out than we would like, or than is required by an accreditor.

We want to enable people without a background in formal methods to build real systems that take advantage of strong isolation, and which can demonstrate the link between automated proofs for an underlying microkernel, and high-level safety case. We believe that taking advantage of this isolation will reduce the self-censorship (inadvertently) caused by certification bodies, and spur innovation in both academia and industry, while still being able to make the required security and safety cases. This talk will explore how far we’ve come, what has worked well, and what we see as the remaining challenges.