TY  - JOUR
T1  - Lightweight Equivalence Checking of Code Transformation for Code Pointer Integrity
AU  - Lee, Jaeseo 
AU  - Choi, Tae-Hyoung 
AU  - Lee, Gyuho 
AU  - Yu, Jaegwan 
AU  - Bae, Kyungmin 
JO  - Journal of KIISE, JOK
PY  - 2019
DA  - 2019/1/14
DO  - 10.5626/JOK.2019.46.12.1279
KW  - code transformation
KW  - translation validation
KW  - code pointer integrity
AB  - 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.