What You Get is What You C: Controlling Side Effects in Mainstream C Compilers
- 1 April 2018
- conference paper
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
Abstract
Security engineers have been fighting with C compilers for years. A careful programmer would test for null pointer dereferencing or division by zero; but the compiler would fail to understand, and optimize the test away. Modern compilers now have dedicated options to mitigate this. But when a programmer tries to control side effects of code, such as to make a cryptographic algorithm execute in constant time, the problem remains. Programmers devise complex tricks to obscure their intentions, but compiler writers find ever smarter ways to optimize code. A compiler upgrade can suddenly and without warning open a timing channel in previously secure code. This arms race is pointless and has to stop. We argue that we must stop fighting the compiler, and instead make it our ally. As a starting point, we analyze the ways in which compiler optimization breaks implicit properties of crypto code; and add guarantees for two of these properties in Clang/LLVM. Our work explores what is actually involved in controlling side effects on modern CPUs with a standard toolchain. Similar techniques can and should be applied to other security properties; achieving intentions by compiler commands or annotations makes them explicit, so we can reason about them. It is already understood that explicitness is essential for cryptographic protocol security and for compiler performance; it is essential for language security too. We therefore argue that this should be only the first step in a sustained engineering effort.Keywords
This publication has 28 references indexed in Scilit:
- Crellvm: verified credible compilation for LLVMPublished by Association for Computing Machinery (ACM) ,2018
- Verified low-level programming embedded in F*Proceedings of the ACM on Programming Languages, 2017
- Securing the SSA TransformLecture Notes in Computer Science, 2017
- Sanitizing Sensitive Data: How to Get It Right (or at Least Less Wrong…)Lecture Notes in Computer Science, 2017
- When Constant-Time Source Yields Variable-Time Binary: Exploiting Curve25519-donna Built with MSVC 2015Published by Springer Science and Business Media LLC ,2016
- Securing a Compiler TransformationPublished by Springer Science and Business Media LLC ,2016
- The Correctness-Security Gap in Compiler OptimizationPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2015
- Implementing TLS with Verified Cryptographic SecurityPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2013
- The Program Counter Security Model: Automatic Detection and Removal of Control-Flow Side Channel AttacksLecture Notes in Computer Science, 2006
- Proof-carrying codePublished by Association for Computing Machinery (ACM) ,1997