OK Labs公司推出可供下载及原型设计的移动安全内核OKL4 Verified

OK Labs公司推出可供下载及原型设计的新型移动安全内核：OKL4 Verified

有安全意识的OEM厂商、开发商和研究人员现在可以评估这一经过全面测试的无缺陷内核产品，开发稳定可靠的安全移动与无线应用

领先的手机及宽带互联网设备嵌入式虚拟软件提供商Open Kernel Labs (OK Labs)日前推出了可供下载的OKL4 Verified（项目名称为seL4），一款经过全面认证的无缺陷安全微核，专为移动/无线设备中的关键业务和任务应用而设计。现在，无论是强调安全性的设备制造商（OEMs）、移动网络运营商(MNOs)、应用开发商、研究人员，还是其他感兴趣的人士，都可以下载、运行并在嵌入式ARM11平台上测试OKL4 Verified。

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只读格式）

产品上市时间

现在就可以通过以下方式下载和运行OKL4 Verified微核：

• 筛选基于ARM11的评估和产品板，包括Kyoto Microcomputer公司的KZM-ARM11-01（详情请联系OK Labs公司）
• X86/PC-AT硬件，作为独立操作系统的
• X86/PC-AT硬件，半虚拟化Linux系统的主执行程序，