Sign In

Communications of the ACM

ACM TechNews

Certikos: A Breakthrough Toward Hacker-Resistant Operating Systems

View as: Print Mobile App Share: Send by email Share on reddit Share on StumbleUpon Share on Hacker News Share on Tweeter Share on Facebook
CertiKOS, illustration

Researchers at Yale University have developed CertiKOS, a new operating system they say could lead to a new generation of reliable and secure systems. The researchers say CertiKOS is the first OS to run on multi-core processors and protects against cyberattacks.

CertiKOS incorporates formal verification to ensure a program performs precisely as its designers intended, a safeguard that could shield home appliances, Internet of Things devices, self-driving cars, and digital currency from hacking. CertiKOS supports concurrency, which sets it apart from other previously verified systems and enables it to run on the latest multi-core machines. The architecture also is designed to take on new functionalities and be used for different application domains.

"CertiKOS demonstrates that it is feasible and practical to build verified software that additionally provides evidence — through machine-checkable mathematical proof — that it is functionally correct," says Anindya Banerjee, program director at the U.S. National Science Foundation, which funded the effort.

The CertiKOS verified operating system kernel is a critical element in the U.S. Defense Advanced Research Projects Agency's High Assurance cyber Military Systems program, which is used to build cyber-physical systems that are demonstrably free from cyber vulnerabilities.

From Yale University 
View Full Article


Abstracts Copyright © 2016 Information Inc., Bethesda, Maryland, USA


No entries found