BT

如何利用碎片时间提升技术认知与能力? 点击获取答案

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

| 作者 James Vastbinder 关注 0 他的粉丝 ,译者 侯伯薇 关注 0 他的粉丝 发布于 2010年12月21日. 估计阅读时间: 3 分钟 | 如何结合区块链技术,帮助企业降本增效?让我们深度了解几个成功的案例。

最近微软研究院发布了一篇通告,声明 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账号 或者 才能进行评论。在您完成注册后还需要进行一些设置。

获得来自InfoQ的更多体验。

告诉我们您的想法

允许的HTML标签: a,b,br,blockquote,i,li,pre,u,ul,p

当有人回复此评论时请E-mail通知我

文章太简单。 by 李 佩亮

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

Re: 文章太简单。 by Shichao Liu

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

允许的HTML标签: a,b,br,blockquote,i,li,pre,u,ul,p

当有人回复此评论时请E-mail通知我

允许的HTML标签: a,b,br,blockquote,i,li,pre,u,ul,p

当有人回复此评论时请E-mail通知我

2 讨论

登陆InfoQ,与你最关心的话题互动。


找回密码....

Follow

关注你最喜爱的话题和作者

快速浏览网站内你所感兴趣话题的精选内容。

Like

内容自由定制

选择想要阅读的主题和喜爱的作者定制自己的新闻源。

Notifications

获取更新

设置通知机制以获取内容更新对您而言是否重要

BT