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

最近微软研究院发布了一篇通告，声明 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