Verve (operating system)
Encyclopedia
Verve is a research operating system
developed by Microsoft Research
.
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 C# and compiled by Bartok (originally developed for the Singularity
project) into typed assembly language
, 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 SMT 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
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.
Operating system
An operating system is a set of programs that manage computer hardware resources and provide common services for application software. The operating system is the most important type of system software in a computer system...
developed by Microsoft Research
Microsoft Research
Microsoft Research is the research division of Microsoft created in 1991 for developing various computer science ideas and integrating them into Microsoft products. It currently employs Turing Award winners C.A.R. Hoare, Butler Lampson, and Charles P...
.
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 C# and compiled by Bartok (originally developed for the Singularity
Singularity (operating system)
Singularity is an experimental operating system being built by Microsoft Research since 2003. It is intended as a highly-dependable OS in which the kernel, device drivers, and applications are all written in managed code.- Workings :...
project) into typed assembly language
Typed Assembly Language
In computer science, a typed assembly language 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 that processes the assembly language code in order to analyse how...
, 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
Formal verification
In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal methods of mathematics .- Usage :Formal verification can be...
, which proves the Nucleus correct using the Z3 SMT 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
Kernel panic
A kernel panic is an action taken by an operating system upon detecting an internal fatal error from which it cannot safely recover. The term is largely specific to Unix and Unix-like systems; for Microsoft Windows operating systems the equivalent term is "Bug check" .The kernel routines that...
.
Verve's trusted computing base
Trusted computing base
The trusted computing base of a computer system is the set of all hardware, firmware, and/or software components that are critical to its security, in the sense that bugs or vulnerabilities occurring inside the TCB might jeopardize the security properties of the entire system...
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.