Verifying Constant-time

Ways to verify constant-time.

Intro

Constant-time is an important property of cryptographic implementations, and it plays a crucial role in defending against side-channels. Especially in this post-Spectre era, microarchitectural-level side-channel attacks have become a major threat. In recent years, researchers in this area have cranked out a lot of papers on constant-time, many of them related to microarchitectural side-channels. Among them, Almeida (A-bro) and Barthe (B-bro) stand out in particular. I’ve also noticed that a lot of the big names in this field seem to be European — perhaps related to Europeans being good at math and fond of doing all sorts of verification.

Broadly speaking, constant-time means that the running time is independent of the secret. Differences in running time mainly stem from:

• Control-flow dependency: e.g. the secret appears in an if
• Latency of instruction: some instructions don’t have a fixed running time; it may depend on the operands. (e.g. idiv)
• Data/Code access dependency: when data is accessed based on the secret, accessing memory obviously takes longer than accessing a register/cache
• Microarchitectural: even if constant-time is satisfied under the usual model, speculative execution may leak the secret

Summary

A Dilemma in Verification

For constant-time verification, this is an especially hard problem. There’s a gap between source code and assembly code. This means that in some cases, even when the source code passes constant-time verification, the corresponding assembly code may still not satisfy the constant-time property. Compilers generally guarantee semantic consistency during optimization, but they can’t guarantee constant-time. Verifying at the source level offers richer context and more information, but verification results on the binary are more reliable.

This makes verification difficult. The current mainstream approach is to do verification at the IR level. It can preserve semantic information to a large degree, while also sitting fairly close to low-level assembly in the compilation pipeline.

Abstract Language Model

Work at this level mainly solves some problems theoretically. The author first defines an abstract language model, then defines possible side-channel leaks on top of this model, e.g. small-step semantics PLDI'20. This model needs to be able to help reason about constant-time for real-world assembly/IR.

At IR Level

Most work does verification at the IR level, especially LLVM IR. At this level there are many analysis tools available, and it’s fairly close to low-level assembly code. There may also be some gap here between IR constant-time and assembly constant-time.

Executable Binary

Work at this level is generally not very easy to formalize. Most of it seems to use test-like approaches (DATE'17, SP'20).

Related Work

Patching

Rewrite the code/binary to make it constant-time

Implementation

There are quite a few implementations out in industry. How do you achieve constant-time while keeping high performance?

Some Thoughts

How do you achieve constant-time in other general-purpose languages (not C/C++)? These days Rust can guarantee safety, which is also very important for applications like crypto. How would you achieve constant-time in Rust? I’ve come across the subtle crate, but I’m not sure whether it can actually achieve constant-time in a constantly evolving language like Rust. The two problems I can think of are:

• When emitting assembly code, rustc actually doesn’t have that much control over the LLVM backend. How (or if at all) do you make sure the LLVM IR to ASM step doesn’t violate constant-time? This problem actually also exists in those earlier works that use LLVM to verify constant-time.
• Rust is still evolving (e.g., MIR). Is there a reasonably effective way to (high-levelly) verify constant-time on such a system? MIRAI actually provides constant-time verification. But based on our experience, its verification is pretty lousy.

Reference

1. PLDI'20 Sunjay Cauligi, Craig Disselkoen, Klaus v. Gleissenthall, Dean Tullsen, Deian Stefan, Tamara Rezk, and Gilles Barthe. 2020. Constant-time foundations for the new spectre era. In Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2020). Association for Computing Machinery, New York, NY, USA, 913–926. https://doi.org/10.1145/3385412.3385970
2. PLDI'20 Gilles Barthe, Sandrine Blazy, Benjamin Grégoire, Rémi Hutin, Vincent Laporte, David Pichardie, and Alix Trieu. 2019. Formal verification of a constant-time preserving C compiler. Proc. ACM Program. Lang. 4, POPL, Article 7 (January 2020), 30 pages. https://doi.org/10.1145/3371075
3. Security'16 Almeida, Jose Bacelar, et al. “Verifying {Constant-Time} Implementations.” 25th USENIX Security Symposium (USENIX Security 16). 2016.
4. DATE'17 Reparaz, Oscar, Josep Balasch, and Ingrid Verbauwhede. “Dude, is my code constant time?.” Design, Automation & Test in Europe Conference & Exhibition (DATE), 2017. IEEE, 2017.
5. EuroSP'18 Simon, Laurent, David Chisnall, and Ross Anderson. “What you get is what you C: Controlling side effects in mainstream C compilers.” 2018 IEEE European Symposium on Security and Privacy (EuroS&P). IEEE, 2018.
6. CCS'22 Ammanaghatta Shivakumar, Basavesh, et al. “Enforcing Fine-grained Constant-time Policies.” Proceedings of the 2022 ACM SIGSAC Conference on Computer and Communications Security. 2022.
7. INDOCRYPT'20 Almeida, José Bacelar, et al. “Certified compilation for cryptography: Extended x86 instructions and constant-time verification.” Progress in Cryptology–INDOCRYPT 2020: 21st International Conference on Cryptology in India, Bangalore, India, December 13–16, 2020, Proceedings 21. Springer International Publishing, 2020.
8. Security'19 Gleissenthall, Klaus V., et al. “IODINE: Verifying constant-time execution of hardware.” Usenix Security. Vol. 19. No. 10.5555. 2019.
9. PLDI'19 Cauligi, Sunjay, et al. “Fact: a DSL for timing-sensitive computation.” Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation. 2019.
10. SP'20 Daniel, Lesly-Ann, Sébastien Bardin, and Tamara Rezk. “Binsec/rel: Efficient relational symbolic execution for constant-time at binary-level.” 2020 IEEE Symposium on Security and Privacy (SP). IEEE, 2020.

Less Related Papers

1. “They’re not that hard to mitigate”: What Cryptographic Library Developers Think About Timing Attacks
2. Jasmin: High-Assurance and High-Speed Cryptography
3. SoK: Computer-Aided Cryptography
4. Eliminating timing side-channel leaks using program repair
5. Memory-Safe Elimination of Side Channels
6. Constantine: Automatic Side- Channel Resistance Using Efficient Control and Data Flow Linearization

Other Resources

1. Agner Software optimization resources There is a table of instruction latency and throughput: pdf.
2. Is CLMUL constant time?
3. Intel: Guidelines for Mitigating Timing Side Channels Against Cryptographic Implementations
4. Intel® 64 and IA-32 Architectures Software Developer Manuals