形式验证在高级别安全认证中的应用


高级别安全认证强烈推荐或强制使用形式验证。在很多行业认证标准中，对形式化方法的使用都越来越重视。如：IEC 61508、DO-178 C、ISO 26262、CC等对形式化方法的使用均作出了具体的规定。
IEC 61508随着认证系统的安全等级逐渐提高，形式化方法的使用程度也逐步提升，如下图所示：

IEC 61508认证对形式化方法使用的要求



SIL 4强烈推荐在系统和软件的各阶段采用形式化方法来进行开发和验证。Common Criteria的EAL 6/7则强制要求在软件研制的各阶段采用形式化方法，如下图所示。2012年颁布的DO-178 C标准，增加了DO-333 “形式化方法”附件，对系统研发过程中的形式化方法应用提出具体要求。

Common Criteria认证对形式化方法使用的要求