望安科技为华为公司提供技术培训： 信息安全评估CC及形式化验证技术

4月22日-24日，望安科技在云端为华为公司提供了一场别开生面的培训会，主题为：信息安全评估CC及形式化验证技术。望安科技创始人赵永望教授将多年的研究成果和经验作了为期3天的介绍和分享。

本次培训会华为公司计划已久，受疫情影响，选择通过云端的方式展开。在云端培训会上，赵教授从形式化方法、技术工具与应用，CC认证及CC形式化需求，符合CC 形式化开发与验证框架、Linux操作系统形式化验证等方面作了介绍。向华为公司相关技术专家在形式化技术应用至软件开发、对已开发软件和操作系统如何进行CC验证等内容进行了详细介绍。

   

近几年来，形式化验证和方法在越来越多的领域中得以应用，尤其是保障生命、财产的重大安全领域，包括：航空航天、轨道交通、无人机/车、金融，尤其是最近区块链技术崛起，也是直接的触发因素之一。形式化验证通过清晰无歧义的形式化语言，基于形式验证方法，可以进行全自动的穷举形式验证，去保证系统无 Bug。形式化验证是安全关键系统的最佳伙伴，也是安全关键系统的最佳解决方案。目前，在操作系统和软件开发上被应用的越来越广泛。

随着我国技术自主可控不断提高的安全、自主、可靠性要求，国产操作系统和软件的安全可靠性验证，国家和主要企业都十分重视。如何确保开发的产品是100%安全可信的呢？这必将离不开形式化验证技术。

华为研究所作为国内自主研发的先导企业，本次向望安科技发出关于形式化验证技术的培训需求和邀请，也是基于前期鸿蒙操作系统CC EAL5级认证的认知基础，进一步拓展对自主研发的操作系统和软件的安全性要求。通过这次培训，进一步展示了望安科技在形式化验证领航者的实力，也给望安科技基于形式化技术的安全服务赋予了新的内涵，具有不可替代的重要意义。