EDN China > 产品新闻 > 嵌入式系统 > 操作系统 > 正文
? 2016博客大赛-不限主题,寻找电子导师,大奖升级??

OK Labs推出新型移动安全内核:OKL4 Verified

EDN China?? 2011年01月28日 ?? 收藏0

  Open Kernel Labs (OK Labs)日前推出了可供下载的OKL4 Verified(项目名称为seL4),一款经过全面认证的无缺陷安全微核,专为移动/无线设备中的关键业务和任务应用而设计。现在,无论是强调安全性的设备制造商(OEMs)、移动网络运营商(MNOs)、应用开发商、研究人员,还是其他感兴趣的人士,都可以下载、运行并在嵌入式ARM11平台上测试OKL4 Verified。(下载OKL4 Verified 的链接地址:http://www.ok-labs.com/registrations/software-EULA

)

  OK Labs公司之前曾宣布完成了由OK Labs公司、澳大利亚国家信息与通信技术研究机构(NICTA)和新南威尔士大学(UNSW)共同合作的突破性研究,该项研究为内核正确性提供了正式的数学论证。OKL4 Verified使用的认证流程在很大程度上消除了内核的开发性错误,包括设计缺陷、缓冲溢出、空指针解引用及其它指针错误等代码性错误,以及内存泄漏、算法溢出和异常等。

  随着OKL4 Verified推出开放下载,有兴趣的人士可以通过可用的用户程序库和/或半虚拟化Linux内核,使用OKL4 Verified进行评估和原型设计。

  OK Labs公司创始人兼CEO Steve Subar表示: “经充分验证且100%无缺陷的操作系统内核可以满足移动/无线和其他嵌入应用对更高安全性的迫切需求。OKL4 Verified为人们增强了信心和保障,其底层技术在移动/无线设备上实现了一系列高安全性和有保障的应用。这是通向安全移动通信的最佳方式。”

  作为OK Labs公司创始人之一和NICTA可靠嵌入式系统的负责人,Gernot Heiser和新南威尔士大学的John Lions教授评论道:“OKL4 Verified项目的完成使我们独一无二的验证技术引起了广泛关注。作为首个经验证无非标运行的操作系统内核,OKL4 Verified奠定了可信基础——它为广泛的应用程序域提供了关键性的安全应用。

  主要内容

  ??经精确数学验证,OKL4 Verified是现有唯一一种源代码正确执行规范要求的操作系统。

?????? ??OK Labs公司的OKL4 Verified(项目名称为seL4)是与NICTA和新南威尔士大学共同花费四年多时间获得的研究成果,用于验证微核的准确性和无缺陷性。

?????? ??设备制造商、开发商、研究人员和其他有兴趣的人士现在就可以直接下载、运行,并为真实应用测试OKL4 Verified微核。

?????? ??OKL4 Verified与OKL4 Microvisor以及OK Labs公司移动虚拟化方案采用同样的底层技术,它是OK Labs公司在安全移动通信领域投资的重要内容。

?????? ??下载内容包括x86 和 ARM11的启动画面、用户空间数据库和其他构建应用需要的代码、OKL4 Verified上运行的半虚拟Linux系统、用户指南以及正式的规格参数(Isabelle格式和PDF只读格式)


?? ?? ??


打开微信“扫一扫”,打开网页后点击屏幕右上角分享按钮

1.扫描左侧二维码
2.点击右上角的分享按钮
3.选择分享给朋友
?? ??

OK Labs? 移动安全内核? OKL4 Verified?

上一篇: 慢速内存和快速内存可“合二为一”
下一篇: 德州仪器推出 64 款超低功耗微控制器
相关文章

我来评论
美国的游客
美国的游客 ??? (您将以游客身份发表,请登录 | 注册)
?
今日头条
精彩图集
有问题请反馈