POPL 2024
Sun 14 - Sat 20 January 2024 London, United Kingdom
Sat 20 Jan 2024 16:00 - 16:22 at Turing Lecture - Session 4 Chair(s): Dominique Devriese

Universal Composability (UC) is the gold standard for cryptographic security, but mechanizing proofs of UC is notoriously difficult. A recently-discovered connection between UC and Robust Compilation (RC)-a novel theory of secure compilation-provides a means to verify UC proofs using tools that mechanize equality results. Unfortunately, the existing methods apply only to perfect UC security, and real-world protocols relying on cryptography are only computationally secure.

This work addresses this gap by lifting the connection between UC and RC to the computational setting, extending techniques from the RC setting to apply to computational UC security. Moreover, it further generalizes the UC-RC connection beyond computational security to arbitrary equalities, providing a framework to subsume the existing perfect case, and to instantiate future theories with more complex notions of security. This connection allows the use of tools for proofs of computational indistinguishability to properly mechanize proofs of computational UC security. We demonstrate this power by using CryptoVerif to mechanize a proof that parts of the Wireguard protocol are computationally UC secure. Finally, all proofs of the framework itself are verified in Isabelle/HOL.

Sat 20 Jan

Displayed time zone: London change

16:00 - 17:30
Session 4PriSC at Turing Lecture
Chair(s): Dominique Devriese KU Leuven
16:00
22m
Talk
Computational-Bounded Robust Compilation and Universally Composable Security
PriSC
Robert Künnemann CISPA Helmholtz Center for Information Security, Ethan Cecchetti University of Wisconsin-Madison
File Attached
16:22
22m
Talk
Gradual Verification for Smart Contracts
PriSC
Haojia Sun Shanghai Jiao Tong University, Kunal Singh Carnegie Mellon University, Jan-Paul Ramos-Davila Cornell University, Jonathan Aldrich Carnegie Mellon University, Jenna DiVincenzo (Wise) Purdue University
File Attached
16:45
22m
Talk
Towards Modular Specification and Verification of Concurrent Hypervisor-based Isolation
PriSC
Hoang-Hai Dang BedRock Systems, David Swasey BedRock Systems, Gregory Malecha BedRock Systems
File Attached
17:07
8m
Day closing
Closing Remarks
PriSC
Shweta Shinde ETH Zurich