SynthCT: Towards Portable Constant-Time Code
Sushant Dinesh, Grant Garrett-Grossman, Christopher W. Fletcher
摘要
—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.
问问这篇 Paper
智能体会读完全文。
Lune 把这篇 Paper 索引到了每一个公式,引用它的顶会 Paper 也一样。你提问,回答直接引用原文。
引用它的顶会 Paper6
- Serberus: Protecting Cryptographic Code from Spectres at Compile-TimeNicholas Mosier, Hamed Nemati, John C. Mitchell, Caroline TrippelS&P 2024 · 被引用 16 次
- Core slicing: closing the gap between leaky confidential VMs and bare-metal cloudZiqiao Zhou, Yizhou Shan, Weidong Cui, Xinyang Ge 等OSDI 2023 · 被引用 12 次
- RTL2MμPATH: Multi-μPATH Synthesis with Applications to Hardware Security VerificationYao Hsiao, Nikos Nikoleris, Artem Khyzha, Dominic P. Mulligan 等MICRO 2024 · 被引用 12 次
- Architectural Mimicry: Innovative Instructions to Efficiently Address Control-Flow Leakage in Data-Oblivious ProgramsHans Winderix, Marton Bognar, Job Noorman, Lesly-Ann Daniel 等S&P 2024 · 被引用 5 次
- Synthesizing axiomatizations using logic learningPaul Krogmeier, Zhengyao Lin, Adithya Murali, P. MadhusudanOOPSLA 2022 · 被引用 3 次
它引用的顶会 Paper20
- Spectre Attacks: Exploiting Speculative ExecutionPaul Kocher, Jann Horn, Anders Fogh, Daniel Genkin 等S&P 2019 · 被引用 2,435 次
- Oblivious Multi-Party Machine Learning on Trusted ProcessorsOlga Ohrimenko, Felix Schuster, Cédric Fournet, Aastha Mehta 等USENIX Security 2016 · 被引用 594 次
- A Systematic Evaluation of Transient Execution Attacks and DefensesClaudio Canella, Jo Van Bulck, Michael Schwarz, Moritz Lipp 等USENIX Security 2019 · 被引用 442 次
- Leaky Cauldron on the Dark Land: Understanding Memory Side-Channel Hazards in SGXWenhao Wang, Guoxing Chen, Xiaorui Pan, Yinqian Zhang 等CCS 2017 · 被引用 403 次
- ZeroTrace : Oblivious Memory Primitives from Intel SGXSajin Sasy, Sergey Gorbunov, Christopher W. FletcherNDSS 2018 · 被引用 244 次
相关 Paper
- Constantine: Automatic Side-Channel Resistance Using Efficient Control and Data Flow LinearizationPietro Borrello, Daniele Cono D'Elia, Leonardo Querzoni, Cristiano GiuffridaCCS 2021 · 被引用 43 次
- Towards a formally verified hardware root-of-trust for data-oblivious computingLucas Deutschmann, Johannes Müller, Mohammad Rahmani Fadiheh, Dominik Stoffel 等DAC 2022 · 被引用 11 次
- 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 次
- Constant-time foundations for the new spectre eraSunjay Cauligi, Craig Disselkoen, Klaus von Gleissenthall, Dean M. Tullsen 等PLDI 2020 · 被引用 90 次
