Source: https://www.cs.utah.edu/~regehr/alive2-pldi21.pdf
Authors: Nuno P. Lopes Juneyoung Lee Chung-Kil Hur Zhengyang Liu John Regehr
Download Note: https://jbox.sjtu.edu.cn/l/aF3N9R
Contributor: pdh
Overview
Alive2是一个针对LLVM IR的有界翻译验证(bounded translation validation)工作，是一个纯自动化的工具。它通过对程序的资源消耗进行限制，例如将循环展开成某个特定的次数，到达某个可能触发漏洞的边界。Alive2可以避免误报，是一个全自动化的使用SMT求解器的工具，并且无需对LLVM做任何的修改。Alive2检测出了LLVM中存在的47个新的漏洞，其中28个修复了。除此之外，还对LLVM的语言参考，也就是IR的语义定义，打了8个补丁，并且参与了很多LLVM的修订和改错工作。