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

随着OKL4 Verified推出开放下载，有兴趣的人士可以通过可用的用户程序库和/或半虚拟化Linux内核，使用OKL4 现在，无论是强调安全性的设备制造商（OEMs）、移动网络运营商（MNOs）、应用开发商、研究人员，还是其他感兴趣的人士，都可以下载、运行并在嵌入式ARM11平台上测试OKL4 Verified，OKL4 Verified是一款很强大的东西，给社会带来了无穷的，给一些公司解决了很大的困难，给他们带来了丰厚的利润。

OK Labs公司之前曾宣布完成了由OK Labs公司、澳大利亚国家信息与通信技术研究机构（NICTA）和新南威尔士大学（UNSW）共同合作的突破性研究，该项研究为内核正确性提供了正式的数学论证。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只读名目）。

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

OK Labs公司业务开发副总裁Carl Nerup表示：我们只能推出新型移动安全内核OKL4 Verified 这款产品，是基于我们的跟一些优秀的公司合作还有我们永远一批卓越的人才，有了这样的一个优秀的环境新型移动安全内核OKL4 Verified 才被我公司推出的。