SampCert - GitLite

KO | EN

gitlite — search

#hacktoberfest #ai #typescript #golang #android #machine-learning #deep-learning #macos #java #windows #cli #vue #security #ios

SampCert

(★ 103)

SampCert : Verified Differential Privacy

File Explorer

Download Latest Version (.zip)

- - ffitest.yml
  - lean_build.yml
  - static.yml
- - Abstract.lean
  - Generic.lean
  - Neighbours.lean
  - RenyiDivergence.lean
  - Sensitivity.lean
- - Align.lean
  - Dafny.lean
  - Export.lean
  - Extension.lean
  - IR.lean
  - IRToDafny.lean
  - Print.lean
  - Translate.lean
  - VMC.lean
- - Auto.lean
  - Basic.lean
  - Monad.lean
  - UniformByte.lean
  - UniformP2.lean
  - Until.lean
  - While.lean
- - Log.lean
  - Shift.lean
  - Util.lean
  - UtilMathlib.lean
- Extraction.lean
- SLang.lean
- benchmarks.py
- discretegauss.py
- IBM
- Load.py
- Random.py
- README.md
- run_benchmark.sh
- testing-kolmogorov-discretegaussian.py
- testing-kolmogorov-discretelaplace.py
.gitignore
.gitmodules
CITATION.cff
CONTRIBUTING.md
Dockerfile
FastExtract.lean
ffi.cpp
index.html
lake-manifest.json
lakefile.lean
lean-toolchain
LICENSE
paper_mapping.md
pbuild.sh
README.md
REPRODUCING.md
SampCert.lean
SampCertCheck.lean
Test.lean
VMC.lean

// repository documentation

Was this content helpful?

★ 0 (0 ratings)

# SampCert

A verified implementation using [Lean](https://github.com/leanprover/lean4) and [Mathlib](https://github.com/leanprover-community/mathlib4) of randomized algorithms including [the discrete Gaussian sampler for differential privacy](https://arxiv.org/abs/2004.00010), key results in [zero concentrated differential privacy](https://arxiv.org/abs/1605.02065), and [some verified (unbounded) private queries](https://arxiv.org/pdf/1909.01917).

SampCert is deployed and used in the [AWS Clean Rooms Differential Privacy service](https://docs.aws.amazon.com/clean-rooms/latest/userguide/differential-privacy.html#dp-overview). SampCert proves deep properties about some of its randomized algorithm and makes heavy use of Mathlib. For example, we use theorems such as [the Poisson summation formula](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/Fourier/PoissonSummation.html#Real.tsum_eq_tsum_fourierIntegral_of_rpow_decay).

The principal developer of SampCert is [Jean-Baptiste Tristan](https://jtristan.github.io/). It is also developed by [Markus de Medeiros](https://www.markusde.ca/).

Other people have contributed important ideas or tools for deployment including (in no particular order): Leo de Moura, Anjali Joshi, Joseph Tassarotti, Stefan Zetzsche, Aws Albharghouti, Muhammad Naveed, Tristan Ravitch, Fabian Zaiser, Tomas Skrivan.

To cite SampCert you can currently use the following reference:
```
@software{Tristan_SampCert_Verified_2024,
author = {Tristan, Jean-Baptiste},
doi = {10.5281/zenodo.11204806},
month = may,
title = {{SampCert : Verified Differential Privacy}},
url = {https://github.com/leanprover/SampCert},
version = {1.0.0},
year = {2024}
}
```