This video was recorded at Lambda Days 2022 -https://www.lambdadays.org/lambdadays2022 Anosy: Approximate Knowledge Synthesis with Refinement Types | Niki Vazou - Research Assistant Professor at IMDEA Software Institute in Madrid. ABSTRACT 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. • Follow us on social: Twitter: https://twitter.com/LambdaDays LinkedIn: https://www.linkedin.com/company/lambda-days/ • Looking for a unique learning experience? Attend the next Lambda Days conference near you! • SUBSCRIBE TO OUR CHANNEL https://www.youtube.com/channel/UC47eUBNO8KBH_V8AfowOWOw See what's coming up at: https://codesync.global