Back To Schedule
Monday, April 8 • 12:05pm - 12:30pm
Compilation and optimization with security annotations

Sign up or log in to save this to your schedule, view media, leave feedback and see who's attending!

Program analysis and program transformation systems need to express additional program properties, to specify test and verification goals, and to enhance their effectiveness. Such annotations are typically inserted to the representation on which the tool operates; e.g., source level for establishing compliance with a specification, and binary level for the validation of secure code. While several annotation languages have been proposed, these typically target the expression of functional properties. For the purpose of implementing secure code, there has been little effort to support non functional properties about side-channels or faults. Furthermore, analyses and transformations making use of such annotations may target different representations encountered along the compilation flow.

We extend an annotation language to express a wider range of functional and non-functional properties, enabling security-oriented analyses and influencing the application of code transformations along the compilation flow. We translate this language to the different compiler representations from abstract syntax down to binary code. We explore these concepts through the design and implementation of an optimizing, annotation-aware compiler, capturing annotations from the program source, propagating and emitting them in the binary, so that binary-level analysis tools can use them.


Son Tuan Vu

Sorbonne University

Monday April 8, 2019 12:05pm - 12:30pm CEST