基于時(shí)間自動(dòng)機(jī)的操作系統(tǒng)中斷管理建模與驗(yàn)證*

王若川，楊孟飛，2，喬 磊

(1.北京控制工程研究所，北京100190;2.中國空間技術(shù)研究院，北京100094)

0 引言

操作系統(tǒng)在整個(gè)計(jì)算機(jī)軟件體系中的重要性不言而喻.傳統(tǒng)的測(cè)試技術(shù)難以保證此類復(fù)雜系統(tǒng)的設(shè)計(jì)完全正確.完全地形式化驗(yàn)證是已知的、并且唯一的能保證整個(gè)系統(tǒng)遠(yuǎn)離程序設(shè)計(jì)錯(cuò)誤的方法［1］.

國內(nèi)外學(xué)者很早就開始研究如何運(yùn)用形式化的方法來驗(yàn)證操作系統(tǒng)行為的正確性.例如Walker等提出的安全內(nèi)核［2］，Bevier對(duì)操作系統(tǒng)內(nèi)核形式化模型的研究［3］，Horning等在操作系統(tǒng)形式化規(guī)約方面做了有益的探討［4］.如果模型建的足夠精確，確實(shí)可以很好地證明系統(tǒng)的可靠性.但是隨著軟件規(guī)模急劇膨脹，這常常是很難實(shí)現(xiàn)的.

通用的解決辦法是優(yōu)化代碼結(jié)構(gòu)，降低代碼規(guī)模，從而降低錯(cuò)誤出現(xiàn)的概率.以此為主要?jiǎng)訖C(jī)，出現(xiàn)了許多新概念與新技術(shù)，如安全內(nèi)核與分離內(nèi)核［5］、MILS 方法［6］、微內(nèi)核［7］、以及隔離內(nèi)核［8］等，包括CC(common criteria)［9］標(biāo)準(zhǔn)中的最高評(píng)價(jià)等級(jí)也要求待評(píng)價(jià)系統(tǒng)采用精簡(jiǎn)的設(shè)計(jì).

針對(duì)一個(gè)真正的微內(nèi)核，可以更好地保證其安全性和魯棒性，從這一點(diǎn)上來說，有可能避免程序錯(cuò)誤的出現(xiàn)［10］.澳大利亞的 Gerwin 等［1］對(duì) SeL4微內(nèi)核從頂層的抽象規(guī)約到低層的C實(shí)現(xiàn)，進(jìn)行了完整的形式化驗(yàn)證，這是第一個(gè)對(duì)通用操作系統(tǒng)內(nèi)核進(jìn)行的完整的功能正確性形式化驗(yàn)證，確保了低層實(shí)現(xiàn)總是嚴(yán)格遵照內(nèi)核行為的高層抽象規(guī)約，內(nèi)核永遠(yuǎn)不會(huì)崩潰，也不會(huì)出現(xiàn)一些不安全的行為.

同上述關(guān)于操作系統(tǒng)形式化驗(yàn)證的研究成果相比，本文更關(guān)注動(dòng)態(tài)時(shí)序正確性驗(yàn)證.使用時(shí)間自動(dòng)機(jī)建模，使多任務(wù)能直觀地在系統(tǒng)內(nèi)執(zhí)行.這是考慮到在實(shí)際工程應(yīng)用中有很多嚴(yán)格的時(shí)間約束，從時(shí)序的角度對(duì)系統(tǒng)進(jìn)行形式化建模與驗(yàn)證是很有必要的.

本文第1節(jié)簡(jiǎn)要分析某星載操作系統(tǒng)［11］中斷管理特點(diǎn)，并提出驗(yàn)證模型;第2節(jié)給出基于時(shí)間自動(dòng)機(jī)的具體建模過程;第3節(jié)結(jié)合具體例子描述如何基于以上模型進(jìn)行行為正確性驗(yàn)證;第4節(jié)總結(jié)全文，討論可以改進(jìn)和優(yōu)化的方向.

1 中斷管理模型

1.1 中斷管理特點(diǎn)

中斷管理流程如圖1所示，具有以下3個(gè)特點(diǎn):

1)中斷管理支持中斷嵌套，在執(zhí)行中斷服務(wù)程序過程中允許更高級(jí)別的中斷打斷當(dāng)前任務(wù);

2)從中斷服務(wù)程序返回之后首先判斷是不是最外層中斷，結(jié)果為假則進(jìn)行中斷上下文恢復(fù)，繼而返回到更外一層的中斷程序中去.結(jié)果為真則進(jìn)行中斷級(jí)的任務(wù)調(diào)度;

3)中斷級(jí)的任務(wù)調(diào)度主要進(jìn)行兩個(gè)判斷:就緒態(tài)任務(wù)的最高優(yōu)先級(jí)是否大于當(dāng)前運(yùn)行任務(wù)的優(yōu)先級(jí)，當(dāng)前運(yùn)行任務(wù)的時(shí)間片是否已經(jīng)用完.若有任意一個(gè)判斷結(jié)果為真，則進(jìn)行任務(wù)的上下文切換.若兩個(gè)判斷結(jié)果都為假，則進(jìn)行正常的中斷上下文恢復(fù).

1.2 對(duì)象實(shí)體

由圖1可以看出，中斷管理與一組硬件設(shè)備相關(guān)，本文將它們抽象為4類對(duì)象實(shí)體，分別是:CPU、中斷控制器、中斷請(qǐng)求源和存儲(chǔ)設(shè)備.

1.3 服務(wù)行為

上文已經(jīng)抽象出了中斷管理模塊涉及的對(duì)象實(shí)體，側(cè)重描述了該模塊的靜態(tài)屬性.下面將中斷管理的動(dòng)態(tài)屬性抽象為4個(gè)服務(wù)行為，它們分別是:中斷上下文保護(hù)行為、執(zhí)行中斷服務(wù)程序行為、中斷級(jí)任務(wù)調(diào)度行為、中斷上下文恢復(fù)行為.

圖1 中斷管理流程圖Fig.1 Flow diagram of interrupt management

值得注意的是，所有的對(duì)象實(shí)體都是獨(dú)立于中斷管理的服務(wù)而存在的，中斷管理服務(wù)的能力體現(xiàn)在與對(duì)象實(shí)體的交互，使對(duì)象實(shí)體的狀態(tài)發(fā)生改變.一種中斷管理服務(wù)總是與特定的對(duì)象實(shí)體集交互完成的.

1.4 中斷管理驗(yàn)證模型

基于以上的分析，進(jìn)一步提出中斷管理驗(yàn)證模型，如圖2所示.

圖2 中斷管理驗(yàn)證模型Fig.2 Verification model of interrupt management

2 基于時(shí)間自動(dòng)機(jī)的建模過程

2.1 時(shí)間自動(dòng)機(jī)

由Alur和Dill所提出的時(shí)間自動(dòng)機(jī)［12］是一種對(duì)實(shí)時(shí)系統(tǒng)行為建模的工具，它是一種簡(jiǎn)單的、卻強(qiáng)有力的描述方式.定義為一個(gè)有窮定向圖，由一組可被重置的非負(fù)實(shí)值時(shí)鐘和時(shí)間約束所標(biāo)注.特定的時(shí)間自動(dòng)機(jī)接收特定的時(shí)間字.下面給出本文使用的時(shí)間自動(dòng)機(jī)定義.

定義1.一個(gè)時(shí)間自動(dòng)機(jī)(TA，timed automata)是一個(gè)六元組(L，l0，C，A，E，I)，其中 L是位置的集合，l0∈L是初始位置，C是時(shí)鐘變量集，A是動(dòng)作集，包括自動(dòng)機(jī)內(nèi)部動(dòng)作及自動(dòng)機(jī)間動(dòng)作，E?L×A×Φ(C)×2C×L是邊集，由位置、動(dòng)作、保衛(wèi)公式、需要被重置的時(shí)鐘變量集所組成，I:L→Φ(C)，將一個(gè)位置映射為一個(gè)保衛(wèi)公式，稱為狀態(tài)的不變量(invariant).

定義2.假設(shè)有n個(gè)時(shí)間自動(dòng)機(jī)TA1，…，TAn，其中給定任意自然數(shù)i，對(duì) 1≤i≤n，TAi=(Li，li0，Ci，Ai，Ei，Ii)，由這n個(gè)時(shí)間自動(dòng)機(jī)構(gòu)成的網(wǎng)絡(luò)記為N=TA1||TA2|| … ||TAn.格局(configuration)是用來描述網(wǎng)絡(luò)中所有自動(dòng)機(jī)運(yùn)行時(shí)的狀態(tài)(全局狀態(tài))的概念.

2.2 對(duì)象實(shí)體建模

對(duì)象實(shí)體的形式化描述如下:

定義3.一個(gè)對(duì)象實(shí)體類為T=＜Tid，A，O，M＞，其中Tid為對(duì)象實(shí)體類的標(biāo)識(shí)符;A為對(duì)象實(shí)體屬性的集合;O為對(duì)象實(shí)體操作的集合;M表示從屬性集合到各個(gè)數(shù)據(jù)類型的一個(gè)映射，數(shù)據(jù)類型包括基本數(shù)據(jù)類型如Int、Boolean、Float等，也包括用戶自己定義的類型.將所有對(duì)象實(shí)體類的集合記為TOE，對(duì)于任意的T∈TOE，T.A表示類型T的所有屬性，T.O表示類型T的所有動(dòng)作.

在對(duì)象實(shí)體類的基礎(chǔ)上，可以創(chuàng)建具體的對(duì)象實(shí)體.

定義4.一個(gè)對(duì)象實(shí)體為三元組t=＜tid，T，TA＞，其中tid為該對(duì)象實(shí)體唯一標(biāo)識(shí)符;T∈TOE表示該對(duì)象實(shí)體所屬的對(duì)象實(shí)體類;TA=(L，l0，C，A，E，I)為符合定義1的時(shí)間自動(dòng)機(jī)，用于描述環(huán)境實(shí)體的動(dòng)態(tài)行為.

根據(jù)上述定義所得到的對(duì)象實(shí)體和對(duì)象實(shí)體類就構(gòu)成了中斷管理驗(yàn)證模型中的對(duì)象實(shí)體庫.采用時(shí)間自動(dòng)機(jī)，一個(gè)屬于存儲(chǔ)設(shè)備類的對(duì)象實(shí)體可表示為如圖3所示.

圖3 存儲(chǔ)設(shè)備時(shí)間自動(dòng)機(jī)描述Fig.3 Timed automata of memory

2.3 服務(wù)行為建模

服務(wù)行為的形式化描述如下:

定義5.一個(gè)服務(wù)行為可形式化地表示為一個(gè)三元組＜Sid，Eset，STA＞，其中Sid為該行為的唯一標(biāo)識(shí)符;Eset?TOE表示與該行為有交互的對(duì)象實(shí)體類的集合;STA為一個(gè)時(shí)間自動(dòng)機(jī)，用于描述行為的動(dòng)態(tài)特征.

例如，中斷上下文保護(hù)行為可表示為＜IProtect，{EMemory，EInterruptController}，SIP＞，其中SIP如圖4所示.

圖4 中斷上下文保護(hù)行為時(shí)間自動(dòng)機(jī)描述Fig.4 Timed automata of context protection behavior

2.4 環(huán)境建模

定義6.假設(shè)一個(gè) OS行為S= ＜Sid，Eset，STA＞，環(huán)境實(shí)體集合Env=∪n i=1＜i，Ti，ETAi＞ 稱為S的一個(gè)環(huán)境，若滿足對(duì)于任意T∈Eset，存在1≤i≤n使Ti=T，即對(duì)于服務(wù)中的每個(gè)對(duì)象實(shí)體類，在環(huán)境中都至少存在該類的一個(gè)實(shí)例化對(duì)象實(shí)體.行為S與它的環(huán)境Env之間的交互用時(shí)間自動(dòng)機(jī)網(wǎng)絡(luò)STA||ETA1||…||ETAn來表示.

到目前為止，OS行為與它對(duì)應(yīng)的運(yùn)行環(huán)境已經(jīng)完全建模為時(shí)間自動(dòng)機(jī)網(wǎng)絡(luò)，對(duì)行為的正確性驗(yàn)證實(shí)際上轉(zhuǎn)化成了對(duì)相應(yīng)時(shí)間自動(dòng)機(jī)網(wǎng)絡(luò)的分析.

3 中斷管理驗(yàn)證

下面以一個(gè)具體的行為以及與該行為相關(guān)的兩個(gè)實(shí)體為例來說明驗(yàn)證過程，將中斷管理模塊行為的時(shí)序正確性分解為以下3類性質(zhì):

1)可達(dá)性(reachability)，即考察是否存在一條從初始狀態(tài)開始的路徑，沿著這條路徑最終φ被滿足.在Uppaal中書寫該條性質(zhì)的語法為E＜＞φ.

2)安全性(safety)，即不好的事情永遠(yuǎn)不會(huì)發(fā)生.在Uppaal中記為A［］φ，A表示在所有可達(dá)的狀態(tài)中φ都是真的.例如在任何情況下，都不希望操作系統(tǒng)發(fā)生死鎖.

3)活性(liveness)，即某件事最終是會(huì)發(fā)生的.常用的一種形式是“導(dǎo)致”或者“反應(yīng)”，記為φ→Φ，意思是任何時(shí)候只要φ被滿足，那么最終Φ將會(huì)被滿足.在Uppaal記作φ→Φ.例如一個(gè)中斷產(chǎn)生以后，最終是會(huì)被響應(yīng)的，而不會(huì)被無限期地?cái)R置.下面是具體的例子.

中斷上下文保護(hù)行為發(fā)生在新中斷到來的時(shí)候，它與存儲(chǔ)設(shè)備和中斷控制器兩個(gè)實(shí)體相交互.存儲(chǔ)設(shè)備和上下文保護(hù)行為的自動(dòng)機(jī)分別見圖3和圖4，圖5是中斷控制器的自動(dòng)機(jī)模型.

中斷控制器的時(shí)間自動(dòng)機(jī)帶有一個(gè)形式參數(shù)，用來表示該自動(dòng)機(jī)描述的中斷等級(jí)，這里假設(shè)一共有三級(jí)中斷，第三級(jí)的優(yōu)先級(jí)最高.

對(duì)中斷管理的正確性驗(yàn)證需要將行為和相關(guān)的環(huán)境組合成一個(gè)整體系統(tǒng):

首先要驗(yàn)證的性質(zhì)是在任何情況下，都不希望系統(tǒng)出現(xiàn)死鎖，驗(yàn)證輸入邏輯公式為:A［］not deadlock，驗(yàn)證通過.

圖5 中斷控制器時(shí)間自動(dòng)機(jī)描述Fig.5 Timed automata of interrupt controller

其次驗(yàn)證系統(tǒng)一些比較重要的狀態(tài)可達(dá)性.這里舉其中一例說明，輸入公式為:E＜＞InterruptProtect.Can_not_be_interrupted，表示關(guān)中斷以后的狀態(tài)是可以達(dá)到的，驗(yàn)證通過.其余可達(dá)性同理均驗(yàn)證通過.

再次是安全性驗(yàn)證，輸入公式為:A［］Interrupt-Controller1.S2+InterruptController2.S2+Interrupt-Controller3.S2＜=1，意思是任何情況下只能保存一個(gè)中斷的現(xiàn)場(chǎng)，不可能出現(xiàn)關(guān)中斷后有兩個(gè)或以上中斷需要被保存的情況，驗(yàn)證通過.

最后驗(yàn)證活性，輸入公式為:Curlevel==3--＞ not InterruptController1.S2 Curlevel==3-- ＞not InterruptController2.S2表示的意思是如果當(dāng)前是第三級(jí)中斷搶占了CPU資源，那么低級(jí)中斷無法打斷高級(jí)中斷的執(zhí)行，驗(yàn)證通過.

部分性質(zhì)的驗(yàn)證結(jié)果如圖6所示.同理可以驗(yàn)證中斷管理其他行為的時(shí)序正確性，從而說明，該模塊滿足設(shè)計(jì)需求.

由于涉及到多個(gè)時(shí)間自動(dòng)機(jī)的聯(lián)動(dòng)，使?fàn)顟B(tài)空間爆炸問題更加突出.下一步工作的重點(diǎn)是使用偏序技術(shù)［13-14］來約簡(jiǎn)時(shí)間自動(dòng)機(jī)的狀態(tài)空間，使其能盡可能的精簡(jiǎn)，從而提高正確性驗(yàn)證的效率.

圖6 性質(zhì)驗(yàn)證結(jié)果Fig.6 Verification results

4 結(jié)論

本文在分析某嵌入式操作系統(tǒng)中斷管理模塊的基礎(chǔ)上，著眼于時(shí)序特性，提出了一套形式化建模與驗(yàn)證方法:提取出不同的對(duì)象實(shí)體和系統(tǒng)行為，并且運(yùn)用時(shí)間自動(dòng)機(jī)理論對(duì)它們分別建模，將它們之間的相互作用關(guān)系轉(zhuǎn)化為時(shí)間自動(dòng)機(jī)網(wǎng)絡(luò)的描述.同時(shí)將需要驗(yàn)證的一系列時(shí)序性質(zhì)使用形式化方法表示，并輸入到該時(shí)間自動(dòng)機(jī)網(wǎng)絡(luò)中，利用模型檢測(cè)工具箱Uppaal驗(yàn)證了這些性質(zhì)，證明了其服務(wù)行為的正確性.

［1］GERWIN K，JUNE A，KEVIN E，et al.SeL4:formal verification of an OS kernel［J］.Communications of the ACM，2010，53(6):107-115.

［2］WALKER B，KEMMERER R，POPEK L.Specification and verification of the UCLA unix security kernel［J］.Communications of the ACM，1980，23(2):18-131.

［3］BEVIER W.A verified operating system kernel［D］.Austin:University of Texas，1987.

［4］BIRRELL A，GUTTAG J，HORNING J，et al.Synchronization primitives for a multiprocessor:a formal specification［R］.New York:Gilles，1987.

［5］U.S.Government protection profile for separation kernels in environments requiring high robustness［R］.Washington D.C.:Information Assurance Directorate，2007.

［6］ALVES J，OMAN P，TAYLOR C，et al.The MILS architecture for high-assurance embedded systems［J］.International Journal of Embedded Systems，2006(2):239-247.

［7］HOHMUTH M，PETER M，H¨ARTIG H，et al.Reducing TCB size by using untrusted components—small kernels versus virtual-machine monitors［C］∥Proceedings of the 11thACM SIGOPS European Workshop.Belgium:Leuven，2004:53-79.

［8］WHITAKER A，GRIBBLE S.Scale and performance in the Denali isolation kernel［C］∥Proceedings of the 5thSymposium on Operating Systems Design and Implementation.Boston:Godefroid，2002:195-210.

［9］The National Security Agency.ISO/IEC 15408 common criteria for information technology security evaluation［S］.Gaithersburg:the National Institute of Standards and Technology(NIST)，2009:32-38.

［10］ELPHINSTONE K，KLEIN G，DERRIN P，et al.Towards a practical，verified kernel［J］.International 11thWorkshop on Hot Topics in Operating Systems，2007，75(3):117-122.

［11］QIAO L，GU B，YANG H，et al.An embedded operating system design for the lunar exploration rover CPS［J］.The First International Workshop on Safety and Security in Cyber-Physic-al Systems，2011(6):88-101.

［12］ALUR R，DILL D.A theory of timed automata［J］.Theoretical Computer Science，1994，126:183-235.

［13］BENGTSSON J，JONSSON B，LILIUS J.Partial order reductions for timed systems［C］∥Proceedings of the 9thInternational Conference on Concurrency Theory(CONCUR98).Netherlands:Zindhoven，1998:485-500.

［14］MINES M.Partial order reduction for modeling checking of timed automata［C］∥Proceedings of the 10thInternational Conference on Concurrency Theory(CONCUR99).Netherlands:Zindhoven，1999:431-446.