计算机工程
計算機工程
계산궤공정
COMPUTER ENGINEERING
2013年
12期
130-135
,共6页
BLP模型%安全策略%形式化方法%自动化验证%定理证明%安全操作系统
BLP模型%安全策略%形式化方法%自動化驗證%定理證明%安全操作繫統
BLP모형%안전책략%형식화방법%자동화험증%정리증명%안전조작계통
BLP model%security policy%formal method%automated verification%theorem proving%security operating system
在《雷息安全技术操作系统安全技术要求》中，提出访问验证保护级安全操作系统的研发过程需要完全形式化的安全策略模型。针对该情况，对经典的数据机密性BLP模型进行陒应改进，为系统中的主客体引入多级安全标签以及安全迁移规则，使其满足实际系统开发的需求。运用完全形式化的方法对改进模型的状态、不变量、迁移规则等进行描述，使用Isabelle定理证明器证明了迁移规则对模型的不变量保持性，从而实现对模型正确性的自动形式化验证，并保证了模型的可靠性。
在《雷息安全技術操作繫統安全技術要求》中，提齣訪問驗證保護級安全操作繫統的研髮過程需要完全形式化的安全策略模型。針對該情況，對經典的數據機密性BLP模型進行陒應改進，為繫統中的主客體引入多級安全標籤以及安全遷移規則，使其滿足實際繫統開髮的需求。運用完全形式化的方法對改進模型的狀態、不變量、遷移規則等進行描述，使用Isabelle定理證明器證明瞭遷移規則對模型的不變量保持性，從而實現對模型正確性的自動形式化驗證，併保證瞭模型的可靠性。
재《뢰식안전기술조작계통안전기술요구》중，제출방문험증보호급안전조작계통적연발과정수요완전형식화적안전책략모형。침대해정황，대경전적수거궤밀성BLP모형진행희응개진，위계통중적주객체인입다급안전표첨이급안전천이규칙，사기만족실제계통개발적수구。운용완전형식화적방법대개진모형적상태、불변량、천이규칙등진행묘술，사용Isabelle정리증명기증명료천이규칙대모형적불변량보지성，종이실현대모형정학성적자동형식화험증，병보증료모형적가고성。
According to the《Information Security Technology--Security Techniques Requirement for Operating System》, formal security policy model is required in the development of access verification and protection level of security operating systems. Aiming at the situation, an improved BLP model which has multi-level security labels and security transition rules is proposed based on the traditional data confidentiality BLP model to satisfy the development of actual systems. The states, invariants, transition rules are described by formal method and theorem prover Isabelle is used to prove that all the rules hold the invariants in the model which guarantees the model’s reliability, and it realizes the automatic formal verification of model correctness.
