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

Alturki, Musab A.; Roşu, Grigore

Permalink

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

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

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

Language

en

Permalink

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

Owning Collections