Web site: (not active)
Origin: USA
Category: Desktop
Desktop environment: CLI
Architecture: x86
Based on: unknown
Wikipedia: Verve
Media: Install
The last version | Released: r73999 | November 10, 2013
Verve – a research operating system developed by Microsoft Research. Verve is verified end-to-end for type safety and memory safety.
Because of their complexity, a holy grail of software verification 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. The 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 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 C# and compiled by Bartok (originally developed for the Singularity project) into typed assembly language (TAL), which is verified by a TAL checker.
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.
Source: Wikipedia; License: Creative Commons Attribution-ShareAlike 4.0.
