ANOSY: Approximated Knowledge Synthesis with Refinement Types for Declassification
Non-interference is a popular way to enforce confidentiality of sensitive data. However, declassification of sensitive information is often needed in realistic applications but breaks non-interference. We present ANOSY, an approximate knowledge synthesizer for quantitative declassification policies. ANOSY uses refinement types to automatically construct machine checked over- and under-approximations of attacker knowledge for boolean queries on multi-integer secrets. It also provides an AnosyT monad transformer to track the attacker knowledge over multiple declassification queries, and checks for violations against the user-specified policies on information flow control applications. We implemented a prototype of ANOSY and showed that it is precise and permissive: up to 14 declassification queries were permitted before policy violation using the powersets of interval domain.
Wed 15 JunDisplayed time zone: Pacific Time (US & Canada) change
10:40 - 12:00 | |||
10:40 20mTalk | P4BID: Information Flow Control in P4 PLDI DOI | ||
11:00 20mTalk | ANOSY: Approximated Knowledge Synthesis with Refinement Types for Declassification PLDI Sankha Narayan Guria University of Maryland, College Park, Niki Vazou IMDEA Software Institute, Marco Guarnieri IMDEA Software Institute, James Parker Galois, Inc. DOI Pre-print | ||
11:20 20mTalk | Hardening Attack Surfaces with Formally Proven Binary Format Parsers PLDI Nikhil Swamy Microsoft Research, Tahina Ramananandro Microsoft Research, Aseem Rastogi Microsoft Research, Irina Spiridonova Microsoft Research, Haobin Ni Cornell University, Dmitry Malloy Microsoft, Juan Vazquez Microsoft, Michael Tang Microsoft, Omar Cardona Microsoft, Arti Gupta Microsoft DOI | ||
11:40 20mTalk | Modular Information Flow Through Ownership PLDI Will Crichton Stanford University, Marco Patrignani University of Trento, Maneesh Agrawala Stanford University, Pat Hanrahan Stanford University, USA DOI Pre-print | ||
22:40 - 00:00 | |||
22:40 20mTalk | P4BID: Information Flow Control in P4 PLDI DOI | ||
23:00 20mTalk | ANOSY: Approximated Knowledge Synthesis with Refinement Types for Declassification PLDI Sankha Narayan Guria University of Maryland, College Park, Niki Vazou IMDEA Software Institute, Marco Guarnieri IMDEA Software Institute, James Parker Galois, Inc. DOI Pre-print | ||
23:20 20mTalk | Hardening Attack Surfaces with Formally Proven Binary Format Parsers PLDI Nikhil Swamy Microsoft Research, Tahina Ramananandro Microsoft Research, Aseem Rastogi Microsoft Research, Irina Spiridonova Microsoft Research, Haobin Ni Cornell University, Dmitry Malloy Microsoft, Juan Vazquez Microsoft, Michael Tang Microsoft, Omar Cardona Microsoft, Arti Gupta Microsoft DOI | ||
23:40 20mTalk | Modular Information Flow Through Ownership PLDI Will Crichton Stanford University, Marco Patrignani University of Trento, Maneesh Agrawala Stanford University, Pat Hanrahan Stanford University, USA DOI Pre-print | ||