[OOPSLA23] Compositional Security Definitions for Higher-Order Where Declassification

Описание: Compositional Security Definitions for Higher-Order Where Declassification (Video, OOPSLA1 2023)
Jan Menz, Andrew K. Hirsch, Peixuan Li, and Deepak Garg
(MPI-SWS, Germany; University at Buffalo, USA; Pennsylvania State University, USA; MPI-SWS, Germany)

Abstract: 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.

Article: https://doi.org/10.1145/3586041

ORCID: https://orcid.org/0009-0004-6821-1987, https://orcid.org/0000-0003-2518-614X, https://orcid.org/0009-0005-9392-3481, https://orcid.org/0000-0002-0888-3093

Video Tags: where declassification, logical relations, relevant declassification, oopslaa23main-p75-p, doi:10.1145/3586041, orcid:0009-0004-6821-1987, orcid:0000-0003-2518-614X, orcid:0009-0005-9392-3481, orcid:0000-0002-0888-3093

Presentation at the OOPSLA1 2023 conference, October 22–27, 2023, https://2023.splashcon.org/track/spla...
Sponsored by ACM SIGPLAN,