一种实用动态完整性保护模型的形式化分析

从完整性保护模型提出到现在,其成熟度远不如机密性模型.究其原因,完整级划分以及模型实用性是制约其发展的根本因素.从完整性模型的实用性角度出发,归纳总结几种现有完整性保护模型的优缺点,提出了一种实用型的动态完整性保护模型(dynamic integrity protection model,DMIP).它面向Linux系统,解决了完整性级别划分困难以及现有完整性模型可用性不强的问题.针对来自网络的攻击以及本地恶意代码破坏系统完整性等问题给出了保护策略.从与Linux系统及系统中已有的应用程序的兼容性角度出发,DMIP做到了无代价兼容.给出了DMIP模型的不变式和约束,针对模型进行了安全定理的形式化证明,保证了模型的安全性.