演講嘉賓 | 趙永望

回顧整理 | 廖 濤

排版校對(duì) | 李萍萍

嘉賓簡(jiǎn)介

趙永望，浙江大學(xué)教授/博士生導(dǎo)師。擔(dān)任移動(dòng)終端安全技術(shù)浙江省工程研究中心主任、ARINC653國際操作系統(tǒng)標(biāo)準(zhǔn)委員會(huì)委員（國內(nèi)唯一委員）、國際信息技術(shù)安全評(píng)估標(biāo)準(zhǔn)(Common Criteria,CC)操作系統(tǒng)內(nèi)核技術(shù)委員會(huì)委員、中國計(jì)算機(jī)學(xué)會(huì)(CCF)高級(jí)會(huì)員、CCF系統(tǒng)軟件專委會(huì)和形式化方法專委會(huì)委員。任國際標(biāo)準(zhǔn)化組織 ISO/IEC JTC1 SOA研究組組長(zhǎng)、國家信標(biāo)委分委會(huì)委員，起草4項(xiàng)ISO國際標(biāo)準(zhǔn)、12項(xiàng)國家標(biāo)準(zhǔn)。曾任新加坡南洋理工大學(xué)高級(jí)研究員。主要研究方向包括操作系統(tǒng)安全、形式驗(yàn)證、編程語言原理等。主持和參與國家自然基金、核高基重大專項(xiàng)、重點(diǎn)研發(fā)計(jì)劃、載人航天工程重點(diǎn)項(xiàng)目、工信部物聯(lián)網(wǎng)創(chuàng)新項(xiàng)目等10余項(xiàng)，2011和2017年分別獲得中國電子學(xué)會(huì)和山東省科技進(jìn)步一等獎(jiǎng)。相關(guān)研究成果得到美國波音、法國空客和國際知名實(shí)時(shí)操作系統(tǒng)廠商的認(rèn)可，被納入國際標(biāo)準(zhǔn)，并在開源實(shí)時(shí)操作系統(tǒng)社區(qū)產(chǎn)生影響力。

內(nèi)容來源

第一屆開放原子開源基金會(huì)OpenHarmony技術(shù)峰會(huì)——OpenHarmony高校技術(shù)俱樂部分論壇

正 文 內(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代碼中，通過形式驗(yàn)證發(fā)現(xiàn)了160多個(gè)新問題；Zephyr RTOS中也存在多個(gè)內(nèi)存管理錯(cuò)誤。其中，seL4作為演變了多年的成熟開源微內(nèi)核，仍存在較多代碼層的安全漏洞和問題。OpenHarmony作為一個(gè)開源社區(qū)，包含了幾千萬甚至上億行代碼，潛在的風(fēng)險(xiǎn)和問題不容忽視。

為什么操作系統(tǒng)會(huì)潛在如此多的問題呢？客觀上，現(xiàn)在的軟件越來越復(fù)雜，很難摸透運(yùn)行規(guī)律和質(zhì)量特征。主觀上，開源社區(qū)、互聯(lián)網(wǎng)公司等大都采用敏捷式開發(fā)或者瀑布式開發(fā)，這種主流軟件開發(fā)方法難以滿足高安全可靠要求。

操作系統(tǒng)安全問題

安全認(rèn)證通過嚴(yán)格的過程和證據(jù)解決軟件的安全問題，對(duì)證據(jù)鏈的要求很高。其證據(jù)鏈由非形式化、半形式化以及形式化的數(shù)據(jù)組成，包括文檔、數(shù)據(jù)、模型等。目前，證據(jù)鏈在很多場(chǎng)合通過文檔和人工評(píng)審的方式來形成，但對(duì)于安全等級(jí)非常高的場(chǎng)景仍難以滿足相關(guān)要求。因此，在該場(chǎng)景下可通過形式化方法，完成準(zhǔn)確且完備的軟件建模和認(rèn)證。

形式化方法

形式化方法基于嚴(yán)格數(shù)學(xué)基礎(chǔ)對(duì)計(jì)算機(jī)軟硬件系統(tǒng)進(jìn)行描述、開發(fā)和驗(yàn)證的技術(shù)，具有精確、嚴(yán)格以及完備的特點(diǎn)。在高級(jí)別安全認(rèn)證中，強(qiáng)烈推薦或強(qiáng)制使用形式化方法。目前，與國外相比，國內(nè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)一的開發(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ī)約語言及編譯器、規(guī)約求精框架、并發(fā)驗(yàn)證方法、安全性驗(yàn)證方法、系統(tǒng)級(jí)執(zhí)行模型、自動(dòng)化驗(yàn)證方法、源代碼形式語義以及邏輯證明內(nèi)核等形式語義和支撐工具。此外，趙永望所在團(tuán)隊(duì)基于Isabelle定理證明器自研了操作系統(tǒng)形式驗(yàn)證工具：Isabelle/Cloud云平臺(tái)，通過云化和開源的方式，讓社區(qū)的開發(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。目前，該框架在某國產(chǎn)安全微內(nèi)核操作系統(tǒng)的形式驗(yàn)證中，獲得了國內(nèi)評(píng)測(cè)機(jī)構(gòu)頒發(fā)的首個(gè)軟件領(lǐng)域的EAL5+的證書，且正在實(shí)施國內(nèi)最早的一批軟件EAL5+形式驗(yàn)證與評(píng)估項(xiàng)目。

03?

未來挑戰(zhàn)與建議

操作系統(tǒng)形式驗(yàn)證與安全認(rèn)證技術(shù)在進(jìn)一步的發(fā)展中仍在面臨諸多挑戰(zhàn)和困難。在技術(shù)方面，需要考慮多核并發(fā)、執(zhí)行搶占、C語言自身復(fù)雜性、ISA耦合、操作系統(tǒng)數(shù)據(jù)結(jié)構(gòu)與算法復(fù)雜以及代碼規(guī)模大等因素；在工程方面，存在領(lǐng)域知識(shí)專業(yè)門檻高、沒有針對(duì)性的驗(yàn)證工具、模型編寫難、驗(yàn)證難度高、工作量大、代碼規(guī)模大以及操作系統(tǒng)版本迭代等問題。其中，針對(duì)操作系統(tǒng)資料/文檔的形式化建模效率低、源碼驗(yàn)證代碼規(guī)模大、結(jié)構(gòu)復(fù)雜、語言類型多、驗(yàn)證難度大以及成本高等問題，可以考慮自動(dòng)形式模型生成和源碼自動(dòng)形式驗(yàn)證等方法。

操作系統(tǒng)形式驗(yàn)證部分痛點(diǎn)

OpenHarmony是一個(gè)面向全場(chǎng)景智能終端的開源操作系統(tǒng)，覆蓋全場(chǎng)景應(yīng)用，同時(shí)也支持多樣性設(shè)備。對(duì)于OpenHarmony來說，形式驗(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ù)國產(chǎn)化的成功，符合目前操作系統(tǒng)國產(chǎn)化替代和發(fā)展的策略；（4）挑戰(zhàn)性：OpenHarmony這樣大規(guī)模軟件系統(tǒng)的自動(dòng)化形式驗(yàn)證難度較高，高效率安全認(rèn)證面臨挑戰(zhàn)；（5）可行性：目前，國內(nèi)已積累一定的形式驗(yàn)證與安全認(rèn)證基礎(chǔ)，且國內(nèi)外形式化技術(shù)快速發(fā)展，OpenHarmony開源社區(qū)同樣發(fā)展迅速，能夠提供助力，進(jìn)一步發(fā)展OpenHarmony形式驗(yàn)證與安全認(rèn)證具備可行性。

形式驗(yàn)證與安全認(rèn)證是保障OpenHarmony操作系統(tǒng)安全的重要一環(huán)，期待后續(xù)能夠有更多的開發(fā)者與高校師生加入到相關(guān)領(lǐng)域的研究中來，共同促進(jìn)OpenHarmony開源社區(qū)繁榮發(fā)展。

E N D

審核編輯 黃宇