當(dāng)我們談?dòng)?jì)算機(jī)安全的時(shí)候我們?cè)谡勈裁?noninterference)

Pre

相信大家都學(xué)過(guò)不少關(guān)于計(jì)算機(jī)安全的課程和知識(shí)， 大家多多少少對(duì)各種各樣的攻擊方式有一定的了解。但是當(dāng)談及到底什么樣的程序可以被認(rèn)為是安全的時(shí)候， 這都不會(huì)是一個(gè)容易回答的問(wèn)題。 說(shuō)出幾條例如內(nèi)存安全， 權(quán)限不會(huì)泄漏之類的規(guī)則不難，但是什么是安全規(guī)則卻很難回答。畢竟這種本質(zhì)論多少有點(diǎn)形而上學(xué)的意思。 我記得我在這個(gè)學(xué)校也學(xué)習(xí)過(guò)一學(xué)期的計(jì)算機(jī)安全的課程，但是唯一的印象也只剩下了各種攻擊和內(nèi)存排布之類的東西。 但是如果想要驗(yàn)證程序是安全的首先我們必須回答這個(gè)問(wèn)題。 這里說(shuō)的驗(yàn)證當(dāng)然是嚴(yán)謹(jǐn)?shù)?rigorous), 并不簡(jiǎn)單的經(jīng)驗(yàn)主義的使用測(cè)試來(lái)說(shuō)明程序的安全性， 而是使用形式化方法嚴(yán)格證明程序安全。

計(jì)算機(jī)科學(xué)家們?cè)?0年代末[1] 對(duì)這個(gè)問(wèn)題進(jìn)行了不少的探索， 最后在1982年, J.A. Goguen 和J Meseguer發(fā)布了一篇非常重要的論文， Secruity Policies and Secruity Models. 在這篇文章中他們第一次提出了不相干(noniterference)的概念，并抽象了一個(gè)語(yǔ)義模型(使用抽象代數(shù)類型)， 在這個(gè)模型下，大量的安全規(guī)則可以被形式化的描述了。

Noninterference

從比較高的層次上來(lái)講noninterference的概念非常簡(jiǎn)單，如果我們?nèi)サ舫绦蛑袚碛懈邎?zhí)行權(quán)限的用戶和他相關(guān)的行為，從低權(quán)限的用戶看來(lái)系統(tǒng)不會(huì)發(fā)生任何的變化。但是既然是形式化的描述我們還是要嚴(yán)謹(jǐn)?shù)膩?lái)說(shuō)明。

security model

模型必然是為了描述某種特定的系統(tǒng)來(lái)使得。 noninterference主要希望描述的對(duì)象是動(dòng)態(tài)的capability 系統(tǒng)， 在這種系統(tǒng)中，有高權(quán)限用戶和低權(quán)限的用戶, 他們都可以在自己權(quán)限下使用對(duì)應(yīng)的指令，于此同時(shí)，系統(tǒng)也存在權(quán)限變更指令，也就是在程序運(yùn)行中，可以動(dòng)態(tài)的給予不同的用戶不同的權(quán)限。如果一個(gè)指令滿足權(quán)限那么系統(tǒng)狀態(tài)會(huì)發(fā)生對(duì)應(yīng)的變化， 如果不滿足，系統(tǒng)將保持當(dāng)前狀態(tài)(非常有model checking的味道)。
但是遺憾的是我們這里討論的程序都是確定程序，也就是說(shuō)對(duì)于不同用戶的指令輸入，輸出總是相同的， 因而整個(gè)系統(tǒng)也就成了一個(gè)有限狀態(tài)機(jī)。

系統(tǒng)可以有如下的形式化定義：

  • U: user用戶
  • S: state程序運(yùn)行中的狀態(tài)
  • SC: 狀態(tài)轉(zhuǎn)移指令
  • Out: 程序輸出
  • Capt: Capability table: 權(quán)限表，角色對(duì)應(yīng)的指令權(quán)限
  • CC: Capability Command權(quán)限變更指令
  • out: S \times Capt \times U \to Out 輸出函數(shù) ,表示程序在某一狀態(tài)下，某一用戶在其權(quán)限下觀察到的程序輸出
  • do: S \times Capt \times SC \to S 狀態(tài)轉(zhuǎn)移函數(shù)，表示程序在某一用戶在其權(quán)限下使用命令程序狀態(tài)發(fā)生的的變化
  • cdo: Capt \times U \times CC \to Capt 權(quán)限轉(zhuǎn)移函數(shù)，和上面類似，不過(guò)是權(quán)限指令造成的權(quán)限變化(權(quán)限指令并不由用戶輸入)
  • t0,s0: 初始狀態(tài)和初始權(quán)限

其中我們把C = SC \cup CC的子集叫做能力(ability)，簡(jiǎn)稱Ab. 然后我們可以給出Capt 的類型
Capt : [U \to Ab]
也就是說(shuō)權(quán)限表是記錄不同用戶所對(duì)應(yīng)能力的這么一種抽象數(shù)據(jù)結(jié)構(gòu)。

最后我們可以使用ML風(fēng)格的偽代碼來(lái)描述我們整個(gè)狀態(tài)機(jī)的轉(zhuǎn)移函數(shù)(同時(shí)包含了權(quán)限狀態(tài)和控制狀態(tài)的變化):
csdo : S \times Capt \times (U \times C)^* \to S \times Capt
csdo (s, t,nil) = (s,t)
csdo (s, t, w.(u,c)) = csdo(csdo(s,t,w), u, c)
其中第三個(gè)參數(shù)可能比較誤導(dǎo)，原文說(shuō)指令可以看作一個(gè)字符串w, 而這個(gè)輸入中包括了多組的用戶和輸入元組對(duì)，這里的第三行的點(diǎn)是字符串連接函數(shù)。這個(gè)類型顯然是對(duì)不上的。原因主要是因?yàn)檫@個(gè)文章的年代比較久,82年這個(gè)時(shí)候甚至還沒(méi)有ML語(yǔ)言之類的類型系統(tǒng)， 如果用現(xiàn)代一點(diǎn)的方法嚴(yán)謹(jǐn)?shù)恼f(shuō)就是第三個(gè)參數(shù)的類型應(yīng)該為list \; (pair \; U \; C )。其中點(diǎn)是cons.而第三句的后半部分也是懂得都懂，默認(rèn)科里化加上構(gòu)造。
增加記號(hào)：
[[w]] = csdo(t_0,c_0,w)
這里我們可以很明顯的看出整個(gè)狀態(tài)機(jī)所描述的是一個(gè)確定性(deterministic)系統(tǒng)。這其實(shí)是一個(gè)限制很大條件，因?yàn)槲覀兩钪械拇蠖鄶?shù)程序都不是確定性的。

定義刪除操作(purge)
G，A,分別是用戶集合和命令集合,P_G(w)刪除包含G中用戶的Pair(U,C), P_A(w)刪除包含A中命令的元組對(duì)，P_{G,A}(w)，表示刪除在上面這個(gè)list中包含的G,A所有相關(guān)用戶命令

noninterference rule

在定義了模型之后我們可以來(lái)形式化的闡述不相干性了。

一組用戶G 如果滿足
\forall \; (w \in (U \times C)^*) \;\; (u \in G),\quad [[\;w\;]] = [[\; P_{G}(w) \;]]
那么G用戶和其他用戶G‘不相干。記做：
G :| \; G'

對(duì)于一種能力A, 一組用戶G 如果滿足
\forall \; (w \in (U \times C)^*) \;\; (u \in G),\quad [[\;w\;]] = [[\; P_{A}(w) \;]]
能力A與用戶組G中的用戶不相干。記做：
A :| \; G

對(duì)于一種能力A,一組用戶G 如果滿足
\forall \; (w \in (U \times C)^*) \;\; (u \in G),\quad [[\;w\;]] = [[\; P_{G,A}(w) \;]]
那么G中擁有能力A的用戶和剩下的用戶G'不相干。記做：
G,A :| \; G'

\square
在后續(xù)的很多論文中，上面的模型一般被稱為GMNI模型.

security policy

很多安全策略都可以使用上面說(shuō)的模型來(lái)描述,?？磦z例子吧：

isolation: -G |: G, -U |: U
channel control: -A,G |: G' and -A,G' | G

不相干模型的局限性和后續(xù)工作

首先顯然不相干模型是一種有限狀態(tài)機(jī)的模型，他在對(duì)應(yīng)nondeterminitic的情況時(shí)是不適用的，也就意味著我們對(duì)于系統(tǒng)的抽象是非常粗糙的。McLean 的工作擴(kuò)展了這個(gè)模型使得它可以適用與不確定性的情況。但是隨著人們對(duì)計(jì)算機(jī)安全的認(rèn)識(shí)，很多的規(guī)則其實(shí)還是無(wú)法用這個(gè)來(lái)表示的。比如我們看到GMNI這種思路本質(zhì)還是在規(guī)定什么樣的行為是“不好”的，這種也被稱為safety性質(zhì)，但是只有safety是不夠的,很多時(shí)候我們也需要去告訴系統(tǒng)什么樣的行為是安全的或者說(shuō)是"好的"，這也被稱為liveness性質(zhì)。這在這種模型中就完全無(wú)法描述， 所以后續(xù)又出現(xiàn)了大量各種各樣的安全模型。

在2010年，Micheal Clarkson[3]提出了一種大一統(tǒng)論,他稱其為超性質(zhì)(hyperproperties),這種理論試圖在拓?fù)渖蠈?duì)世界上所有的安全模型進(jìn)行描述和統(tǒng)一，并且期待模型檢查技術(shù)能夠給出比較好的解決方案，但是目前對(duì)于超性質(zhì)相關(guān)的實(shí)際model checker還沒(méi)有太多的進(jìn)展。

然而我們永遠(yuǎn)不可能擁有完美的模型。模型復(fù)雜化帶來(lái)的問(wèn)題1是驗(yàn)證的難度大大提升了， 但是還有一個(gè)本質(zhì)的問(wèn)題無(wú)法解決，那就是側(cè)信道攻擊，即使你的軟件在邏輯上完美無(wú)缺，對(duì)于某些物理世界的觀察依然可能導(dǎo)致信息泄露，一個(gè)非常好的例子就是有一種攻擊可以通過(guò)服務(wù)返回?cái)?shù)據(jù)的CPU計(jì)算時(shí)間的周期變化來(lái)推測(cè)服務(wù)器中某些密鑰數(shù)據(jù)。
我在雪城安全課上最大的收獲是，我的老師上課講了這么一個(gè)故事。 如何在所有知情人都守口如瓶的情況下知道一個(gè)房間里的燈亮過(guò)沒(méi)有。最簡(jiǎn)單的方法就是摸摸那個(gè)燈泡燙不燙。這其中沒(méi)有任何信息流上的泄露但是側(cè)信道卻能告訴我們很多。

不過(guò)不管怎么樣安全模型加上很多形式化方法確實(shí)在這兩年有了很多的應(yīng)用，比如之前很有名的seL4操作系統(tǒng)內(nèi)核，就是一個(gè)成功使用GMNI模型的例子。

Reference

[1] R. J. Feiertag, K. N. Levitt, and L. Robinson. 1977. Proving multilevel security of a system design. SIGOPS Oper. Syst. Rev. 11, 5 (November 1977), 57–65. DOI:https://doi.org/10.1145/1067625.806547
[2] J. A. Goguen and J. Meseguer, "Security Policies and Security Models," 1982 IEEE Symposium on Security and Privacy, Oakland, CA, USA, 1982, pp. 11-11, doi: 10.1109/SP.1982.10014.
[3]Michael R. Clarkson and Fred B. Schneider. 2010. Hyperproperties. J. Comput. Secur. 18, 6 (September 2010), 1157–1210.

?著作權(quán)歸作者所有,轉(zhuǎn)載或內(nèi)容合作請(qǐng)聯(lián)系作者
【社區(qū)內(nèi)容提示】社區(qū)部分內(nèi)容疑似由AI輔助生成，瀏覽時(shí)請(qǐng)結(jié)合常識(shí)與多方信息審慎甄別。
平臺(tái)聲明：文章內(nèi)容（如有圖片或視頻亦包括在內(nèi)）由作者上傳并發(fā)布，文章內(nèi)容僅代表作者本人觀點(diǎn)，簡(jiǎn)書(shū)系信息發(fā)布平臺(tái)，僅提供信息存儲(chǔ)服務(wù)。

相關(guān)閱讀更多精彩內(nèi)容

友情鏈接更多精彩內(nèi)容