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.”
Read more here: yaledailynews.com/blog/2016/11/18/yale-computer-scientists-unveil-new-os/