Verve is a research

operating system An operating system (OS) is system software that manages computer hardware, software resources, and provides common daemon (computing), services for computer programs. Time-sharing operating systems scheduler (computing), schedule tasks for ef ...

developed by

Microsoft Research Microsoft Research (MSR) is the research subsidiary of Microsoft. It was created in 1991 by Richard Rashid, Bill Gates and Nathan Myhrvold with the intent to advance state-of-the-art computing and solve difficult world problems through technolog ...

. Verve is verified end-to-end for

type safety In computer science, type safety and type soundness are the extent to which a programming language discourages or prevents type errors. Type safety is sometimes alternatively considered to be a property of facilities of a computer language; that i ...

and memory safety. Because of their complexity, a holy grail of

software verification Software verification is a discipline of software engineering whose goal is to assure that software fully satisfies all the expected requirements. Broad scope and classification A broad definition of verification makes it equivalent to software t ...

has been to verify properties of operating systems. Operating systems are usually written in low-level languages, such as C, that provide very few guarantees. Th
Singularity project
took the approach of writing an operating system in C#, a type-safe, memory-safe language. A weakness of this approach is that operating systems necessarily need to call lower-level code to, for instance, move the stack pointer. Verve addresses this problem by partitioning the operating system into verified

assembly language In computer programming, assembly language (or assembler language, or symbolic machine code), often referred to simply as Assembly and commonly abbreviated as ASM or asm, is any low-level programming language with a very strong correspondence b ...

that is required to be low-level and a trusted interface to rest of the operating system, written in C#. There is a trusted specification that guarantees the low-level assembly code does not modify the heap and that the high-level C# code does not modify the stacks. Verve consists of a small ''Nucleus'', which acts as a minimal hardware abstraction layer, and a ''Kernel'', which uses primitives provided by the Nucleus to expose a more traditional interface to applications. All components of the system other than the Nucleus are written in

managed code Managed code is computer program code that requires and will execute only under the management of a Common Language Infrastructure (CLI); Virtual Execution System (VES); virtual machine, e.g. .NET, CoreFX, or .NET Framework; Common Language Runt ...

C# and compiled by Bartok (originally developed for the Singularity project) into

typed assembly language In computer science, a typed assembly language (TAL) is an assembly language that is extended to include a method of annotating the datatype of each value that is manipulated by the code. These annotations can then be used by a program (type check ...

(TAL), which is verified by a TAL checker. The Nucleus implements a memory allocator and garbage collection, support for stack switching, and managing interrupt handlers. It is written in BoogiePL, which serves as input to MSR's Boogie verifier, which proves the Nucleus correct using the

Z3 Theorem Prover Z3, also known as the Z3 Theorem Prover, is a cross-platform satisfiability modulo theories (SMT) solver by Microsoft. Overview Z3 was developed in the ''Research in Software Engineering'' (RiSE) group at Microsoft Research and is targeted at so ...

satisfiability modulo theories In computer science and mathematical logic, satisfiability modulo theories (SMT) is the problem of determining whether a mathematical formula is satisfiable. It generalizes the Boolean satisfiability problem (SAT) to more complex formulas involvi ...

(SMT)

automated theorem prover Automated theorem proving (also known as ATP or automated deduction) is a subfield of automated reasoning and mathematical logic dealing with proving mathematical theorems by computer programs. Automated reasoning over mathematical proof was a m ...

(solver). The Nucleus relies on the Kernel to implement threads, scheduling, synchronization, and to provide most interrupt handlers. Even though the Kernel is not formally verified, so, for example, a bug in scheduling could cause the system to hang, it cannot violate type or memory safety, and thus cannot directly cause undefined behavior. If it attempts to make invalid requests to the Nucleus, formal verification guarantees that the Nucleus handles the situation in a controlled manner. Verve's trusted computing base (TCB) is limited to: Boogie/Z3 for verifying the Nucleus's correctness; BoogieASM for translating it into x86 assembly; the BoogiePL specification of how the Nucleus should behave; the TAL verifier; the assembler and linker; and the bootloader. Notably, neither the C# compiler/runtime nor the Bartok compiler are part of the TCB.

References

Safe to the Last Instruction: Automated Verification of a Type-Safe Operating System
Jean Yang and Chris Hawblitzel. ''Programming Language Design and Implementation'', 2010.
Safe to the Last Instruction: Automated Verification of a Type-Safe Operating System
Jean Yang and Chris Hawblitzel. CACM Research Highlight. ''Communications of the ACM'', September 2010.
Technical Perspective: Safety First!

Verve: A Type Safe Operating System
Interview with Chris Hawblitzel.
Verve: A Type Safe Operating System
''OSnews''.
Announcing Verve – A Type-Safe Operating System
''InfoQ''. {{DEFAULTSORT:Verve (Operating System) Microsoft operating systems Microsoft Research Microkernel-based operating systems Microkernels Nanokernels