《計(jì)算機(jī)系統(tǒng)安全》課件第5章

第5章安全模型的構(gòu)建5.1建模的方法步驟5.2模型構(gòu)建實(shí)例習(xí)題

5.1建模的方法步驟

利用訪問矩陣—監(jiān)控器安全模型證明(或說明)系統(tǒng)的安全性，需要在模型中定義或證明以下內(nèi)容：

(1)分析系統(tǒng)的安全需求，確定系統(tǒng)的安全策略，并給出其形式化描述。(2)根據(jù)安全策略定義系統(tǒng)的安全狀態(tài)，主要是確定訪問矩陣中的內(nèi)容，包括主體、客體的安全屬性、訪問關(guān)系與訪問權(quán)限等內(nèi)容。

(3)定義安全狀態(tài)不變式，它表明在安全狀態(tài)中，狀態(tài)變量值之間必須保持的關(guān)系。

(4)定義狀態(tài)轉(zhuǎn)換函數(shù)(或稱操作命令)，它描述了因安全狀態(tài)變量的值發(fā)生變化而引起系統(tǒng)安全狀態(tài)的變化。(5)證明轉(zhuǎn)換函數(shù)能夠維持系統(tǒng)安全狀態(tài)，即證明轉(zhuǎn)換函數(shù)在執(zhí)行前與執(zhí)行后，系統(tǒng)都處于安全狀態(tài)。為了確保維持系統(tǒng)的安全狀態(tài)，常常需要對轉(zhuǎn)換函數(shù)增加約束條件。

(6)用安全狀態(tài)的定義證明初始狀態(tài)是安全的。5.2模型構(gòu)建實(shí)例5.2.1安全策略的描述不失一般性，在我們所研究的模型中，假定訪問的對象是文件，對這些對象的自主訪問控制策略都體現(xiàn)在訪問矩陣中。我們可以把其中的主要控制策略歸納為以下幾條(自然語言表述)：

策略(a)：只有當(dāng)某用戶對某文件有訪問關(guān)系時(shí)，該用戶才能按規(guī)定的訪問權(quán)對該文件進(jìn)行訪問。策略(b)：只有系統(tǒng)管理員才能夠創(chuàng)建與刪除用戶和修改它們的安全屬性與訪問權(quán)限。

策略(c)：每個(gè)用戶都有權(quán)創(chuàng)建與刪除自己的文件，并可以賦予或修改它們的安全屬性或訪問權(quán)限。策略(d)：只有當(dāng)某用戶是某文件的主人時(shí)，該用戶才有權(quán)把對該文件的訪問權(quán)轉(zhuǎn)授其他用戶或撤銷其他用戶對自已文件的訪問權(quán)。

策略(e)：只有當(dāng)用戶的敏感級(jí)不低于文件的敏感級(jí)時(shí)，用戶才可以閱讀該文件或者執(zhí)行該文件。策略(f)：只有當(dāng)文件P的敏感級(jí)不低于文件o的敏感級(jí)時(shí)，讀過文件o的用戶才能夠?qū)懳募。表5-1安全策略中的術(shù)語對照

該表中，符號(hào)欄內(nèi)的“t∈A［s,o］”表示t為矩陣項(xiàng)A［s,o］中的某個(gè)訪問權(quán)；SC表示安全類，是securityclass的縮寫。根據(jù)表中術(shù)語的抽象，上述策略(a)～(f)可以形式化地表述為如下的模型安全性質(zhì)：性質(zhì)(a)僅當(dāng)某主體對某客體有訪問關(guān)系時(shí)，該主體才能按規(guī)定的訪問權(quán)訪問該客體。

性質(zhì)(b)僅當(dāng)主體是系統(tǒng)管理員時(shí)才有權(quán)創(chuàng)建與刪除主體和修改主體的安全屬性與訪問權(quán)限。

性質(zhì)(c)每個(gè)主體都有權(quán)創(chuàng)建與刪除自已的客體，并可以賦予或修改自已客體的安全屬性或訪問權(quán)限。性質(zhì)(d)僅當(dāng)某主體是某客體的擁有者時(shí)，該主體才有權(quán)把對該客體的訪問權(quán)轉(zhuǎn)授其他主體或撤銷其他主體對自已客體的訪問權(quán)。性質(zhì)(e)僅當(dāng)某主體的安全類不低于某客體的安全類時(shí)，該主體才可以讀該客體或執(zhí)行該客體。性質(zhì)(f)僅當(dāng)客體p的安全類不低于客體o的安全類時(shí)，讀過客體a的主體s才能夠?qū)懣腕wp。5.2.2實(shí)例模型的定義

1.定義模型的狀態(tài)變量系統(tǒng)的狀態(tài)由系統(tǒng)中所有的狀態(tài)變量所決定，系統(tǒng)在某一時(shí)刻的狀態(tài)是由該時(shí)刻下所有狀態(tài)變量的值決定的。系統(tǒng)的安全狀態(tài)則是由系統(tǒng)中所有與安全有關(guān)的狀態(tài)變量所決定的。一旦這些狀態(tài)變量的值發(fā)生了變化，安全狀態(tài)也就隨著發(fā)生變化。表5-2是模型中將要使用的與安全有關(guān)的狀態(tài)變量。表5-2模型中的狀態(tài)變量

請注意，content和live狀態(tài)變量在上述幾個(gè)性質(zhì)中沒有直接涉及到，它們是與安全相關(guān)的輔助狀態(tài)變量，其作用后面將可以看到。模型(也就是系統(tǒng))的安全狀態(tài)由表5-2中這些狀態(tài)變量的集合組成，可以表示為

security-state={S,O,A［S,O］,SC(S),SC(O),contents(O),live}

其中:A［s,o］表示整個(gè)訪問矩陣(而A［s，o］表示單個(gè)矩陣元素，類似符號(hào)類推)，是最重要的狀態(tài)變量;SC(s)與SC(o)可以分別被認(rèn)為是附著在矩陣A［s,o］中的一行與一列。由于主體也可能是受訪問控制的對象，因此在矩陣的列中也包括所有主體。表5-3給出了本模型中訪問矩陣的結(jié)構(gòu)示意圖。表5-3本模型中訪問矩陣的結(jié)構(gòu)示意圖2.定義安全狀態(tài)不變式安全狀態(tài)不變式表明了系統(tǒng)對安全狀態(tài)的要求。安全狀態(tài)的定義就是根據(jù)上述6個(gè)安全策略的要求，把它們抽象為數(shù)學(xué)上的一個(gè)安全不變式。該安全不變式的含義表示，不論系統(tǒng)的安全狀態(tài)如何轉(zhuǎn)換，如果安全不變式的要求仍能得到滿足，那么系統(tǒng)總是處于安全狀態(tài)的。表5-4模型的安全不變式3.定義狀態(tài)轉(zhuǎn)換函數(shù)。在實(shí)際系統(tǒng)中，經(jīng)常需要進(jìn)行增加或刪除用戶或文件，修改用戶的訪問權(quán)限和文件的安全屬性等操作，這些操作都會(huì)改變系統(tǒng)的安全狀態(tài)。系統(tǒng)把這些操作功能作為系統(tǒng)服務(wù)提供給主體調(diào)用，調(diào)用的結(jié)果是改變系統(tǒng)中的安全變量(如訪問矩陣)。表5-5是根據(jù)安全策略的要求定義的部分狀態(tài)轉(zhuǎn)換函數(shù)，這些函數(shù)在模型中都要使用到。表5-5狀態(tài)轉(zhuǎn)換函數(shù)

表5-6中給出了creat-subject(s,sc)，creat-object(s,f,sc)，entertintoA［s,o］，confert(s,s1,o)幾個(gè)轉(zhuǎn)換函數(shù)的詳細(xì)描述。表5-6狀態(tài)轉(zhuǎn)換函數(shù)的描述上述各狀態(tài)轉(zhuǎn)換函數(shù)的主要作用是完成對狀態(tài)變量值的修改，進(jìn)而使得模型(或系統(tǒng))的狀態(tài)從當(dāng)前狀態(tài)變換為新狀態(tài)。需要強(qiáng)調(diào)的是，這些函數(shù)都是原子型的，它們的執(zhí)行是不可中斷的，如果狀態(tài)需要發(fā)生變化，那么這種變化是在瞬間完成的，可以認(rèn)為是不花費(fèi)時(shí)間的。在多道程序系統(tǒng)中，要特別注意異步進(jìn)程對狀態(tài)轉(zhuǎn)換的影響。在各個(gè)函數(shù)中只給出了相關(guān)狀態(tài)的變化，凡是在函數(shù)中未涉及的狀態(tài)的內(nèi)容都將保持不變。從這一點(diǎn)來說，不能把這些函數(shù)完全看成為計(jì)算機(jī)程序，而應(yīng)理解為描述系統(tǒng)狀態(tài)轉(zhuǎn)換前后狀態(tài)變量之間的關(guān)系。對于函數(shù)creat-subject(s,SC)，其作用是創(chuàng)建一個(gè)新主體(用戶)。函數(shù)中限定:在不存在重名的主體與客體的情況下，只能由系統(tǒng)管理員admin創(chuàng)建，創(chuàng)建后設(shè)置該用戶的安全類，并且不允許該用戶訪問任何客體。該主體要想訪問客體，要么由自己創(chuàng)建新的客體，要么等別的主體轉(zhuǎn)授對自己客體的訪問權(quán)。對于函數(shù)creat-object(s,f,SC)，其作用是由主體s創(chuàng)建具有安全類SC的客體(文件)f。創(chuàng)建f后，把f的安全類設(shè)為SC，并不允許其他任何主體對f有訪問權(quán)。但是對于創(chuàng)建者自己，可以自動(dòng)擁有對f的讀、寫、擁有和執(zhí)行權(quán)(如果是可執(zhí)行文件的話)。5.2.3實(shí)例模型的安全性分析

1.狀態(tài)轉(zhuǎn)換函數(shù)的安全性分析從數(shù)學(xué)角度講，對于每個(gè)狀態(tài)轉(zhuǎn)換函數(shù)，如果要證明它是安全的，必須證明它滿足以下定理：對于任意狀態(tài)轉(zhuǎn)換函數(shù)，當(dāng)且僅當(dāng)在滿足安全不變式的某個(gè)安全狀態(tài)下執(zhí)行該函數(shù)以后，系統(tǒng)仍能在新安全狀態(tài)下滿足安全不變式的要求，該轉(zhuǎn)換函數(shù)才是安全的。下面對上面給出的幾個(gè)狀態(tài)轉(zhuǎn)換函數(shù)的安全性進(jìn)行分析。在函數(shù)creat-object(s,f,SC)中，s是創(chuàng)建客體f的主體，該函數(shù)的作用是s為自己創(chuàng)建一個(gè)具有SC安全類的客體f。我們這里認(rèn)為創(chuàng)建者就是文件的擁有者，并且可以對自己的文件擁有全部訪問權(quán)(這也是實(shí)際系統(tǒng)中采用的方法)。函數(shù)中的“foralla∈S′A′［a,f］=”語句是為了防止同時(shí)對其他主體授予對文件f的任何訪問權(quán)，這樣處理的目的是確保該轉(zhuǎn)換函數(shù)的安全性。因?yàn)樵诒竞瘮?shù)執(zhí)行后，其他轉(zhuǎn)換函數(shù)執(zhí)行之前，系統(tǒng)中雖然增加了一個(gè)客體，但除了文件的擁有者外，其他任何主體都不能對該文件進(jìn)行任何訪問，因此就不會(huì)發(fā)生訪問權(quán)被偷竊或信息泄露的問題。而且這樣處理可以使模型的安全性證明方法具有更大的靈活性，還可以使函數(shù)變得更加簡潔。為了使其他主體能夠訪問新客體文件f，可以利用entertintoA［s，f］狀態(tài)轉(zhuǎn)換函數(shù)為其他主體設(shè)置對f的任何訪問權(quán)，只要能夠滿足安全不變式就行。為了防止低于f安全類的主體訪問f的情況發(fā)生，函數(shù)中在把訪問權(quán)t增加到A［s，o］中之前設(shè)置了條件限制，要求必須滿足SC(s)≥SC(o)。有了這一條限制后，就可以保證執(zhí)行該狀態(tài)轉(zhuǎn)換函數(shù)后，系統(tǒng)仍能滿足安全不變式的要求，即仍然能夠保持系統(tǒng)在新狀態(tài)下的安全性。狀態(tài)轉(zhuǎn)換函數(shù)creat-subject(si，SC)的作用是在系統(tǒng)中增加一個(gè)具有SC安全類的新主體s，并且只允許系統(tǒng)管理員admin創(chuàng)建新的用戶。為了保證該函數(shù)執(zhí)行后不影響系統(tǒng)的安全性，對新主體不設(shè)置對任何客體的任何訪問權(quán)。新主體對系統(tǒng)中客體的訪問權(quán)，可以通過enter函數(shù)設(shè)置。enter函數(shù)的執(zhí)行可以保持安全不變式的成立。狀態(tài)轉(zhuǎn)換函數(shù)confert(s，si，o)的作用是主體s把對自己的客體o的訪問權(quán)t轉(zhuǎn)授給另一主體si。函數(shù)中的轉(zhuǎn)授條件是“′own′inA［s,o］andSC(s)≤SC(si)andtinA［s,o］”，其含義為：s必須是客體o的擁有者并且si的安全級(jí)不低于s的安全級(jí);同時(shí),s對o有訪問權(quán)t。如果不設(shè)置SC(s)≤SC(si)的限制，就有可能將訪問權(quán)授予低于o的安全級(jí)的主體而讓它對o進(jìn)行訪問，這將破壞安全不變式的要求。由于條件SC(s)≤SC(si)保證了接收訪問權(quán)的主體si的安全類不低于s的安全類，因此防止了信息的泄露問題，保證了系統(tǒng)處于安全狀態(tài)。2.模型的初始狀態(tài)及其安全性分析正確地定義模型的(也就是系統(tǒng)的)初始狀態(tài)，確保其安全性，對于模型所有狀態(tài)下的安全性都是非常關(guān)鍵的。因?yàn)樵谧C明了轉(zhuǎn)換函數(shù)的安全性之后，如果能夠保證模型的初始狀態(tài)是安全的，那么就可以保證在任何狀態(tài)下執(zhí)行狀態(tài)轉(zhuǎn)換函數(shù)后，模型仍是安全的。

初始狀態(tài)是模型中所有狀態(tài)變量的初始值的集合。模型的初始安全狀態(tài)則是由模型中與安全密切相關(guān)的狀態(tài)變量所決定的。在我們的模型中,這些變量中最主要的就是訪問矩陣A［S,O］，此外還包括其他一些輔助安全變量如contents和lives等。在矩陣A中包括了所有的主體與客體以及它們的安全屬性、主體對客體的訪問關(guān)系與訪問權(quán)限等安全信息。對于contents和lives而言，在模型的初始狀態(tài)中，由于還沒有進(jìn)行任何狀態(tài)轉(zhuǎn)換操作，因此它們的內(nèi)容都是空的。模型的初始狀態(tài)主要由訪問矩陣的初始狀態(tài)決定。我們可以分析訪問矩陣的三種初始狀態(tài)下的安全性。

(1)訪問矩陣初始狀態(tài)為空。這種情況意味著主體集與客體集都為空，相互之間不存在任何訪問關(guān)系，因而模型中不存在泄漏信息的可能。很顯然，這種初始狀態(tài)肯定是滿足安全不變式的要求的。在這種初始狀態(tài)下，第一個(gè)可執(zhí)行的狀態(tài)轉(zhuǎn)換函數(shù)應(yīng)該是創(chuàng)建主體(create-subject)，接著就可以執(zhí)行創(chuàng)建對象的函數(shù)(create-object)了，然后其他函數(shù)也都可以開始執(zhí)行。一旦執(zhí)行創(chuàng)建主體的函數(shù)后，模型的初始狀態(tài)就會(huì)轉(zhuǎn)換到另一個(gè)狀態(tài)。這種初始狀態(tài)可以定義為

S＝Φ,O=Φ,SC(S)=Φ,SC(O)=Φ,A［S,O］=Φ

這里:A［S,O］＝Φ表示所有的矩陣項(xiàng)都為空;SC(S)＝Φ和SC(O)=Φ分別表示所有的主體與所有的客體的安全類都是空的。(2)初始狀態(tài)時(shí)訪問矩陣中只含主體。這種初始狀態(tài)是符合實(shí)際情況的，因?yàn)樾孪到y(tǒng)安裝后，系統(tǒng)管理員往往首先在系統(tǒng)中注冊用戶。由于此時(shí)系統(tǒng)中不存在客體，矩陣中的訪問關(guān)系(即矩陣元素內(nèi))是空的，因此系統(tǒng)也一定處于安全狀態(tài)。這種初始狀態(tài)可描述為：

S≠φ,O＝Sforalls∈S,o∈O,A［s,o］=φ

(3)初始狀態(tài)時(shí)只允許主體訪問自已的客體。這種初始狀態(tài)也是比較符合實(shí)際情況的。系統(tǒng)管理員在把每個(gè)用戶注冊到系統(tǒng)中之后，可以允許每個(gè)用戶只創(chuàng)建自已的文件、設(shè)置文件的安全類和對文件的訪問權(quán)限，不允許用戶之間轉(zhuǎn)授訪問權(quán)。在初始狀態(tài)下，各個(gè)主體只能訪問各自的客體，不存在相互訪問的問題，因而也就不存在信息泄漏問題，系統(tǒng)也就處于安全狀態(tài)了。這種初始狀態(tài)可以描述為：S≠φ,O≠φforalls∈S,o∈OSC(s)=sc,SC(o)=scA［s,o］=φ,whensisnotownerofoA［s,o］={r,e,w,own},whensisownerofo5.2.4模型的安全約束條件

1.對不安全轉(zhuǎn)換的約束在實(shí)際系統(tǒng)中，一般都允許用戶修改文件的安全類。假設(shè)在模型中定義了以下的修改客體安全類的函數(shù)

modify-SC(o,sc):function5modify-SC(o,sc)′SC(o)=sc；稍微分析一下，就可以發(fā)現(xiàn)這樣定義的轉(zhuǎn)換函數(shù)是很不安全的，因?yàn)樗梢詫腕w的安全類進(jìn)行任意的修改。性質(zhì)(g)：任何客體的安全類不能降低。把這條性質(zhì)可以表述為以下的數(shù)學(xué)形式：約束(1)：

forallo∈O

′SC(o)≥SC(o)

該約束條件表明新狀態(tài)下的客體o的安全類必須不低于前一狀態(tài)下該客體的安全類。一個(gè)函數(shù)是安全的，它不僅要滿足約束條件，還要滿足安全不變式的要求。根據(jù)這個(gè)約束條件，修改安全類的函數(shù)可重寫如下：

function5modify-SC(o,sc)ifsc≥SC(o)and′own′inA［lives,o］

′SC(o)=sc2.對主體的約束轉(zhuǎn)換函數(shù)操作的內(nèi)容與對象不同，所涉及的對象與內(nèi)容的敏感程度也不同，對它們的調(diào)用應(yīng)該受到嚴(yán)格的限制。例如，遵照自主訪問控制的原則，允許一個(gè)主體向另一個(gè)主體轉(zhuǎn)授訪問權(quán)。但是如果對此不加限制，系統(tǒng)中將會(huì)出現(xiàn)權(quán)利的轉(zhuǎn)授不受限制的情況，這將嚴(yán)重影響系統(tǒng)的安全性。防止這種情況出現(xiàn)的方法是，對主體調(diào)用函數(shù)進(jìn)行限制。在前面給出的性質(zhì)(d)就是控制對訪問權(quán)的轉(zhuǎn)授的，根據(jù)這個(gè)性質(zhì)可以給出以下約束：

約束(2)：

forallo∈Oif′own′notinA［lives,o］

thenforalls∈S，′A［s,o］=A［s,o］在該約束中，條件′own′notinA［lives,o］表示當(dāng)前正在調(diào)用函數(shù)的主體(lives)不是客體o的擁有者。在該約束中，條件′own′notinA［lives,o］表示當(dāng)前正在調(diào)用函數(shù)的主體(lives)不是客體o的擁有者。如果該條件成立，該主體將不能修改矩陣中的任何元素，也就是說將保持新狀態(tài)中的矩陣元素與原狀態(tài)下的矩陣元素的內(nèi)容相同(即′A［s,o］=A［s,o］)。我們在前面定義的函數(shù)function4confert(s,si,o)可以滿足這一限制條件，但該函數(shù)本身沒有滿足安全不變式的要求，因?yàn)樵谡{(diào)用enter函數(shù)時(shí)沒有限定si的安全類不能低于客體的安全類。幸好在函數(shù)enter中有這樣的控制條件，可以避免不符合安全要求的權(quán)利轉(zhuǎn)授問題的發(fā)生。函數(shù)funcion3也滿足該約束條件的限制。在設(shè)計(jì)約束條件時(shí)，要盡量使條件一般化，不要在約束條件中涉及到特殊操作的特殊要求，否則將使約束條件復(fù)雜化。更有可能因考慮了特殊要求而遺漏了對其他情況的限制，反而造成不安全情況的發(fā)生。3.對信息訪問的限制對于單純的訪問矩陣—監(jiān)控器模型而言，一般只控制是否允許主體去訪問客體，如果通過了訪問控制機(jī)制的核查，那么主體對客體內(nèi)容(信息)的修改則不受任何限制。

性質(zhì)(h)：僅當(dāng)某主體對某客體具有寫訪問權(quán)時(shí)，該主體才可以修改該客體的內(nèi)容。對于模型的這條性質(zhì)，可以用以下約束來描述：約束(3)：forallo∈Oif′w′notinA［lives,o］

thencontents(o)=contents(o)

根據(jù)這條約束，我們可以給出轉(zhuǎn)換函數(shù)write-object(o,date)的定義：

function6Write-object(o,date)ifo∈Oand′w′inA［lives,o］andSC(lives)≥SC(o)thenwritedataintocontents(o)

約束(4)：

forallo∈Oandp∈Oando,pisopenedbylivesif′r′inA［lives,o］and′w′inA［lives,p］andSC(o)>SC(p)thencontents(p)=contents(p)在該約束條件中，正在對兩個(gè)客體分別執(zhí)行讀與寫操作的lives，如果對客體o沒有讀權(quán)，或者對客體p沒有寫權(quán)，或者客體o的安全級(jí)高于客體p的安全級(jí)，那么就不允許向p寫入數(shù)據(jù)，即p的內(nèi)容保持不變。該約束條件對于在某個(gè)主體lives同時(shí)打開o與p兩個(gè)文件的情況下，試圖從其中一個(gè)文件讀出，并同時(shí)寫入另一個(gè)文件的操作可以發(fā)揮作用。但是如果一個(gè)用戶把從一個(gè)文件o讀出的數(shù)據(jù)先存入到某個(gè)緩沖區(qū)后再關(guān)閉該文件，然后再打開另一個(gè)文件p，并把緩沖區(qū)中的內(nèi)容寫入到p中，那么對于這種情況，該約束條件是不起作用的。因此，還沒有一種一般性的方法，它能夠給出一種約束，防止對客體內(nèi)容進(jìn)行非法的讀并將讀出的內(nèi)容非法轉(zhuǎn)移到其他客體的情況的發(fā)生。如果在系統(tǒng)實(shí)現(xiàn)時(shí)特別加以注意(參見一些相關(guān)的歷史記錄)，是可以發(fā)現(xiàn)一個(gè)主體同時(shí)打開多個(gè)文件，并對它們進(jìn)行關(guān)聯(lián)操作(例如從其中一個(gè)文件讀出，而向另一個(gè)文件寫入)的情況的。以上情況說明該約束條件的使用還存在漏洞，因?yàn)橹肋@種奧妙的程序員可以在編程時(shí)故意避開該約束條件的約束。

根據(jù)該約束條件，我們可以給出狀態(tài)轉(zhuǎn)換函數(shù)copy-object(from,to)的描述：

function7copy-object(from,to)

iffrom∈Oandto∈Oandfrom,toisopenedbylives

then

if′r′inA［lives,from］and′w′inA［lives,to］andSC(from)≤SC(to)

thencontents(to)=contents(from)在該函數(shù)中，只有對客體from有讀權(quán)和對客體to有寫權(quán)的主體，并且客體from的安全級(jí)不高于客體to的安全級(jí)，才允許從from復(fù)制數(shù)據(jù)到客體to。由于約束(4)不能有效地約束非法的讀然后轉(zhuǎn)移的情況，即存在著安全漏洞，因此系統(tǒng)難以處理許多非法的讀情況。如果在實(shí)際系統(tǒng)中，除文件外，還有其他客體，如緩沖池、全局計(jì)數(shù)器等是可以由主體修改的，那么判斷對這些客體的讀訪問是合法的還是違反安全要求的，是非常困難的，因?yàn)樾枰獙赡馨l(fā)生這種情況的所有函數(shù)進(jìn)行逐一分析。系統(tǒng)中也需要進(jìn)行一些讀、寫關(guān)聯(lián)的歷史記錄，以判斷是否存在非法的讀與寫的操作。5.2.5從模型到系統(tǒng)的映射