Solo: A Lightweight Static Analysis for Differential Privacy
summary
Solo claims a practical, sound type system that enforces differential privacy inside Haskell without linear or relational refinement types. It encodes sensitivities as type-level strings, provides a privacy-indexed monad, uses Singletons, type families and polymorphism, and proves soundness with a core language and a step‑indexed logical relation. Implemented primitives carry correct types but many are not yet executed so large experiments are not run; case studies include k‑means, CDF, gradient descent and MWEM with the system working on 10–30 line examples.
AI-written summary · about
chapters (13)
- 0:00Differential privacy basics
- 2:47Reconstruction attacks protection
- 7:20Solo: Type system intro
- 10:10Comparison with Fuzz
- 13:18Sensitivity in Haskell types
- 18:38Handling sensitive functions
- 20:44Differentially private primitives
- 22:37Summary and future work
- 23:19Q&A: Limitations
- 24:44Q&A: Global sensitivity
- 25:29Q&A: Sensitive functions
- 26:11Q&A: Annotations
- 27:37Q&A: Case studies
related talks
21mModular Verification of Differential Privacy in Probabilistic Higher-Order Separation(…)
17mObservable...Yet Still Private? An Offensive Privacy Perspective on Observability
38mBuilding Secure Systems in Haskell
29mPrivacy-preserving methods: Building secure projects
42mWhy Privacy Matters
45mAutomated Verification meets Differential Privacy
32mYou've got trust issues, we've got solutions: Differential Privacy
08mLLMs Without Leaks: Keep Your Code, Data & IP