出具证明编译器中代码优化与程序规范转换

Code Optimization and Specification Transformation in Certifying Compiler

出具证明编译器在软件安全研究得到越来越多的关注,是程序验证研究的一个重要方向.但目前关于出具证明编译器的研究主要是在程序逻辑设计和定理自动化证明方面,很少关注编译优化对规范的影响.而编译优化是决定出具证明编译器是否能走向应用的关键因素之一.通过研究数据流优化的基本行为,提出利用数据流分析结果来变换规范的方法,以使原规范的约束准确而充分地施加于优化后的代码,并实现了一个包含多种优化和相应规范转换的编译器原型系统,展示了方法的可行性.

As an important research field of program verification, certifying compiler is an increasing concern by many researchers of software security. However, current researches mostly focus on the design of program logic and automated theorem proving, while code optimization which we believe is significant for certifying compiler to become practical, is less concerned by the community. In this paper, we propose a dataflow analysis based method to transform specification to pass the constraint of original specification to the optimized code. We also develop a prototype compiler with multiple optimizations to demonstrate the feasibility of our approach.