C代码自动化验证平台（W-AVC）
产品功能：
W-AVC是⼀款C语⾔代码程序的形式化验证云平台。平台基于形式化验证技术，通过数学证明排查代码中的缺陷和安全隐患 ；同时通过开发验证⼈员编写的规约基准代码，⾃动检查代码中的安全漏洞，从而在开发流程的早期增强系统的安全性，减少现代⼤型软件架构带来的⻛险。
1、运行时安全
⾃动检查算术溢出、除零错误、指针越界、指针解引⽤错误等。
2、功能正确性
根据描述接口设计的规约代码，检查代码实现与需求设计是否一致。
形式化验证：
形式化验证是指根据代码的形式规范或属性，使⽤数学的⽅法证明其正确性或⾮正确性的⼀种技术⼿段。相较传统的程序分析⼿段，形式化验证⾄少具备以下特点：
1、无需测试用例
通过前后置条件对输⼊输出进⾏形式化描述，不再需要构造单独测试⽤例。
2、严格数学证明
通过模型检查、定理证明等手段，配合 SAT/SMT 求解器，对待验证命题进行严格证明。
3、提供错误反例
对被违反的规约性质，通常可以提供完整的反例和错误发⽣路径。
免费试用：
登陆 w-avc.wonsec.com,申请免费试⽤。
01
更轻，迅速上手
云端部署
项目云端验证，支持私有云部署，省去繁琐环境配置工作。为企业用户私有云等定制化服务。
C语法规约
规约完全采用C语言语法，无需为消耗额外语言学习成本，开发测试人员无缝上手。
02
更易，贴近工程
规约分离
W-AVC实现了项目源代码与验证代码分离，支持桩函数等实践方法论，开发、验证代码互不干扰，提升开发/验证管理效率。
多任务管理
平台支持证任务并行验证和中断操作，全方位升级验证工程效率。
03
更安全，形式化验证保驾护航
形式化验证
W-AVC采用学界领先的形式化验证技术，无需专门设计测试用例，验证通过可百分百确保规约满足性，用数学证明保证无漏洞。
验证报告中，对错误提供反例和生成路径，方便定位问题、调试代码。
04
W-AVC成功案例
1 操作系统
操作系统是航空航天、国防、⽆⼈⻋、⽆⼈机、物联⽹等系统的基础软件，它位于计算机系统软件栈的底层，操作系统的错误可能导致系统奔溃、被攻击等问题，涉及功能安全和信息安全等问题。操作系统功能结构复杂，多核多任务的并发度⾼，开发与调试都⼗分困难，⼀些隐藏的错误⽤常⻅的软件测试技术难以发现。
望安科技利⽤本产品验证了多个国产操作系统和国外开源操作系统，发现了⼤量操作系统源代码中的错误，并且有⼒⽀撑了相关操作系统产品的⾼安全级别认证，被验证的操作系统⼴泛应⽤与大陆航天、⽹络通信、物联⽹、轨道交通、⽆⼈机、⽆⼈⻋和⼿机等。
2 军科院嵌入式系统
操作系统是航空航天、国防、⽆⼈⻋、⽆⼈机、物联⽹等系统的基础软件，它位于计算机系统软件栈的底层，操作系统的错误可能导致系统奔溃、被攻击等问题，涉及功能安全和信息安全等问题。操作系统功能结构复杂，多核多任务的并发度⾼，开发与调试都⼗分困难，⼀些隐藏的错误⽤常⻅的软件测试技术难以发现。
望安科技利⽤本产品验证了多个国产操作系统和国外开源操作系统，发现了⼤量操作系统源代码中的错误，并且有⼒⽀撑了相关操作系统产品的⾼安全级别认证，被验证的操作系统⼴泛应⽤与大陆航天、⽹络通信、物联⽹、轨道交通、⽆⼈机、⽆⼈⻋和⼿机等。
3 载人航天项目
载⼈航天⼯程已经进⼊第三个阶段，即空间站⼯程阶段。空间站⼯程中软件数量激增，已调研的研制单位汇报的配置项已经达到上千个；软件规模增⼤，中⼤规模的软件⽐例增加较多；技术难度更⼤，可靠性、安全性要求⾼，涉及⻓期在轨运⾏等要求；对软件研制能⼒有更⾼要求。对任务有重要影响的A/B级软件数量上激增。
针对载⼈航天⼯程⾯临的重⼤技术问题，望安采⽤该⼯具对某航天器软件需求和嵌⼊式软件源代码、某控制器软件进⾏形式化验证和检测，发现并修复了应⽤案例中的多个关键错误，相关成果得到了航天院所的⾼度评价。
4 航天压力控制系统
压⼒系统是航天空间轨道系统⾄关重要的⼀环，系统对实时性可靠性等性质有较⾼的要求。现有的软件分析验证⽅法难以满⾜软件的安全性和可靠性需求。⼯程的软件研制过程中，软件的分析验证主要依赖⼈⼯⽅式完成，⽆法保证软件的分析验证的完备性、正确性、⼀致性。
望安与某航天院合作，定制提供了形式化整体解决⽅案， ⽅案中对系统的氧箱增压控制模块进⾏了双层形式化建模，并采⽤⼯具对模块代码进⾏了形式规约与验证，确保了系统全⽣命周期安全，同时优化安全有关软件开发流程，提⾼了测试效率与可靠性。
05
W-AVC产品视频讲解
视频加载中...