基于CC的安全性规格形式化描述及验证方法

摘要：

随着信息系统在社会生活中越来越重要,越来越必不可缺,人们对信息系统的安全性需求也不断地增加.不允许出现安全性漏洞的非常重要的信息系统,其安全性规格必须要使用形式化方法来描述且验证才是可靠的.介绍了在世界上首先提出的基于国际通用标准CC(ISO/IEC15408)的安全性规格描述及验证方法.把国际通用标准CC中定义的功能元素作为信息安全性评价标准,用形式化规格描述语言Z和时序逻辑来进行形式化描述.另一方面,用UML把保护轮廓PP模式化,并在用Z形式化地描述了目标信息系统的安全性规格之后,采用定理证明方法和模型检测方法来对目标系统的安全性规格进行形式化验证.为了让只具备基础知识的验证者也能够轻松使用该方法,开发了其支援工具FORVEST.

关键词：安全性规格、CC、Z、时序逻辑.、形式化、验证方法

所属期刊栏目：3

分类号：TP301.2(计算技术、计算机技术)

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

页数：共7页

页码：617-623