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.

翻译：形式化方法在保证协议满足密码学安全定义方面取得了显著进展，但这类方法仍需要大量人力投入，且目前仍然缺乏一种能够自动识别不安全协议的自动化工具。本研究证明，基于属性的测试（"多次运行并观察是否出现故障"）能够有效检测安全协议中的安全漏洞。我们专门针对安全多方计算（MPC）展开研究，这是因为针对比特模型实现的安全定义的形式化方法实施难度极大。通过借鉴概率编程语言与统计推断领域的文献成果，我们设计了一种可检测MPC协议比特级实现中各类缺陷的测试方法。该测试属于灰盒测试，仅需获取协议消耗的随机数记录以及输入、输出和消息的通信记录。通过在两套不同的经典GMW协议实现中成功检测出多种错误和偏差，实验验证了该方法的有效性。对数百个随机生成的协议进行测试后，该方法几乎能识别出所有不安全协议。我们还分析了测试参数，并探讨了MPC安全性检测的难点成因。