论文部分内容阅读
为了发展，高度固定数据库系统为类 B2 满足要求， BLP (Bell-LaPudula ) 模型根据数据库系统的特征被扩大。为为数据库系统验证安全模型的一个方法被建议。根据这个方法，由使用 Coq 证明助手保证扩大模型的正确性和安全的分析被介绍。我们的正式安全模型被验证了安全。这个工作证明我们的确认方法有效、足够。