ANOSY: Approximated Knowledge Synthesis with Refinement Types for Declassification
summary
ANOSY verifies attacker-knowledge approximations and synthesizes posterior-update functions using refinement types, then checks them with Liquid Haskell and an SMT solver (Z3). It encodes abstract domains (intervals and power-set-of-intervals), handles secrets in 2–4 dimensions, and pays a compile-time synthesis cost but gives almost zero runtime overhead. Evaluation shows higher accuracy than FROG/PROB and that increasing power-set size (e.g., 1 interval → ~8 queries, 10 intervals → ~15 queries) answers more queries; code is open source.
AI-written summary · about
chapters (17)
- 0:00Intro
- 0:18Information Leaks are Common
- 0:32Information Flow Control
- 1:27Declassification
- 1:59Putting Guardrails
- 2:32Contributions
- 3:04Example: Restaurant Ads
- 3:50Example: Updating Knowledge
- 4:42Example: Location Reveal
- 6:22Downgrade
- 7:33Tracking Knowledge
- 9:34Approximations
- 10:18Refinement Type Formulation
- 10:46Verifying Indistinguishable Set
- 11:24Synthesizing Indistinguishable Sets
- 12:26Evaluation
- 14:12Summary
related talks
29mSyntia: Synthesizing the Semantics of Obfuscated Code
22mBi-abductive adversarial program synthesis
15mTabby: A Synthesis-Aided Compiler for High-Performance Zero-Knowledge Proof Circuits
12mFully Abstract and Robust Compilation and How to Reconcile the Two, Abstractly
58mAutomating Relational Verification of Infinite-State Programs
18mScalable Bug Detection for Internally Unsafe Libraries: A Logical Approach to Type(…)
12mAutomated Synthesis of Verified Firewalls
31mDistance-Aware OT with Application to Fuzzy PSI