Researchers from Yale University have unveiled CertiKOS, the world’s first operating system that runs on multi-core processors and shields against cyber-attacks. Scientists believe this could lead to a new generation of reliable and secure systems software.
Led by Zhong Shao, professor of computer science at Yale, the researchers developed an operating system that incorporates formal verification to ensure that a program performs precisely as its designers intended — a safeguard that could prevent the hacking of anything from home appliances and Internet of Things (IoT) devices to self-driving cars and digital currency. Their paper on CertiKOS was presented at the 12th USENIX Symposium on Operating Systems Design and Implementation held November 2-4 in Savannah, Ga.
Computer scientists have long believed that computers’ operating systems should have at their core a small, trustworthy kernel that facilitates communication between the systems’ software and hardware. But operating systems are complicated, and all it takes is a single weak link in the code — one that is virtually impossible to detect via traditional testing — to leave a system vulnerable to hackers.
One of the main breakthroughs of CertiKOS is that it supports concurrency, meaning that it can simultaneously run 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 run on modern multi-core machines. The CertiKOS architecture is also designed to be highly extensible — that is, it can take on new functionalities and be used for different application domains.
Concurrency allows overlapped execution of multiple program threads, which makes it impossible to consider all circumstances and eliminate all cracks in the system via 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.
“The construction of functionally correct systems software has been one of the grand challenges of computing since at least the mid-20th century,” said Anindya Banerjee, program director at the National Science Foundation (NSF), which funds the CertiKOS effort partly through its Expeditions in Computing program. “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.”
In constructing the CertiKOS system, Shao and his team incorporate formal logic and new, layered deductive verification techniques. That is, they carefully untangle the kernel’s interdependent components, organize the code into a large collection of hierarchical modules, and write a mathematical specification for each kernel module’s intended behavior. The use of formal deductive verification to certify the system differs from the conventional method of checking a program’s reliability, in which the code writer tests the program against numerous scenarios.
“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 program will not behave as expected,” Shao said. “The person who wrote the software worked with all good intentions, but couldn’t consider all cases.”
The CertiKOS verified operating system kernel is a key component of the Defense Advanced Research Agency’s (DARPA) High Assurance cyber Military Systems (HACMS) program, which is used to build cyber-physical systems that are provably free from cyber vulnerabilities.
“The HACMS team uses the virtualization capability provided by CertiKOS to separate trusted from untrusted components,” DARPA program manager Ray Richards said. “This is an important ability that allows us to effectively build cyber-resilient systems. In the world where cybersecurity is a growing concern, this resiliency is a powerful attribute that we hope will be widely adopted by system designers.”
Only in recent years would a system like CertiKOS be possible, since the proofs for a certified kernel are too big for any human to check. Powerful computer programs known as proof assistants have been developed within the last 10 years, however, that can automatically generate and check large formal proofs.
“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.”
Andrew Appel, director of NSF’s DeepSpec consortium and a professor of computer science at Princeton, called CertiKOS “a real breakthrough,” noting that it can serve as a base for building highly secure systems from combinations of verified and untrustworthy components.
“But just as important, the modular layered verification methods used in CertiKOS will be applicable not just to operating systems, but to many other kinds of software,” Appel said.
Reference: “CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels” by Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan (Newman) Wu, Jieung Kim, Vilhelm Sjöberg and David Costanzo, 2 November 2016, OSDI’16: Proceedings of the 12th USENIX conference on Operating Systems Design and Implementation.
PDF
Never miss a breakthrough: Join the SciTechDaily newsletter.
Follow us on Google and Google News.
2 Comments
What we have learned from Stuxnet is that no proprietary software can be safe. The more people who buy it the more dangerous its use becomes. Stuxnet attacked Windows. Its all over the world now in stand-alone P/Cs and huge networks. You want buggy software, buy Windows.
Governments employ hackers to write the malicious code in Stuxnet for uncontrolled distribution. If CERTIKOS becomes popular they will write bugs for it too.
The only protection is for everyone to write his own code and bring an end to the business niche filled by Microsoft, Apple and the commercial software industry.
Regard Magister Akuntansi
What’s a monolithic kernel?