SynthCT: Towards Portable Constant-Time Code
Sushant Dinesh, Grant Garrett-Grossman, Christopher W. Fletcher
Abstract
—Recent attacks have demonstrated that modern microarchitectures are fraught with microarchitectural side channels. Constant-time (CT) programming is a software development methodology where programs are carefully written to avoid these channels. In a nutshell, the idea is to only pass secret data to safe instructions, i.e., those whose execution creates operand-independent hardware resource usage. Yet, current CT programming practices have significant security and performance issues. CT code is written and compiled once, but may execute on multiple different microarchitectures. Yet, what instructions are safe vs. unsafe is fundamentally a microarchitecture-specific issue. A new microarchitectural optimization (or vulnerability) may change the set of safe instructions and break CT guarantees. In this work, we develop SYNTH CT to address the above issues. Given a specification of safe/unsafe instructions, SYNTH CT automatically synthesizes translations for all unsafe instructions in the ISA using only instructions from the safe set. The synthesized translations can be used as a part of a late-stage compiler pass to generate hardened binaries for a specific microarchitecture. This closes the security hole as the specification, and hence the safe translations, can target each microarchitecture individually. This also allows CT code to reclaim some performance, e.g., use more complex/higher-performing instructions, when they are deemed safe for a specific microarchitecture. Using the techniques we develop in SYNTH CT, we are able to synthesize translations for a majority of the x86 64 ISA. Specifically, SYNTH CT is able to generate safe translations for 75% of the ISA using only the remaining 25% of the ISA. Interestingly, the majority of the instructions that SYNTH CT was unable to generate translations for are instructions that experts believe are safe instructions on today’s x86 64 microarchitectures.
Ask about this paper
Your agent reads all of it.
Lune indexed this paper to the last equation, along with the top-tier papers that cite it. Ask a question and the answer quotes them.
Your agent calls
Luneget_paper_fulltext
Free to start. No credit card required.
Terminal
Install the CLIlune papers fulltext 631185f6-30ea-40d2-913a-c2576fe50254Cited by top-tier papers6
- Serberus: Protecting Cryptographic Code from Spectres at Compile-TimeNicholas Mosier, Hamed Nemati, John C. Mitchell, Caroline TrippelS&P 2024 · 16 citations
- Core slicing: closing the gap between leaky confidential VMs and bare-metal cloudZiqiao Zhou, Yizhou Shan, Weidong Cui, Xinyang Ge et al.OSDI 2023 · 12 citations
- RTL2MμPATH: Multi-μPATH Synthesis with Applications to Hardware Security VerificationYao Hsiao, Nikos Nikoleris, Artem Khyzha, Dominic P. Mulligan et al.MICRO 2024 · 12 citations
- Architectural Mimicry: Innovative Instructions to Efficiently Address Control-Flow Leakage in Data-Oblivious ProgramsHans Winderix, Marton Bognar, Job Noorman, Lesly-Ann Daniel et al.S&P 2024 · 5 citations
- Synthesizing axiomatizations using logic learningPaul Krogmeier, Zhengyao Lin, Adithya Murali, P. MadhusudanOOPSLA 2022 · 3 citations
Builds on20
- Spectre Attacks: Exploiting Speculative ExecutionPaul Kocher, Jann Horn, Anders Fogh, Daniel Genkin et al.S&P 2019 · 2,435 citations
- Oblivious Multi-Party Machine Learning on Trusted ProcessorsOlga Ohrimenko, Felix Schuster, Cédric Fournet, Aastha Mehta et al.USENIX Security 2016 · 594 citations
- A Systematic Evaluation of Transient Execution Attacks and DefensesClaudio Canella, Jo Van Bulck, Michael Schwarz, Moritz Lipp et al.USENIX Security 2019 · 442 citations
- Leaky Cauldron on the Dark Land: Understanding Memory Side-Channel Hazards in SGXWenhao Wang, Guoxing Chen, Xiaorui Pan, Yinqian Zhang et al.CCS 2017 · 403 citations
- ZeroTrace : Oblivious Memory Primitives from Intel SGXSajin Sasy, Sergey Gorbunov, Christopher W. FletcherNDSS 2018 · 244 citations
Related papers
- Constantine: Automatic Side-Channel Resistance Using Efficient Control and Data Flow LinearizationPietro Borrello, Daniele Cono D'Elia, Leonardo Querzoni, Cristiano GiuffridaCCS 2021 · 43 citations
- Towards a formally verified hardware root-of-trust for data-oblivious computingLucas Deutschmann, Johannes Müller, Mohammad Rahmani Fadiheh, Dominik Stoffel et al.DAC 2022 · 11 citations
- Helium: Quantifying Microarchitectural Side-Channel Leakage with Probabilistic GuaranteesSamantha Archer, Mohammad Rahmani Fadiheh, Caroline TrippelISCA 2026
- Binsec/Rel: Efficient Relational Symbolic Execution for Constant-Time at Binary-LevelLesly-Ann Daniel, Sébastien Bardin, Tamara RezkS&P 2020 · 76 citations
- Constant-time foundations for the new spectre eraSunjay Cauligi, Craig Disselkoen, Klaus von Gleissenthall, Dean M. Tullsen et al.PLDI 2020 · 90 citations
