基于iP-可观测属性的动态非传递无干扰模型

Dynamic Intransitive Noninterference Model Based on iP-observability Attribute

针对现有信息流模型对于系统动态可信性判定过于严格的问题,提出一种基于iP-可观测属性检查的动态非传递无干扰模型。将系统抽象为一个六元组,从无干扰理论、系统状态可观察性和系统状态影响因素三方面出发,通过引入iP-可观测属性,经由有限状态自动机模型,将其转变为有限状态自动机中的P-可观测属性,并进一步利用P-可观测属性检查算法反推原系统满足动态非传递无干扰理论。对抽象系统实例的分析结果验证了该模型的有效性。

In order to solve the problem that the existing information flow model is too strict to determine the dynamic trusted of system,a dynamic Intransitive Noninterference(INI)model based on iP-observability attribute checking is proposed.It abstracts the system into a six-tuple,which introduces the iP-observability attribute from the noninterference theory,the observability of system states and system states’influencing factors,and transforms the iP-observability into P-observability attribute in automatic machine by automatic machine model,and then uses the P-observability attribute checking algorithm to reverse that the original system can meet the Dynamic INI(DINI)theory.Finally,an example of the corresponding abstract system is given to illustrate the effectiveness of the model.