Unhackable OS? CertiKOS enables creation of secure system kernels
Operating systems are the core of our digital civilization. Hack-proofing them means that billions of devices - PCs, network switches, IoT devices, drones and much more - are much more secure. That forces cybercriminals to move up to less common layers of the software stack.
CertiKOS is just such a system, enabling the creation of secure system kernels. CertiKOS, produced by a team at Yale University led by Professor Zhong Shao, has been used to build a secure OS that hosts a hypervisor that can run multiple OS instances concurrently.
Grand Challenge
As Anindya Banerjee, a program director at the National Science Foundation (NSF), which is helping fund the research, noted in an interview with YaleNews,
The construction of functionally correct systems software has been one of the grand challenges of computing since at least the mid-20th century. CertiKOS demonstrates that it is feasible and practical to build verified software that additionally provides evidence - through machine-checkable mathematical proofs - that it is functionally correct.
Building a provably secure OS that supports concurrency - multiple threads - on multiprocessors was thought for years to be impossible given the complex interactions between software layers, threads, locking, and processor cores. The CertiKOS team's key insight, from their recent paper, was to develop and verify a
. . . compositional specification that can untangle all the kernel interdependencies and encapsulate interference among different kernel objects. Because the very purpose of an OS kernel is to build layers of abstraction over bare machines, we insist on meticulously uncovering and specifying these layers, and then verifying each kernel module at its proper abstraction level.
But is it practical?
The team developed a fully certified OS kernel called mC2 with fine-grained locking that runs on stock x86 multicore processors. It can also double as a hypervisor and boot multiple Linux instances in guest VMs on different cores.
These were the biggest hacks, leaks and data breaches of 2016
While the goal of the research was not a full-fledged performance test, they did look at mC2's hypervisor overhead, and found it was similar to KVM. However, there are still subsystems, such as a file system and storage I/O, that haven't yet been built using the CertiKOS tools. But that's a question of time and resources, not feasibility.
The Storage Bits take
CertiKOS isn't the only player in secure systems. Kaspersky Labs recently unveiled their own OS, but it's not clear if they've done formal validation. There's also seL4, which has been formally verified.
The seL4 FAQ also has a good discussion of what formal verification actually delivers. Short answer: system architects still have to pay attention to the assumptions and the specific goals of the implementation to ensure maximum security. You can't just slip in a verified kernel and be secure.
Today, the internet is the wild west, where outlaws run wild and honest citizens are victims. But slowly, efforts like CertiKOS mean that we will be able to enforce law and order, one of these days.
For me, those days can't come soon enough.
Courteous comments welcome, of course.