Files in this item

FilesDescriptionFormat

application/pdf

application/pdfrdao-analysis.pdf (903kB)
(no description provided)PDF

Description

Title:Statistical Model Checking of RANDAO’s Resilience Against Pre-computed Reveal Strategies
Author(s):Alturki, Musab A.; Rosu, Grigore
Subject(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.
Issue Date:2018-11-19
Genre:Report (Grant or Annual)
Technical Report
Article
Type:Text
Language:English
URI:http://hdl.handle.net/2142/102076
Date Available in IDEALS:2018-11-25


This item appears in the following Collection(s)

Item Statistics