The role of operating systems has evolved over time, from sharing one device’s resources among many users in the mainframe era, to providing convenient user interface, storage, and networking abstractions in the personal computer era. As we transition to the ubiquitous computing era, operating systems must now manage a user’s information and computation across many computers and devices. Yale is developing new operating system architectures, application environments, and security frameworks to meet today’s challenges across the computing spectrum, including IoT devices, cyber-physical systems (such as self-driving cars and quadcopters), cloud computers, and blockchain ecosystems.
Zhong Shao and his FLINT team at Yale are working to develop a new class of formally verified operating systems for modern heterogeneous platforms. In the last few years, they have made multiple breakthroughs showing that building hacker-resistant concurrent OS kernel is not only feasible but also practical. They developed a novel language-based account of certified concurrent abstraction layers, advocated abstraction over a particularly rich class of specification (called deep specification), and then constructed new methodologies and tools for formally specifying, programming, verifying, and composing abstraction layers. They have successfully developed the CertiKOS opearting system and verified its contextual functional correctness in Coq. CertiKOS is written in 6500 lines of C and x86 assembly and runs on stock x86 multicore machines. This is the world’s first proof of functional correctness of a complete, general-purpose concurrent OS kernel with fine-grained locking.