Sie befinden Sich nicht im Netzwerk der Universität Paderborn. Der Zugriff auf elektronische Ressourcen ist gegebenenfalls nur via VPN oder Shibboleth (DFN-AAI) möglich. mehr Informationen...
The functional correctness of compiler optimization does not ensure the security properties of the source program. A functionally correct compiler optimization may introduce new security vulnerabilities in the optimized program. In a compiler, ensuring the security of every optimization is a challenging task as it applies hundreds of optimizations. Thus, this work aims to develop a translation validation of information leakage for the optimization phase of the compiler without considering any intermediate information from the compiler. Our method measures the information leakage in a path, uses a concept of leak propagation over paths and loops, and defines the relative security between the source and optimized programs. This work considers two attack models based on different observation points to access the local memory and proposes different translation validation approaches. The correctness and complexity of the translation validation method are also provided. The experimental results in the SPARK compiler on various benchmarks show that the optimized program is not relatively secure in many cases.