使用Alloy建模驗證系統於存取控制

Abstract

在這篇論文中，我們在Alloy建模驗證系統中驗證存取控制機制是否滿足線性代數上的某些特質為首要目標。在此論文中，以三個典型的存取控制機制為驗證目標，這三個存取控制分別為(1)Bell-LaPadula Model，驗證以此模型的機制下，安全標籤是否符合代數中的大小關係，如:a>b>c。且安全層級越高者可讀檔案越多。(2) China Wall Security Policy (中國城牆策略)，傳統的China Wall Security Policy 規定過為嚴格，於此我們將其規定放寬，使得一家公司的顧問可將此公司的資訊流出，但不得讓相同性質公司獲得此公司的資訊，我們以此驗證我們所提出的策略是否符合代數性質中的遞移關係且不會讓資料外流至不開取得此資料之公司。(3)角色型存取控制，我們加上角色責任分離機制，以驗證任一使用者不得獲得兩個以上有衝突的角色。最後再結論時討論我們處理三種存取控制與驗證結果，以及簡略討論Alloy建模驗證系統的效能。

Throughout the thesis, our main goal is to verify access control schema to see if they satisfy certain algebraic properties. In the thesis, we exercise verifications on three access control policies. The first one is the Bell-LaPadula Model. By exercising Bell-LaPadula Model in Alloy, we verify the order relations between the security label and the user who possesses higher security level can read more files. The second one is the China Wall Security Policy. The Brew and Nash model for China Wall Security Policy is too restrictive to practice. We loosen the policy to be less restrictive. One company’s information can be written into the other company, as long as there two companies do not belong to the same conflict of interest. We exercise this model and to verify if there’s any possible information goes from one to another and the two companies are in the same conflict of interest class. ( Belongs to transitive relation). The last one is the Role-Based Access Control with Separation of Duty concept. In the conclusion, we conclude the result of the verification and briefly discuss the effectiveness of the Alloy SAT model checker.