An official website of the United States government
The constant-time discipline is a software-based countermeasure used for protecting high assurance cryptographic implementations against timing side-channel attacks. Constant-time is effective (it protects against many known attacks), rigorous (it can be formalized using program semantics), and amenable to automated verification. Yet, the advent of micro-architectural attacks makes constant-time as it exists today far less useful. This paper lays foundations for constant-time programming in the presence of speculative and out-of-order execution. We present an operational semantics and a formal definition of constant-time programs in this extended setting. Our semantics eschews formalization of microarchitectural features (that are instead assumed under adversary control), and yields a notion of constant-time that retains the elegance and tractability of the usual notion. We demonstrate the relevance of our semantics in two ways: First, by contrasting existing Spectre-like attacks with our definition of constant-time. Second, by implementing a static analysis tool, Pitchfork, which detects violations of our extended constant-time property in real world cryptographic libraries.
more »
« less
This content will become publicly available on September 11, 2025
{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 by enabling field-sensitivity, context-sensitivity and partial 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 one minute. Moreover, CtChecker reveals that some repaired code generated by program rewriters supposedly remove timing channels are still not constant-time.
more »
« less
- PAR ID:
- 10541392
- Editor(s):
- Aldrich, Jonathan; Salvaneschi, Guido
- Publisher / Repository:
- Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- Date Published:
- Volume:
- 313
- ISSN:
- 1868-8969
- ISBN:
- 978-3-95977-341-6
- Page Range / eLocation ID:
- 313-313
- Subject(s) / Keyword(s):
- Information flow control static analysis side channel constant-time programming Security and privacy → Information flow control
- Format(s):
- Medium: X Size: 26 pages; 991826 bytes Other: application/pdf
- Size(s):
- 26 pages 991826 bytes
- Right(s):
- Creative Commons Attribution 4.0 International license; info:eu-repo/semantics/openAccess
- Sponsoring Org:
- National Science Foundation
More Like this
-
-
Extensive research has been conducted to explore cryptographic API misuse in Java. However, despite the tremendous popularity of the Python language, uncovering similar issues has not been fully explored. The current static code analysis tools for Python are unable to scan the increasing complexity of the source code. This limitation decreases the analysis depth, resulting in more undetected cryptographic misuses. In this research, we propose Cryptolation, a Static Code Analysis (SCA) tool that provides security guarantees for complex Python cryptographic code. Most existing analysis tools for Python solely focus on specific Frameworks such as Django or Flask. However, using a SCA approach, Cryptolation focuses on the language and not any framework. Cryptolation performs an inter-procedural data-flow analysis to handle many Python language features through variable inference (statically predicting what the variable value is) and SCA. Cryptolation covers 59 Python cryptographic modules and can identify 18 potential cryptographic misuses that involve complex language features. In this paper, we also provide a comprehensive analysis and a state-of-the-art benchmark for understanding the Python cryptographic Application Program Interface (API) misuses and their detection. Our state-of-the-art benchmark PyCryptoBench includes 1,836 Python cryptographic test cases that cover both 18 cryptographic rules and five language features. PyCryptoBench also provides a framework for evaluating and comparing different cryptographic scanners for Python. To evaluate the performance of our proposed cryptographic Python scanner, we evaluated Cryptolation against three other state-of-the-art tools: Bandit, Semgrep, and Dlint. We evaluated these four tools using our benchmark PyCryptoBench and manual evaluation of (four Top-Ranked and 939 Un-Ranked) real-world projects. Our results reveal that, overall, Cryptolation achieved the highest precision throughout our testing; and the highest accuracy on our benchmark. Cryptolation had 100% precision on PyCryptoBench, and the highest precision on real-world projects.more » « less
-
Existing design techniques for providing security guarantees against network-based attacks in cyber-physical systems (CPS) are based on continuous use of standard cryptographic tools to ensure data integrity. This creates an apparent conflict with common resource limitations in these systems, given that, for instance, lengthy message authentication codes (MAC) introduce significant overheads. We present a framework to ensure both timing guarantees for real-time network messages and Quality-of-Control (QoC) in the presence of network-based attacks. We exploit physical properties of controlled systems to relax constant integrity enforcement requirements, and show how the problem of feasibility testing of intermittently authenticated real-time messages can be cast as a mixed integer linear programming problem. Besides scheduling a set of real-time messages with predefined authentication rates obtained from QoC requirements, we show how to optimally increase the overall system QoC while ensuring that all real-time messages are schedulable. Finally, we introduce an efficient runtime bandwidth allocation method, based on opportunistic scheduling, in order to improve QoC. We evaluate our framework on a standard benchmark designed for CAN bus, and show how an infeasible message set with strong security guarantees can be scheduled if dynamics of controlled systems are taken into account along with real-time requirements.more » « less
-
Confidential computing aims to secure the code and data in use by providing a Trusted Execution Environment (TEE) for applications using hardware features such as Intel SGX.Timing and cache side-channel attacks, however, are often outside the scope of the threat model, although once exploited they are able to break all the default security guarantees enforced by hardware. Unfortunately, tools detecting potential side-channel vulnerabilities within applications are limited and usually ignore the strong attack model and the unique programming model imposed by Intel SGX. This paper proposes a precise side-channel analysis tool, ENCIDER, detecting both timing and cache side-channel vulnerabilities within SGX applications via inferring potential timing observation points and incorporating the SGX programming model into analysis. ENCIDER uses dynamic symbolic execution to decompose the side-channel requirement based on the bounded non-interference property and implements byte-level information flow tracking via API modeling. We have applied ENCIDER to 4 real-world SGX applications, 2 SGX crypto libraries, and 3 widely-used crypto libraries, and found 29 timing side channels and 73 code and data cache side channels. We have reported our findings to the corresponding parties, e.g., Intel and ARM, who have confirmed most of the vulnerabilities detected.more » « less
-
We present SERBERUS, the first comprehensive mitigation for hardening constant-time (CT) code against Spectre attacks (involving the PHT, BTB, RSB, STL, and/or PSF speculation primitives) on existing hardware. SERBERUS is based on three insights. First, some hardware control-flow integrity (CFI) protections restrict transient control-flow to the extent that it may be comprehensively considered by software analyses. Second, conformance to the accepted CT code discipline permits two code patterns that are unsafe in the post-Spectre era. Third, once these code patterns are addressed, all Spectre leakage of secrets in CT programs can be attributed to one of four classes of taint primitives—instructions that can transiently assign a secret value to a publicly-typed register. We evaluate SERBERUS on cryptographic primitives in the OPENSSL, LIBSODIUM, and HACL* libraries. SERBERUS introduces 21.3% runtime overhead on average, compared to 24.9% for the next closest state-of-the-art software mitigation, which is less secure.more » « less
