Secure Delivery of Program Properties Through Optimizing Compilation
Abstract
Annotations and assertions capturing static program properties are
ubiquitous, from robust software engineering to safety-critical or
secure code. These may be functional or non-functional properties of
control and data flow, memory usage, I/O and real time.
We propose an approach to encode, translate, and
preserve the semantics of both functional and non-functional
properties along the optimizing compilation of C to machine
code. The approach involves (1) capturing and translating source-level
properties through lowering passes and intermediate representations,
such that data and control flow optimizations will preserve their
consistency with the transformed program, and (2) carrying properties
and their translation as debug information down to machine code.
Our experiments using LLVM validate the soundness, expressiveness and efficiency of the
approach, considering a reference suite of functional properties
as well as established security properties and applications hardened
against side-channel attacks.
Research Areas
