POPL 2022 (series) / PriSC 2022 (series) / PriSC 2022 / Type-directed Program Transformation for Constant-Time Enforcement
Type-directed Program Transformation for Constant-Time EnforcementRemote
Constant-time is a programming discipline which protects cryptographic code against a wide class of timing attacks. This discipline can be formalised as a non-interference property and enforced by an information-flow type-system which prevents branching and memory accesses over secret data. We propose a relaxed information-flow type system which tracks indirect flows but only rejects programs leaking secrets through direct flows. We exploit typing information to guide a program transformation which compiles any well-typed program into a semantically equivalent constant-time program.
Type-directed Program Transformation for Constant-Time Enforcement (Extended Abstract) (PriSC_22_extended.pdf) | 475KiB |
Sat 22 JanDisplayed time zone: Eastern Time (US & Canada) change
Sat 22 Jan
Displayed time zone: Eastern Time (US & Canada) change
10:20 - 11:35 | |||
10:20 25mTalk | Type-directed Program Transformation for Constant-Time EnforcementRemote PriSC File Attached | ||
10:45 25mTalk | Towards Understanding Spectre-PHT in Memory-Safe LanguagesRemote PriSC Zirui Neil Zhao University of Illinois at Urbana-Champaign, Fangfei Liu Intel Corporation, Scott Constable Intel Corporation, Carlos Rozas Intel Corporation | ||
11:10 25mTalk | Synthesizing Evidence of Emergent ComputationRemote PriSC Media Attached File Attached |