MLightDP

Zhang and Kifer [ZK17] designed the language LightDP in which they track the distance of a variable, i.e. how different its values are during two executions on almost identical inputs. If the returned expression has distance zero, then it returns identical values in both executions. Using the notion of randomness alignment they allow noise to compensate for any non-zero distance at a cost to the privacy budget. This is all encapsulated in a type system and program transformations, such that if a program type checks and the transformed program is validated by off-the-shelf verification software, then a program is differentially private [ZK17]. Furthermore, they implement a small prototype for LightDP in Python capable of type checking and transforming a Python program [Wan+17].

We follow up on the work of Zhang and Kifer by implementing a tool in OCaml capable of parsing, type checking and transforming a LightDP program into an input for our software verification tool of choice, Dafny [Lei10]. The primary goal of this project, aptly named MLightDP, is to hopefully provide a less prototypical and more fully fleshed experience than the current Python prototype of [Wan+17].

Table of Contents

• MLightDP
  • Dependencies
  • Usage
  • Examples
  • References

Dependencies

To compile the source code and run our tool, one needs to have the OCaml compiler installed together with the opam packages menhir and ounit.

To verify the transformed program, one needs Dafny version 2.3.0 or higher. Versions 2.0 and higher of Dafny may be enough.

Usage

By merely writing make one should be able to freshly compile the source code and run the compiled tool on all the examples present in examples/. The list of relevant make targets are provided in the table below.

Target	Effect
compile O=<output>	Compile the MLightDP tool and bash script. Default output O is mlightdp.o
clean	Remove all compilation output from make compile
examples	Transform all provided examples with the MLightDP tool
clean-examples	Remove all compiled examples of the MLightDP tool from make examples
test	Run all unit tests

Compilation and usage

The tool can be compiled with make compile, which generates a bash script mlightdp to run it. Adding the repository root to your path should allow one to use the tool globally.

To run the tool on some file write

./mlightdp path/to/file.mldp

Unit Tests

All tests can be compiled and run with make test. More precisely one can choose to only run some of the unit tests with the following targets.

Target	Test
test-parser	Run unit tests for AST creation from strings
test-menhir	Get Menhir output for shift-reduce conflicts
test-semant	Test semantic analysis step

As one can see in the table above, we do yet not cover the refinement or the differential privacy type checking steps in the unit testing. Currently these are only tested in the end-to-end tests.

Examples

In examples/ one can find multiple examples that all compile with our tool. We mark in the list below the examples where the transformed output is verified by Dafny.

• laplace_mechanism.mldp: The simplest possible program based on the presentation of randomness alignment in [Wan+19].

• sparse_vector.mldp: The running example in [ZK17], that outputs boolean values detailing the relation between the query results and a given threshold.

• numerical_sparse_vector.mldp: A variation of the sparse_vector example from [ZK17].

• gap_sparse_vector.mldp: A variation of the sparse_vector example from [Wan+19].

• partial_sum.mldp: A summation algorithm from [ZK17].

• sum.mldp: A variant of partial_sum on simpler to reason about input.

• smart_sum.mldp: A more complicated summation algorithm also from [ZK17].

After compiling the tool with make compile, then all examples can be processed with make examples and again removed with clean-examples.

References

• [Lei10] Rustan Leino. “Dafny: An Automatic Program Verifier for Functional Correctness”. In: 16th International Conference, LPAR-16, Dakar, Senegal. Springer Berlin Heidelberg, Apr. 2010, pp. 348–370.

• [Wan+17] Yuxin Wang, Zeyu Ding, Guanhong Wang, Danfeng Zhang, and Daniel Kifer. “github.com/yxwangcs/lightdp”. 2017

• [Wan+19] Yuxin Wang, Zeyu Ding, Guanhong Wang, Daniel Kifer, and Danfeng Zhang. “Proving Differential Privacy with Shadow Execution”. In: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation. PLDI 2019. Phoenix, AZ, USA: ACM, 2019, pp. 655 - 669

• [ZK17] Danfeng Zhang and Daniel Kifer. “LightDP: towards automating differential privacy proofs”. In: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages. POPL 2017. ACM Press, 2017.