Information Flow Analysis for Detecting Non-Determinism in Blockchain (Artifact)

Authors Luca Olivieri , Luca Negrini , Vincenzo Arceri , Fabio Tagliaferro , Pietro Ferrara , Agostino Cortesi , Fausto Spoto



PDF
Thumbnail PDF

Artifact Description

DARTS.9.2.23.pdf
  • Filesize: 0.5 MB
  • 3 pages

Document Identifiers

Author Details

Luca Olivieri
  • University of Verona, Italy
  • Corvallis Srl, Padova, Italy
Luca Negrini
  • Corvallis Srl, Padova, Italy
Vincenzo Arceri
  • University of Parma, Italy
Fabio Tagliaferro
  • CYS4 Srl, Florence, Italy
Pietro Ferrara
  • Ca' Foscari University of Venice, Italy
Agostino Cortesi
  • Ca' Foscari University of Venice, Italy
Fausto Spoto
  • University of Verona, Italy

Cite As Get BibTex

Luca Olivieri, Luca Negrini, Vincenzo Arceri, Fabio Tagliaferro, Pietro Ferrara, Agostino Cortesi, and Fausto Spoto. Information Flow Analysis for Detecting Non-Determinism in Blockchain (Artifact). In Special Issue of the 37th European Conference on Object-Oriented Programming (ECOOP 2023). Dagstuhl Artifacts Series (DARTS), Volume 9, Issue 2, pp. 23:1-23:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023) https://doi.org/10.4230/DARTS.9.2.23

Artifact

  MD5 Sum: 82404092ce81342ef212de6cefb3e5e2 (Get MD5 Sum)

Artifact Evaluation Policy

The artifact has been evaluated as described in the ECOOP 2023 Call for Artifacts and the ACM Artifact Review and Badging Policy

Abstract

A mandatory feature for blockchain software, such as smart contracts and decentralized applications, is determinism. In fact, non-deterministic behaviors do not allow blockchain nodes to reach one common consensual state or a deterministic response, which causes the blockchain to be forked, stopped, or to deny services. While domain-specific languages are deterministic by design, general-purpose languages widely used for the development of smart contracts such as Go, provide many sources of non-determinism. However, not all non-deterministic behaviours are critical. In fact, only those that affect the state or the response of the blockchain can cause problems, as other uses (for example, logging) are only observable by the node that executes the application and not by others. Therefore, some frameworks for blockchains, such as Hyperledger Fabric or Cosmos SDK, do not prohibit the use of non-deterministic constructs but leave the programmer the burden of ensuring that the blockchain application is deterministic. In this paper, we present a flow-based approach to detect non-deterministic vulnerabilities which could compromise the blockchain. The analysis is implemented in GoLiSA, a semantics-based static analyzer for Go applications. Our experimental results show that GoLiSA is able to detect all vulnerabilities related to non-determinism on a significant set of applications, with better results than other open-source analyzers for blockchain software written in Go.

Subject Classification

ACM Subject Classification
  • Security and privacy → Distributed systems security
  • Theory of computation → Program analysis
  • Theory of computation → Program verification
  • Software and its engineering → Software notations and tools
Keywords
  • Static Analysis
  • Program Verification
  • Non-determinism
  • Blockchain
  • Smart contracts
  • DApps
  • Go language

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail