Explore the latest research from Facebook

All Publications

November 3, 2020 Lefteris Kokoris Kogias, Dahlia Malkhi, Alexander Spiegelman
Paper

Asynchronous Distributed Key Generation for Computationally Secure Randomness, Consensus, and Threshold Signatures

In this paper, we present the first Asynchronous Distributed Key Generation (ADKG) algorithm which is also the first distributed key generation algorithm that can generate cryptographic keys with a dual (𝑓, 2𝑓 + 1)−threshold (where 𝑓 is the number of faulty parties).
Paper
November 1, 2020 Mathieu Baudet, George Danezis, Alberto Sonnino
Paper

FastPay: High-Performance Byzantine Fault Tolerant Settlement

FastPay allows a set of distributed authorities, some of which are Byzantine, to maintain a high-integrity and availability settlement system for pre-funded payments. It can be used to settle payments in a native unit of value (crypto-currency), or as a financial side-infrastructure to support retail payments in fiat currencies. FastPay is based on Byzantine Consistent Broadcast as its core primitive, foregoing the expenses of full atomic commit channels (consensus).
Paper
October 23, 2020 Sarah Azouvi, George Danezis, Valeria Nikolaenko
Paper

Winkle: Foiling Long-Range Attacks in Proof-of-Stake Systems

Winkle protects any validator-based byzantine fault tolerant consensus mechanisms, such as those used in modern Proof-of-Stake blockchains, against long-range attacks where old validators’ signature keys get compromised. Winkle is a decentralized secondary layer of client-based validation, where a client includes a single additional field into a transaction that they sign: a hash of the previously sequenced block.
Paper
October 22, 2020 Kostas Chalkias, François Garillot, Valeria Nikolaenko
Paper

Taming the many EdDSAs

This paper analyses security of concrete instantiations of EdDSA by identifying exploitable inconsistencies between standardization recommendations and Ed25519 implementations. We mainly focus on current ambiguity regarding signature verification equations, binding and malleability guarantees, and incompatibilities between randomized batch and single verification.
Paper
October 21, 2020 Emma Zhong, Kevin Cheang, Shaz Qadeer, Wolfgang Grieskamp, Sam Blackshear, Junkil Park, Yoni Zohar, Clark Barrett, David Dill
Paper

The Move Prover

The Libra blockchain is designed to store billions of dollars in assets, so the security of code that executes transactions is important. The Libra blockchain has a new language for implementing transactions, called “Move.” This paper describes the Move Prover, an automatic formal verification system for Move.
Paper
September 15, 2020 Ankush Das, Shaz Qadeer
Paper

Exact and Linear-Time Gas-Cost Analysis

Blockchains support execution of smart contracts: programs encoding complex transaction protocols between distrusting parties. Due to their distributed nature, blockchains rely on third-party miners to execute and validate transactions. Miners are compensated by charging users with gas based on the execution cost of the transaction. To compute the exact gas cost, blockchains track gas cost dynamically creating its own overhead. This paper presents a static exact gas-cost analysis technique that can be employed to eliminate dynamic gas tracking.
Paper
July 15, 2020 Bernhard Kragl, Shaz Qadeer, Thomas A. Henzinger
Paper

Refinement for Structured Concurrent Programs

This paper presents a foundation for refining concurrent programs with structured control flow. The verification problem is decomposed into subproblems that aid interactive program development, proof reuse, and automation. The formalization in this paper is the basis of a new design and implementation of the Civl verifier.
Paper
July 15, 2020 Bernhard Kragl, Constantin Enea, Thomas A. Henzinger, Suha Orhun Mutluergil, Shaz Qadeer
Paper

Inductive Sequentialization of Asynchronous Programs

In this paper, we introduce inductive sequentialization, a new proof rule that sidesteps this complexity via a sequential reduction, a sequential program that captures every behavior of the original program up to reordering of coarse-grained commutative actions.
Paper
July 15, 2020 Jacob R. Lorch, Yixuan Chen, Manos Kapritsos, Bryan Parno, Shaz Qadeer, Upamanyu Sharma, James R. Wilcox, Xueyuan Zhao
Paper

Armada: Low-Effort Verification of High-Performance Concurrent Programs

Safely writing high-performance concurrent programs is notoriously difficult. To aid developers, we introduce Armada, a language and tool designed to formally verify such programs with relatively little effort.
Paper
April 22, 2020 Kostas Chalkias, Kevin Lewi, Payman Mohassel, Valeria Nikolaenko
Paper

Distributed Auditing Proofs of Liabilities

The Distributed Auditing Proofs of Liabilities (DAPOL) are schemes designed to let companies that accept (i) monetary deposits from consumers (i.e., custodial wallets, blockchain exchanges, banks, gambling industry etc.) or (ii) fungible obligations and report claims from users (i.e., daily reporting of COVID-19 cases, negative product reviews, unemployment rate, disapproval voting etc.) to prove their total amount of liabilities or obligations without compromising the privacy of both users’ identity and individual amounts. Throughout this document we’ll often refer to one of DAPOL’s most popular use cases, which is proving solvency of cryptocurrency exchanges.
Paper