演講嘉賓 | 趙永望

回顧整理 | 廖 濤

排版校對 | 李萍萍

嘉賓簡介

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

內(nèi)容來源

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

正 文 內(nèi) 容

形式驗證根據(jù)某個或某些形式規(guī)范或?qū)傩裕褂脭?shù)學(xué)的方法證明其正確性或非正確性，對保障操作系統(tǒng)安全起到重要作用。OpenHarmony形式驗證與安全認(rèn)證面臨哪些挑戰(zhàn)，又有哪些技術(shù)方法和思路呢？浙江大學(xué)教授、移動終端安全技術(shù)浙江省工程研究中心主任趙永望在第一屆OpenHarmony技術(shù)峰會上分享了精彩觀點。

01?

為什么需要形式驗證與安全認(rèn)證？

隨著計算機技術(shù)創(chuàng)新與行業(yè)發(fā)展，操作系統(tǒng)與軟件層出不窮，在航空航天、手機、車機、物聯(lián)網(wǎng)、醫(yī)療以及金融等領(lǐng)域應(yīng)用廣泛。在各行各業(yè)綜合化、網(wǎng)絡(luò)化、智能化以及軟件化轉(zhuǎn)型的關(guān)鍵階段，操作系統(tǒng)安全的重要性日益凸顯，同時面臨新的安全挑戰(zhàn)。操作系統(tǒng)形式驗證與安全認(rèn)證，是保障操作系統(tǒng)安全的關(guān)鍵手段之一。

目前，操作系統(tǒng)仍潛在較多安全風(fēng)險。例如，VxWorks 6.5版本被發(fā)現(xiàn)存在11個漏洞，影響2億臺關(guān)鍵設(shè)備；seL4的8900行C代碼中，通過形式驗證發(fā)現(xiàn)了160多個新問題；Zephyr RTOS中也存在多個內(nèi)存管理錯誤。其中，seL4作為演變了多年的成熟開源微內(nèi)核，仍存在較多代碼層的安全漏洞和問題。OpenHarmony作為一個開源社區(qū)，包含了幾千萬甚至上億行代碼，潛在的風(fēng)險和問題不容忽視。

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

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

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

形式化方法

形式化方法基于嚴(yán)格數(shù)學(xué)基礎(chǔ)對計算機軟硬件系統(tǒng)進(jìn)行描述、開發(fā)和驗證的技術(shù)，具有精確、嚴(yán)格以及完備的特點。在高級別安全認(rèn)證中，強烈推薦或強制使用形式化方法。目前，與國外相比，國內(nèi)開源操作系統(tǒng)在關(guān)鍵的DO-178 A和CC EAL 6/7等高安全等級的形式驗證與安全認(rèn)證方法相關(guān)研究基本處于空白狀態(tài)。

安全認(rèn)證及相關(guān)標(biāo)準(zhǔn)

02?

如何實現(xiàn)操作系統(tǒng)形式驗證？

浙江大學(xué)提出的操作系統(tǒng)形式驗證框架涉及操作系統(tǒng)各個不同層面，兼顧功能安全和信息安全，符合EAL7/SIL4等安全級別和ARINC653等工業(yè)標(biāo)準(zhǔn)，且支持多核/可搶占并發(fā)內(nèi)核，覆蓋需求到C代碼的形式驗證，并具有統(tǒng)一的開發(fā)與驗證環(huán)境。

浙江大學(xué)操作系統(tǒng)形式驗證的理論與技術(shù)框架

在該框架中，操作系統(tǒng)領(lǐng)域知識層面包括信息流安全/功能安全、ARINC 653標(biāo)準(zhǔn)、操作系統(tǒng)設(shè)計以及操作系統(tǒng)C代碼等；操作系統(tǒng)模型與證明層面包括安全需求、功能規(guī)約、高層設(shè)計規(guī)約、低層設(shè)計規(guī)約以及實現(xiàn)模型等。此外，還包含形式規(guī)約語言及編譯器、規(guī)約求精框架、并發(fā)驗證方法、安全性驗證方法、系統(tǒng)級執(zhí)行模型、自動化驗證方法、源代碼形式語義以及邏輯證明內(nèi)核等形式語義和支撐工具。此外，趙永望所在團(tuán)隊基于Isabelle定理證明器自研了操作系統(tǒng)形式驗證工具：Isabelle/Cloud云平臺，通過云化和開源的方式，讓社區(qū)的開發(fā)者和高校師生都能夠在該平臺上做相應(yīng)的驗證和建模等工作。

該框架具有以下特征：（1）采用逐步求精方法，覆蓋安全、需求、設(shè)計、源碼全部層面；（2）提供完整的形式化模型；（3）提供完整的自頂向下證據(jù)鏈，最終保障內(nèi)核代碼的安全性和正確性；（4）模型和驗證可擴展；（5）采用自研工具；（6）整體框架和采用的技術(shù)符合CC最高安全級EAL7。目前，該框架在某國產(chǎn)安全微內(nèi)核操作系統(tǒng)的形式驗證中，獲得了國內(nèi)評測機構(gòu)頒發(fā)的首個軟件領(lǐng)域的EAL5+的證書，且正在實施國內(nèi)最早的一批軟件EAL5+形式驗證與評估項目。

03?

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

操作系統(tǒng)形式驗證與安全認(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)域知識專業(yè)門檻高、沒有針對性的驗證工具、模型編寫難、驗證難度高、工作量大、代碼規(guī)模大以及操作系統(tǒng)版本迭代等問題。其中，針對操作系統(tǒng)資料/文檔的形式化建模效率低、源碼驗證代碼規(guī)模大、結(jié)構(gòu)復(fù)雜、語言類型多、驗證難度大以及成本高等問題，可以考慮自動形式模型生成和源碼自動形式驗證等方法。

操作系統(tǒng)形式驗證部分痛點

OpenHarmony是一個面向全場景智能終端的開源操作系統(tǒng)，覆蓋全場景應(yīng)用，同時也支持多樣性設(shè)備。對于OpenHarmony來說，形式驗證與安全認(rèn)證有以下5個關(guān)鍵點：（1）重要性：OpenHarmony作為信息基礎(chǔ)設(shè)施底座，如果缺少形式驗證與安全認(rèn)證，潛在風(fēng)險程度很高；（2）必要性：OpenHarmony賦能千行百業(yè)，其中囊括了許多安全關(guān)鍵產(chǎn)業(yè)，形式驗證與安全認(rèn)證是安全關(guān)鍵行業(yè)所必須的。此外，一個安全可靠的操作系統(tǒng)將具有更高數(shù)量級的產(chǎn)業(yè)價值；（3）OpenHarmony這樣大規(guī)模操作系統(tǒng)的形式驗證與安全認(rèn)證技術(shù)國產(chǎn)化的成功，符合目前操作系統(tǒng)國產(chǎn)化替代和發(fā)展的策略；（4）挑戰(zhàn)性：OpenHarmony這樣大規(guī)模軟件系統(tǒng)的自動化形式驗證難度較高，高效率安全認(rèn)證面臨挑戰(zhàn)；（5）可行性：目前，國內(nèi)已積累一定的形式驗證與安全認(rèn)證基礎(chǔ)，且國內(nèi)外形式化技術(shù)快速發(fā)展，OpenHarmony開源社區(qū)同樣發(fā)展迅速，能夠提供助力，進(jìn)一步發(fā)展OpenHarmony形式驗證與安全認(rèn)證具備可行性。

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

E N D

審核編輯 黃宇