The world is now one step closer to the large-scale development of hacker-resistant operating systems, thanks to the efforts of a team from the Yale Computer Science Department.
Led by computer science professor Zhong Shao, the Yale researchers have built CertiKOS, an operating system that comes with its own proof. This means that the operating system will always behave exactly as the designers planned, which guarantees that it is free of loopholes that can be exploited by hackers. According to Shao, CertiKOS can lay the groundwork for building more complex, hacker-resistant operating systems in the future. This has implications for technologies ranging from household appliances and digital currency to drones and self-driving cars.
“More and more of our real-world environment relies on all types of computing devices, which all run on some kind of operating system,” Shao said. “If your software is not designed well or thoroughly tested, there will be loopholes that a hacker can exploit, so it can be very difficult to rely on these devices and infrastructure.”
The CertiKOS project officially commenced in 2010, but researchers have been interested in building secure, reliable operating systems as early as the 1960s, Shao said.
CertiKOS also addresses what Shao called one of the “grand challenges” of the field: writing a proof for a concurrent operating system — an operating system that runs on machines with multiple processors.
According to Shao, concurrency is a powerful feature of modern computer systems. For example, it allows our laptops and smartphones to simultaneously run multiple applications. However, this complexity means that it can be very difficult and expensive to certify concurrent operating systems are loophole-free, said Ronghui Gu GRD ’16, a research associate at Yale and one of CertiKOS’ lead developers.
Joan Feigenbaum, the chair of the Yale Computer Science Department, praised the team for showing that certification of concurrent operating systems is “technologically feasible and practical, as well as desirable.”
“CertiKOS is essentially a whole level more secure, just by the way it’s constructed and proved, than conventional operating systems,” said Andrew Appel, a computer science professor at Princeton University and Shao’s former advisor. “It means that people will be able to build correct and secure software stacks, all the way down to the bottom. The breakthrough is that nobody has previously been able to build an operating system at this scale and get it proved correct with a maintainable, machine-checked proof.”
Computer science professor Ruzica Piskac noted that unreliable software can lead to not only cybersecurity issues, but also economic inefficiency. She pointed to a 2013 University of Cambridge report that found the global, annual cost of debugging software had risen to $312 billion. Piskac, who was not part of the CertiKOS project, added that CertiKOS is significant because it can reduce the consequences associated with software errors, which can impact issues ranging from medical treatment to the online storage of information.
CertiKOS’ value extends beyond direct applications to everyday devices. It can also serve as an important instructional tool, due to the operating system’s organized, layered structure, Shao said.
This semester, Shao is teaching an undergraduate class called “Design and Implementation of Operating Systems,” which allows students to use a version of CertiKOS in their problem sets. According to Wendy Chen ’17, a computer science major enrolled in the class, each problem set involves working with a subset of CertiKOS’ layers to learn about concepts such as virtual memory and address translation.
“It’s amazing that we put so much trust into software that might not work 100 percent of the time,” Chen said. “Especially once driverless cars are on the road and human life can be in danger, can we trust the [operating system] running the car if it is not fully verified? I think Professor Shao and his group’s work on CertiKOS points to the way that [operating systems] should be designed, considering the growing roles that an [operating system] is taking on in our increasingly software-dependent day-to-day life.”
According to Gu, in the future, the team wishes to explore other applications of CertiKOS, including use of the system in banking and the “Cloud.”
[Source:- Yale daily news]
