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

最新ubuntu/linux/开源新闻或者其它IT相关资讯
回复
头像
vikyzhang
帖子: 677
注册时间: 2010-10-18 14:39
送出感谢: 0
接收感谢: 1 次
联系:

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

#1

帖子 vikyzhang » 2010-12-11 9:56

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
Linux人社区开源新闻资讯翻译专版小编。翻译来自互联网上最新的英文开源资讯,提供给大家最迅即、最忠实于原文的开源业界动态、软件更新、有用技能等等。不至之处欢迎指正!xyxzfj@gmail.com
xllongxiao
帖子: 2
注册时间: 2009-04-17 13:15
送出感谢: 0
接收感谢: 0

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

#2

帖子 xllongxiao » 2010-12-11 10:54

:em04 :em04 顶起来
回复

回到 “新闻和通知”