DISCLAIMER: Even though we analyzed the theoretical framework which we are basing our privacy guarantees on, and extensively tested the implementation, we cannot entirely exclude the possibility of bugs or of privacy risks in a program which our typechecker claims to be safe. Use at your own risk. Feedback and questions are very welcome.
The goal of this project is to create a type checker which can automatically analyze Julia programs for (ε, δ)-differential privacy guarantees.
This software is capable of inferring the ε and δ parameters of (ε, δ)-differentially private programs written in Julia, as long as they use only supported syntax and our builtin primitive privacy mechanisms. Its main purpose is enabling the implementaion of novel private mechanisms, using primitives whose privacy guarantees are known from literature, without having to make manual proofs about their properties.
We provide a verifiable implementation of Differentially Private Stochastic Gradient Descent using the Flux.jl machine learning framework. Head to the tutorial for a walkthrough, and check out the code!
Our type inference algorithm for Julia code is based on the Duet type system and the corresponding Haskell implementation. The main part of our analysis is written in Haskell as well, head to our Haskell repo.
If you have any questions, feel free to get in touch :)
To use this package, you will need to have the Haskell Tool Stack installed on your system, as the main part of the typechecker is implemented in Haskell. Once this is done, install the Julia package from the REPL:
] add https://github.com/DiffMu/DiffPrivacyInference.jlTo install from source, head to the installation instructions in our documentation.
For a short guide on how to write typecheckable code as well as example usage, head to the quick guide in our documentation.