Sat 22 Jan 2022 11:10 - 11:35 at Independence - Attacks and defenses Chair(s): Jonathan Protzenko

Proving a compiler to be secure is costly, and even testing its security often requires domain knowledge about potential attacks. In this work, we present a tool to synthesize examples of compiler insecurity from just specifications of the languages and the compiler between them. The tool also provides evidence of how severe discovered vulnerabilities may be by synthesizing gadgets that represent composable exploitation APIs within implementations.

Synthesizing Evidence of Emergent Execution (Extended Abstract) (prisc22-SEEC.pdf)413KiB

Sat 22 Jan

Displayed time zone: Eastern Time (US & Canada) change

10:20 - 11:35
Attacks and defensesPriSC at Independence
Chair(s): Jonathan Protzenko Microsoft Research, Redmond
10:20
25m
Talk
Type-directed Program Transformation for Constant-Time EnforcementRemote
PriSC
File Attached
10:45
25m
Talk
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
25m
Talk
Synthesizing Evidence of Emergent ComputationRemote
PriSC
Scott Moore Galois, Inc., Jennifer Paykin Galois, Inc., Olivier Savary Bélanger Galois, Inc.
Media Attached File Attached