Jaeseo Lee  Tae-Hyoung Choi  Gyuho Lee  Jaegwan Yu  Kyungmin Bae

10.5626/JOK.2019.46.12.1279

code transformation translation validation code pointer integrity

Code transformation is widely used to improve the performance and security of programs, but serious software errors can occur in this process if the generated program is not equivalent to the original program. There are a number of approaches for translation validation that can be used to prove the equivalence of programs, but the high cost of proof checking restricts the applicability of these techniques for large programs. In this paper, we propose a practical approach for checking the correctness of LLVM code transformation. We first prove the correctness of the transformation rules using automated theorem proving before compilation. We then perform a simple code analysis method—as opposed to directly proving the program equivalence— to check whether the transformations rules are correctly applied to the generated code. As the complexity of the proposed code analysis is linear, our technique can be effectively applied to large programs, unlike previous techniques. To prove the effectiveness of the proposed approach, we present a case study on LLVM code transformation for a code pointer integrity instrumentation.