Microsoft Verve OS: a Type Safe Operating System

[M2G]

There’s a new operating system project at Microsoft, dubbed Verve. Read on in order to get information on Verve, a type safe OS developed by Microsoft Research.

The Singularity project (an OS written in managed code used for research purposes) has provided several very useful research results and opened new avenues for exploration in operating system design. Recently, 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 is what you think it is: Assembly with types (implemented as annotations and verified statically using the verification technology Boogie and the theorem prover Z3(Boogie generates verification conditions that are then statically proven by Z3. Boogie is also a language used to build program verifiers for other languages)). As with Singularity, the C# Bartok compiler is used, but this time it generates TAL. The entire OS stack is verifiably type safe (the Nucleus is essentially the Verve HAL) and all objects are garbage collected. It does not employ the SIP model of process isolation (like Singularity). In this case, again, the entire operating system is type safe and statically proven as such using world-class theorem provers.

Here’s the basic idea (from the introduction of the paper):

Typed assembly language (TAL) and Hoare logic can verify the absence of many kinds of errors in low-level code. 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 applications (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 applications that run on top of the kernel.

Here, Microsoft research scientist and operating system expert (he worked on the Singularity project) Chris Hawblitzel sits down with me to discuss the rationale behind the Verve project, the architecture and design of Verve and the Nucleus, Typed Assembly Language (TAL), potential for Verve in the real world, and much more. This is a conversational piece (no demos, no whiteboarding), but if you are into operating research and strategies for building type safe systems at the lowest levels, then this is for you. If you are interested, perhaps we could get Chris into our studio for a lecture or two on OS design.

Sursa: Introducing Verve: a Type Safe Operating System | CodenameWindows

[adonisslanic]

Hmm, imi place ca fac si astia ceva research. Macar la asta sa fie buni astia de la Microsoft. Ca dupa parerea mea Windowze e facut doar sa fie crapat <(._.)>

[M2G]

Din cate am inteles(pe partea de securitate) vor sa creeze un sistem de operare care nu e vulnerabil la buffer overflow folosind acel limbaj type-safe.

Codul sursa este public si se poate descarca de aici: Singularity RDK

Am gasit si un video dar nu am apucat inca sa il vizionez. http://channel9.msdn.com/Shows/Going+Deep/Verve-A-Type-Safe-Operating-System

[parazitul29]

interesanta ideea cu tal si hoare logic desi nu cred ca va intrece windows-ul vre-o data

[BGS]

@parazitul29 si mario intrece windows no offense .

[Paul4games]

Nu vreau sa incepem o alta dezbatere despre care OS este mai bun dar BGS nu cred ca esti in masura sa comentezi ca Windowsul nu este bun, daca si amrio il intrece atunci de ce nu creezi tu un windows mai bun?windowsul este facut pentru utilizatori de zi cu zi si este foarte bun pentru dezvoltatori de software pentru ca are o multime de useri, are mult buguri/rahaturi/nu il poti configura ca pe linux dar priunde bine la piata din cauza interfetei user friendly+cei de la microsoft in ultimul timp incearca sa il faca cat mai bun.

Edited July 16, 2011 by Paul4games

[BGS]

Prinde pe piata din cauza politici de monopol pe care a aplicato si o aplica microsoft .

Daca Linux nu are interfata user friendly eu imi tai bratu de sus pana jos cu cutitu .

PS: windows was built to be cracked .

[parazitul29]

tot cea conteaza e strategia de marketing , nu conteaza care e mai bun, chiar daca linux poate e de sute ori mai bun decat windows tot ceea ce conteaza e promovarea si microsoft e excelat in domeniul asta