In order to develop highly secure database systems to meet the requirements for class B2,the BLP (Bell-LaPudula) model is extended according to the features of database systems. A method for verifying security model for database systems is pro-posed. According to this method,an analysis by using Coq proof assistant to ensure the correctness and security of the extended model is introduced. Our formal security model has been verified secure. This work demonstrates that our verification method is effective and sufficient.
展开▼
机译：ada编译器验证摘要报告。证书编号：900726W1.11017，Verdix Corporation VaDs IBm RIsC system / 6000，aIX 3.1，Vada-110-7171，版本6.0 IBm RIsC system / 6000 model 530 => IBm RIsC system / 6000 model 530
