Communications of the ACM
Certikos: A Breakthrough Toward Hacker-Resistant Operating Systems
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