Verve：一个类型安全的操作系统

[vikyzhang]

Verve：一个类型安全的操作系统
发表于：2010-12-10 23:22 UTC

“Singularity（一个用用于调查目的的代码写成的操作系统）项目提供了几个非常有用的调查结果，为操作系统的设计开辟了新的探索之路。最近，微软研究院发布了一个描述一个操作系统调查项目的文件，它寻求出了一个新的、用可检验与类型安全的管理代码建造OS栈的途径。此项目以新奇的方式使用了类型化汇编语言；后者即为你从字面意思理解到的——带型（以注释形式实现，使用Boogie认证技术和定理谁器Z3（Boogie生成出认证条件，之后它们会被Z3静态证明。Boogie同时也是一个用于编译其他语言的程序认证器的语言）静态认证）汇编语言。Singularity中，C# Bartok编译器也被使用了，不过这次它生成的是TAL（事物处理应用语言）。整个OS栈经证实是类型安全的（其Nucleus本质上是Verve HAL），并且所有对象都可被垃圾回收。这并没有使用进程隔离的SIP（SIP是一个计算机网络中应用层的信令控制协议）模型（像Singularity）。这种情况下，整个操作系统再次被确保是类型安全的，并使用世界级定理认明器被静态认证。Channel9有一个与其中一位开发者有关他该项目的视频采谈。Verve源码可用。

英文原文：http://www.osnews.com/story/24115/Ver ... ype_Safe_Operating_System
转载请注明：Linux人社区 英文资讯翻译专版 编译
http://www.linux-ren.org/modules/newbb/ ... post320003

[xllongxiao]

顶起来