演講嘉賓 | 趙永望
回顧整理 | 廖 濤
排版校對(duì) | 李萍萍
嘉賓簡(jiǎn)介
趙永望,浙江大學(xué)教授/博士生導(dǎo)師。擔(dān)任移動(dòng)終端安全技術(shù)浙江省工程研究中心主任、ARINC653國(guó)際操作系統(tǒng)標(biāo)準(zhǔn)委員會(huì)委員(國(guó)內(nèi)唯一委員)、國(guó)際信息技術(shù)安全評(píng)估標(biāo)準(zhǔn)(Common Criteria,CC)操作系統(tǒng)內(nèi)核技術(shù)委員會(huì)委員、中國(guó)計(jì)算機(jī)學(xué)會(huì)(CCF)高級(jí)會(huì)員、CCF系統(tǒng)軟件專委會(huì)和形式化方法專委會(huì)委員。任國(guó)際標(biāo)準(zhǔn)化組織 ISO/IEC JTC1 SOA研究組組長(zhǎng)、國(guó)家信標(biāo)委分委會(huì)委員,起草4項(xiàng)ISO國(guó)際標(biāo)準(zhǔn)、12項(xiàng)國(guó)家標(biāo)準(zhǔn)。曾任新加坡南洋理工大學(xué)高級(jí)研究員。主要研究方向包括操作系統(tǒng)安全、形式驗(yàn)證、編程語(yǔ)言原理等。主持和參與國(guó)家自然基金、核高基重大專項(xiàng)、重點(diǎn)研發(fā)計(jì)劃、載人航天工程重點(diǎn)項(xiàng)目、工信部物聯(lián)網(wǎng)創(chuàng)新項(xiàng)目等10余項(xiàng),2011和2017年分別獲得中國(guó)電子學(xué)會(huì)和山東省科技進(jìn)步一等獎(jiǎng)。相關(guān)研究成果得到美國(guó)波音、法國(guó)空客和國(guó)際知名實(shí)時(shí)操作系統(tǒng)廠商的認(rèn)可,被納入國(guó)際標(biāo)準(zhǔn),并在開(kāi)源實(shí)時(shí)操作系統(tǒng)社區(qū)產(chǎn)生影響力。
內(nèi)容來(lái)源
第一屆開(kāi)放原子開(kāi)源基金會(huì)OpenHarmony技術(shù)峰會(huì)——OpenHarmony高校技術(shù)俱樂(lè)部分論壇
正 文 內(nèi) 容
形式驗(yàn)證根據(jù)某個(gè)或某些形式規(guī)范或?qū)傩?,使用?shù)學(xué)的方法證明其正確性或非正確性,對(duì)保障操作系統(tǒng)安全起到重要作用。OpenHarmony形式驗(yàn)證與安全認(rèn)證面臨哪些挑戰(zhàn),又有哪些技術(shù)方法和思路呢?浙江大學(xué)教授、移動(dòng)終端安全技術(shù)浙江省工程研究中心主任趙永望在第一屆OpenHarmony技術(shù)峰會(huì)上分享了精彩觀點(diǎn)。
01?
為什么需要形式驗(yàn)證與安全認(rèn)證?
隨著計(jì)算機(jī)技術(shù)創(chuàng)新與行業(yè)發(fā)展,操作系統(tǒng)與軟件層出不窮,在航空航天、手機(jī)、車機(jī)、物聯(lián)網(wǎng)、醫(yī)療以及金融等領(lǐng)域應(yīng)用廣泛。在各行各業(yè)綜合化、網(wǎng)絡(luò)化、智能化以及軟件化轉(zhuǎn)型的關(guān)鍵階段,操作系統(tǒng)安全的重要性日益凸顯,同時(shí)面臨新的安全挑戰(zhàn)。操作系統(tǒng)形式驗(yàn)證與安全認(rèn)證,是保障操作系統(tǒng)安全的關(guān)鍵手段之一。
目前,操作系統(tǒng)仍潛在較多安全風(fēng)險(xiǎn)。例如,VxWorks 6.5版本被發(fā)現(xiàn)存在11個(gè)漏洞,影響2億臺(tái)關(guān)鍵設(shè)備;seL4的8900行C代碼中,通過(guò)形式驗(yàn)證發(fā)現(xiàn)了160多個(gè)新問(wèn)題;Zephyr RTOS中也存在多個(gè)內(nèi)存管理錯(cuò)誤。其中,seL4作為演變了多年的成熟開(kāi)源微內(nèi)核,仍存在較多代碼層的安全漏洞和問(wèn)題。OpenHarmony作為一個(gè)開(kāi)源社區(qū),包含了幾千萬(wàn)甚至上億行代碼,潛在的風(fēng)險(xiǎn)和問(wèn)題不容忽視。
為什么操作系統(tǒng)會(huì)潛在如此多的問(wèn)題呢?客觀上,現(xiàn)在的軟件越來(lái)越復(fù)雜,很難摸透運(yùn)行規(guī)律和質(zhì)量特征。主觀上,開(kāi)源社區(qū)、互聯(lián)網(wǎng)公司等大都采用敏捷式開(kāi)發(fā)或者瀑布式開(kāi)發(fā),這種主流軟件開(kāi)發(fā)方法難以滿足高安全可靠要求。
操作系統(tǒng)安全問(wèn)題
安全認(rèn)證通過(guò)嚴(yán)格的過(guò)程和證據(jù)解決軟件的安全問(wèn)題,對(duì)證據(jù)鏈的要求很高。其證據(jù)鏈由非形式化、半形式化以及形式化的數(shù)據(jù)組成,包括文檔、數(shù)據(jù)、模型等。目前,證據(jù)鏈在很多場(chǎng)合通過(guò)文檔和人工評(píng)審的方式來(lái)形成,但對(duì)于安全等級(jí)非常高的場(chǎng)景仍難以滿足相關(guān)要求。因此,在該場(chǎng)景下可通過(guò)形式化方法,完成準(zhǔn)確且完備的軟件建模和認(rèn)證。
形式化方法
形式化方法基于嚴(yán)格數(shù)學(xué)基礎(chǔ)對(duì)計(jì)算機(jī)軟硬件系統(tǒng)進(jìn)行描述、開(kāi)發(fā)和驗(yàn)證的技術(shù),具有精確、嚴(yán)格以及完備的特點(diǎn)。在高級(jí)別安全認(rèn)證中,強(qiáng)烈推薦或強(qiáng)制使用形式化方法。目前,與國(guó)外相比,國(guó)內(nèi)開(kāi)源操作系統(tǒng)在關(guān)鍵的DO-178 A和CC EAL 6/7等高安全等級(jí)的形式驗(yàn)證與安全認(rèn)證方法相關(guān)研究基本處于空白狀態(tài)。
安全認(rèn)證及相關(guān)標(biāo)準(zhǔn)
02?
如何實(shí)現(xiàn)操作系統(tǒng)形式驗(yàn)證?
浙江大學(xué)提出的操作系統(tǒng)形式驗(yàn)證框架涉及操作系統(tǒng)各個(gè)不同層面,兼顧功能安全和信息安全,符合EAL7/SIL4等安全級(jí)別和ARINC653等工業(yè)標(biāo)準(zhǔn),且支持多核/可搶占并發(fā)內(nèi)核,覆蓋需求到C代碼的形式驗(yàn)證,并具有統(tǒng)一的開(kāi)發(fā)與驗(yàn)證環(huán)境。
浙江大學(xué)操作系統(tǒng)形式驗(yàn)證的理論與技術(shù)框架
在該框架中,操作系統(tǒng)領(lǐng)域知識(shí)層面包括信息流安全/功能安全、ARINC 653標(biāo)準(zhǔn)、操作系統(tǒng)設(shè)計(jì)以及操作系統(tǒng)C代碼等;操作系統(tǒng)模型與證明層面包括安全需求、功能規(guī)約、高層設(shè)計(jì)規(guī)約、低層設(shè)計(jì)規(guī)約以及實(shí)現(xiàn)模型等。此外,還包含形式規(guī)約語(yǔ)言及編譯器、規(guī)約求精框架、并發(fā)驗(yàn)證方法、安全性驗(yàn)證方法、系統(tǒng)級(jí)執(zhí)行模型、自動(dòng)化驗(yàn)證方法、源代碼形式語(yǔ)義以及邏輯證明內(nèi)核等形式語(yǔ)義和支撐工具。此外,趙永望所在團(tuán)隊(duì)基于Isabelle定理證明器自研了操作系統(tǒng)形式驗(yàn)證工具:Isabelle/Cloud云平臺(tái),通過(guò)云化和開(kāi)源的方式,讓社區(qū)的開(kāi)發(fā)者和高校師生都能夠在該平臺(tái)上做相應(yīng)的驗(yàn)證和建模等工作。
該框架具有以下特征:(1)采用逐步求精方法,覆蓋安全、需求、設(shè)計(jì)、源碼全部層面;(2)提供完整的形式化模型;(3)提供完整的自頂向下證據(jù)鏈,最終保障內(nèi)核代碼的安全性和正確性;(4)模型和驗(yàn)證可擴(kuò)展;(5)采用自研工具;(6)整體框架和采用的技術(shù)符合CC最高安全級(jí)EAL7。目前,該框架在某國(guó)產(chǎn)安全微內(nèi)核操作系統(tǒng)的形式驗(yàn)證中,獲得了國(guó)內(nèi)評(píng)測(cè)機(jī)構(gòu)頒發(fā)的首個(gè)軟件領(lǐng)域的EAL5+的證書,且正在實(shí)施國(guó)內(nèi)最早的一批軟件EAL5+形式驗(yàn)證與評(píng)估項(xiàng)目。
03?
未來(lái)挑戰(zhàn)與建議
操作系統(tǒng)形式驗(yàn)證與安全認(rèn)證技術(shù)在進(jìn)一步的發(fā)展中仍在面臨諸多挑戰(zhàn)和困難。在技術(shù)方面,需要考慮多核并發(fā)、執(zhí)行搶占、C語(yǔ)言自身復(fù)雜性、ISA耦合、操作系統(tǒng)數(shù)據(jù)結(jié)構(gòu)與算法復(fù)雜以及代碼規(guī)模大等因素;在工程方面,存在領(lǐng)域知識(shí)專業(yè)門檻高、沒(méi)有針對(duì)性的驗(yàn)證工具、模型編寫難、驗(yàn)證難度高、工作量大、代碼規(guī)模大以及操作系統(tǒng)版本迭代等問(wèn)題。其中,針對(duì)操作系統(tǒng)資料/文檔的形式化建模效率低、源碼驗(yàn)證代碼規(guī)模大、結(jié)構(gòu)復(fù)雜、語(yǔ)言類型多、驗(yàn)證難度大以及成本高等問(wèn)題,可以考慮自動(dòng)形式模型生成和源碼自動(dòng)形式驗(yàn)證等方法。
操作系統(tǒng)形式驗(yàn)證部分痛點(diǎn)
OpenHarmony是一個(gè)面向全場(chǎng)景智能終端的開(kāi)源操作系統(tǒng),覆蓋全場(chǎng)景應(yīng)用,同時(shí)也支持多樣性設(shè)備。對(duì)于OpenHarmony來(lái)說(shuō),形式驗(yàn)證與安全認(rèn)證有以下5個(gè)關(guān)鍵點(diǎn):(1)重要性:OpenHarmony作為信息基礎(chǔ)設(shè)施底座,如果缺少形式驗(yàn)證與安全認(rèn)證,潛在風(fēng)險(xiǎn)程度很高;(2)必要性:OpenHarmony賦能千行百業(yè),其中囊括了許多安全關(guān)鍵產(chǎn)業(yè),形式驗(yàn)證與安全認(rèn)證是安全關(guān)鍵行業(yè)所必須的。此外,一個(gè)安全可靠的操作系統(tǒng)將具有更高數(shù)量級(jí)的產(chǎn)業(yè)價(jià)值;(3)OpenHarmony這樣大規(guī)模操作系統(tǒng)的形式驗(yàn)證與安全認(rèn)證技術(shù)國(guó)產(chǎn)化的成功,符合目前操作系統(tǒng)國(guó)產(chǎn)化替代和發(fā)展的策略;(4)挑戰(zhàn)性:OpenHarmony這樣大規(guī)模軟件系統(tǒng)的自動(dòng)化形式驗(yàn)證難度較高,高效率安全認(rèn)證面臨挑戰(zhàn);(5)可行性:目前,國(guó)內(nèi)已積累一定的形式驗(yàn)證與安全認(rèn)證基礎(chǔ),且國(guó)內(nèi)外形式化技術(shù)快速發(fā)展,OpenHarmony開(kāi)源社區(qū)同樣發(fā)展迅速,能夠提供助力,進(jìn)一步發(fā)展OpenHarmony形式驗(yàn)證與安全認(rèn)證具備可行性。
形式驗(yàn)證與安全認(rèn)證是保障OpenHarmony操作系統(tǒng)安全的重要一環(huán),期待后續(xù)能夠有更多的開(kāi)發(fā)者與高校師生加入到相關(guān)領(lǐng)域的研究中來(lái),共同促進(jìn)OpenHarmony開(kāi)源社區(qū)繁榮發(fā)展。
E N D
審核編輯 黃宇
-
操作系統(tǒng)
+關(guān)注
關(guān)注
37文章
6545瀏覽量
122743 -
OpenHarmony
+關(guān)注
關(guān)注
25文章
3548瀏覽量
15737
發(fā)布評(píng)論請(qǐng)先 登錄
相關(guān)推薦
評(píng)論