Security Verification of Compiler Optimizations: An Information Flow Perspective

Simple item page
dc.contributor.authorPanigrahi, Priyanka
dc.date.accessioned2025-01-10T11:20:40Z
dc.date.available2025-01-10T11:20:40Z
dc.date.issued2024
dc.descriptionSupervisor: Kafra, Chandan
dc.description.abstractModern compilers like GCC, LLVM apply various optimizations on the source program to improve the performance of the target code for execution time, code size, resource usage, memory usage, etc. One of its critical requirements is to generate a functional equivalent target code. A target code generated after application of compiler optimization may be functionally equivalent to the source program but it may not be as secure as the source program (i.e., relatively secure). Therefore, it is essential to ensure that the optimized code does not introduce any security vulnerability during the optimization phase. This thesis aims to verify the relative security between the source and optimized programs, irrespective of the optimizations applied by a compiler. Specifically, the information flow is considered as the security property in a program in this thesis. To achieve relative security, we first aim to quantify the information leakage in a program using static taint analysis. Then, we propose a bisimulation method for translation validation of information leakage for relative security verification between a source and an optimized program. The next work explores how a model checker can be utilized to quantify the information leakage in a program. The model checking based security analysis method can further be applied to translation validation of information leakage for relative security verification between the source and optimized programs. With our notion of relative security, we have shown that the register allocation step in a compiler is not secure in the presence of spilling. We then propose a secure register allocation approach for the LLVM compiler framework. Finally, this thesis aims to protect these registers from information leakage, specifically from scan-based attacks.
dc.identifier.otherROLL NO.176101006
dc.identifier.urihttps://gyan.iitg.ac.in/handle/123456789/2786
dc.language.isoen
dc.relation.ispartofseriesTH-3346
dc.titleSecurity Verification of Compiler Optimizations: An Information Flow Perspective
dc.typeThesis
Files
Original bundle
Now showing 1 - 2 of 2
No Thumbnail Available
Name:
Abstract-TH-3346_176101006.pdf
Size:
107.5 KB
Format:
Adobe Portable Document Format
Description:
ABSTRACT
Download
No Thumbnail Available
Name:
TH-3346_176101006.pdf
Size:
4.55 MB
Format:
Adobe Portable Document Format
Description:
THESIS
Download
License bundle
Now showing 1 - 1 of 1
No Thumbnail Available
Name:
license.txt
Size:
1.71 KB
Format:
Item-specific license agreed to upon submission
Description:
Download
Collections
PhD Theses (Computer Science and Engineering)