隨著物聯網技術的發展，物聯網設備安全性問題將是急需解決的核心問題之一。同時，在保障物聯網設備安全的所有措施中作業系統層面的安全是重中之重，從本質上講，可以說物聯網作業系統的安全性直接決定了整個物聯網設備系統的可靠性。
本文在上述背景下提出了一套行之有效的針對物聯網作業系統的理論，目的是解決上述核心問題。
1 作業系統安全性
傳統的作業系統設計方法主要依賴於人的以往經驗和簡單的邏輯分析，因此無法從根本上保證作業系統設計的安全性和正確性。
形式化方法的核心就是形式化語言，以及基於形式化語言構建出來的形式化模型。其基礎思路是將高可靠性系統用語義明確的形式化語言進行建模，採用模型檢測、定理證明的方法對系統目標屬性進行正確性推演和驗證。因此，採用該方法進行作業系統的設計和驗證能夠保證作業系統的安全性和確定性[1-2]。
2 作業系統形式化設計理論模型
經過大量的工程實踐比較與研究，本文提出了基於線性時態邏輯的作業系統形式化設計理論模型[2]，如圖1所示。
如圖1所示的設計方法由四部分組成：
(1)一階數理邏輯+集合論建立頂層數理邏輯模型，該模型是原始需求的數學規格化描述，是進一步設計求精和驗證的依據；
(2)線性時態邏輯表達式,是時態邏輯的規格化描述；
(3)針對並發體描述抽象的第二步線性時態邏輯規格化描述[3]；
(4)針對線性時態邏輯規格化描述的模型驗證[3-5]。
3 基於Zephyr物聯網作業系統內存管理核心功能的設計驗證案例
下面結合圖1的模型以開源物聯網作業系統Zephyr的一個核心內存管理功能為例，說明線性時態邏輯在作業系統內核安全性、正確性設計中的具體應用。
本案例基於Zephyr內存分配器功能進行需求建模、設計求精和驗證。
3.1 頂層邏輯模型設計
按照在圖1中描述的形式化方法，首先要對內存分配需求進行頂層邏輯建模。為了更好地兼容後面線性時態邏輯的求精和驗證，本文選用目前在業界成熟應用的TLA+作為建模工具。頂層的邏輯模型首先考慮構造一個四叉樹模型來表示內存池，樹中的每一個節點代表一個內存塊，每一層的大小一致，從根到葉子降序排列，允許多線程訪問。選用TLA+的Record+Function模型來表達這一概念，如圖2所示。
圖2中k_mem_pool為一個record模型，max_sz是這顆四叉樹頂層最大內存塊尺寸，levels是一個function用來表示樹的每一層擁有的空閒內存塊，每一層空閒塊用集合來表達。
下面考慮兩個基本概念：合適尺寸的內存塊和裂解概念。合適尺寸內存塊可以用數學概念表達，如圖3所示。
對於內存塊裂解概念，需要先考慮一個基本引理，即裂解過程需要一個基於樹的層次區間進行，本文根據裂解層次的開始、結束和釋分配層級設計一套數學公式來表達這個裂解過程[4]，如圖4所示。
最後綜合上述分析過程，內存分配的模型描述如圖5所示。
3.2 線性時態邏輯模型求精
根據頂層邏輯模型的規格化描述，將公式里的OPERATOR進一步展開成狀態流用時態邏輯進行表達。這裡提出一個技巧性原則：如需求描述涉及並發體訪問，則可以先考慮非並發模型的求精過程，之後再逐步加入針對並發體訪問邏輯的時序狀態描述。實踐證明這樣求精的效率非常高。非並發的時態邏輯求精如圖6所示。
這樣可以基於上述非並發時態邏輯簡單增加一個如圖7所示的終止條件。
對非並發體時態邏輯狀態機能正常終止驗證通過後，再增加圖8所示的並發體的時態邏輯。
3.3 時態屬性安全性驗證
通過對頂層邏輯模型求精成線性時態邏輯公式，在時態邏輯層面就可以藉助於TLA+的模型檢查器TLC進行時態屬性驗證。求精到時態邏輯公式實際上有兩個目的：(1)求精之後的模型與底層的目標代碼邏輯已經非常接近，便於將驗證過的模型直接轉換成目標代碼實現；(2)對時態邏輯模型，可以直接構造時態屬性進行模型檢查[6-7]。下面來看上述時態邏輯模型的驗證思路，首先滿足非並發條件下單線程訪問程序最終能夠結束，即圖7所示的終結條件。
屬性需要得到滿足，使用TLC模型檢查的配置及結果如圖9、圖10所示。
在保證非並發單線程執行模型正確後，開始在此基礎上增加對並發模型的屬性檢查，即所有並發體訪問都要保證能夠正常結束，不會發生死鎖、忙等、空等等非法狀態，需要滿足如圖11所示的終止條件。
使用TLC模型檢查器的參數配置及檢查結果如圖12、圖13所示。
由於時態模型在並發訪問層面上是具有歸納性質的，因此這裡選取10個線程集合進行驗證即可。可以看到，上述模型檢查的結果驗證了時態邏輯模型對於多線程並發訪問是安全的（可以正常終止），此外從圖7公式分析單線程模型只有L4狀態，如圖14所示。
由於該狀態涉及對全局變量k_mem_pool的修改，從代碼執行性能角度可以考慮將L4狀態轉換成目標代碼時加鎖，其他狀態模型轉換時不必加鎖，如果使用關開中斷來實現鎖可以保證並發性能最優化[2]。
3.4 時態屬性正確性驗證
上面使用時態屬性進行了軟體模型安全性驗證，最終的目標是在安全性的基礎上讓設計模型滿足預期(即正確性)[8]。對於四叉樹結構，假設同時有N個線程在訪問這個分配器接口，由於分配器的模型本身具有歸納性質，可以簡化正確性的驗證模型為N個線程同時從初始化四叉樹模型中申請大小相同的內存塊所要滿足的預期屬性。該屬性的規格化描述如下：
首先，初始化四叉樹模型如圖15所示。
N個線程申請內存塊大小如圖16所示。
根據模型的歸納性質將N設置為3，預期屬性如圖17所示。
為了計算申請內存塊在四叉樹上面裂解的層數和最終四叉樹裂解層所包含的空閒內存塊數，引入兩個輔助操作函數進行計算，如圖18所示。
這樣就可以在TLC模型檢查器中增加正確性屬性進行檢查，如圖19所示。
遺憾的是如圖20所示的模型檢查沒有通過，證明模型設計存在問題，需要根據TLC反饋的錯誤進行進一步分析問題產生的原因。
經過對TLC Error的分析，這裡面包括兩個關鍵錯誤原因：(1)四叉樹裂解過程中存在可以被其他線程所搶占的時間空隙，會導致內存分配錯誤，從而產生時序狀態違例；(2)L3狀態的內存分配可以被其他線程所搶占造成當前線程內存分配計算的free_l、alloc_l游標與被搶占後的四叉樹模型不一致，從而導致內存分配失敗產生時序違例。針對這兩種情況，考慮將L3、L4狀態進一步優化，如圖21和圖22所示。
優化後考慮將裂解過程中層間內存塊提取的裂解操作合併成一個狀態成為一個原子操作，然後增加L4狀態下的判斷：如果裂解到當前層為空而又不是alloc_l標識的最後一層，則證明裂解過程中存在其他線程搶占情況，重新回到L1狀態重新計算內存分配的格局游標free_l和alloc_l，這樣就可以保證多線程搶占條件下內存分配的正確性。為了防止TLC檢查發生stutterring，將時態修改為如圖23所示。
再次進行驗證，如圖24所示。
圖24所示表示修正後的時態邏輯已經通過正確性檢查。可以直接使用驗證過的數學模型進行目標代碼編寫和測試。
上述案例說明形式化方法可以從系統設計層面就能保證需求實現的完整性和設計模型的安全性、正確性。
4 結束語
對於物聯網作業系統的需求概念模型設計與驗證使用線性時態邏輯來做是比較高效的選擇。使用本文提出的設計方法可以在頂層邏輯程序設計階段就將需求概念模型進行精確描述，即使是錯誤的模型或在求精設計階段存在BUG，也可以通過時態邏輯的屬性驗證發現並進行修改優化。使用線性時態邏輯作為頂層邏輯模型的求精既保證了與頂層需求模型的一致性，又保證了求精模型可以在實現層面很容易向目標代碼轉換。這部分雖然只能做到部分形式化，但是只需經過簡單的目標測試就可以完成產品目標代碼最終的驗證工作。
本文提出的理論方法對於其他對安全性和可靠性要求較高的軟體設計領域也具有極高的參考價值。
參考文獻
[1] LAMPORT L.Specifying systems[M].Boston：Pearson Education，Inc.，2002.
[2] ABELSON H，SUSSMAN G J，SUSSMAN J.Structure and interpretation of computer programs[M].Cambridge，Massachusetts London，England：The MIT Press，1996.
[3] 朱峰，魯征浩，朱青.形式化驗證在處理器浮點運算單元中的應用[J].電子技術應用，2017，43(2)：29-32.
[4] ROSEN K H.離散數學及其應用(原書第七版)[M].徐六通，楊娟，吳斌，譯.北京：機械工業出版社，2017.
[5] 張杰，王少超，關永.基於形式化方法的有限域乘法器的建模與驗證[J].電子技術應用，2018，44(1)：109-113.
[6] Yu Yuan，MANOLIOS P，LAMPORT L.Model checking TLA+ specifications[C].Lecture Notes in Computer Science，Number 1703，Springer-Verlag，1999：54-66.
[7] 賀江，蒲宇亮，李海波，等.一種基於OpenCL的高能效並行KNN算法及其GPU驗證[J].電子技術應用，2016，42(2)：14-16.
[8] NIPKOW T，PAULSON L C，WENZEL M.高階邏輯輔助證明系統[M].陳光喜，劉卓軍，譯.北京：北京理工大學出版社，2013.
作者信息：
張華強，李凱航，王繼剛
(中興通訊成都研發中心，四川 成都610041)