Themis: Fast, strong Order-Fairness in Byzantine Consensus
M. Kelkar, S. Deb, S. Long, A. Juels, and S. Kannan.

We introduce Themis, a scheme for introducing fair ordering of transactions into (permissioned) Byzantine consensus protocols with at most f faulty nodes among n >_ 4f + 1. Themis is the first such scheme to achieve (optimistic) linear communication complexity. at the same time, it enforces the strongest notion of fair ordering proposed to date. Themis also achieves standard liveness, rather than the weaker notion of previous work. We show experimentally that Themis can be integrated into state-of-the-art consensus protocols with minimal modification or performance overhead. Additionally, we introduce a suite of experiments of general interest for evaluating the practical strength of various notions of fair ordering and the resilience of fair-ordering protocols to adversarial manipulation. We use this suite of experiments to show that the notion of fair ordering enforced by Themis is significantly stronger in theory and for realistic workloads than those of competing systems. We believe Themis offers strong practical protection against many types of transaction-ordering attacks - such as front-running - that are currently impacting commonly used smart contract systems.

Publicly Auditable MPC-as-a-Service with succinct verification and universal setup
S. Kanjalkar, Y. Zhang, S. Gandlur, and A. Miller.

In recent years, multiparty computation as a service (MPCaaS) has gained popularity as a way to build distributed privacy-preserving systems. We argue that for many such applications, we should also require that the MPC protocol is publicly auditable, meaning that anyone can check the given computation is carried out correctly -- even if the server nodes carrying out the computation are all corrupt. In a nutshell, the way to make an MPC protocol auditable is to combine an underlying MPC protocol with verifiable computing proof (in particular, a SNARK). Building a general-purpose MPCaaS from existing constructions would require us to perform a costly "trusted setup" every time we wish to run a new or modified application. To address this, we provide the first efficient construction for auditable MPC that has a one-time universal setup. Despite improving the trusted setup, we match the state-of-the-art in asymptotic performance: the server nodes incur a linear computation overhead and constant round communication overhead compared to the underlying MPC, and the audit size and verification are logarithmic in the application circuit size. We also provide an implementation and benchmarks that support our asymptotic analysis in example applications. Furthermore, compared with existing auditable MPC protocols, besides offering a universal setup our construction also has a 3x smaller proof, 3x faster verification time and comparable prover time.

Clockwork Finance: Automated Analysis of Economic Security in Smart Contracts
K. Babel, P. Daian, M. Kelkar, and A. Juels.

We introduce the Clockwork Finance Framework (CFF), a general purpose, formal verification framework for mechanized reasoning about the economic security properties of composed decentralized-finance (DeFi) smart contracts. CFF features three key properties. It is contract complete, meaning that it can model any smart contract platform and all its contracts---Turing complete or otherwise. It does so with asymptotically optimal model size. It is also attack-exhaustive by construction, meaning that it can automatically and mechanically extract all possible economic attacks on users cryptocurrency across modeled contracts. Thanks to these properties, CFF can support multiple goals-economic security analysis of contracts by developers, analysis of DeFi trading risks by users, and optimization of arbitrage opportunities by bots or miners. Because CFF offers composability, it can support these goals with reasoning over any desired set of potentially interacting smart contract models. We instantiate CFF as an executable model for Ethereum contracts that incorporates a state-of-the-art deductive verifier. Building on previous work, we introduce extractable value (EV), a new formal notion of economic security in composed DeFi contracts that is both a basis for CFF analyses and of general interest. We construct modular, human-readable, composable CFF models of four popular, deployed DeFi protocols in Ethereum: Uniswap, Uniswap V2, Sushiwap, and MakerDAO, representing a combined 17 billion USD in value as of August 2021. We use these models to show experimentally that CFF is practical and can drive useful, data-based EV-based insights from real world transaction activity. Without any explicitly programmed attack strategies, CFF uncovers on average an expected $56 million of EV per month in the recent past.

GoAT: File Geolocation via Anchor Timestamping
D. Maram, I. Bentov, M. Kelkar, and A. Juels.

Blockchain systems are rapidly gaining traction. Decentralized storage systems like Filecoin are a crucial component of this ecosystem that aim to provide robust file storage through a Proof of Replication (PoRep) or its variants. However, a PoRep actually offers limited robustness. Indeed if all the file replicas are stored on a single hard disk, a single catastrophic event is enough to lose the file. We introduce a new primitive, Proof of Geo-Retrievability or in short "GeoPoRet", that enables proving that a file is located within a strict geographic boundary. Using GeoPoRet, one can trivially construct a PoRep by proving that a file is in several distinct geographic regions. We define what it means for a GeoPoRet scheme to be complete and sound, in the process making important extentions to prior formalism. We propose GoAT, a practical GeoPoRet scheme to prove file geolocation. Unlike previous geolocation systems that rely on trusted-verifiers, GoAT bootstraps using public timestamping servers on the internet that serve as geolocation anchors, tolerating a local threshold of dishonest anchors. GoAT internally uses a communication-efficient Proof-of-Retrievability (PoRet) scheme in a novel way to achieve constant-size PoRet-component in its proofs. We validate GoAT's practicality by conducting an initial measurement study to find usable anchors and also perform a real-world experiment. The results show that a significant fraction of the internet can be used as GoAT anchors. Furthermore, GoAT achieves geolocation radii as little as 1000km.

Forsage: Anatomy of a Smart-Contract Pyramid Scheme
T. Kell, H. Yousaf, S. Allen, S. Meiklejohn, and A. Juels.

Pyramid schemes are investment scams in which top-level participants in a hierarchical network recruit and profit from an expanding base of defrauded newer participants. Pyramid schemes have existed for over a century, but there have been no in-depth studies of their dynamics and communities because of the opacity of participants' transactions. In this paper, we present an empirical study of Forsage, a pyramid scheme implemented as a smart contract and at its peak one of the largest consumers of resources in Ethereum. As a smart contract, Forsage makes its (byte)code and all of its transactions visible on the blockchain. We take advantage of this unprecedented transparency to gain insight into the mechanics, impact on participants, and evolution of Forsage. We quantify the (multi-million-dollar) gains of top-level participants as well as the losses of the vast majority (around 88%) of users. We analyze Forsage code both manually and using a purpose-built transaction simulator to uncover the complex mechanics of the scheme. Through complementary study of promotional videos and social media, we show how Forsage promoters have leveraged the unique features of smart contracts to lure users with false claims of trustworthiness and profitability, and how Forsage activity is concentrated within a small number of national communities.

Early Evidence of Effectiveness of Digital Contact Tracing for SARS-CoV-2 in Switzerland
M. Salathe, C. L. Althaus, N. Anderegg, D. Antonioli, T. Ballouz, E. Bugnion, S. Capkun, D. Jackson, S.-I. Kim, J. R. Larus, N. Low, W. Lueks, D. Menges, C. Moullet, M. Payer, J. Riou, T. Stadler, C. Troncoso, E. Vayena, and V. von Wyl.

In the wake of the pandemic of coronavirus disease 2019 (COVID-19), contact tracing has become a key element of strategies to control the spread of severe acute respiratory syndrome coronavirus 2019 (SARS-CoV-2). Given the rapid and intense spread of SARS-CoV-2, digital contact tracing has emerged as a potential complementary tool to support containment and mitigation efforts. Early modelling studies highlighted the potential of digital contact tracing to break transmission chains, and Google and Apple subsequently developed the Exposure Notification (EN) framework, making it available to the vast majority of smartphones. A growing number of governments have launched or announced EN-based contact tracing apps, but their effectiveness remains unknown. Here, we report early findings of the digital contact tracing app deployment in Switzerland. We demonstrate proof-of-principle that digital contact tracing reaches exposed contacts, who then test positive for SARS-CoV-2. This indicates that digital contact tracing is an effective complementary tool for controlling the spread of SARS-CoV-2. Continued technical improvement and international compatibility can further increase the efficacy, particularly also across country borders.

PriFi: Low-Latency Anonymity for Organizational Networks
L. Barman, I. Dacosta, M. Zamani, E. Zhai, A. Pyrgelis, B. Ford, J. Feigenbaum, and J-P. Hubaux.

Organizational networks are vulnerable to traffic-analysis attacks that enable adversaries to infer sensitive information from network traffic — even if encryption is used. Typical anonymous communication networks are tailored to the Internet and are poorly suited for organizational networks. We present PriFi, an anonymous communication protocol for LANs, which protects users against eaves-droppers and provides high-performance traffic-analysis resistance. PriFi builds on Dining Cryptographers networks (DC-nets), but reduces the high communication latency of prior designs via a new client/relay/server architecture, in which a client’s packets remain on their usual network path without additional hops, and in which a set of remote servers assist the anonymization process without adding latency. PriFi also solves the challenge of equivocation attacks, which are not addressed by related work, by encrypting traffic based on communication history. Our evaluation shows that PriFi introduces modest latency overhead (≈100ms for 100 clients) and is compatible with delay-sensitive applications such as Voice-over-IP

Tuning PoW with Hybrid Expenditure
I. Tsabary, A. Spiegelman, and I. Eyal.

Proof of Work (PoW) is a Sybil-deterrence security mechanism. It introduces an external cost to a system by requiring computational effort to perform actions. However, since its inception, a central challenge was to tune this cost. Initial designs for deterring spam email and DoS attacks applied overhead equally to honest participants and attackers. Requiring too little effort did not deter attacks, whereas too much encumbered honest participation. This might be the reason it was never widely adopted. Nakamoto overcame this trade-off in Bitcoin by distinguishing desired from malicious behavior and introducing internal rewards for the former. This solution gained popularity in securing cryptocurrencies and using the virtual internally-minted tokens for rewards. However, in existing blockchain protocols the internal rewards fund (almost) the same value of external expenses. Thus, as the token value soars, so does the PoW expenditure. Bitcoin PoW, for example, already expends as much electricity as Colombia or Switzerland. This amount of resource-guzzling is unsustainable and hinders even wider adoption of these systems. In this work we present Hybrid Expenditure Blockchain (HEB), a novel PoW mechanism. HEB is a generalization of Nakamoto's protocol that enables tuning the external expenditure by introducing a complementary internal-expenditure mechanism. Thus, for the first time, HEB decouples external expenditure from the reward value. We show a practical parameter choice by which HEB requires significantly less external consumption compare to Nakamoto's protocol, its resilience against rational attackers is similar, and it retains the decentralized and permissionless nature of the system. Taking the Bitcoin ecosystem as an example, HEB cuts the electricity consumption by half.

Foundations of Distributed Consensus and Blockchains
E. Shi.

Back in the 1970s, it became clear that computers were going to be used in aircraft control. Since this was a mission-critical system, it was important to replicate it on multiple machines. But how do we make sure that the multiple machines share a consistent view and make consistent decision? To understand this problem better, NASA sponsored the Software Implemented Fault Tolerance (SIFT) project [WLG+89], whose goal was to build a resilient aircraft control system that tolerated faults of its components. The famous work of Lambort et al. [LSP82] which introduced the well-known Byzantine Generals problem, came out of this project. This work laid the foundation of distributed consensus. Since then, distributed consensus has come a long way and has been deployed in many application settings. In the past couple of decades, companies like Google and Facebook have adopted distributed consensus as part of their computing infrastructure, e.g., to replicate mission-critical services such as Google Wallet and Facebook Credit. Starting in 2009, Bitcoin and various subsequent cryptocurrencies came around and became popular. The cryptocurrencies achieved a new breakthrough in distributed consensus, since they showed, for the first time, that consensus is viable in a decentralized, permissionless environment where anyone is allowed to participate. In this course, you will learn the mathematical foundations of distributed consensus as well as how to construct consensus protocols and prove them secure. We will motivate distributed consensus with a modern narrative, and yet we will cover the classical theoretical foundations of consensus. We will cover both classical, permissioned consensus protocols, as well as modern, permissionless consensus protocols such as Bitcoin.

Published Papers








2015 and Older