0 引言

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

3.3 時(shí)態(tài)屬性安全性驗(yàn)證

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

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

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

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

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

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

3.4 時(shí)態(tài)屬性正確性驗(yàn)證

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

    首先,，初始化四叉樹(shù)模型如圖15所示,。

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

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

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

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

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

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

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

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

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

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

4 結(jié)束語(yǔ)

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

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

參考文獻(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àn)證在處理器浮點(diǎn)運(yùn)算單元中的應(yīng)用[J].電子技術(shù)應(yīng)用,，2017，43(2)：29-32.

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

[5] 張杰,，王少超，關(guān)永.基于形式化方法的有限域乘法器的建模與驗(yà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驗(yàn)證[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)