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産品視訊講解
視訊加載中...