领先的手机及宽带互联网设备嵌入式虚拟软件提供商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系统的主执行程序，

    注：OKL4 Verified仅限于非商业用途。下载OKL4 Verified。如需了解商业部署和更多OKL4 Verified、OKL4和OK Labs 移动虚拟化方案等内容。