McFIL: Model Counting Functionality-Inherent Leakage

TL;DR

McFIL is an algorithmic tool that quantifies and maximizes the inherent information leakage in secure protocols by leveraging model counting within SAT solvers, aiding in understanding confidentiality risks.

Contribution

The paper introduces McFIL, a novel approach that automatically measures and maximizes functionality-inherent leakage using maximum model counting, extending existing attack frameworks.

Findings

Quantifies intrinsic leakage in secure functionalities.

Maximizes information leakage using SAT-based model counting.

Provides a practical heuristic for leakage analysis.

Abstract

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.