AbsInt—確保代碼安全的靜態性能分析工具

        德國AbsInt公司是專注于安全苛求軟件研發、確認、驗證和認證的工具鏈供應商。能夠為客戶提供完整的確保代碼安全的性能分析工具套件以及軟件分析、驗證、確認和編譯器技術相關咨詢服務。AbsInt產品廣泛地應用于工業、交通、汽車、 軌交、通信和能源等行業的安全苛求軟件研發過程中。 

產品介紹 
        AbsInt代碼安全性能分析套件主要包括以下幾種產品：

• aiT WCET Analyzer/ 最差情況執行時間分析工具
• StackAnalyzer/最差情況堆棧使用量分析工具
• TimingProfiler/代碼執行時間分析工具
• Astrée/C代碼運行時錯誤和數據競爭檢查工具
• RuleChecker/C代碼規則檢查工具
• CompCert/形式化方法驗證的優化C語言編譯器

二進制代碼分析工具

• aiT

        針對特定的處理器和編譯器，能夠分析出較接近實際運行情況的最差執行時間，真實反映系統性能。在分析過程中充分考慮了高速緩存和流水線（pipeline）的影響，從而避免了過于保守的WCET值，亦即避免了硬件資源的浪費。

• StackAnalyzer

        針對特定的處理器族和編譯器，能夠自動分析出任務的最差堆棧使用量，即避免了人為低估造成的堆棧溢出，又避免了人為高估而造成的資源浪費。

• TimingProfiler

        針對特定的處理器族和編譯器，能夠從初期開始對代碼執行時間進行持續分析和評估。

• 特點

? 代碼靜態分析工具，可直接導入編譯后的.elf/*.out等二進制可執行文件進行自動分析，不會對現有的工具鏈造成影響
? 圖形化顯示程序的調用和控制流及不同程序點的機器狀態，為優化提供依據
? 遍歷所有程序執行路徑，對所有場景有效，無需提供測試用例
? 支持批量測試，支持Jenkins，可實現軟件持續集成測試
? aiT和StackAnalyzer有認證支持包，能夠提供認證支持服務（ISO-26262,IEC-61508,EN-50128等）

C代碼分析工具

• Astrée

? Astrée能夠確保找出所有的代碼運行時錯誤(run-time error)和數據競爭(data race)問題，控制流和數據流基本達到100%的覆蓋度
? Astrée分析方法，確保較低的誤報率
? Astrée在分析過程中能夠考慮OSEK\AUTOSAR等OS配置環境的影響，提高分析結果精確度
? Astrée的分析結果支持交互式瀏覽，能夠幫助用戶迅速定位問題，并進行備注及修改
? Astrée可與dSPACE TargetLink實現無縫集成
? Astrée有認證支持包，能夠提供認證支持服務（ISO-26262,IEC-61508,EN-50128等）

• RuleChecker RuleChecker是C代碼規則檢查工具，支持以下代碼規則標準：

? MISRA 2004、2012、2012Amendment 1 
? ISO/IEC TS17961:2013 
? SEI CERT Secure C 
? MITRE CWE 
? 客戶訂制標準 

應用&案例

• 豐田汽車非預期加速事件調查，2010年aiT被NASA作為工業標準靜態分析工具用于豐田汽車公司非預期加速事件調查，以排除與時間相關的軟件缺陷
• Daimler在動力總成控制系統等多個軟件研發項目中，成功運用StackAnalyzer工具進行相關分析，在研發前期即對軟件的堆棧使用量情況進行有效分析和預估，避免了堆棧溢出等問題造成的項目延期和成本損失