Anitha Gollamudi and Stephen Chong. 4/22/2021. “Expressive Authorization Policies using Computation Principles ”. Publisher's VersionAbstract

In authorization logics, it is natural to treat computations as principals, since systems need to decide how much authority to give computations when they execute. But unlike other kinds of principals, the authority that we want to give to computations might be based on properties of the computation itself, such as whether the computation is differentially private, or whether the computation is memory safe.

Existing authorization logics do not treat computation principals specially. Instead, they identify computation principals using a brittle hash-based naming scheme: minor changes to the code produce a distinct principal, even if the new computation is equivalent to the original one. Moreover, existing authorization logics typically treat computation principals as “black boxes,” leaving any reasoning about the structure, semantics, or other properties of the computation out of the logic.

We introduce Coal, a novel programming-language calculus that embeds an authorization logic in its type system via the Curry-Howard isomorphism. A key innovation of Coal is computation principals: computations that can be treated like other principals but also allow reasoning about the computation itself. Critically, Coal allows equivalent computations to be treated as equivalent principals, avoiding the brittleness of identity-based approaches to computation principals. Coal enables us to cleanly express fine-grained access control policies that are dependent on the structure and semantics of computations, such as expressing trust in all computations that are analyzed to be differentially private by any program analyzer that has been verified correct.

Matheus V. X. Ferreira, Daniel J. Moroz, David C. Parkes, and Mitchell Stern. 3/25/2021. “Dynamic Posted-Price Mechanisms for the Blockchain Transaction-Fee Market,” Pp. 2103.14144. Publisher's VersionAbstract

In recent years, prominent blockchain systems such as Bitcoin and Ethereum have experienced explosive growth in transaction volume, leading to frequent surges in demand for limited block space, causing transaction fees to fluctuate by orders of magnitude. Under the standard first-price auction approach, users find it difficult to estimate how much they need to bid to get their transactions accepted (balancing the risk of delay with a preference to avoid paying more than is necessary).

In light of these issues, new transaction fee mechanisms have been proposed, most notably EIP-1559, proposed by Buterin et al. [4]. A problem with EIP-1559 is that under market instability, it again reduces to a first-price auction. Here, we propose dynamic posted-price mechanisms, which are ex post Nash incentive compatible for myopic bidders and dominant strategy incentive compatible for myopic miners. We give sufficient conditions for which our mechanisms are stable and approximately welfare optimal in the probabilistic setting where each time step, bidders are drawn i.i.d. from a static (but unknown) distribution. Under this setting, we show instances where our dynamic mechanisms are stable, but EIP-1559 is unstable. Our main technical contribution is an iterative algorithm that, given oracle access to a Lipschitz continuous and concave function f, converges to a fixed point of f.

Michael Neuder, Daniel J. Moroz, Rithvik Rao, and David C. Parkes. 2/3/2021. “Low-cost attacks on Ethereum 2.0 by sub-1/3 stakeholders.” Workshop on Game Theory in Blockchain at the 16th Conference on Web and Internet Economics (WINE)., Pp. 2102.02247. Publisher's VersionAbstract
We outline two dishonest strategies that can be cheaply executed on the Ethereum 2.0 beacon chain, even by validators holding less than one-third of the total stake: malicious chain reorganizations (“reorgs”) and finality delays. In a malicious reorg, an attacker withholds their blocks and attestations before releasing them at an opportune time in order to force a chain reorganization, which they can take advantage of by double-spending or front-running transactions. To execute a finality delay an attacker uses delayed block releases and withholding of attestations to increase the mean and variance of the time it takes blocks to become finalized. This impacts the efficiency and predictability of the system. We provide a probabilistic and cost analysis for each of these attacks, considering a validator with 30% of the total stake.
Ran Ben Basat, Gil Einziger, Michael Mitzenmacher, and Shay Vargaftik. 2021. “SALSA: Self-Adjusting Lean Streaming Analytics .” 37th IEEE International Conference on Data Engineering (ICDE 2021). Publisher's VersionAbstract
Counters are the fundamental building block of many data sketching schemes, which hash items to a small number of counters and account for collisions to provide good approximations for frequencies and other measures. Most exist- ing methods rely on fixed-size counters, which may be wasteful in terms of space, as counters must be large enough to eliminate any risk of overflow. Instead, some solutions use small, fixed-size counters that may overflow into secondary structures. This paper takes a different approach. We propose a simple and general method called SALSA for dynamic re-sizing of counters, and show its effectiveness. SALSA starts with small counters, and overflowing counters simply merge with their neighbors. SALSA can thereby allow more counters for a given space, expanding them as necessary to represent large numbers. Our evaluation demonstrates that, at the cost of a small overhead for its merging logic, SALSA significantly improves the accuracy of popular schemes (such as Count-Min Sketch and Count Sketch) over a variety of tasks. Our code is released as open source [1].
Owen Ardena, Anitha Gollamudib, Ethan Cecchettic, Stephen Chongb, and Andrew C. Myers. 2021. A Calculus for Flow-Limited Authorization . Publisher's VersionAbstract
Real-world applications routinely make authorization decisions based on dynamic computation. Reasoning about dynamically computed authority is challenging. Integrity of the system might be compromised if attackers can improperly influence the authorizing computation. Confidentiality can also be compromised by authorization, since authorization decisions are often based on sensitive data such as membership lists and passwords. Previous formal models for authorization do not fully address the security implications of permitting trust relationships to change, which limits their ability to reason about authority that derives from dynamic computation. Our goal is an approach to constructing dynamic authorization mechanisms that do not violate confidentiality or integrity. The Flow-Limited Authorization Calculus (FLAC) is a simple, expressive model for reasoning about dynamic authorization as well as an information flow control language for securely implementing various authorization mechanisms. FLAC combines the insights of two previous models: it extends the Dependency Core Calculus with features made possible by the Flow-Limited Authorization Model. FLAC provides strong end-to-end information security guarantees even for programs that incorporate and implement rich dynamic authorization mechanisms. These guarantees include noninterference and robust declassification, which prevent attackers from influencing information disclosures in unauthorized ways. We prove these security properties formally for all FLAC programs and explore the expressiveness of FLAC with several examples.
Ran Ben Basat, Michael Mitzenmacher, and Shay Vargaftik. 2021. “How to Send a Real Number Using a Single Bit (and Some Shared Randomness).” International Colloquium on Automata, Languages, and Programming (ICALP 2021). Publisher's VersionAbstract

We consider the fundamental problem of communicating an estimate of a real number x ∈ [0, 1] using a single bit. A sender that knows x chooses a value X ∈ {0, 1} to transmit. In turn, a receiver estimates x based on the value of X. The goal is to minimize the cost, defined as the worst-case (over the choice of x) expected squared error.

We first overview common biased and unbiased estimation approaches and prove their optimality when no shared randomness is allowed. We then show how a small amount of shared randomness, which can be as low as a single bit, reduces the cost in both cases. Specifically, we derive lower bounds on the cost attainable by any algorithm with unrestricted use of shared randomness and propose optimal and near-optimal solutions that use a small number of shared random bits. Finally, we discuss open problems and future directions.

Kapil Vaidya, Eric Knorr, Tim Kraska, and Michael Mitzenmacher. 10/4/2020. “Partitioned Learned Bloom Filters .” International Conference On Learned Representations (ICLR 2021. Publisher's VersionAbstract
Bloom filters are space-efficient probabilistic data structures that are used to test whether an element is a member of a set, and may return false positives. Recently, variations referred to as learned Bloom filters were developed that can provide improved performance in terms of the rate of false positives, by using a learned model for the represented set. However, previous methods for learned Bloom filters do not take full advantage of the learned model. Here we show how to frame the problem of optimal model utilization as an optimization problem, and using our framework derive algorithms that can achieve near-optimal performance in many cases. Experimental results from both simulated and real-world datasets show significant performance improvements from our optimization approach over both the original learned Bloom filter constructions and previously proposed heuristic improvements.
Michael Neuder, Daniel J. Moroz, Rithvik Rao, and David C. Parkes. 4/8/2020. “Selfish Behavior in the Tezos Proof-of-Stake Protocol.” Cryptoeconomic Systems (CES) Conference 4/8/2020. Publisher's VersionAbstract
Proof-of-Stake consensus protocols give rise to complex mod- eling challenges. We analyze the Babylon update (October 2019) to the Proof-of-Stake protocol on the Tezos blockchain, and demonstrate that, under certain conditions, rational partic- ipants are incentivized to behave dishonestly. In doing so, we provide a theoretical analysis of the feasibility and profitabil- ity of a block stealing attack that we call selfish endorsing, a concrete instance of an attack previously only theoretically considered. We propose and analyze a simple change to the Tezos protocol which significantly reduces the (already small) profitability of this dishonest behavior, and introduce a new de- lay and reward scheme that is provably secure against length-1 and length-2 selfish endorsing attacks. Our framework pro- vides a template for analyzing other Proof-of-Stake protocols for the possibility of selfish behavior.
Barton E. Lee, Daniel J. Moroz, and David C. Parkes. 2/8/2020. “The Political Economy of Blockchain Governance”. Publisher's VersionAbstract
We develop a theory of blockchain governance using tools from formal political theory. The software underlying blockchain projects is frequently updated (forked) to implement new policies, and these forks are the subject of our inquiry. We investigate the ways in which the decentralized governance structure and preferences of users influence which policies are implemented, considering network effects as well as user preferences for different policies. We describe several types of forks and identify the strategic conditions necessary for each. We show that network-effects can motivate less moderate policy proposals, and highlight the role of market frictions created by cryptocurrency exchanges in promoting non-contentious forks that are adopted by all users. The model explains counter-intuitive phenomena that have been observed in the governance of blockchain systems.
Daniel J. Moroz, Daniel J. Aronoff, Neha Narula, and David C. Parkes. 2/2020. “Double-Spend Counterattacks: Threat of Retaliation in Proof-of-Work Systems.” Cryptoeconomic Systems (CES) Conference 2020, Pp. 2002.10736. Publisher's VersionAbstract
Proof-of-Work mining is intended to provide blockchains with robustness against double-spend attacks. However, an economic analysis that follows from Budish (2018), which considers free entry conditions together with the ability to rent sufficient hashrate to conduct an attack, suggests that the resulting block rewards can make an attack cheap. We formalize a defense to double-spend attacks. We show that when the victim can counterattack in the same way as the attacker, this leads to a variation on the classic game-theoretic War of Attrition model. The threat of this kind of counterattack induces a subgame perfect equilibrium in which no attack occurs in the first place.
Michael Neuder, Daniel J. Moroz, Rithvik Rao, and David C. Parkes. 2020. “Defending Against Malicious Reorgs in Tezos Proof-of-Stake.” ACM Conference on Advances in Financial Technologies (AFT) 2020, Pp. 46-58. Publisher's VersionAbstract
Blockchains are intended to be immutable, so an attacker who is able to delete transactions through a chain reorganization (a malicious reorg) can perform a profitable double-spend attack. We study the rate at which an attacker can execute reorgs in the Tezos Proof-of-Stake protocol. As an example, an attacker with 40% of the staking power is able to execute a 20-block malicious reorg at an average rate of once per day, and the attack probability increases super-linearly as the staking power grows beyond 40%. Moreover, an attacker of the Tezos protocol knows in advance when an attack opportunity will arise, and can use this knowledge to arrange transactions to double-spend. We show that in particular cases, the Tezos protocol can be adjusted to protect against deep reorgs. For instance, we demonstrate protocol parameters that reduce the rate of length-20 reorg opportunities for a 40% attacker by two orders of magnitude. We also observe a trade-off between optimizing for robustness to deep reorgs (costly deviations that may be net profitable because they enable double-spends) and robustness to selfish mining (mining deviations that result in typically short reorgs that are profitable even without double-spends). That is, the parameters that optimally protect against one make the other attack easy. Finally, we develop a method that monitors the Tezos blockchain health with respect to malicious reorgs using only publicly available information.
Shrutarshi Basu, Nate Foster, and James Grimmelmann. 10/23/2019. “Property conveyances as a programming language.” 2019 ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software. Athens Greece. Publisher's VersionAbstract
Anglo-American law enables property owners to split up rights among multiple entities by breaking their ownership apart into future interests that may evolve over time. The conveyances that owners use to transfer and subdivide property rights follow rigid syntactic conventions and are governed by an intricate body of interlocking doctrines that determine their legal effect. These doctrines have been codified, but only in informal and potentially ambiguous ways. This paper presents preliminary work in developing a formal model for expressing and analyzing property conveyances. We develop a domain-specific language capable of expressing a wide range of conveyances in a syntax approximating natural language. This language desugars into a core calculus for which we develop operational and denotational semantics capturing a variety of important properties of property law in practice. We evaluate an initial implementation of our languages and semantics on examples from a popular property law textbook.
David C. Parkes, Paul Tylkin, and Lirong Xi. 11/25/2017. “Thwarting Vote Buying Through Decoy Ballots .” Proceedings of the 26th International Joint Conference on Artificial Intelligence (IJCAI 2017). Melbourne, Australia. Publisher's VersionAbstract
There is increasing interest in promoting participa- tory democracy, in particular by allowing voting by mail or internet and through random-sample elec- tions. A pernicious concern, though, is that of vote buying, which occurs when a bad actor seeks to buy ballots, paying someone to vote against their own intent. This becomes possible whenever a voter is able to sell evidence of which way she voted. We show how to thwart vote buying through de- coy ballots, which are not counted but are indistin- guishable from real ballots to a buyer. We show that an Election Authority can significantly reduce the power of vote buying through a small number of optimally distributed decoys, and model societal processes by which decoys could be distributed.