SPLASH 2023
Sun 22 - Fri 27 October 2023 Cascais, Portugal
Fri 27 Oct 2023 14:00 - 14:18 at Room XII - security & privacy Chair(s): Arjun Guha

To ensure programs do not leak private data, we often want to be able to provide formal guarantees ensuring such data is handled correctly. Often, we cannot keep such data secret entirely; instead programmers specify how private data may be declassified. While security definitions for declassification exist, they mostly do not handle higher-order programs. In fact, in the higher-order setting no compositional security definition exists for intensional information-flow properties such as where declassification, which allows declassification in specific parts of a program. We use logical relations to build a model (and thus security definition) of where declassification. The key insight required for our model is that we must stop enforcing indistinguishability once a relevant declassification has occurred. We show that the resulting security definition provides more security than the most related previous definition, which is for the lower-order setting.

Fri 27 Oct

Displayed time zone: Lisbon change

14:00 - 15:30
security & privacyOOPSLA at Room XII
Chair(s): Arjun Guha Northeastern University; Roblox
14:00
18m
Talk
Compositional Security Definitions for Higher-Order Where Declassification
OOPSLA
Jan Menz MPI-SWS, Andrew K. Hirsch University at Buffalo, SUNY, Peixuan Li Pennsylvania State University, Deepak Garg MPI-SWS
DOI
14:18
18m
Talk
Fat Pointers for Temporal Memory Safety of C
OOPSLA
Jie Zhou University of Rochester, John Criswell University of Rochester, Michael Hicks Amazon Web Services and the University of Maryland
DOI
14:36
18m
Talk
Quantifying and Mitigating Cache Side Channel Leakage with Differential Set
OOPSLA
Cong Ma University of Waterloo, Dinghao Wu Pennsylvania State University, Gang Tan Pennsylvania State University, Mahmut Taylan Kandemir Pennsylvania State University, Danfeng Zhang Duke University; Pennsylvania State University
DOI
14:54
18m
Talk
A Verification Methodology for the ArmĀ® Confidential Computing Architecture: From a Secure Specification to Safe Implementations
OOPSLA
Anthony C. J. Fox ARM, Gareth Stockwell ARM, Shale Xiong ARM, Hanno Becker Amazon Web Services, Dominic P. Mulligan Amazon Web Services, Gustavo Petri Amazon Web Services, Nathan Chong Amazon Web Services
DOI
15:12
18m
Talk
Verifying Indistinguishability of Privacy-Preserving Protocols
OOPSLA
Kirby Linvill University of Colorado Boulder, Gowtham Kaki University of Colorado at Boulder, Eric Wustrow University of Colorado Boulder
DOI