典型安全网关的形式化设计与证明

摘要：

传统上依靠经验设计的安全网关侧重于功能实现,缺少严格的安全模型.对此,针对一种典型安全网关,首先根据其安全需求给出相应的安全策略,然后利用BLP模型对给出的安全策略进行形式化建模并对安全模型的内部一致性进行证明,最后对安全网关的功能规约和安全模型的一致性进行验证.为保证推理过程的正确性,使用定理证明器Isabelle/HOL对上述过程进行描述和推理,保证了安全网关顶层设计的安全性.研究结果为安全网关的形式化设计提供了一定的借鉴意义.

关键词：典型安全网关、形式化设计、BLP模型、功能规约、一致性验证、Isabelle/HOL

所属期刊栏目：44

分类号：TP309.1(计算技术、计算机技术)

资助基金：面向用户的可信云计算环境安全研究61572517

在线出版日期：2017-10-20（万方平台首次上网日期，不代表论文的发表时间）

页数：共6页

页码：142-147