Secure delivery of program properties through optimizing compilation - Sorbonne Université
Conference Papers Year : 2020

Secure delivery of program properties through optimizing compilation

Arnaud de Grandmaison
  • Function : Author
  • PersonId : 1049419
Albert Cohen

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.

Dates and versions

hal-02931645 , version 1 (07-09-2020)

Identifiers

Cite

Son Tuan Vu, Karine Heydemann, Arnaud de Grandmaison, Albert Cohen. Secure delivery of program properties through optimizing compilation. CC '20: 29th International Conference on Compiler Construction, Feb 2020, San Diego, CA, United States. pp.14-26, ⟨10.1145/3377555.3377897⟩. ⟨hal-02931645⟩
150 View
3 Download

Altmetric

Share

More