重磅！望安科技发表的自主创新成果论文被International Symposium on Formal Methods录用！

日前，望安科技的自主创新成果论文《Apply Formal Methods in Certifying the SyberX High-Assurance Kernel》被International Symposium on Formal Methods（FM 2021）录用。

FM 2021是由欧洲形式化方法协会（FME）组织的第24届国际研讨会，会议汇聚了来自各国的形式化研究学者，是形式化方法领域的顶级会议。FM 2021强调形式化方法在广泛领域的开发和应用，包括软件、网络物理系统和基于计算机的综合系统。形式化方法以严格的数学化和机械化方法为基础来规约、构建和验证计算系统，是改善和确保计算系统质量的重要方法，其模型、技术和工具已延生成为计算思维的重要载体。

该论文的发布标志着公司形式化验证技术在内核操作系统领域取得重大突破。

论文基于形式化方法在SyberX微内核操作系统的EAL5+认证评估。SyberX是一种操作系统微内核，应用于关键安全和安保领域，如航空电子设备、无人驾驶车辆等。

在论文中，我们将形式化方法应用于基于信息安全评估通用准则 CC（Common Criteria for Information Technology Security Evaluation）的SyberX高保证级别的开发和安全评估。CC是美、日、英等31个国家制定的评估信息安全产品和系统安全特性的基础准则，是当前互信最高的评估信息安全产品和系统安全特性的基础准则。此项认证是第一个在国内进行CC EAL5+认证的操作系统软件。

我们描述了一种基于通用标准为 SyberX 微内核开发形式模型的实用方法。该方法应用于 SyberX 微内核的所有安全相关部分，并为安全策略模型、功能规范和TOE设计规范之间的对应关系提供了形式化模型与证明。

论文发表是公司研发人员智慧的结晶，凝结着公司研发人员在形式化验证技术研究及应用上的成果，也展示了公司技术实力。望安科技将持续提升自主创新能力与核心竞争力，为信息安全产品提供优秀的解决方案和专业的产品及服务，筑牢信息安全产品防线，为信息安全产品保障贡献企业力量。