An Operating System is of course, a bridge between a computer and us, responsible for managing both hardware and software resources, and performing all basic tasks like memory management, process management, handling input and outputs and file management. There really is no need to stress on the importance of securing an OS.
For instance, the Google’s Android was a victim of a massive fraud campaign recently that compromised close to 1.3 million Google accounts. Reportedly the largest Google account breach to date, this attack used an Android malware variant called Gooligan that roots infected devices and steals the Google account authentication tokens associated with that user. With all operating systems at the brink of danger, the need of the hour lies in a computer operating system with a stricter security.
What does the new OS entail?
A team of 7 Yale researchers have come up with a solution to tackle increasing cyber-attacks – they have developed the world’s first OS run by multi-core processors, based on a novel compositional approach used to build the OS kernel. They’re calling it CertiKOS.
Before we elaborate on the technical architecture of the new OS, let us define what a kernel is. In computing, the kernel is the central module of code that loads first while booting and remains protected from overwriting or corruption in the internal physical memory of the computer. It is small in terms of data requirement, as it is supposed to run all essential services on the system while being stored in the main memory. OS kernels and Hypervisors are an integral part of safety-critical software systems. While most of these existing modules can guarantee functional correctness of the code, none of these can address the issues of concurrency. Concurrency provides room for overlapped execution of multiple program threads. This makes it impossible to consider all circumstances and eliminate all cracks in the system via traditional testing. Experts in the field believe that the complexity of such a system makes formal verification of functional correctness problematic or expensive.
Deciphering the architecture of CertiKOS
CertiKOS, the novel OS developed by the team of researchers from Yale University boasts of an extensible architecture built with certified concurrent kernels. The paper on the new OS was published and presented at the 12th USENIX Symposium on Operating Systems Design and Implementation organized from 2nd to 4th November, 2016 in Savannah, Ga. It uses contextual refinement of environment contexts of running kernels to formulate different concurrent user objects (kernels) at different abstraction levels.
Each abstraction layer is parameterized over a specific environmental context and then allows users to apply standard techniques for verifying sequential programs to in turn, verify concurrent programs. CertiKOS thus decomposes the prohibitive verification tasks into several simple and automatable modules and then writes a mathematical specification for each hierarchical module. Incorporation of formal logic and new, layered deductive verification techniques sets CertiKOS apart from the conventional method of verifying a program’s reliability. It is the first architecture that can build certified concurrent kernels and transfer global properties proved at kernel specification level down to the concrete assembly machine level.
The use of an environmental context to localize each layer allows one to apply better formal verification techniques at the source code level. The kernel programs are then compiled and linked together using thread-safe version of the CompCert compiler, CompCertX. Using CertiKOS, the researchers have successfully built a fully certified concurrent kernel, mC2 that supports both fine-grained locking and thread yield/sleep/wakeup primitives. It can run on stock x86 multicore machines and can also double as a hypervisor to boot multiple Linux instances in guest VMs running on different CPUs.
The team, led by Zhong Shao, intended to design a safeguard that could prevent hacking of anything, including home appliances, Internet of Things (IoT) devices and even digital currency. Their vision translated into a clean-slate design with an end-to-end guarantee of factors like extensibility, security and reliance. CertiKOS logically distinguishes the utilization of private memory from shared memory. The shared memory access can be protected if implemented using atomic hardware instructions like fetch-and-add. The underlying layered structure of CertiKOS is not only feasible but also practical. The architecture boasts of ‘not only an efficient assembly implementation but also machine-checkable contextual correctness proofs’ as the developers quoted in their paper. Anindya Banerjee, program director at the National Science Foundation (NSF) said, “The construction of functionally correct systems software has been one of the grand challenges of computing since at least the mid-20th century.”
For further details on the architecture read: CertiKOS: An extensible architecture for building certified concurrent OS kernels
Further Developmental Scope
However, Shao believes that there is room for improvement in the scope of security offered by the kernel. He was quoted saying, “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.”
The virtualization capability provided by the novel OS technology is used to separate the trusted components from the untrusted ones in the DARPA High Assurance cyber Military Systems (HACMS) program, which is used for building cyber-physical systems that are free from cyber vulnerabilities. “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,” DARPA program manager Ray Richards said.
CertiKOS also found reputation amongst the academic experts in the field. Greg Morrisett from Cornell University claims its formulation to be an ‘amazing progress’. The new OS infrastructure is believed to be used in multiple kinds of software. As per Andrew Appel, director of NSF’s DeepSpec consortium and a professor of computer science at Princeton, ‘the modular layered verification methods used in CertiKOS will be applicable not just to operating systems, but to many other kinds of software.’
The breakthrough in the field of computing has certainly been noted as a ‘base for building highly secure systems from combinations of verified and untrustworthy components.’ Its feasibility and practical applicability will be something to look out for.