新型移動安全內核OKL4 Verified（OK Labs ）

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系統的主執行程序，