CtChecker: a Precise, Sound and Efficient Static Analysis for Constant-Time Programming
Timing channel attacks are emerging as real-world threats to computer security. In cryptographic systems, an effective countermeasure against timing attacks is the constant-time programming discipline. However, strictly enforcing the discipline manually is both time-consuming and error-prone. While various tools exist for analyzing/verifying constant-time programs, they sacrifice at least one feature among precision, soundness and efficiency.
In this paper, we build CtChecker, a sound static analysis for constant-time programming. Under the hood, CtChecker uses a static information flow analysis to identify violations of constant-time discipline. Despite the common wisdom that sound, static information flow analysis lacks precision for real-world applications, we show that with field-sensitivity, context-sensitivity and flow-sensitivity, CtChecker reports fewer false positives compared with existing sound tools. Evaluation on real-world cryptographic systems shows that CtChecker analyzes 24K lines of source code in under 30 seconds. Moreover, CtChecker reveals that some repaired code generated by program rewriters supposedly remove timing channels are still not constant-time.
Mon 16 SepDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
15:30 - 17:00 | |||
15:30 15mTalk | Partial Redundancy Elimination in Two Iterative Data Flow Analyses Technical Papers Reshma Roy National Institute of Technology, Calicut, Sreekala S National Institute of Technology, Calicut, Vineeth Paleri National Institute of Technology, Calicut | ||
15:45 15mTalk | Indirection-Bounded Call Graph Analysis Technical Papers Madhurima Chakraborty University of California, Riverside, Aakash Gnanakumar University of California, Riverside, Manu Sridharan University of California at Riverside, Anders Møller Aarhus University | ||
16:00 15mTalk | Dynamically Generating Callback Summaries for Enhancing Static Analysis Technical Papers Steven Arzt Fraunhofer SIT; ATHENE, Marc Miltenberger Fraunhofer SIT | ATHENE - National Research Center for Applied Cybersecurity, Darmstadt, Julius Näumann TU Darmstadt | ATHENE - National Research Center for Applied Cybersecurity, Darmstadt | ||
16:15 15mTalk | A CFL-Reachability Formulation of Callsite-Sensitive Pointer Analysis with Built-in On-the-Fly Call Graph Construction Technical Papers Dongjie He Chongqing University, China, Jingbo Lu University of New South Wales, Jingling Xue UNSW Sydney | ||
16:30 15mTalk | Scaling Interprocedural Static Data-Flow Analysis to Large C/C++ Applications Technical Papers Fabian Schiebel Fraunhofer IEM, Florian Sattler Saarland Informatics Campus, Saarland University, Philipp Dominik Schubert Heinz Nixdorf Institut, Paderborn University, Sven Apel Saarland University, Eric Bodden | ||
16:45 15mTalk | CtChecker: a Precise, Sound and Efficient Static Analysis for Constant-Time Programming Technical Papers |