Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

DT-SIM: Property-Based Testing for MPC Security

Mako Bates, Joseph P. Near

TL;DR

This work demonstrates that property-based testing, "run it a bunch of times and see if it breaks", is effective for detecting security bugs in secure protocols.

Abstract

Formal methods for guaranteeing that a protocol satisfies a cryptographic security definition have advanced substantially, but such methods are still labor intensive and the need remains for an automated tool that can positively identify an insecure protocol. In this work, we demonstrate that property-based testing, "run it a bunch of times and see if it breaks", is effective for detecting security bugs in secure protocols. We specifically target Secure Multi-Party Computation (MPC), because formal methods targeting this security definition for bit-model implementations are particularly difficult. Using results from the literature for Probabilistic Programming Languages and statistical inference, we devise a test that can detect various flaws in a bit-level implementation of an MPC protocol. The test is grey-box; it requires only transcripts of randomness consumed by the protocol and of the inputs, outputs, and messages. It successfully detects several different mistakes and biases introduced into two different implementations of the classic GMW protocol. Applied to hundreds of randomly generated protocols, it identifies nearly all of them as insecure. We also include an analysis of the parameters of the test, and discussion of what makes detection of MPC (in)security difficult.

DT-SIM: Property-Based Testing for MPC Security

TL;DR

This work demonstrates that property-based testing, "run it a bunch of times and see if it breaks", is effective for detecting security bugs in secure protocols.

Abstract

Formal methods for guaranteeing that a protocol satisfies a cryptographic security definition have advanced substantially, but such methods are still labor intensive and the need remains for an automated tool that can positively identify an insecure protocol. In this work, we demonstrate that property-based testing, "run it a bunch of times and see if it breaks", is effective for detecting security bugs in secure protocols. We specifically target Secure Multi-Party Computation (MPC), because formal methods targeting this security definition for bit-model implementations are particularly difficult. Using results from the literature for Probabilistic Programming Languages and statistical inference, we devise a test that can detect various flaws in a bit-level implementation of an MPC protocol. The test is grey-box; it requires only transcripts of randomness consumed by the protocol and of the inputs, outputs, and messages. It successfully detects several different mistakes and biases introduced into two different implementations of the classic GMW protocol. Applied to hundreds of randomly generated protocols, it identifies nearly all of them as insecure. We also include an analysis of the parameters of the test, and discussion of what makes detection of MPC (in)security difficult.
Paper Structure (36 sections, 2 equations, 8 figures, 1 table, 1 algorithm)

This paper contains 36 sections, 2 equations, 8 figures, 1 table, 1 algorithm.

Table of Contents

  1. Introduction
  2. Contributions.
  3. Background
  4. MPC security
  5. Vacuousness.
  6. Non-interference.
  7. Inference in PPLs
  8. Property-based testing
  9. DT-SIM: a Statistical Test for Security
  10. Conditional Independence Testing by Classification
  11. The DT-SIM Algorithm
  12. Interpreting Test Results
  13. Implementation
  14. Evaluation
  15. A Choreography Language
  16. ...and 21 more sections

Figures (8)

  • Figure 1: Experimental results: performance on random protocols under increasing test power.
  • Figure 2: Experimental results: runtime with increasing test power.
  • Figure 3: Experimental results: trade-offs in power and runtime under different test parameters.
  • Figure 4: Experimental results: ability to detect security bugs. We set the number of iterations to 128 and the training set size to 1024. Results for other settings appear in Appendix \ref{['sec:addit-exper-results']}.
  • Figure 5: Experimental results: decision tree training time.
  • ...and 3 more figures

Theorems & Definitions (1)

  • Definition 1: Passive MPC Security