SELinux中策略有效性的形式化模型研究

文章提出了一个形式化模型AMACP（Analyzing Model of SELinux＇Accegs Control Pplicy）,用它来分析SELinux中的策略配置文件的有效性,SELinux中的策略数目是巨大而又复杂的.SELinux系统实现的几个子模型是由配置文件中的规则构成,但却很难全面把握这些规则对系统本身的影响.文章的目的就是根据SELinux中策略配置构建语义并且模型化这些规则之间的关系.在此基础上提出一种算法,用来验证某个主体是否可以利用某种给定的存取模式来访问某个给定的客体对象.

Research of formal model for Security policies' validation in SELinux

This paper presents a formal model called AMACP(Formal Model of SELinux' Access Control),for analyzing the Security policies' validation in SELinux.The security policy of SELinux is large and complex,it is made by many configuration rules that refer to the access control sub-models implemented in the SELinux system.Among the so many rules,it is extremely difficult to understand their overall effects in the system.Our aim is to define semantics for the rules and to model the relationships among sets of configuration rules.Finally,we develop an algorithm based upon AMACP,we can verify whether,given an arbitrary security policy configuration,a given subject can access a given object in a given mode.