形式化解决方案

 方案类型 

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


 面向 IT 开发厂商和关联领域的客户，提供完整的形式化方法、技术和工具的培训和咨询服务。


 包括模型检验、定理证明等基本方法，面向系统的需求、架构、设计等形式化建模与验证，程序形式化验证技术，以及 Event-B、SPIN、NuSMV、PAT、Isabelle/HOL、Frama-C/Why 等工具。



 形式化验证项目总体方案设计


 针对基础软、硬件的形式化验证面向应用系统的形式化验证等，提供整体方案咨询和设计服务。结合客户具体的安全目标，设计特定的形式化验证解决方案，并整合本公司和第三方的形式化验证工具，设计具体实施办法、评价指标体系等。




    安全评测


    为CC EAL 5+以上认证提供评估服务。

    轨道交通


    为轨道交通安全认证、应用软件安全认证提供评估服务。


    国防


    为国防软件安全认证提供评估服务。


    区块链


    为数字金融企业安全认证提供评估服务。


    航空航天


    为航空航天软件系统安全认证提供评估服务。


    芯片设计


    为芯片设计安全认证提供评估服务。


    车联网


    以车内网、车际网和车载移动互联网为基础的通信协议和数据交互


    互联网金融


    为支付设备、应用软件安全认证提供评估服务。

 形式化代码审计服务


  基于形式化验证技术对代码进行安全审计，确保代码实现与设计和需求的一致性及自身的安全性，出具审计报告。



 国内外安全认证标准、操作系统标准的咨询与服务


 1.Common Criteria (对应国标)、DO-178 B/C 安全认证标准的形式化方法、技术、工具和应用的研发。

 

 2.ARINC 653 标准咨询与服务。



形式化解决方案是结合客户具体的安全目标，设计特定的形式化验证解决方案，并整合本公司和第三方的形式化验证工具，设计具体实施办法、评价指标体系等​​​​​