CC信息安全评估的形式化服务案例

CC要求结合开发者自证及评估者他证的做法，来论证IT产品的安全措施是充分的，正确的，从而可以有效地抵抗已知的威胁。

望安科技拥有形式化验证核心技术，可提供安全关键系统、网络、软件形式化验证技术，覆盖需求、设计、源代码的系统级形式化验证技术，支持多核、中断、抢占的并发系统验证技术，支持多任务并发的源代码完全形式化验证技术。对嵌入式实时操作系统可提供形式化验证，可广泛应用于航空、航天，物联网、5G、互联网金融终端等。公司产品与服务范围涵盖操作系统、安全关键系统及软件的形式化验证与安全认证，形式化方法、技术、工具和应用的研发，Common Criteria认证实施，形式化方法、技术、工具和应用的咨询与服务，形式化代码审计服务，形式化验证项目总体方案、ARINC653标准咨询与服务等。

一、望安科技结合CC认证可提供的主要产品和服务

1.Common Criteria（对应国标）认证实施，尤其是CC等级评估形式化验证服务：EAL5/6/7级。

按照EAL高等级评估的要求，提供形式化/办形式化的设计与测试。包括：对验证产品提供完整的安全策略、安全需求、功能规范和模块设计的形式化/半形式化模型，并进行模型的安全性验证。按照EAL评估要求，编写相应文档。对验证产品提供安全需求、功能规约及设计等。

2.系统、软件安全保障测评前验证服务：EAL1/2/3/4级。

对测评产品提供安全策略、安全需求、功能规约及设计等，查找需求、设计、实现等各个阶段中存在的安全缺陷和隐患，分析并给出修复建议。编写评估文档，配合评估机构的评估实施。

3.形式化方法、技术、工具和应用的咨询与培训。

面向IT开发厂商和关联领域的客户，提供完整的形式化方法、技术和工具的培训和咨询服务。包括模型检验、定理证明等基本方法，面向系统的需求、架构、设计等形式化建模与验证，程序形式化验证技术，以及Event-B、SPIN、NuSMV、PAT、Isabelle/HOL、Frama-C/Why等工具。

4.开发、验证、认证工具。

公司已形成一套相对成熟的开发和验证工具。分别为安全关键C代码自动化验证工具、并发系统形式化验证工具、满足Common Criteria的系统形式化开发与认证证据工具以及安全关键系统模型驱动开发、验证、代码生成工具集。

二、CC EAL5-7服务案例：Linux内核安全模块

操作系统提供了确保计算机处理安全的基本机制。随着Linux在各种安全环境中的应用，其安全机制越来越受到工业界的重视。Linux安全模块（LSM）在Linux 2.6版本之后被Linux内核接受成为内核安全机制的标准，在各个Linux发行版中提供给用户使用。LSM是Linux内核的一个轻量级通用访问控制框架。它使得各种不同的安全访问控制模型能够以Linux可加载模块的形式实现出来，用户可以根据其需求选择适合的安全模块加载到Linux内核中，从而大大提高了Linux安全访问控制机制的灵活性和易用性。目前已经有很多著名的增强访问控制系统移植到Linux安全模块上实现，包括SELinux、Smack、TOMOYO、AppArmor、Yama等。

为了支持Linux内核安全模块的CC认证，我们开发了一个符合EAL 5/6/7要求的LSM验证框架 —— VeriLSM。VeriLSM框架首先包含一个通用的形式化安全策略模型，来满足相应的形式化安全性质要求，它们对应CC中的安全策略和安全目的。另外，VeriLSM提供一个与内核LSM一致的形式化模型，对应CC中的功能规范(FSP)。VeriLSM的形式化FSP模型提供了参数化的能力，它对于所有LSM实现是通用的，可以通过模型的实例化得到具体LSM实现的设计模型。最后针对LSM的具体实现，如Smack模块等，VeriLSM提供相应的形式化设计层模型，对应CC中的设计(TDS)。为了满足EAL7的要求，VeriLSM提供了CC认证所需的全部形式化证据。

浙江望安科技有限公司是国内一家以形式化验证为核心技术的安全服务企业；企业致力于为国家重大项目、核心软件及企业提供安全认证保障。

公司自主研发的安全产品，可面向航空、航天、国防、区块链、互联网金融、区块链、物联网、工业控制、芯片设计制造、轨道交通等重大领域。该核心技术已应用于C919国产大飞机、载人航天工程、中航工业集团、航天科技集团等。

高安全可靠性、高安全等级认证，都离不开形式化验证；通过形式化验证，达到零bug。