0 引言

    隨著物聯(lián)網(wǎng)技術(shù)的發(fā)展，物聯(lián)網(wǎng)設(shè)備安全性問題將是急需解決的核心問題之一。同時，在保障物聯(lián)網(wǎng)設(shè)備安全的所有措施中操作系統(tǒng)層面的安全是重中之重，從本質(zhì)上講，可以說物聯(lián)網(wǎng)操作系統(tǒng)的安全性直接決定了整個物聯(lián)網(wǎng)設(shè)備系統(tǒng)的可靠性。

    本文在上述背景下提出了一套行之有效的針對物聯(lián)網(wǎng)操作系統(tǒng)的安全性設(shè)計理論，目的是解決上述核心問題。

1 操作系統(tǒng)安全性

    傳統(tǒng)的操作系統(tǒng)設(shè)計方法主要依賴于人的以往經(jīng)驗和簡單的邏輯分析，因此無法從根本上保證操作系統(tǒng)設(shè)計的安全性和正確性。

    形式化方法的核心就是形式化語言，以及基于形式化語言構(gòu)建出來的形式化模型。其基礎(chǔ)思路是將高可靠性系統(tǒng)用語義明確的形式化語言進(jìn)行建模，采用模型檢測、定理證明的方法對系統(tǒng)目標(biāo)屬性進(jìn)行正確性推演和驗證。因此，采用該方法進(jìn)行操作系統(tǒng)的設(shè)計和驗證能夠保證操作系統(tǒng)的安全性和確定性^[1-2]。

2 操作系統(tǒng)形式化設(shè)計理論模型

    經(jīng)過大量的工程實踐比較與研究，本文提出了基于線性時態(tài)邏輯的操作系統(tǒng)形式化設(shè)計理論模型^[2]，如圖1所示。

    如圖1所示的設(shè)計方法由四部分組成：

    (1)一階數(shù)理邏輯+集合論建立頂層數(shù)理邏輯模型，該模型是原始需求的數(shù)學(xué)規(guī)格化描述，是進(jìn)一步設(shè)計求精和驗證的依據(jù)；

    (2)線性時態(tài)邏輯表達(dá)式,是時態(tài)邏輯的規(guī)格化描述；

    (3)針對并發(fā)體描述抽象的第二步線性時態(tài)邏輯規(guī)格化描述^[3]；

    (4)針對線性時態(tài)邏輯規(guī)格化描述的模型驗證^[3-5]。

3 基于Zephyr物聯(lián)網(wǎng)操作系統(tǒng)內(nèi)存管理核心功能的設(shè)計驗證案例

    下面結(jié)合圖1的模型以開源物聯(lián)網(wǎng)操作系統(tǒng)Zephyr的一個核心內(nèi)存管理功能為例，說明線性時態(tài)邏輯在操作系統(tǒng)內(nèi)核安全性、正確性設(shè)計中的具體應(yīng)用。

    本案例基于Zephyr內(nèi)存分配器功能進(jìn)行需求建模、設(shè)計求精和驗證。

3.1 頂層邏輯模型設(shè)計

    按照在圖1中描述的形式化方法，首先要對內(nèi)存分配需求進(jìn)行頂層邏輯建模。為了更好地兼容后面線性時態(tài)邏輯的求精和驗證，本文選用目前在業(yè)界成熟應(yīng)用的TLA+作為建模工具。頂層的邏輯模型首先考慮構(gòu)造一個四叉樹模型來表示內(nèi)存池，樹中的每一個節(jié)點代表一個內(nèi)存塊，每一層的大小一致，從根到葉子降序排列，允許多線程訪問。選用TLA+的Record+Function模型來表達(dá)這一概念，如圖2所示。

    圖2中k_mem_pool為一個record模型，max_sz是這顆四叉樹頂層最大內(nèi)存塊尺寸，levels是一個function用來表示樹的每一層擁有的空閑內(nèi)存塊，每一層空閑塊用集合來表達(dá)。

    下面考慮兩個基本概念：合適尺寸的內(nèi)存塊和裂解概念。合適尺寸內(nèi)存塊可以用數(shù)學(xué)概念表達(dá)，如圖3所示。

    對于內(nèi)存塊裂解概念，需要先考慮一個基本引理，即裂解過程需要一個基于樹的層次區(qū)間進(jìn)行，本文根據(jù)裂解層次的開始、結(jié)束和釋分配層級設(shè)計一套數(shù)學(xué)公式來表達(dá)這個裂解過程^[4]，如圖4所示。

    最后綜合上述分析過程，內(nèi)存分配的模型描述如圖5所示。

3.2 線性時態(tài)邏輯模型求精

    根據(jù)頂層邏輯模型的規(guī)格化描述，將公式里的OPERATOR進(jìn)一步展開成狀態(tài)流用時態(tài)邏輯進(jìn)行表達(dá)。這里提出一個技巧性原則：如需求描述涉及并發(fā)體訪問，則可以先考慮非并發(fā)模型的求精過程，之后再逐步加入針對并發(fā)體訪問邏輯的時序狀態(tài)描述。實踐證明這樣求精的效率非常高。非并發(fā)的時態(tài)邏輯求精如圖6所示。

    這樣可以基于上述非并發(fā)時態(tài)邏輯簡單增加一個如圖7所示的終止條件。

    對非并發(fā)體時態(tài)邏輯狀態(tài)機(jī)能正常終止驗證通過后，再增加圖8所示的并發(fā)體的時態(tài)邏輯。

3.3 時態(tài)屬性安全性驗證

    通過對頂層邏輯模型求精成線性時態(tài)邏輯公式，在時態(tài)邏輯層面就可以借助于TLA+的模型檢查器TLC進(jìn)行時態(tài)屬性驗證。求精到時態(tài)邏輯公式實際上有兩個目的：(1)求精之后的模型與底層的目標(biāo)代碼邏輯已經(jīng)非常接近，便于將驗證過的模型直接轉(zhuǎn)換成目標(biāo)代碼實現(xiàn)；(2)對時態(tài)邏輯模型，可以直接構(gòu)造時態(tài)屬性進(jìn)行模型檢查^[6-7]。下面來看上述時態(tài)邏輯模型的驗證思路，首先滿足非并發(fā)條件下單線程訪問程序最終能夠結(jié)束，即圖7所示的終結(jié)條件。

    屬性需要得到滿足，使用TLC模型檢查的配置及結(jié)果如圖9、圖10所示。

    在保證非并發(fā)單線程執(zhí)行模型正確后，開始在此基礎(chǔ)上增加對并發(fā)模型的屬性檢查，即所有并發(fā)體訪問都要保證能夠正常結(jié)束，不會發(fā)生死鎖、忙等、空等等非法狀態(tài)，需要滿足如圖11所示的終止條件。

    使用TLC模型檢查器的參數(shù)配置及檢查結(jié)果如圖12、圖13所示。

    由于時態(tài)模型在并發(fā)訪問層面上是具有歸納性質(zhì)的，因此這里選取10個線程集合進(jìn)行驗證即可。可以看到，上述模型檢查的結(jié)果驗證了時態(tài)邏輯模型對于多線程并發(fā)訪問是安全的（可以正常終止），此外從圖7公式分析單線程模型只有L4狀態(tài)，如圖14所示。

    由于該狀態(tài)涉及對全局變量k_mem_pool的修改，從代碼執(zhí)行性能角度可以考慮將L4狀態(tài)轉(zhuǎn)換成目標(biāo)代碼時加鎖，其他狀態(tài)模型轉(zhuǎn)換時不必加鎖，如果使用關(guān)開中斷來實現(xiàn)鎖可以保證并發(fā)性能最優(yōu)化^[2]。

3.4 時態(tài)屬性正確性驗證

    上面使用時態(tài)屬性進(jìn)行了軟件模型安全性驗證，最終的目標(biāo)是在安全性的基礎(chǔ)上讓設(shè)計模型滿足預(yù)期(即正確性)^[8]。對于四叉樹結(jié)構(gòu)，假設(shè)同時有N個線程在訪問這個分配器接口，由于分配器的模型本身具有歸納性質(zhì)，可以簡化正確性的驗證模型為N個線程同時從初始化四叉樹模型中申請大小相同的內(nèi)存塊所要滿足的預(yù)期屬性。該屬性的規(guī)格化描述如下：

    首先，初始化四叉樹模型如圖15所示。

    N個線程申請內(nèi)存塊大小如圖16所示。

    根據(jù)模型的歸納性質(zhì)將N設(shè)置為3，預(yù)期屬性如圖17所示。

    為了計算申請內(nèi)存塊在四叉樹上面裂解的層數(shù)和最終四叉樹裂解層所包含的空閑內(nèi)存塊數(shù)，引入兩個輔助操作函數(shù)進(jìn)行計算，如圖18所示。

    這樣就可以在TLC模型檢查器中增加正確性屬性進(jìn)行檢查，如圖19所示。

    遺憾的是如圖20所示的模型檢查沒有通過，證明模型設(shè)計存在問題，需要根據(jù)TLC反饋的錯誤進(jìn)行進(jìn)一步分析問題產(chǎn)生的原因。

    經(jīng)過對TLC Error的分析，這里面包括兩個關(guān)鍵錯誤原因：(1)四叉樹裂解過程中存在可以被其他線程所搶占的時間空隙，會導(dǎo)致內(nèi)存分配錯誤，從而產(chǎn)生時序狀態(tài)違例；(2)L3狀態(tài)的內(nèi)存分配可以被其他線程所搶占造成當(dāng)前線程內(nèi)存分配計算的free_l、alloc_l游標(biāo)與被搶占后的四叉樹模型不一致，從而導(dǎo)致內(nèi)存分配失敗產(chǎn)生時序違例。針對這兩種情況，考慮將L3、L4狀態(tài)進(jìn)一步優(yōu)化，如圖21和圖22所示。

    優(yōu)化后考慮將裂解過程中層間內(nèi)存塊提取的裂解操作合并成一個狀態(tài)成為一個原子操作，然后增加L4狀態(tài)下的判斷：如果裂解到當(dāng)前層為空而又不是alloc_l標(biāo)識的最后一層，則證明裂解過程中存在其他線程搶占情況，重新回到L1狀態(tài)重新計算內(nèi)存分配的格局游標(biāo)free_l和alloc_l，這樣就可以保證多線程搶占條件下內(nèi)存分配的正確性。為了防止TLC檢查發(fā)生stutterring，將時態(tài)修改為如圖23所示。

    再次進(jìn)行驗證，如圖24所示。

    圖24所示表示修正后的時態(tài)邏輯已經(jīng)通過正確性檢查?？梢灾苯邮褂抿炞C過的數(shù)學(xué)模型進(jìn)行目標(biāo)代碼編寫和測試。

    上述案例說明形式化方法可以從系統(tǒng)設(shè)計層面就能保證需求實現(xiàn)的完整性和設(shè)計模型的安全性、正確性。

4 結(jié)束語

    對于物聯(lián)網(wǎng)操作系統(tǒng)的需求概念模型設(shè)計與驗證使用線性時態(tài)邏輯來做是比較高效的選擇。使用本文提出的設(shè)計方法可以在頂層邏輯程序設(shè)計階段就將需求概念模型進(jìn)行精確描述，即使是錯誤的模型或在求精設(shè)計階段存在BUG，也可以通過時態(tài)邏輯的屬性驗證發(fā)現(xiàn)并進(jìn)行修改優(yōu)化。使用線性時態(tài)邏輯作為頂層邏輯模型的求精既保證了與頂層需求模型的一致性，又保證了求精模型可以在實現(xiàn)層面很容易向目標(biāo)代碼轉(zhuǎn)換。這部分雖然只能做到部分形式化，但是只需經(jīng)過簡單的目標(biāo)測試就可以完成產(chǎn)品目標(biāo)代碼最終的驗證工作。

    本文提出的理論方法對于其他對安全性和可靠性要求較高的軟件設(shè)計領(lǐng)域也具有極高的參考價值。

參考文獻(xiàn)

[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] 朱峰，魯征浩，朱青.形式化驗證在處理器浮點運算單元中的應(yīng)用[J].電子技術(shù)應(yīng)用，2017，43(2)：29-32.

[4] ROSEN K H.離散數(shù)學(xué)及其應(yīng)用(原書第七版)[M].徐六通，楊娟，吳斌，譯.北京：機(jī)械工業(yè)出版社，2017.

[5] 張杰，王少超，關(guān)永.基于形式化方法的有限域乘法器的建模與驗證[J].電子技術(shù)應(yīng)用，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].電子技術(shù)應(yīng)用，2016，42(2)：14-16.

[8] NIPKOW T，PAULSON L C，WENZEL M.高階邏輯輔助證明系統(tǒng)[M].陳光喜，劉卓軍，譯.北京：北京理工大學(xué)出版社，2013.

作者信息：

張華強(qiáng)，李凱航，王繼剛

(中興通訊成都研發(fā)中心，四川 成都610041)