[2021.07.12] [PLDI 2021] Alive2 Bounded Translation Validation for LLVM

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的修订和改错工作。