隨著OKL4 Verified推出開放，有興趣的人士可以通過可用的用戶程序庫(kù)和/或半虛擬化Linux內(nèi)核，使用OKL4 現(xiàn)在，無論是強(qiáng)調(diào)安全性的設(shè)備制造商（OEMs）、移動(dòng)網(wǎng)絡(luò)運(yùn)營(yíng)商（MNOs）、應(yīng)用開發(fā)商、研究人員，還是其他感興趣的人士，都可以、運(yùn)行并在嵌入式ARM11平臺(tái)上測(cè)試OKL4 Verified，OKL4 Verified是一款很強(qiáng)大的東西，給社會(huì)帶來了無窮的，給一些公司解決了很大的困難，給他們帶來了豐厚的利潤(rùn)。

　　OK Labs公司之前曾宣布完成了由OK Labs公司、澳大利亞國(guó)家信息與通信技術(shù)研究機(jī)構(gòu)（NICTA）和新南威爾士大學(xué)（UNSW）共同合作的突破性研究，該項(xiàng)研究為內(nèi)核正確性提供了正式的數(shù)學(xué)論證。OKL4 Verified使用的流程在很大程度上消除了內(nèi)核的開發(fā)性錯(cuò)誤，緩沖溢出、包括設(shè)計(jì)缺陷、空指針解引用及其它指針錯(cuò)誤等代碼性錯(cuò)誤，以及內(nèi)存泄漏、算法溢出和異常等。

　　OK Labs公司創(chuàng)始人兼CEO Steve Subar表示： “經(jīng)充分驗(yàn)證且100%無缺陷的操作系統(tǒng)內(nèi)核可以滿足移動(dòng)/無線和其他嵌入應(yīng)用對(duì)更高安全性的迫切需求。OKL4 Verified為人們?cè)鰪?qiáng)了信心和保障，其底層技術(shù)在移動(dòng)/無線設(shè)備上實(shí)現(xiàn)了一系列高安全性和有保障的應(yīng)用?！?/P>

　　作為OK Labs公司創(chuàng)始人之一和NICTA靠得住嵌入式系統(tǒng)的負(fù)責(zé)人，Gernot Heiser和新南威爾士年夜學(xué)的John Lions教授評(píng)論道：“OKL4 Verified項(xiàng)目的完成使我們并世無雙的驗(yàn)證手藝引起了普遍關(guān)注。作為經(jīng)驗(yàn)證無非標(biāo)運(yùn)行的操作系統(tǒng)內(nèi)核，OKL4 Verified奠基了可托根本——它為普遍的應(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)用測(cè)試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ù)庫(kù)和其他構(gòu)建應(yīng)用需要的代碼、OKL4 Verified上運(yùn)行的半虛擬Linux系統(tǒng)、用戶指南以及正式的規(guī)格參數(shù)（Isabelle名目和PDF只讀名目）。

　　隨著OKL4 Verified推出開放，有興趣的人士可以通過可用的用戶程序庫(kù)和/或半虛擬化Linux內(nèi)核，使用OKL4 Verified進(jìn)行評(píng)估和原型設(shè)計(jì)。

　　OK Labs公司業(yè)務(wù)開發(fā)副總裁Carl Nerup表示：我們只能推出新型移動(dòng)安全內(nèi)核OKL4 Verified 這款產(chǎn)品，是基于我們的跟一些的公司合作還有我們永遠(yuǎn)一批卓越的人才，有了這樣的一個(gè)的環(huán)境新型移動(dòng)安全內(nèi)核OKL4 Verified 才被我公司推出的。