2019 EuroLLVM Developers’ Meeting: S. Vu “Compilation and optimization with security annotations”
http://llvm.org/devmtg/2019-04/
—
Compilation and optimization with security annotations - Son Tuan Vu (LIP6)
Slides: http://llvm.org/devmtg/2019-04/slides...
—
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.
—
Videos Filmed & Edited by Bash Films: http://www.BashFilms.com