Secure Multiparty Computation (MPC) is a cryptographic primitive that allows a number of parties to participate in a computation without revealing any party’s secret inputs to the computation to any of the other parties. Proofs of security of \emph{implementations} of MPC have generally been done manually; we are working on a domain-specific language and accompanying static analyzer for automating these proofs.
Our proposed system validates programs in two stages. An initial layer of type inference and checking will ensure that appropriate preconditions are met for the second stage. The second stage will apply probabilistic programming techniques to verify an invariant about posterior inference of input distributions based on output distributions. The final piece of the formalism will be a constructive proof of MPC security in the traditional Simulator framework based on the enforced probabilistic guarantees.
