安全訪問的輕量級完整性模型研究及實施
2007-12-31 00:00:00陳莉君石莉劉霞林
計算機應用研究 2007年8期
摘要：對傳統的完整性模型進行了分析，并對其完整性給予形式化描述。在此基礎上，提出了輕量級的ClarkWilson模型，并給出了其在安全增強操作系統SELinux中的實施。
關鍵詞： 機密性；完整性；SELinux；輕量級模型
中圖分類號：TP316;TP309文獻標志碼：A
文章編號：1001－3695(2007)08－0173－03
機密性（confidentiality）與完整性（integrity）是計算機安全領域中所需要解決的兩個根本問題。
在目前的系統中，主要套用BLP（保密）模型和Biba（完整）模型等理論來指導實際系統的安全。BLP（BellLaPadula）模型是D. Bell和L. LaPadula提出的第一個計算機保密模型。BLP基于兩條基本規則來保障數據的保密性，即不上讀和不下寫。上級保密的東西不讓下級讀，上級保密的東西不準寫給下級。Biba模型是Ken Biba提出的，該模型對數據提供了完整性保障。它基于兩條基本規則來保證數據的完整性，即不下讀和不上寫。
BLP著眼于保密性，而不是防止竄改，而Biba模型是著眼于完整性，這兩個性質是互相獨立的，一個文件或進程是可以同時擁有這兩個性質的。如系統中可以存在雖是低完整性的，但是高保密性質的進程，即允許某些進程出錯但絕對不允許泄密，如應用在軍事方面。也有高完整性低保密性進程，如公用進程，因為這樣的進程必須保證系統正常運行。又如高完整性低保密性文件，如Windows系統的注冊表等。
完整性是比機密性更加重要的需求，因為在完整性被破壞的情況下，可能會影響到整個系統的運轉和最終結果。
1完整性模型分析
盡管操作系統為每個進程提供了獨立的內存空間，但是進程依然可以通過文件、管道、網絡連接，共享內存以及其他機制進行通信。如果進程A對進程B使用的某些資源（如文件或管道）進行寫，那么就說進程A與進程B之間有信息流（information flow）。信息流完整性驗證問題說明高安全性（或高完整性）的進程不能依賴出自不可信（或低完整性）進程的信息流。
例如，如果不可信用戶可以對可信的OPenSSH配置文件sshd config進行寫，這就違背了信息流完整性。對傳遞的信息流也要進行檢查：如果不可信的用戶可以寫cron（定期執行指定的任務），而cron寫了sshd config，那么這明顯違背了完整性。僅僅設置文件權限還不足以防范攻擊，因為攻擊還可以來自管道或共享內存，也即必須嚴加防范各種輸入。一般來說，如果可信程序依賴不可信輸入，那么攻擊者就可能獲取逐步升高的權力或者入侵系統。為了維護信息流的完整性，必須對系統進行適當配置，即權限的集合必須確保不存在從不可信進程到可信進程的非法信息流。采用Biba[2]模型可以趨于達到這樣的目的， 可信進程僅依賴只可讀取的資源，即不允許不可信輸入流向可信進程。
信息流完整性需要兩個條件的組合：a)合適的配置。這就要確保程序信任的輸入（如config文件）不能被不可信用戶修改。b)過濾代碼，這就要確保對程序不信任的輸入（如網絡輸入）進行形式化和針對具體應用限制的檢查。
ClarkWilson完整性模型覆蓋了以上兩個方面，適合于當前可信進程，但需要所有進程的輸入均進行過濾。但是，ClarkWilson模型與Biba類似，是比較重量級的，需要對程序進行形式化驗證。當要對程序進行深入、完整的安全分析時，對其一一進行形式化驗證不僅不可能，也不現實，而且大多數正在使用的系統根本沒有任何類型的信息流驗證，這種問題雖然已早被認識，但在實踐中根本沒有得到解決。
1．1基本信息流的完整性
在基本信息流完整模型中，依賴于低完整性的數據是根據信息流定義的。這樣的模型需要非低完整性信息流可以輸入到高完整性主體。定義信息流的兩種標準操作，即修改（modify）和查看（observe）。這里mod(s， o)是修改操作符，表示標簽為s的主體（如進程或用戶）寫標簽為o的客體（如文件或套接字）；obs(s， o)是查看操作符，表示標簽為s的主體從標簽為o的客體中讀。用S表示所有主體的集合。
ClarkWilson應用的程序員預先并不知道系統的信息流，因此必須確保所有的接口均是過濾的接口。在實際中，通常只有少數接口真正需要在實際系統的上下文中能夠進行過濾。在應用的開發中通過使用系統知識（因為開發者可以轉移應用的安全策略），可以減少開發者的過濾負擔。利用這一點來開發輕量級CW模型。
2基于SELinux 的輕量級完整性解決方案
所謂輕量級CW就是對于運行在特定系統上的特定目標應用來說要進行驗證。應用開發者必須對其程序任何小的變化均能進行驗證，而系統管理員對他們的系統進行實際的驗證。用術語TCB（可信計算基）來表示必須信任的主體集合，從而可以信任一組目標應用（如sshd、apeche、bind）。
應用開發者必須做到：
a)假定某些TCB和應用的配置，確定到程序不可信的輸入并對其進行過濾。
b)用FILTER（）過濾函數對這些接口進行過濾。這些過濾由訪問控制系統使用。
c)為應用構造一個缺省的安全策略，有兩種主體類型：缺省的主體允許來自TCB的輸入；對于其他的過濾接口，也可以有不可信的輸入類型。
因為應用開發者無論如何應當過濾他們不可信的輸入，這就表示能使系統級完整性驗證的工作減少到最少。
2．1SELinux
SELinux是由美國國家安全部(National Security Agency)領導開發的GPL項目，它擁有一個靈活而強制性的訪問控制結構，旨在提高Linux系統的安全性，提供強健的安全保證，可防御未知攻擊，相當于B1級的軍事安全性能。應用SELinux后，可減輕惡意攻擊或惡意軟件帶來的災難，并提供對機密性和完整性有很高要求的安全保障。
SELinux模塊是Linux安全模塊，它提供了細粒度、全面的MAC強制訪問。SELinux實現了類型強制（TE）的擴展形式，利用域轉變，能使策略的表達涵蓋多達30多種客體，每個客體大約10種操作。SELinux是全面的，因為其目標在于控制所有程序對與安全相關的所有系統對象的訪問。
在SELinux的主要表示是主體類型和客體類型。一個進程的安全上下文是由它的主體類型決定的。同樣，非主體對象與客體類型相關。與客體相關的權限放在策略文件中；如果apache進程有主體類型apache_t，而它的配置文件有客體類型apache config_t， 就可以在策略文件中進行如下形式的描述：
盡管在SELinux策略模型中，除了從主體到客體的allow權限外，還有幾種訪問控制概念，但只有一種與信息流相關。Relabel操作能使主體改變客體的客體標簽，能使信息流從舊的客體標簽流到新的客體標簽。盡管這讓我們有極大的控制權和靈活性，如達到相當的細粒度，但這種全面的控制權限導致龐大而復雜的訪問控制策略。據統計，缺省的編譯就有500 KB的編譯策略文件。在策略文件中（policy.conf）大約有5 000權限分配。這種策略僅僅包含基本的主體；完整的策略，包括所有應用的策略，會是這個大小的10倍。因此，要理解一個策略所隱含的高級特性，如信息流，就根本無法手動完成。
2．2在MAC策略中支持過濾接口
一旦目標應用（如sshd、apeche、bind）不可信輸入通過過濾主體類型進行了隔離，那么只需要檢查應用程序的缺省主體類型s不再有不可信輸入。可以使用Gokyo工具[4]從SELinux策略[6]中計算信息流。Gokyo把控制策略表示成圖。其中：節點表示SELinux主體類型和權限；邊表示對主體類型賦予的權限?；谑欠裨试Smod操作和obs操作，或者兩者同時操作，Gokyo計算出到s的所有信息流，也即計算出主體類型的集合：
雖然可以修改SELinux將過濾接口從其他接口中分離出來，但是開發者還需要告訴SELinux對于給定的接口是否要進行過濾。在這個過程中，開發者需要確定哪些接口需要過濾。有些可能是明顯的，但是對于在一些微小之處不可信數據的訪問還是需要進行檢查。開發者可以下兩種方式找到過濾接口：通過在默認的策略上運行安全策略分析工具；對應用程序分析所有違背完整性的許可權。
確定一個程序到底在哪里使用了許可權的問題不在SELiunx研究的范圍內，必須實現自己的機制。于是，在SELinux中使用sysfs接口定義一種操作叫做FILTER()，并對SELinux的用戶庫和內核模塊進行修改。當從用戶空間調用FILTER()時，就修改SELinux內核模塊，尋找是否有違背SELinux策略進程。如果有，就向該進程發出信號，用戶庫捕獲到這個信號，并讓進程陷入單獨的xterm調試程序（gdb）中。一旦進入調試程序，問題變得簡單，就可以使用棧跟蹤和數據檢測，從而確定權限錯誤為什么發生，發生在何處，然后進一步采取措施，或刪除隱患操作，或實現一個過濾接口。如果權限從來就沒有被需要過，那就直接從策略中刪除。
要進行過濾，就調用FILTER()，以避免程序接收所有的輸入，對有些輸入加以限制，如不允許從命名管道進行拷貝。當然，如果程序語義改變后包含了對不可信輸入的解釋，那程序員就要實現另外的過濾接口。
如果系統管理員利用策略檢測工具找到涉及一組權限的非法信息流，就要采取適當的措施，對于一些還沒有需要的權限進行刪除。一些信息流可能是由不可信的程序產生的，但對系統來說是可選的，簡單的措施就是刪除這種信息流，從系統去掉有關代碼和主體類型。有些需要的權限是目標應用的可選成分，就可以禁止這種選項，并刪除其權限。如果這種權限是由核心應用使用，系統管理員就可以采取比較小的TCB，而開發者不必施加限制。
3結束語
系統完整性是困惑安全研究者多年的難題。關于完整性的很多工作均集中在信息流模型，由高可信進行補充（如程序正確性的形式化驗證）。Biba完整性模型實際上是BellLaPadula保密模型雙倍，這里從低完整性到高完整性主體的信息流是禁止的。像BellLaPadula，需要有高可信成分來克服限制，但不像保密性的情況，低（低到高）完整性信息流是普遍現象（如用戶的請求）。
Denning在安全信息流模型[8]的工作就像lattice一樣模擬了不同標簽的主體之間的信息流，但也模擬了任何違背lattice結構的非法流。LOMAC（低水?。┩暾砸脖苊飧咄暾灾黧w對低完整性信息流施加影響。在這種情況下，通過對低完整性信息流的接收來降低高完整性主體的級別。ClarkWilson模型優勢在于有能過濾低完整性數據的接口，但是所有的接口均必須能夠自我清理（或丟棄），并且信任這些接口的基礎是高可信[5]。
最近由LI和S.Zdancewic[9]提出了一種形式化類型系統，能夠捕獲程序內標簽的信息流，提供對數據的降低；類型檢查可以用來確保信息流安全。可以將其方法應用到進程間信息流，這是由安全策略而不是程序代碼進行控制。在這里提出的FILTER()過濾接口可以降低在這種上下文中的操作。
參考文獻：
［1］BIBA K J. Integrity considerations for secure computer systems，Technical Report MTR－3153[R]. Bedford， MA:Mitre Corporation， Mitre Corp， 1975.
[2]National Security Agency. Securityenhanced linux[EB/OL].http://www.nsa.gov/selinux/.
[3]BELL D， PADULA LL. Secure computer systems，mathematical foundations，technical report ESDTR－73－278[R]. [S.l.]:Mitre Corp， 1973.
[4]Tresys Corporation. SETools policy tools for SELinux[EB/OL].http://www.tresys.com/selinux/selinux policy tools.shtml.
[5]CLARK D， WILSON DR. A comparison of commercial and military computer security policies[C]//Proc of the IEEE Symposium on Security and Privacy.[S.l.]:IEEE Computer Society Press，1987:184－238.
[6］JAEGER T， EDWARDSA， ZHANGXiaolan. Policy management using access control spaces[J]. ACM Transactions on Information and System Security，2003，6(3):327－364.
[7]JAEGER T，SAILER R， ZHANG Xiaolan. Analyzing integrity protection in the SELinux example policy[C]//Proc of the 12th USENIX Security Symposium.2003.
[8]DENNING D E. A lattice model of secure information flow[J]. Communications of the ACM，1976，19(5):236－243.
[9］LI Peng， ZDANCEWIC S. Downgrading policies and relaxed noninterference[C]//Proc of the Symposium on Principles of Programming Languages.New York:ACM Press，2005.
[10]卿斯漢，溫紅子，雷浩，等.基于ClarkWilson完整性策略的安全監視模型[J].軟件學報，2004，15(8):11241132.
注：“本文中所涉及到的圖表、注解、公式等內容請以PDF格式閱讀原文”
