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（不）安全性的难点所在。