University of Illinois Urbana-Champaign

Statistical Model Checking of RANDAO’s Resilience Against Pre-computed Reveal Strategies

Alturki, Musab A.; Roşu, Grigore

Content Files
rdao-analysis.pdf

Permalink

https://hdl.handle.net/2142/102076

Description

Title
Statistical Model Checking of RANDAO’s Resilience Against Pre-computed Reveal Strategies
Author(s)
  • Alturki, Musab A.
  • Roşu, Grigore
Issue Date
2018-11-19
Keyword(s)
  • Randao
  • formal modeling
  • statistical model checking
Date of Ingest
2018-11-25T20:26:03Z
Abstract
Decentralized (pseudo-)random number generation (RNG) is a core process of many emerging distributed systems, including perhaps most prominently, the upcoming Ethereum 2.0 (a.k.a. Serenity) protocol. To ensure security and proper operation, the randomness beacon must be unpredictable and hard to manipulate. A commonly accepted implementation scheme for decentralized RNG is a commit-reveal scheme, known as RANDAO, coupled with a reward system that incentivizes successful participation. However, this approach may still be susceptible to look-ahead attacks, in which an attacker (controlling a certain subset of participants) may attempt to pre-compute the outcomes of (possibly many) reveal strategies, and thus may bias the generated random number to his advantage. To formally evaluate resilience of RANDAO against such attacks, we develop a probabilistic model in rewriting logic of the RANDAO scheme (in the context of Serenity), and then apply statistical model checking and quantitative verification algorithms (using Maude and PVeStA) to analyze two different properties that provide different measures of bias that the attacker could potentially achieve using pre-computed strategies. We show through this analysis that unless the attacker is already controlling a sizable portion of validators and is aggressively attempting to maximize the number of last compromised proposers in the proposers list, the expected achievable bias is quite limited. The full specification of the models developed in this work are available online at https://github.com/runtimeverification/rdao-smc.
Type of Resource
text
Genre of Resource
  • Report (Grant or Annual)
  • Technical Report
  • Article
Language
en
Permalink
http://hdl.handle.net/2142/102076

Owning Collections

Research and Tech Reports - Computer Science PRIMARY