Details

Autor(en) / Beteiligte

• Panigrahi, Priyanka
• Paul, Abhik
• Karfa, Chandan

Titel

Quantifying Information Leakage for Security Verification of Compiler Optimizations

Ist Teil von

• IEEE transactions on computer-aided design of integrated circuits and systems, 2022-11, Vol.41 (11), p.1-1

Ort / Verlag

New York: IEEE

Erscheinungsjahr

2022

Link zum Volltext

• Volltext

Quelle

IEEE Electronic Library (IEL)

Beschreibungen/Notizen

• Compiler optimizations can be functionally correct but not secure. In this work, we attempt to quantify the information leakage in a program for the security verification of compiler optimizations. Our work has the following contributions: We demonstrate that static taint analysis is applicable for security verification of compile optimizations. We develop a completely automated approach for quantifying the information leak in a program in the context of compiler optimizations. Our method avoids many false-positives scenarios due to implicit flow. It can handle leaks in a loop and propagates leaks over paths using the leak propagation vector. With our quantification parameters, we verify the relative security of source and transformed programs considering the optimizations phase of a compiler as a black box. Our experimental evaluations on benchmarks for various compiler optimizations in SPARK show that the SPARK compiler is actually leaky.