Verve: A Type Safe Operating System by Microsoft Research

MSR released a paper covering an operating system research project that takes a new approach to building an OS stack with verifiable and type safe managed code. This project employs a novel use of Typed Assembly Language, which's what you think it's: Assembly with types (implemented as annotations and verified statically using verification technology Boogie […]

Share online:

MSR released a paper covering an operating system research project that takes a new approach to building an OS stack with verifiable and type safe managed code. This project employs a novel use of Typed Assembly Language, which's what you think it's: Assembly with types (implemented as annotations and verified statically using verification technology Boogie and theorem prover Z3 (Boogie generates verification conditions that're then statically proven by Z3.

"We use TAL and Hoare logic to achieve highly automated, static verification of the safety of a new operating system called "Verve." Our techniques and tools mechanically verify the safety of every assembly language instruction in the operating system, run-time system, drivers, and apps (in fact, every part of the system software except the boot loader). Verve consists of a "Nucleus" that provides primitive access to hardware and memory, a kernel that builds services on top of the Nucleus, and apps that run on top of the kernel."

About The Author

Deepak Gupta is a IT & Web Consultant. He is the founder and CEO of diTii.com & DIT Technologies, where he's engaged in providing Technology Consultancy, Design and Development of Desktop, Web and Mobile applications using various tools and softwares. Sign-up for the Email for daily updates. Google+ Profile.