CertiKOS: a breakthrough towards hacker-resistant operating systems

A team of Yale researchers has unveiled CertiKOS, the world’s first operating system that runs on multi-core processors and shields against cyberattacks, a step that scientists say could lead to a new generation of reliable systems software and secured.

Led by Zhong Shao, a professor of computer science at Yale, the researchers have developed an operating system that incorporates formal verification to ensure that a program works exactly as its designers intended – a protection that could prevent the hacking everything related to household appliances and the Internet of Things. (IoT) to self-driving cars and digital currency. Their article on CertiKOS was presented at the 12e USENIX Symposium on Operating Systems Design and Implementation held November 2-4 in Savannah, Georgia.

Computer scientists have long believed that computer operating systems should have a small, reliable kernel at their heart that facilitates communication between the systems software and hardware. But operating systems are complicated, and it only takes one weak link in the code – a link virtually impossible to detect through traditional testing – to make a system vulnerable to hackers.

One of the major breakthroughs of CertiKOS is that it supports concurrency, which means that it can simultaneously execute multiple threads (small sequences of programmed instructions) on multiple central processing unit (CPU) cores. This sets CertiKOS apart from other previously verified systems and allows CertiKOS to work on modern multi-core machines. The CertiKOS architecture is also designed to be highly extensible, i.e. it can support new features and be used for different application domains.

Concurrency allows the overlapping execution of multiple program threads, making it impossible to account for all circumstances and eliminate all cracks in the system through traditional testing. Many in the field have long believed that the complexity of such a system also makes formal verification of functional correctness problematic or prohibitively expensive.

Building functionally correct system software has been one of the great challenges in computing since at least the mid-20e century,” said Anindya Banerjee, program director at the National Science Foundation (NSF), which funds the CertiKOS effort in part through its Expeditions in Computing program. “CertiKOS demonstrates that it is feasible and practical to create verified software that further provides proof – through machine-verifiable mathematical proofs – that it is functionally correct.”

When building the CertiKOS system, Shao and his team incorporate formal logic and new layered deductive verification techniques. That is, they carefully unravel the interrelated components of the kernel, organize the code into a large collection of hierarchical modules, and write a mathematical specification for the intended behavior of each kernel module. Using formal deductive verification to certify the system differs from the conventional method of verifying the reliability of a program, in which the code writer tests the program against many scenarios.

A program can be written 99% correctly – that’s why today you don’t see any obvious problems – but a hacker can still sneak into a particular configuration where the program won’t behave as expected,” Shao said. . “The person who wrote the software worked with all good intentions, but could not consider all cases.”

The CertiKOS Verified Operating System Core is a key component of the Defense Advanced Research Agency (DARPA) High Assurance Cyber ​​Military Systems (HACMS) program, which is used to build cyber-physical systems that are demonstrably free of cyber- vulnerabilities.

The HACMS team uses the virtualization capability provided by CertiKOS to separate reliable components from unreliable components,” said Ray Richards, DARPA program manager. “This is an important capability that allows us to effectively build cyber-resilient systems. In a world where cybersecurity is a growing concern, this resiliency is a powerful attribute that we hope will be widely embraced by system designers.

Only in recent years would a system like CertiKOS be possible, as the evidence of a certified kernel is too large to be verified by a human. Powerful computer programs known as proof assistants have been developed over the past 10 years, however, which can automatically generate and verify large formal proofs.

This is incredible progress,” said Greg Morrisett, a leading software security expert and dean of computer and information science at Cornell University. “Ten years ago, no one would have predicted that we could prove the correctness of a single-threaded kernel, let alone a multi-core kernel. Zhong and his team have truly blazed a spectacular trail for the rest of us.

Andrew Appel, director of NSF’s DeepSpec Consortium and professor of computer science at Princeton, called CertiKOS a “true breakthrough,” noting that it can serve as the foundation for building highly secure systems from combinations of verified and untrusted components. .

But equally important, the modular layered verification methods used in CertiKOS will be applicable not only to operating systems, but to many other types of software,” Appel said.

The other authors of the CertiKOS paper are Ronghui Gu, Xiongnan (Newman) Wu, Hao Chen, Jieung Kim, Vilhelm Sjöberg, and David Costanzo, all from Professor Zhong Shao’s FLINT lab at Yale.

Comments are closed.