Protecting the confidentiality of private data and using it for useful collaboration have long been at odds. Modern cryptography is bridging this gap through rapid growth in secure protocols such as multi-party computation, fully-homomorphic encryption, and zero-knowledge proofs. However, even with provable indistinguishability or zero-knowledgeness, confidentiality loss from leakage inherent to the functionality may partially or even completely compromise secret values without ever falsifying proofs of security. In this work, we describe McFIL, an algorithmic approach and accompanying software implementation which automatically quantifies intrinsic leakage for a given functionality. Extending and generalizing the Chosen-Ciphertext attack framework of Beck et al. with a practical heuristic, our approach not only quantifies but maximizes functionality-inherent leakage using Maximum Model Counting within a SAT solver. As a result, McFIL automatically derives approximately-optimal adversary inputs that, when used in secure protocols, maximize information leakage of private values.

翻译：保护私有数据的机密性并用于有效协作长期处于矛盾之中。现代密码学通过安全协议（如多方计算、全同态加密和零知识证明）的快速发展正在弥合这一鸿沟。然而，即使具有可证明的不可区分性或零知识性，由功能固有泄漏导致的机密性损失可能会部分甚至完全泄露秘密值，而不会使安全性证明失效。本文描述了McFIL——一种算法方法及配套软件实现，能够自动量化给定功能的固有泄漏。通过扩展并推广Beck等人的选择密文攻击框架并引入实用启发式方法，我们的方法不仅量化了功能固有泄漏，还利用SAT求解器中的最大模型计数将其最大化。因此，McFIL能够自动推导出近似最优的敌手输入，这些输入在安全协议中使用时，能够最大化私有值的信息泄漏。