SEAS Works to Usher an Era of Hacker-Proof Computing

by William Weir,   YaleNews

Every few days, the news brings us stories of massive data breaches, resulting in the theft of massive amounts of money, or the release of sensitive information. Whether you’re making a routine online transaction or casting a vote in a national election, the issue of cybersecurity has everyone on watch.

As fast as technology progresses, hackers find new means to exploit it. It’s a problem that requires strategies on several fronts and rethinking approaches to software, hardware and the law. At SEAS, a number of faculty members are exploring the question of how we make computing more secure and reliable.

“The evolution of computer systems has been heavily influenced by business considerations?—?people want to be the first to the market,” said Zhong Shao, professor and department chair of computer science. To save time, developers often rely on legacy code, a practice that seemed fine when no one imagined that computers would play such a critical role in our lives. Now, with so many different platforms in use, the Internet of Things taking off, and self-driving cars just around the corner, we need greater assurances that our operating systems are secure and reliable.

As one way to strengthen computing against hackers, Yale University School of Engineering & Applied Science professor Zhong Shao is spearheading the construction of the Certified Kit Operating System (CertiKOS). CertiKOS is based on formal verification, in which the kernel’s interdependent components are carefully untangled, and mathematical specifications are written for each kernel module’s intended behavior.

“The CertiKOS approach is to apply formal principled techniques to decompose these very complex systems into many carefully designed abstraction layers,” Shao notes. “For each complex component, you try to figure out its semantic structure. We build the operating system in a clean way, layer by layer.”

Shao says CertiKOS seeks to address the unsustainability of the computer industry’s current modus operandi as it pertains to security. “For the future, we need to build a new operating system ecosystem that has to be super clean and provides a bug-free and hacker-proof guarantee,” he says.

The article covers several projects addressing different projects in cyber security