Sushant Dinesh (University of Illinois at Urbana Champaign), Grant Garrett-Grossman (University of Illinois at Urbana Champaign), Christopher W. Fletcher (University of Illinois at Urbana Champaign)

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 SynthCT to address the above issues. Given a specification of safe/unsafe instructions, SynthCT 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 SynthCT, we are able to synthesize translations for a majority of the x86 64 ISA. Specifically, SynthCT 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 SynthCT was unable to generate translations for are instructions that experts believe are safe instructions on today’s x86 64 microarchitectures.

View More Papers

Binary Search in Secure Computation

Marina Blanton (University at Buffalo (SUNY)), Chen Yuan (University at Buffalo (SUNY))

Read More

VPNInspector: Systematic Investigation of the VPN Ecosystem

Reethika Ramesh (University of Michigan), Leonid Evdokimov (Independent), Diwen Xue (University of Michigan), Roya Ensafi (University of Michigan)

Read More

Progressive Scrutiny: Incremental Detection of UBI bugs in the...

Yizhuo Zhai (University of California, Riverside), Yu Hao (University of California, Riverside), Zheng Zhang (University of California, Riverside), Weiteng Chen (University of California, Riverside), Guoren Li (University of California, Riverside), Zhiyun Qian (University of California, Riverside), Chengyu Song (University of California, Riverside), Manu Sridharan (University of California, Riverside), Srikanth V. Krishnamurthy (University of California, Riverside),…

Read More

HeadStart: Efficiently Verifiable and Low-Latency Participatory Randomness Generation at...

Hsun Lee (National Taiwan University), Yuming Hsu (National Taiwan University), Jing-Jie Wang (National Taiwan University), Hao Cheng Yang (National Taiwan University), Yu-Heng Chen (National Taiwan University), Yih-Chun Hu (University of Illinois at Urbana-Champaign), Hsu-Chun Hsiao (National Taiwan University)

Read More