德国absint 公司是全球安全苛求软件研发、确认、验证和认证工具链供应商。能够为客户提供完整的确保代码安全的性能分析工具套件以及软件分析、验证、确认和编译器技术相关咨询服务。absint 产品广泛地应用于汽车等行业的安全苛求软件研发过程中。
产品介绍
absint 代码安全性能分析套件主要包括以下几种产品：
• ait wcet analyzer/最差情况执行时间分析工具
• stackanalyzer /最差情况堆栈使用量分析工具
• timingprofiler/代码执行时间分析工具
• astrée/c代码运行时错误和数据竞争检查工具
• rulechecker/c代码规则检查工具
• compcert/形式化方法验证的优化c语言编译器
二进制代码分析工具
1. ait、stackanalyzer和timingprofiler
• ait针对特定的处理器和编译器，能够分析出接近实际运行情况的最差执行时间，真实反映系统性能。在分析过程中充分考虑了高速缓存和流水线（pipeline）的影响，从而避免了过于保守的wcet值，亦即避免了硬件资源的浪费
• stackanalyzer 针对特定的处理器族和编译器，能够自动分析出任务的最差堆栈使用量，即避免了人为低估造成的堆栈溢出，又避免了人为高估而造成的资源浪费
• timingprofiler 针对特定的处理器族和编译器，能够从初期开始对代码执行时间进行持续分析和评估
2. 特点
• 代码静态分析工具，可直接导入编译后的.elf/*.out等二进制可执行文件进行自动分析，不会对现有的工具链造成影响图形化显示程序的调用和控制流及不同程序点的机器状态，为优化提供依据
• 遍历所有程序执行路径，对所有场景有效，无需提供测试用例
• 支持批量测试，支持jenkins，可实现软件持续集成测试
• ait和stackanalyzer有认证支持包，能够提供认证支持服务（ do-178b, iso-26262, iec-61508, en-50128 等
c 代码分析工具
1. astrée
• astrée 能够确保找出所有的代码运行时错误 (run-timeerror) 和数据竞争(data race) 问题，控制流和数据流达到100% 的覆盖度
• astrée高效分析方法，确保极低的误报率
• astrée 在 分 析 过 程 中 能 够 考 虑 arinc653osekautosar 等os 配置环境的影响，提高分析结果精确度
• astrée的分析结果支持交互式浏览，能够帮助用户迅速定位问题，并进行备注及修改
• astrée可与dspace targetlink实现无缝集成
• astrée有认证支持包，能够提供认证支持服务（do-178b,iso-26262, iec-61508, en-50128 等）
2. rulechecker
• rulechecker 是c 代码规则检查工具，支持以下代码规则标准：
• misra 2004、2012、2012 amendment 1
• iso/iec ts 17961:2013
• sei cert secure c
• mitre cwe
• 客户订制标准
应用& 案例
• daimler在动力总成控制系统等多个软件研发项目中，成功运用stackanalyzer 工具进行相关分析，在研发前期即对软件的堆栈使用量情况进行有效分析和预估，避免了堆栈溢出等问题造成的项目延期和成本损失