Verve已经发布——一种类型安全的操作系统

作者 James Vastbinder 译者 侯伯薇 发布于 2010年12月20日

领域

运维 & 基础架构,

语言 & 开发

主题

.NET ,

编程 ,

操作系统 ,

架构 ,

Z3 ,

Singularity

分享到

最近微软研究院发布了一篇通告，声明 Verve的发布，它是来自于Singularity项目的一种操作系统，基本前提是要使用类型化汇编语言（Typed Assembly Language，TAL）和Hoare逻辑达到高级的保密性（security）和安全性（safety）。Verve操作系统由内核（nucleus）、核心（kernel）和一个或多个应用程序组成。

尽管为了便于自动编译成TAL，Verve是由C#编写的，但它还是执行了二次检查来验证类型安全性。内核本身是用汇编语言编写的，并用断言加上了手工的注解。它还使用Boogie根据规范来验证汇编语言，并确保它可以与TAL代码和硬件安全地交互。

Verve的成功之处

• 它是第一个能够从机制上验证以保证安全性的操作系统，其中包括的所有汇编语言指令都在启动时经过了静态验证，然后才会运行。
• 它可以运行在一般的硬件上，从而支持真正的语言特性，像类、虚拟方法、数组和先发线程（pre-emptive threads）等等。
• 高效，这是通过使用Bartok的对象、方法表和数组的本地布局达到的。
• 它演示了自动化技术、TAL和自动化定理证明，从而验证了操作系统中和运行时复杂的低级代码的安全性。
• 它演示了少量带有自动化定理证明功能，经过验证的代码它能够支持任意数量的TAL代码。

有了类型安全验证的代码，如果想要访问内存，只能通过对象引用和关联的特性——像字段和属性——达到。通过定义好的路径——在当前情况下是运行时——访问内存，核心可以验证代码并没有访问不该访问的内存位置。本质上，类型安全性意味着，除非程序的操作对于类型是合法的，否则就无法在对象上执行操作。类型安全性为高级编程语言（像Java和C#）中的保密性提供了最基本的要素，并且当扩展到操作系统级别时，会得到效率，并转化为性能。

Verve的局限

• 缺少对很多C#特性的支持，像异常处理等
• 不支持标准的.NET类库，因为它包含了不安全的代码
• 缺少对代码的动态载入
• 只能在单处理器上运行
• 缺少全面的隔离机制，像Singularity SIPS、Java Isolates和C# AppDomains
• Verve使用经过验证的垃圾回收器，它会在回收的过程中把一切操作停止，并禁用中断。

尽管Verve还有很多局限性，但它的创建者觉得只有对多处理器的支持是明显的障碍，因为那可能需要对当前的结构进行本质上的修改。

查看英文原文：Announcing Verve – A Type-Safe Operating System

译者 侯伯薇 是InfoQ中文站架构社区编辑，有多年对日和国内项目开发经验，目前关注企业中技术与实际业务之间的融合和协作。

相关厂商内容

保持某些系统的高可用性，是一些企业的重中之重，如何设计？

海量数据处理，海量视频分发，架构热点难点，尽在架构师峰会！

相关赞助商

ArchSummit全球架构师峰会报名启动！7折优惠，5月31日截止！

1. 返回顶部

   文章太简单。

   发表人 李 佩亮

   文章太简单，没有告知verve 系统是什么形态，既然是c# 开发的，那么系统运行的时候还需要基于托管环境么？

   回复

2. 返回顶部

   Re: 文章太简单。

   发表人 Shichao Liu

   虽然使用C#编写的，但编译出来的是本机码，静态验证静态执行，只是用的C#的语法，没有完整实现CLR。

   回复