領(lǐng)先的手機(jī)及寬帶互聯(lián)網(wǎng)設(shè)備嵌入式虛擬軟件提供商Open Kernel Labs (OK Labs)日前推出了可供下載的OKL4 Verified（項(xiàng)目名稱為seL4）,，一款經(jīng)過全面認(rèn)證的無缺陷安全微核,，專為移動(dòng)/無線設(shè)備中的關(guān)鍵業(yè)務(wù)和任務(wù)應(yīng)用而設(shè)計(jì)。現(xiàn)在,，無論是強(qiáng)調(diào)安全性的設(shè)備制造商（OEMs）,、移動(dòng)網(wǎng)絡(luò)運(yùn)營商(MNOs)、應(yīng)用開發(fā)商,、研究人員,，還是其他感興趣的人士，都可以下載,、運(yùn)行并在嵌入式ARM11平臺(tái)上測試OKL4 Verified,。(下載OKL4 Verified 的鏈接地址：http://www.ok-labs.com/registrations/software-EULA)
　
　　OK Labs公司之前曾宣布完成了由OK Labs公司、澳大利亞國家信息與通信技術(shù)研究機(jī)構(gòu)(NICTA)和新南威爾士大學(xué)(UNSW)共同合作的突破性研究,，該項(xiàng)研究為內(nèi)核正確性提供了正式的數(shù)學(xué)論證,。OKL4 Verified使用的認(rèn)證流程在很大程度上消除了內(nèi)核的開發(fā)性錯(cuò)誤,，包括設(shè)計(jì)缺陷、緩沖溢出,、空指針解引用及其它指針錯(cuò)誤等代碼性錯(cuò)誤,，以及內(nèi)存泄漏、算法溢出和異常等,。
　
　　隨著OKL4 Verified推出開放下載,，有興趣的人士可以通過可用的用戶程序庫和/或半虛擬化Linux內(nèi)核，使用OKL4 Verified進(jìn)行評估和原型設(shè)計(jì),。
　
　　OK Labs公司創(chuàng)始人兼CEO Steve Subar表示： “經(jīng)充分驗(yàn)證且100%無缺陷的操作系統(tǒng)內(nèi)核可以滿足移動(dòng)/無線和其他嵌入應(yīng)用對更高安全性的迫切需求,。OKL4 Verified為人們增強(qiáng)了信心和保障，其底層技術(shù)在移動(dòng)/無線設(shè)備上實(shí)現(xiàn)了一系列高安全性和有保障的應(yīng)用,。這是通向安全移動(dòng)通信的最佳方式,。”
　
　　作為OK Labs公司創(chuàng)始人之一和NICTA可靠嵌入式系統(tǒng)的負(fù)責(zé)人，Gernot Heiser和新南威爾士大學(xué)的John Lions教授評論道：“OKL4 Verified項(xiàng)目的完成使我們獨(dú)一無二的驗(yàn)證技術(shù)引起了廣泛關(guān)注,。作為首個(gè)經(jīng)驗(yàn)證無非標(biāo)運(yùn)行的操作系統(tǒng)內(nèi)核,，OKL4 Verified奠定了可信基礎(chǔ)——它為廣泛的應(yīng)用程序域提供了關(guān)鍵性的安全應(yīng)用。
　
主要內(nèi)容
　
　　•經(jīng)精確數(shù)學(xué)驗(yàn)證,，OKL4 Verified是現(xiàn)有唯一一種源代碼正確執(zhí)行規(guī)范要求的操作系統(tǒng),。
　　•OK Labs公司的OKL4 Verified（項(xiàng)目名稱為seL4）是與NICTA和新南威爾士大學(xué)共同花費(fèi)四年多時(shí)間獲得的研究成果，用于驗(yàn)證微核的準(zhǔn)確性和無缺陷性,。
　　•設(shè)備制造商,、開發(fā)商、研究人員和其他有興趣的人士現(xiàn)在就可以直接下載,、運(yùn)行,，并為真實(shí)應(yīng)用測試OKL4 Verified微核。
　　•OKL4 Verified與OKL4 Microvisor以及OK Labs公司移動(dòng)虛擬化方案采用同樣的底層技術(shù),，它是OK Labs公司在安全移動(dòng)通信領(lǐng)域投資的重要內(nèi)容,。
　　•下載內(nèi)容包括x86 和 ARM11的啟動(dòng)畫面、用戶空間數(shù)據(jù)庫和其他構(gòu)建應(yīng)用需要的代碼,、OKL4 Verified上運(yùn)行的半虛擬Linux系統(tǒng),、用戶指南以及正式的規(guī)格參數(shù)（Isabelle格式和PDF只讀格式）
　
產(chǎn)品上市時(shí)間
　
現(xiàn)在就可以通過以下方式下載和運(yùn)行OKL4 Verified微核：
　
　　•篩選基于ARM11的評估和產(chǎn)品板，包括Kyoto Microcomputer公司的KZM-ARM11-01（詳情請聯(lián)系OK Labs公司）
　　•X86/PC-AT硬件,，作為獨(dú)立操作系統(tǒng)的
　　•X86/PC-AT硬件,，半虛擬化Linux系統(tǒng)的主執(zhí)行程序，
　
注：OKL4 Verified僅限于非商業(yè)用途,。下載OKL4 Verified請登錄http://www.ok-labs.com/registrations/software-EULA。如需了解商業(yè)部署和更多OKL4 Verified,、OKL4和OK Labs 移動(dòng)虛擬化方案等內(nèi)容,，請登錄http://www.ok-labs.com,。