Approximate Knowledge Synthesis with Refinement Types

Explore a conference talk from Lambda Days 2022 on Anosy, an approximate knowledge synthesizer for quantitative declassification policies. Delve into the concept of non-interference for enforcing data confidentiality and learn how Anosy addresses the need for declassification in real-world applications. Discover how refinement types are utilized to automatically construct machine-checked approximations of attacker knowledge for boolean queries on multi-integer secrets. Examine the AnosyT monad transformer and its role in tracking attacker knowledge across multiple declassification queries. Gain insights into the implementation of an Anosy prototype and its effectiveness in permitting declassification queries before policy violation. Follow the presentation's progression through topics such as Haskell vs Monarch, Information Flow Control, Bounded Downgrade, Interval Approximation, and Abstract Refinement. Conclude with an evaluation of Anosy's performance and a summary of its capabilities in information flow control applications.

Introduction
Haskell vs Monarch
Information Flow Control
Bounded Downgrade
Example
Interval Approximation
Abstract Refinement
Evaluation
Summary
Questions