操作系統(tǒng)內(nèi)核驗證

1、操作系統(tǒng)內(nèi)核驗證馮新宇中國科學技術大學2017-12-16第五屆開源操作系統(tǒng)年會（OS2ATC 2017）Stuxnet蠕蟲病毒2010年Stuxnet病毒對伊朗核電站的攻擊利用了Windows系統(tǒng)的4個zero-day安全漏洞/information-technology/2017/04/windows-bug-used-to-spread-stuxnet-remains-worlds-most-exploited/報道時間：2017年4月利用Windows操作系統(tǒng)的缺陷2017年5月Wannacry勒索軟件攻擊如何保證OS“沒有bug”？軟件測試工程中廣泛應用，并且有效 入門相對容易、容易

2、自動化 無法保證沒有bug 在并發(fā)（多核/網(wǎng)絡）環(huán)境下面臨挑戰(zhàn)Testing shows the presence, not the absence of bugs. Edsger W. Dijkstra美國東北大停電發(fā)生于2003年8月14日，覆蓋美國東北部、中西部和加拿大的安大略地區(qū)警報系統(tǒng)中的軟件的數(shù)據(jù)競爭錯誤，導致預警無法及時發(fā)出和處理美國東北大停電We test exhaustively, we test with third parties, and we had in excess of three million online operational hours in whic

3、h nothing had ever exercised that bug. Im not sure that more testing would have revealed that. Unfortunately, thats kind of the nature of software you may never find the problem. I dont think thats unique to control systems or any particular vendor software.- Mike Unum, manager at GE Energy程序驗證規(guī)約（數(shù)學

4、描述）證明（可靠性證據(jù)）程序（數(shù)學模型）驗證嚴格保證程序相對于其規(guī)約沒有bug我們的思路：基于程序驗證技術，構造“沒有bug”的軟件從最底層的系統(tǒng)軟件開始做起操作系統(tǒng)、編譯器等相對于規(guī)約操作系統(tǒng)內(nèi)核驗證硬件操作系統(tǒng)應用程序操作系統(tǒng)驗證：主要挑戰(zhàn)C和匯編代碼、指針操作代碼量：近萬行代碼多任務并發(fā)搶占式調(diào)度硬件中斷多模塊抽象級不同單個模塊的性質和系統(tǒng)整體性質兼顧搶占和中斷所產(chǎn)生的復雜并發(fā)導致操作系統(tǒng)驗證變得尤其困難！ 并發(fā)內(nèi)核驗證的挑戰(zhàn)并發(fā)程序的驗證相當困難并發(fā)程序間非確定的交錯執(zhí)行(Non-deterministic interleaving)我們的工作提出了一個用于搶占式操作系統(tǒng)內(nèi)核的驗證框架

5、支持并發(fā)內(nèi)核的驗證支持嵌套中斷和搶占實用操作系統(tǒng)內(nèi)核的驗證C/OS-IISpaceOS2Xu et al. CAV16C/OS-II內(nèi)核的驗證與相關工作的對比我們的工作報告提綱證什么性質：內(nèi)核“正確性”的刻畫如何證：并發(fā)操作系統(tǒng)內(nèi)核驗證框架內(nèi)核建模并發(fā)精化程序邏輯CSL-R自動證明策略我們對實際系統(tǒng)內(nèi)核的驗證報告提綱證什么性質：內(nèi)核“正確性”的刻畫如何證：并發(fā)操作系統(tǒng)內(nèi)核驗證框架內(nèi)核建模并發(fā)精化程序邏輯CSL-R自動證明策略我們對實際系統(tǒng)內(nèi)核的驗證操作系統(tǒng)驗證：正確性定義如何定義操作系統(tǒng)的功能正確性？操作系統(tǒng)的本質是為用戶提供抽象： 掩蓋底層細節(jié)，為用戶提供高層服務和編程接口操作系統(tǒng)正確性：

6、高抽象層和底層實現(xiàn)的一致性操作系統(tǒng)驗證是個精化驗證問題操作系統(tǒng)正確性：抽象層劃分高層語言系統(tǒng)API的高層抽象系統(tǒng)API的底層實現(xiàn)應用程序C + 抽象APIsC +內(nèi)嵌匯編底層語言API規(guī)約應用程序系統(tǒng)實現(xiàn)（代碼）操作系統(tǒng)驗證：程序精化驗證系統(tǒng)調(diào)用系統(tǒng)調(diào)用精化：底層行為是高層行為的子集即：底層不會產(chǎn)生高層沒有預料到的行為系統(tǒng)API上下文精化所有應用程序API規(guī)約系統(tǒng)實現(xiàn)（代碼）系統(tǒng)調(diào)用系統(tǒng)調(diào)用系統(tǒng)API操作系統(tǒng)內(nèi)核正確性：上下文精化從所有應用程序（上下文）的角度看，系統(tǒng)API調(diào)用的時候執(zhí)行具體的代碼實現(xiàn)和執(zhí)行抽象的規(guī)約相比，不會產(chǎn)生新的行為。操作系統(tǒng)內(nèi)核正確性：上下文精化ObsBeh(AO) O

7、bsBeh(AS)A.可觀察行為集合如I/O事件序列A：應用程序O：系統(tǒng)實現(xiàn)代碼S：API規(guī)約O S iffWell-formed(A) 上下文精化用來刻畫API的正確性但操作系統(tǒng)的正確性還包括其他方面：運行時服務的正確性，例如任務調(diào)度器 （后臺運行，不以API的形式暴露給上層）系統(tǒng)的整體性質， 如隔離性、安全性、實時性等并不能通過單個API的正確性來刻畫！運行時服務和系統(tǒng)整體性質的刻畫運行時服務：其行為體現(xiàn)在高層語言的語義上 （如多任務調(diào)度）通過精化進行驗證運行時服務和系統(tǒng)整體性質的刻畫系統(tǒng)整體性質：在高抽象層上描述成完整系統(tǒng)執(zhí)行路徑上的性質在高抽象層上證明，通過上下文精化確保性質在底層得到

8、保持報告提綱證什么性質：內(nèi)核“正確性”的刻畫如何證：并發(fā)操作系統(tǒng)內(nèi)核驗證框架內(nèi)核建模并發(fā)精化程序邏輯CSL-R自動證明策略我們對實際系統(tǒng)內(nèi)核的驗證操作系統(tǒng)內(nèi)核驗證框架B. 并發(fā)精化程序邏輯精化驗證框架A. 內(nèi)核建模C. 自動證明策略驗證目標高層語言系統(tǒng)API的高層抽象系統(tǒng)API的底層實現(xiàn)應用程序C + 抽象APIsC +內(nèi)嵌匯編底層語言操作系統(tǒng)內(nèi)核驗證框架B. 并發(fā)精化程序邏輯精化驗證框架A. 內(nèi)核建模C. 自動證明策略C語言子集匯編原語底層小步操作語義底層語言高層規(guī)范語言高層小步操作語義高層語言底層語言語法底層程序語言 L := C | 匯編原語 | 一個真實的C語言子集 C := whil

9、e e C | if e C1 else C2 | f(e) | e=e | e := &e | *e | ee | e.id | C語言操作語義為了反映中斷可以發(fā)生在任意兩個機器指令之間，C語言程序語句的執(zhí)行和表達式計算都必須是和機器指令相同的粒度。 （x + y）/ 2 采用和CompCertTSO 類似的小步操作語義 求出x的值；求出y的值；計算x+y的值；計算出（x+y）/2的值中斷處理程序： y = y + 2匯編代碼的抽象switchencrtexcrt H := C | S | H;H | . S := sched | (v) | end | S;S | S+S | 表示規(guī)范代碼

10、結束高層語言語法表示此時需要執(zhí)行任務調(diào)度，調(diào)度策略是規(guī)范的一部分表示對抽象內(nèi)核狀態(tài)一步轉換，V表示傳入該抽象規(guī)范的參數(shù)的值C語言子集高層規(guī)范語言一個系統(tǒng)API的例子ticks0; dly(ticks); sched+ticks 0) OS_ENTER_CRITICAL(); OS_EXIT_CRITICAL(); OS_Sched(); return;操作系統(tǒng)內(nèi)核驗證框架B. 并發(fā)精化程序邏輯精化驗證框架A. 內(nèi)核建模C. 自動證明策略C語言子集匯編原語底層小步操作語義底層語言高層規(guī)范語言高層小步操作語義高層語言并發(fā)精化程序邏輯CSL-R上下文精化關系并發(fā)精化程序邏輯CSL-R使用關系型程序邏

11、輯（ relational program logic ）Liang & Feng PLDI13 證明兩個程序間的模擬關系（simulation relation），通過程序模擬關系來得到上下文精化關系使用資源占有權轉移語義（ownership-transfer semantics）推理多級中斷 Feng et. al. PLDI08結合上述兩點設計并發(fā)分離邏輯風格的關系程序邏輯CSL-R（CSL-Style relational program logic）模擬技術證明精化關系callret底層 (AO):call, ret高層 (AS):eeSOA ：應用程序O ：系統(tǒng)實現(xiàn)代碼S：API規(guī)

12、范支持中斷和多任務的程序模擬關系callret底層 (AO):call, ret高層 (AS):ee中斷處理程序:其他任務:IRQiretswitchswitch?如何支持可組合的證明?SO支持中斷和多任務的程序模擬關系callret底層 (AO):call, ret高層 (AS):ee中斷處理程序:其他任務:IRQiretswitchswitchSO使用全局不變式“I” 抽象任務和中斷間不確定的交互行為支持中斷和多任務的程序模擬關系callret底層 (AO):call, ret高層 (AS):eeII環(huán)境的執(zhí)行IIII并發(fā)精化程序邏輯41操作系統(tǒng)內(nèi)核驗證框架高層規(guī)范語言C語言子集匯編原語底

13、層小步操作語義高層小步操作語義高層語言底層語言并發(fā)精化程序邏輯CSL-R上下文精化關系B. 并發(fā)精化程序邏輯精化驗證框架A. 內(nèi)核建模C. 自動證明策略斷言自動推導驗證條件自動生成領域專用求解器驗證步驟給出系統(tǒng)API的抽象規(guī)范定義一個系統(tǒng)API的例子ticks0; dly(ticks); sched+ticks 0) OS_ENTER_CRITICAL(); OS_EXIT_CRITICAL(); OS_Sched(); return;驗證步驟給出系統(tǒng)API的抽象規(guī)范定義API代碼和規(guī)范在定理輔助證明工具Coq中定義OSTimeGet函數(shù)在Coq中的編碼驗證步驟給出系統(tǒng)API的抽象規(guī)約定義AP

14、I代碼和規(guī)范在定理輔助證明工具Coq中定義使用程序邏輯規(guī)則證明代碼對抽象規(guī)約的精化OSTimeGet函數(shù)的驗證I p * |S| C q * |end| OSTimeGet函數(shù)的驗證I p * |S| C q * |end| 證明腳本：手工給出驗證步驟給出系統(tǒng)API的抽象規(guī)約定義API代碼和規(guī)范在定理輔助證明工具Coq中定義使用程序邏輯規(guī)則證明代碼對抽象規(guī)約的精化程序員手工給出交互式，手工為主，部分自動報告提綱證什么性質：內(nèi)核“正確性”的刻畫如何證：并發(fā)操作系統(tǒng)內(nèi)核驗證框架內(nèi)核建模并發(fā)精化程序邏輯CSL-R自動證明策略我們對實際系統(tǒng)內(nèi)核的驗證C/OS-IIC/OS-II 是一個商用的開源嵌入式

15、操作系統(tǒng)，已經(jīng)被廣泛移植到各種嵌入式處理器上并發(fā)多任務、搶占式實時調(diào)度、多級中斷、信號量、時鐘管理、消息隊列等文檔代碼規(guī)整，代碼約6600行驗證C/OS-IIC.自動證明輔助工具B.并發(fā)精化驗證技術A.操作系統(tǒng)內(nèi)核建模D.驗證C/OS-II的核心模塊多級中斷（時鐘中斷&）優(yōu)先級調(diào)度機制四種通信機制消息隊列互斥鎖信號量消息郵箱任務管理時鐘管理操作系統(tǒng)精化驗證框架常用接口：經(jīng)過驗證的覆蓋68%的常用API時鐘中斷任務創(chuàng)建和刪除信號量消息郵箱消息隊列互斥鎖時鐘管理搶占式調(diào)度操作系統(tǒng)內(nèi)核驗證框架高層規(guī)范語言C語言子集匯編原語底層小步操作語義高層小步操作語義高層機器模型底層機器模型并發(fā)精化程序邏輯CSL

16、-R上下文精化關系B. 并發(fā)精化程序邏輯精化驗證框架A. 內(nèi)核建模C. 自動證明策略斷言自動推導驗證條件自動生成領域專用求解器互斥信號量無優(yōu)先級反轉發(fā)現(xiàn)的主要Bug互斥鎖優(yōu)先級反轉的Bug使用一種簡化的priority ceiling算法互斥鎖嵌套使用的時候會導致優(yōu)先級反轉在C/OS-III中修復并發(fā)bug （原子性違背）會導致懸空指針訪問在C/OS-II v2.52 （我們驗證的版本）中發(fā)現(xiàn)在C/OS-II v2.9中修復INT8U OSTaskChangePrio (INT8U oldprio, INT8U newprio)Coq 實現(xiàn)CertiOSframeworkmachinesimulationlogictheorytacticscertiucoscodespecproofs55,00020,000225,000150,000本身是否可信？證明的正確性可自動檢查項目人力：6人年開發(fā)人員副研究員1名、博士生1名、碩士生6名、全職工程師1名60項目子內(nèi)容人力（人年）驗證平臺的設計和實現(xiàn)4圍繞消息隊列模塊展開驗證平臺的調(diào)試、驗證工具開發(fā)及調(diào)試、規(guī)范的定義（約750行C代碼）1其余5個功能模塊的驗證（約3000行代碼）1總計6驗證平臺和相關工具的的逐步成熟將大大減少操作系統(tǒng)驗證的人力成本！實施中案例驗證SpaceOS2嫦娥三號秘密武器:SpaceOS2中國航天科技集團公司五院