本論文提出一套使用 CPN (Coloured Petri Net) 的方法來分析 SELinux (Security-Enhanced Linux) 中安全政策的資訊流。資訊流是系統中主體與受體之間的資訊交換。而一般的存取控制也就是對於各種類型資訊流的控管。SELinux 的存取控制機制是基於其安全政策，代表著系統中所有允許的資訊流都會定義在此安全政策之中。一個標準的 SELinux 安全政策就包含了二十多萬行的規則。因此，對於政策管理者而言，如何確定所制定的政策真的有符合事先定義的安全目標，將是一個重大的挑戰。為了解決此問題，本研究提出一套正規的資訊流模型來描述 SELinux 安全政策，並且提出一套 Query 語言來幫助管理者表示他所期望 / 不期望的資訊流。我們開發了一套方法將 SELinux 安全政策轉換成 Policy CPN Diagram，並且將安全目標轉換成 Query CPN Diagram。為了達到自動化的分析，我們開發了一套工具，名為 SELAnalyzer，可以驗證 SELinux 安全政策是否滿足安全目標。最後，我們比較相關的研究並且提出一個旁波段網路的範例來說明如何使用我們的工具。 This paper presents a Colored Petri Nets (CPN) approach to analyze the information flow in the policy file of Security-Enhanced Linux (SELinux). The SELinux access control decisions are based on a security policy file that contains several thousands of security rules. It becomes a challenge for policy administrator to determine whether the modification of the security policy file conforms to the pre-specified security goals. To address this issue, this paper proposes a formal information flow model for SELinux security policy file, and presents a simple query language to help administrators to express the expected/unexpected information flow. We developed a method to transform the SELinux policy and security goal into Policy CPN Diagram and Query CPN Diagram. A tool named SEAnalyzer that can automatically verify the SELinux policy has been developed and two application examples of this tool will be presented in the context.
