C/C++开源静态代码分析及验证工具介绍
【摘要】 本文介绍部分业界知名的面向 C/C++ 的开源的静态代码分析工具或者框架，部分比较好的程序验证工具也会收集。
本文列出部分C/C++静态代码分析及验证工具，会不断完善（主要目的是为了 ① 自研静态代码分析框架，或者 ② 提升检查检查能力或者精度，或者 ③ 在企业内直接选择开源工具集成或者优化使用而收集的，部分小众，或者没有太大参考价值的，就不收集了）。
工具 |
开源协议 |
基础框架 |
检查算法 |
基本情况介绍 |
| Cooddy | GPL v3.0 | clang | 自底向上的数据流+约束求解 | 该框架是华为开源的静态代码分析工具，基于clang生成自研的AST之后，所有的分析都在自研AST上实现，基于自底向上的分析方法，能够有效节省分析时长。推荐指数：5颗星（自底向上的数据流分析、函数摘要的建立等对商业工具有非常大的参考价值） |
| vast | Apache2.0 | clang | 该框架基于LLVM中的MLIR来实现的一个分析框架，面向实现一款商用的SAST工具，我个人并不看好基于纯AST或者完全基于LLVM IR来开发（可以看我之前针对IR的解释），而MLIR就是处于两个中间的一种IR形式。所以虽然当前该框架还不是很成熟，我仍然将其列在靠前的位置。 |
|
| Clang Static Analyzer | Apache2.0 | clang | 符号执行 | 当前最火的一款静态代码分析工具，是llvm-project中的一个模块，很多公司内部自研或者商用的静态代码分析工具，都是基于该检查框架扩展的。推荐指数：5颗星（养活了一大堆的做静态代码分析的公司内部团队或者初创公司） |
| clang-tidy | Apache2.0 | clang | AST | 也是 llvm-project 中的一个模块，主要用于做基于AST的风格类检查，提供了简易扩展接口，可以非常方便地扩展，同时，可以拉起clang static analyzer 的检查，也是企业自研使用非常广的一个框架。推荐指数：5颗星（养活了一大堆的做静态代码分析的公司团队） |
| Klee | NCSA | llvm | 符号执行 | 提到基于 llvm 的符号执行引擎，绝对绕不开 klee，klee 可以自动生成测试用例，同时，klee可以检查漏洞，自发布起，就有大量的论文和研究基于klee展开。虽然有些资料将klee归为动态执行引擎，但是不管怎么样，提到程序分析，到哪里都要klee的一席之地。推荐指数：5颗星（用例生成、缺陷检查、误报确认） |
| IKOS | NASA1.3 | llvm | 抽象解释 | 将 llvm IR 转换为 AR 格式之后，使用 APRON 进行抽象解释运算，当前还在非常活跃地进行开发。推荐指数：5颗星（可以结合实际场景好好学习一下抽象解释是什么） |
| Phasar | MIT | llvm | IFDS/IDE | 基于llvm IR，实现了一套 IFDS/IDE数据流分析框架，同时还支持了一套跨过程的数据流分析框架，是一个非常好的基础框架，只是当前上面没有成熟的检查实现，需要自己以Phasar作为库自己实现。推荐指数：5颗星（我喜欢拿它当学习材料，支持不少的基础框架） |
| SVF | GPL v3.0 | llvm | 该框架基于llvm IR，提供了 PAG、SVFG 等图及相关遍历方式，最大的贡献，就是实现了一系列的指针分析方法，也是目前业界基于 llvm 实现的指针分析最好的框架之一。推荐指数：5颗星（指针分析实现业界最强） | |
| cppcheck | GPL v3.0 | AST | 业界使用非常火的一款静态代码分析工具，不基于编译，是企业内部集成和扩展的相当多的一款工具。而且因为不基于编译，所以使用方便、更易集成，当然，检查能力和精度无法跟上面提到的基于编译的clang-tidy、csa相比。推荐指数：5颗星（企业内部轻量级静态检查首选工具，方便扩展，也养活了一大堆企业内部的静态代码检查团队） | |
| CodeChecker | Apache2.0 | 这款工具集成了 clang-tidy、clang static analyzer、cppcheck 等工具，并且增加了编译捕获、告警可视化等功能，为当前很多初创公司做所谓的SAST工具的经典案例。推荐指数：5颗星（很多企业内部安全部门或者初创公司做产品抄作业的首选） | ||
| SonarQube | LGPL | 这个工具可以很方便地集成其他插件，本身该工具的开源版本自己不提供c/c++检查能力，但是有个开源插件sonar-cxx可以集成其他的能力，方便使用，自己的c/c++检查能力，需要采购商用版本，而且能力也并不突出。推荐指数：5颗星（不是给它自己的检查能力的，而是给它超强的工具集成能力） | ||
| Infer | MIT | 程序验证、抽象解释 |
说老实话，我对这款工具神往已久，只是对OCaml不是很熟悉，所以没有结合代码细研究实现。不过大家有兴趣可以看看他们的论文。推荐指数：5颗星（基于OCaml实现，就是要设置点儿门槛） | |
| CodeQL | 非标协议 | 最大的贡献，是提供了一套看起来非常高大上的DSL实现（目前我知道的能提供DSL的工具，没有能跟它比的），可以简化规则开发，也是该工具的亮点，内部的实现机制，资料来看，是基于Datalog实现，工具的论文，也都是围绕它的DSL（QL）和Datalog展开的。推荐指数：5颗星（牛x的DSL实现和业界少有的基于Datalog实现的检查工具） | ||
| Joern | Apache2.0 | 程序属性图 | 最大的贡献是提供了一个代码属性图，给静态代码分析工具实现开拓了一个新的分支，后续基于该方向的论文和工具也变多了。推荐指数：5颗星（代码属性图领域的开拓者） | |
| SMACK | MIT | llvm + Boogie | 程序验证 | 一种基于 llvm 的程序验证工具，将 llvm IR 转换成 Boogie 的 IVL 后，进行验证。推荐指数：5颗星（程序验证工具） |
【版权声明】本文为华为云社区用户原创内容，转载时必须标注文章的来源（华为云社区）、文章链接、文章作者等基本信息， 否则作者和本社区有权追究责任。如果您发现本社区中有涉嫌抄袭的内容，欢迎发送邮件进行举报，并提供相关证据，一经查实，本社区将立刻删除涉嫌侵权内容，举报邮箱：
cloudbbs@huaweicloud.com
- 点赞
- 收藏
- 关注作者
评论（0）