Reconciling Optimization with Secure Compilation

被引:3
|
作者
Son Tuan Vu [1 ]
Cohen, Albert [2 ]
De Grandmaison, Arnaud [3 ]
Guillon, Christophe [4 ]
Heydemann, Karine [1 ]
机构
[1] Sorbonne Univ, CNRS, LIP6, 4 Pl Jussieu, F-75252 Paris, France
[2] Google, Paris, France
[3] Arm, Paris, France
[4] STMicroelectronics, Grenoble, France
来源
PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL | 2021年 / 5卷
关键词
compilation; security; optimization; debugging; LLVM;
D O I
10.1145/3485519
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
Software protections against side-channel and physical attacks are essential to the development of secure applications. Such protections are meaningful at machine code or micro-architectural level, but they typically do not carry observable semantics at source level. This renders them susceptible to miscompilation, and security engineers embed input/output side-effects to prevent optimizing compilers from altering them. Yet these side-effects are error-prone and compiler-dependent. The current practice involves analyzing the generated machine code to make sure security or privacy properties are still enforced. These side-effects may also be too expensive in fine-grained protections such as control-flow integrity. We introduce observations of the program state that are intrinsic to the correct execution of security protections, along with means to specify and preserve observations across the compilation flow. Such observations complement the input/output semantics-preservation contract of compilers. We introduce an opacification mechanism to preserve and enforce a partial ordering of observations. This approach is compatible with a production compiler and does not incur any modification to its optimization passes. We validate the effectiveness and performance of our approach on a range of benchmarks, expressing the secure compilation of these applications in terms of observations to be made at specific program points.
引用
收藏
页数:30
相关论文
共 50 条
  • [1] Witnessing Secure Compilation
    Namjoshi, Kedar S.
    Tabajara, Lucas M.
    VERIFICATION, MODEL CHECKING, AND ABSTRACT INTERPRETATION, VMCAI 2020, 2020, 11990 : 1 - 22
  • [2] Robustly Safe Compilation, an Efficient Form of Secure Compilation
    Patrignani, Marco
    Garg, Deepak
    ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 2021, 43 (01):
  • [3] Secure Compilation to Modern Processors
    Agten, Pieter
    Strackx, Raoul
    Jacobs, Bart
    Piessens, Frank
    2012 IEEE 25TH COMPUTER SECURITY FOUNDATIONS SYMPOSIUM (CSF), 2012, : 171 - 185
  • [4] Secure compilation and hyperproperty preservation
    Patrignani, Marco
    Garg, Deepak
    2017 IEEE 30TH COMPUTER SECURITY FOUNDATIONS SYMPOSIUM (CSF), 2017, : 392 - 404
  • [5] A Categorical Approach to Secure Compilation
    Tsampas, Stelios
    Nuyts, Andreas
    Devriese, Dominique
    Piessens, Frank
    COALGEBRAIC METHODS IN COMPUTER SCIENCE, CMCS 2020, 2020, 12094 : 155 - 179
  • [6] Secure Compilation of Constant -Resource Programs
    Barthe, Gilles
    Blazy, Sandrine
    Hutin, Remi
    Pichardie, David
    2021 IEEE 34TH COMPUTER SECURITY FOUNDATIONS SYMPOSIUM (CSF 2021), 2021, : 237 - 248
  • [7] Secure Compilation to Protected Module Architectures
    Patrignani, Marco
    Agten, Pieter
    Strackx, Raoul
    Jacobs, Bart
    Clarke, Dave
    Piessens, Frank
    ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 2015, 37 (02):
  • [8] Reconciling Compiler Optimizations and WCET Estimation Using Iterative Compilation
    Dardaillon, Mickael
    Skalistis, Stefanos
    Puaut, Isabelle
    Derrien, Steven
    2019 IEEE 40TH REAL-TIME SYSTEMS SYMPOSIUM (RTSS 2019), 2019, : 133 - 145
  • [9] Formal Approaches to Secure Compilation: A Survey of Fully Abstract Compilation and Related Work
    Patrignani, Marco
    Ahmed, Amal
    Clarke, Dave
    ACM COMPUTING SURVEYS, 2019, 51 (06)
  • [10] HyCC: Compilation of Hybrid Protocols for Practical Secure Computation
    Buescher, Niklas
    Demmler, Daniel
    Katzenbeisser, Stefan
    Kretzmer, David
    Schneider, Thomas
    PROCEEDINGS OF THE 2018 ACM SIGSAC CONFERENCE ON COMPUTER AND COMMUNICATIONS SECURITY (CCS'18), 2018, : 847 - 861