演講嘉賓 | 趙永望

回顧整理 | 廖 濤

排版校對 | 李萍萍

嘉賓簡介

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

內容來源

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

正 文 內 容

形式驗證根據某個或某些形式規范或屬性，使用數學的方法證明其正確性或非正確性，對保障操作系統安全起到重要作用。OpenHarmony形式驗證與安全認證面臨哪些挑戰，又有哪些技術方法和思路呢？浙江大學教授、移動終端安全技術浙江省工程研究中心主任趙永望在第一屆OpenHarmony技術峰會上分享了精彩觀點。

01?

為什么需要形式驗證與安全認證？

隨著計算機技術創新與行業發展，操作系統與軟件層出不窮，在航空航天、手機、車機、物聯網、醫療以及金融等領域應用廣泛。在各行各業綜合化、網絡化、智能化以及軟件化轉型的關鍵階段，操作系統安全的重要性日益凸顯，同時面臨新的安全挑戰。操作系統形式驗證與安全認證，是保障操作系統安全的關鍵手段之一。

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

為什么操作系統會潛在如此多的問題呢？客觀上，現在的軟件越來越復雜，很難摸透運行規律和質量特征。主觀上，開源社區、互聯網公司等大都采用敏捷式開發或者瀑布式開發，這種主流軟件開發方法難以滿足高安全可靠要求。

操作系統安全問題

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

形式化方法

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

安全認證及相關標準

02?

如何實現操作系統形式驗證？

浙江大學提出的操作系統形式驗證框架涉及操作系統各個不同層面，兼顧功能安全和信息安全，符合EAL7/SIL4等安全級別和ARINC653等工業標準，且支持多核/可搶占并發內核，覆蓋需求到C代碼的形式驗證，并具有統一的開發與驗證環境。

浙江大學操作系統形式驗證的理論與技術框架

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

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

03?

未來挑戰與建議

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

操作系統形式驗證部分痛點

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

形式驗證與安全認證是保障OpenHarmony操作系統安全的重要一環，期待后續能夠有更多的開發者與高校師生加入到相關領域的研究中來，共同促進OpenHarmony開源社區繁榮發展。

E N D

審核編輯 黃宇