CertiKOS: Yale develops world's first hacker-resistant operating system

Computer scientists at Yale University in the US have developed the world's first super-secure computer operating system running on multi-core processors. It aims to keep hackers out and shield against cyberattacks by reengineering the way computers are traditionally built.

The kernel is the central core of a computer's operating system and has complete control over everything that occurs in the system. It is usually loaded into a protected area of the computer's memory, and helps to connect software applications to the hardware in a computer.

At the moment, computer operating systems tend to be very complicated, and if there is just one weak link in the code that cannot be detected using traditional testing methods, then the system is vulnerable to being hacked into.

The CertiKOS operating system is different in that it supports concurrency, which means that it enables multiple sequences of programmed instructions, known as 'threads', to run simultaneously on multiple CPU core processors.

It was previously believed that having concurrency in a computer would be incredibly expensive and make it far too complex for problems to be detected using traditional testing. However, the researchers managed to make it work by untangling all the interdependent components within the kernel.

They then reorganised the operating system's code into a large collection of hierarchical modules and wrote a mathematical specification for each kernel module's intended behaviour.

This is a departure from the traditional way of checking a software programme's reliability, because usually coders test software for bugs by putting it into numerous scenarios. It also means that the kernel can take on new functionalities and be used for different application domains.

Mathematically proving a multi-core kernel

"A program can be written 99% correctly – that's why today you don't see obvious issues – but a hacker can still sneak into a particular set-up where the programme will not behave as expected," Yale professor of computer science and leader of the research, Zhong Shao, said. "The person who wrote the software worked with all good intentions, but couldn't consider all cases."

In the past, it would have been impossible for a certified kernel to be verified because the mathematical proofs would be far too large for any human to check. However, over the last decade, the computing industry has developed power software programmes known as 'proof assistants' that are able to take over and automatically generate and check huge formal proofs, which means that a much more secure kernel is now possible.

"This is amazing progress," said Greg Morrisett, a leading expert on software security and dean of computing and information sciences at Cornell University. "Ten years ago, no one would predict that we could prove the correctness of a single-threaded kernel, much less a multi-core one. Zhong and his team have really blazed a spectacular trail for the rest of us."

Yale developed CertiKOS for the US Defense Advanced Research Projects Agency (Darpa) in order to enable the US military to build physical computer systems that are provably free from security vulnerabilities that can be exploited in a cyberattack, as part of Darpa's High Assurance cyber Military Systems (HACMS) programme.

The open-access paper, entitled CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels, was presented by the Yale researchers at the 12th USENIX Symposium on Operating Systems Design and Implementation held from 2 to 4 November in Savannah, Georgia.