Verve (operating system)

Short description: Research operating system from Microsoft Research

VerveDeveloper| Microsoft Research

|

Written in| BoogiePL, C#; bootloader in assembly language, C++; may use other Common Intermediate Languages (CIL)
OS family| Language-based operating systems
Working state| In development
Source model| Source-available (via Shared Source Initiative)
Initial release| September 2010; 15 years ago (2010-09)
|Final release|Latest release}}| r73999 / November 10, 2013; 12 years ago (2013-11-10)
Platforms| x86
Kernel type| Microkernel, language-based
License| Microsoft Research License

Verve is 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.

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 satisfiability modulo theories (SMT) automated theorem prover (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.

* v
* t
* e

Microsoft Research (MSR)

Main
projects|

| Languages and compilers|

* Polyphonic C#
* Cω
* Spec#
* Sing#
* Bartok
* F*
* Phoenix

|

Distributed/grid computing|

* Bigtop
* Gridline
* BitVault
* Orleans

Internet and networking|

* AjaxView
* Avalanche
* Conference XP
* Gazelle
* HoneyMonkey
* Penny Black
* Wallop

Other projects|

* Cognitive Toolkit
* IllumiRoom
* Image Composite Editor
* MyLifeBits
* LiveStation
* SLAM
* Terminator
* WorldWide Telescope
* PhotoDNA
* Z3 Theorem Prover

Operating systems|

* Barrelfish
* HomeOS
* Midori
* Singularity
* Verve

APIs|

* Joins
* Accelerator
* Dryad
* SXM

Launched as products|

* C#
* Comic Chat
* Detours
* F#
* Sideshow
* PixelSense (TouchLight)
* SenseCam
* ClearType
* Group Shot
* Allegiance
* TrueSkill
* Songsmith
* Xbox
* Kinect

MSR Labs
applied
research|

| Live Labs|

| Current|

* Pivot
* Seadragon
* Deep Zoom
* DeepZoomPix

|

Discontinued|

* Deepfish
* Listas
* Live Clipboard
* Photosynth
* Volta

FUSE Labs|

* Bing Twitter
* Docs.com
* Kodu

Other labs|

* Academic Search
* adCenter Labs
* Office Labs

* v
* t
* e

Operating systems by Microsoft

Desktop / Server|

* Microsoft Windows
* 9x
* NT
* MS-DOS
* MSX-DOS
* Multitasking MS-DOS 4.0/4.1
* DOS/V
* Z-DOS
* OS/2
* Xenix

Mobile|

* Nokia Asha platform
* Nokia X platform
* KIN OS
* Windows Mobile
* Windows Phone
* Zune
* Windows 10 Mobile

Embedded / IoT|

* Azure Sphere
* ThreadX
* Windows Embedded Compact
* Windows IoT

Video game console|

* Xbox
* Xbox 360
* Xbox One

Network operating systems|

* MS-Net
* LAN Manager

Projects|

* Barrelfish
* Bigtop
* Cairo
* HomeOS
* Linux distros
* MIDAS
* Midori
* Singularity
* Verve

* v
* t
* e

Microkernels-nanokernels

Kernels|

* ADEOS
* EPOC
* EKA1
* EKA2
* Eumel
* Exec
* ExecSG
* EROS
* K42
* L3
* L4
* Little Kernel
* Mac OS nanokernel
* Mach
* GNU Mach
* MicroEmpix
* µ-velOSity
* nucleus
* NuKernel
* Off++
* Opus
* PowerUP
* Quark
* TI-RTOS kernel
* Vanguard
* WarpOS
* Zircon

Operating
systems|

* AmigaOS
* Amoeba
* AROS
* AspireOS
* Broadway
* Icaros Desktop
* ARX
* BeRTOS
* ChibiOS/RT
* ChorusOS
* Copland
* Cosmos
* EROS
* FreeRTOS
* Fuchsia
* Genode
* GNOSIS
* GNU Hurd
* HelenOS
* Hydra
* Integrity
* JX
* JavaOS
* KeyKOS
* Lites
* Classic Mac OS (PowerPC kernel)
* MachTen
* MacMach
* MeikOS
* MERT
* µC/OS
* Midori
* MINIX
* Minix-vmd
* MINIX 3
* MkLinux
* MorphOS
* MQX
* NLTSS
* Nucleus RTOS
* NuttX
* OS2000
* OSE
* Phantom OS
* PikeOS
* QNX
* RC 4000
* Redox
* REX OS
* RIOT
* SharpOS
* Singularity
* SPIN
* Spring
* Symbian
* Taligent OS
* ThreadX
* TI-RTOS
* Tinix
* UNICOS
* V
* Verve
* VRTX
* VSTa
* Wombat OS
* Workplace OS
* Zephyr

0.00

(0 votes)

Original source: https://en.wikipedia.org/wiki/Verve (operating system). Read more

|

Retrieved from "https://handwiki.org/wiki/index.php?title=Software:Verve_(operating_system)&oldid=779569"
*[v]: View this template
*[t]: Discuss this template
*[e]: Edit this template