高安全评估形式化工具

W-Cert（高安全评估形式化工具Wonsec Certification）是满足CC标准全部形式化建模与验证需求的高可信形式化开发工具，可有效支持CC标准中安全策略SPM（Security Policy Model）、功能规约FSP（Function Specification）与TOE设计TDS（TOE Design）的形式化建模与验证任务，并可生成模型对应的相关评估证据供第三方评估机构使用。

该工具使得符合CC标准的形式化建模和验证工作可信且高效，极大降低开发人员对CC标准和形式化技术的掌握程度，使开发人员可以专注于产品本身的特点和功能。

W-Cert包含完整的符合CC标准的安全功能要求SFRs（Security Functional Requirements），可根据安全目标ST（Security Target）自由组合，得到符合CC标准的形式化安全策略模型SPM（Security Policy Model）。

W-Cert提供了灵活的方式方便地进行FSP的形式化模型的建模与验证。用户可自由选择State Monad方式或Isabelle进行形式化建模和验证。通常复杂系统采用预定义的通用形式化模型State Monad进行建模，简单系统则采用Isabelle进行建模。

W-Cert采用预定义通用形式化模型State Monad进行建模和验证。State Monad通过预定义的模型和预验证的证明可以大大减轻构建复杂形式化模型的工作量。不仅如此，State Monad创新性地提供了与代码实现更为相近的模型提供方法，从而减少了评估人员对照形式化模型进行代码审查的工作量。

W-Cert支持直接在形式化模型中增加注释，并且根据注释生成符合CC标准的评估证据，大幅度降低开发人员提供评估证据的工作量。

W-Cert根据CC标准进行开发研制，符合国际标准ISO/IEC 15408，且符合中国国家GB/T 18336。且满足EAL5/6/7对代码审查的严格要求。

W-Cert功能全面，可覆盖CC标准全部的形式化建模与验证需求。具有严格定义形式化语法语义，在W-Cert中构建的模型、进行的验证完全符合EAL 5/6/7对形式化要求。

符合标准

可信、可定制

W-Cert的建模和验证过程完全可信，可进行自动检查；且W-Cert作为开源软件，支持客户的定制化开发。

提升效率

W-Cert可提高形式化建模和验证的复用率，可大幅提高形式化建模和验证效率；可生成符合CC要求的评估证据证据文档，减少开发人员工作量。

功能全面