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

  • James Vastbinder
  • 侯伯薇

2010 年 12 月 20 日

话题:.NET架构DevOps语言 & 开发

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

.NET架构DevOps语言 & 开发