Document Open Access Logo

Information Flow Analysis for Detecting Non-Determinism in Blockchain

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

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2023.23.pdf
  • Filesize: 1.29 MB
  • 25 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

Funding

  • Arceri, Vincenzo: Bando di Ateneo per la ricerca 2022, founded by University of Parma, project number: MUR_DM737_2022_FIL_PROGETTI_B_ARCERI_COFIN, Formal verification of GPLs blockchain smart contracts
  • Ferrara, Pietro: SERICS (PE00000014) under the NRRP MUR program funded by the EU - NGEU, iNEST-Interconnected NordEst Innovation Ecosystem funded by PNRR (Mission 4.2, Investment 1.5) NextGeneration EU - Project ID: ECS 00000043, and SPIN-2021 "Static Analysis for Data Scientists" funded by Ca' Foscari University
  • Cortesi, Agostino: SERICS (PE00000014) under the NRRP MUR program funded by the EU - NGEU, iNEST-Interconnected NordEst Innovation Ecosystem funded by PNRR (Mission 4.2, Investment 1.5) NextGeneration EU - Project ID: ECS 00000043, and SPIN-2021 "Ressa-Rob" funded by Ca' Foscari University

Cite AsGet 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. In 37th European Conference on Object-Oriented Programming (ECOOP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 263, pp. 23:1-23:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.ECOOP.2023.23

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
    0
    Metadata Views

Supplementary Materials

References

  1. Lars Ole Andersen. Program Analysis and Specialization for the C Programming Language, 1994. Accessed: 01-12-2022. URL: https://www.cs.cornell.edu/courses/cs711/2005fa/papers/andersen-thesis94.pdf.
  2. Elli Androulaki, Artem Barger, Vita Bortnikov, Christian Cachin, Konstantinos Christidis, Angelo De Caro, David Enyeart, Christopher Ferris, Gennady Laventman, Yacov Manevich, Srinivasan Muralidharan, Chet Murthy, Binh Nguyen, Manish Sethi, Gari Singh, Keith Smith, Alessandro Sorniotti, Chrysoula Stathakopoulou, Marko Vukolic, Sharon Weed Cocco, and Jason Yellick. Hyperledger Fabric: A Distributed Operating System for Permissioned Blockchains. In Proceedings of the Thirteenth EuroSys Conference, EuroSys 2018, Porto, Portugal, April 23-26, 2018, pages 30:1-30:15. ACM, 2018. URL: https://doi.org/10.1145/3190508.3190538.
  3. A. M. Antonopoulos. Mastering Bitcoin: Programming the Open Blockchain. O'Reilly, 2nd edition, 2017. Google Scholar
  4. A. M. Antonopoulos and G. Wood. Mastering Ethereum: Building Smart Contracts and Dapps. O'Reilly, 2018. Google Scholar
  5. Sotirios Brotsis, Nicholas Kolokotronis, Konstantinos Limniotis, Gueltoum Bendiab, and Stavros Shiaeles. On the security and privacy of hyperledger fabric: Challenges and open issues. In 2020 IEEE World Congress on Services (SERVICES), pages 197-204, 2020. URL: https://doi.org/10.1109/SERVICES48979.2020.00049.
  6. E. Buchman. Tendermint: Byzantine Fault Tolerance in the Age of Blockchains. PhD thesis, University of Guelph, 2016. Google Scholar
  7. Ethan Buchman. Byzantine Fault Tolerant State Machine Replication in Any Programming Language. In Proceedings of the 2019 ACM Symposium on Principles of Distributed Computing, PODC '19, page 546, New York, NY, USA, 2019. Association for Computing Machinery. Google Scholar
  8. V. Buterin. Ethereum Whitepaper, 2013. Available at URL: https://ethereum.org/en/whitepaper/.
  9. Krishnendu Chatterjee, Amir Kafshdar Goharshady, and Arash Pourdamghani. Probabilistic Smart Contracts: Secure Randomness on the Blockchain. In IEEE International Conference on Blockchain and Cryptocurrency, ICBC 2019, Seoul, Korea (South), May 14-17, 2019, pages 403-412. IEEE, 2019. URL: https://doi.org/10.1109/BLOC.2019.8751326.
  10. Patrick Cousot. Principles of Abstract Interpretation. MIT Press, 2021. Google Scholar
  11. Dorothy E. Denning. A Lattice Model of Secure Information Flow. Commun. ACM, 19(5):236-243, 1976. URL: https://doi.org/10.1145/360051.360056.
  12. ebuchman. Cosmos-SDK Vulnerability Retrospective: Security Advisory Jackfruit, October 12, 2021, 2021. Accessed: 01-12-2022. URL: https://forum.cosmos.network/t/cosmos-sdk-vulnerability-retrospective-security-advisory-jackfruit-october-12-2021/5349.
  13. Perry A. Emrath and David A. Padua. Automatic Detection of Nondeterminacy in Parallel Programs. In Proceedings of the 1988 ACM SIGPLAN and SIGOPS Workshop on Parallel and Distributed Debugging, PADD '88, pages 89-99, New York, NY, USA, 1988. Association for Computing Machinery. URL: https://doi.org/10.1145/68210.69224.
  14. Michael D. Ernst, Alberto Lovato, Damiano Macedonio, Ciprian Spiridon, and Fausto Spoto. Boolean Formulas for the Static Identification of Injection Attacks in java. In Logic for Programming, Artificial Intelligence, and Reasoning - 20th International Conference, LPAR-20 2015, Suva, Fiji, November 24-28, 2015, Proceedings, volume 9450 of Lecture Notes in Computer Science, pages 130-145. Springer, 2015. URL: https://doi.org/10.1007/978-3-662-48899-7_10.
  15. Pietro Ferrara. A generic framework for heap and value analyses of object-oriented programming languages. Theor. Comput. Sci., 631:43-72, 2016. URL: https://doi.org/10.1016/j.tcs.2016.04.001.
  16. Pietro Ferrara, Elisa Burato, and Fausto Spoto. Security Analysis of the OWASP Benchmark with Julia. In Proceedings of the First Italian Conference on Cybersecurity (ITASEC17), Venice, Italy, January 17-20, 2017, volume 1816 of CEUR Workshop Proceedings, pages 242-247. CEUR-WS.org, 2017. Accessed: 01-12-2022. URL: http://ceur-ws.org/Vol-1816/paper-24.pdf.
  17. Pietro Ferrara, Amit Kr Mandal, Agostino Cortesi, and Fausto Spoto. Static analysis for discovering IoT vulnerabilities. Int. J. Softw. Tools Technol. Transf., 23(1):71-88, 2021. URL: https://doi.org/10.1007/s10009-020-00592-x.
  18. Pietro Ferrara and Luca Negrini. SARL: Oo framework specification for static analysis. In Maria Christakis, Nadia Polikarpova, Parasara Sridhar Duggirala, and Peter Schrammel, editors, Software Verification, pages 3-20, Cham, 2020. Springer International Publishing. Google Scholar
  19. Pietro Ferrara, Luca Negrini, Vincenzo Arceri, and Agostino Cortesi. Static analysis for dummies: experiencing lisa. In Lisa Nguyen Quang Do and Caterina Urban, editors, SOAP@PLDI 2021: Proceedings of the 10th ACM SIGPLAN International Workshop on the State Of the Art in Program Analysis, Virtual Event, Canada, 22 June, 2021, pages 1-6. ACM, 2021. URL: https://doi.org/10.1145/3460946.3464316.
  20. Pietro Ferrara, Luca Olivieri, and Fausto Spoto. Tailoring Taint Analysis to GDPR. In Privacy Technologies and Policy - 6th Annual Privacy Forum, APF 2018, Barcelona, Spain, June 13-14, 2018, Revised Selected Papers, volume 11079 of Lecture Notes in Computer Science, pages 63-76. Springer, 2018. URL: https://doi.org/10.1007/978-3-030-02547-2_4.
  21. Pietro Ferrara, Luca Olivieri, and Fausto Spoto. Backflow: Backward context-sensitive flow reconstruction of taint analysis results. In Verification, Model Checking, and Abstract Interpretation, pages 23-43, Cham, 2020. Springer International Publishing. Google Scholar
  22. Pietro Ferrara, Luca Olivieri, and Fausto Spoto. Static Privacy Analysis by Flow Reconstruction of Tainted data. Int. J. Softw. Eng. Knowl. Eng., 31(7):973-1016, 2021. URL: https://doi.org/10.1142/S0218194021500303.
  23. Luca Foschini, Andrea Gavagna, Giuseppe Martuscelli, and Rebecca Montanari. Hyperledger Fabric Blockchain: Chaincode Performance Analysis. In 2020 IEEE International Conference on Communications, ICC 2020, Dublin, Ireland, June 7-11, 2020, pages 1-6. IEEE, 2020. URL: https://doi.org/10.1109/ICC40277.2020.9149080.
  24. Joseph A. Goguen and José Meseguer. Security Policies and Security Models. In 1982 IEEE Symposium on Security and Privacy, Oakland, CA, USA, April 26-28, 1982, pages 11-20. IEEE Computer Society, 1982. URL: https://doi.org/10.1109/SP.1982.10014.
  25. Joseph A. Goguen and José Meseguer. Unwinding and Inference Control. In Proceedings of the 1984 IEEE Symposium on Security and Privacy, Oakland, California, USA, April 29 - May 2, 1984, pages 75-87. IEEE Computer Society, 1984. URL: https://doi.org/10.1109/SP.1984.10019.
  26. Hyperledger. Hyperledger fabric documentation. URL: https://hyperledger-fabric.readthedocs.io/en/release-2.2/blockchain.html#what-is-hyperledger-fabric.
  27. Tendermint Inc. What is Tendermint: A Note on Determinism, 2022. Accessed: 01-12-2022. URL: https://github.com/tendermint/tendermint/blob/7983f9cc36c31e140e46ae5cb00ed39f637ef283/docs/introduction/what-is-tendermint.md#a-note-on-determinism.
  28. Uday P. Khedker and Bageshri Karkare. Efficiency, precision, simplicity, and generality in interprocedural data flow analysis: Resurrecting the classical call strings method. In Compiler Construction, pages 213-228, Berlin, Heidelberg, 2008. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-540-78791-4_15.
  29. J. Kwon. Tendermint: Consensus without mining, 2014. Google Scholar
  30. J. Kwon and E. Buchman. Cosmos whitepaper, 2019. Google Scholar
  31. kzhry. Chaincode Analyzer, 2021. Accessed: 01-12-2022. URL: https://github.com/hyperledger-labs/chaincode-analyzer.
  32. Penghui Lv, Yu Wang, Yazhe Wang, and Qihui Zhou. Potential Risk Detection System of Hyperledger Fabric Smart Contract based on Static Analysis. In IEEE Symposium on Computers and Communications, ISCC 2021, Athens, Greece, September 5-8, 2021, pages 1-7. IEEE, 2021. URL: https://doi.org/10.1109/ISCC53001.2021.9631249.
  33. S. Nakamoto. Bitcoin: A Peer-to-Peer Electronic Cash System. Available at https://bitcoin.org/bitcoin.pdf, 2008.
  34. Luca Negrini. A generic framework for multilanguage analysis. PhD thesis, Universitá Ca' Foscari Venezia, 2023. Google Scholar
  35. Luca Olivieri, Fausto Spoto, and Fabio Tagliaferro. On-Chain Smart Contract Verification over Tendermint. In Financial Cryptography and Data Security. FC 2021 International Workshops - CoDecFin, DeFi, VOTING, and WTSC, Virtual Event, March 5, 2021, Revised Selected Papers, volume 12676 of Lecture Notes in Computer Science, pages 333-347. Springer, 2021. URL: https://doi.org/10.1007/978-3-662-63958-0_28.
  36. Luca Olivieri, Fabio Tagliaferro, Vincenzo Arceri, Marco Ruaro, Luca Negrini, Agostino Cortesi, Pietro Ferrara, Fausto Spoto, and Enrico Talin. Ensuring determinism in blockchain software with golisa: an industrial experience report. In Laure Gonnord and Laura Titolo, editors, SOAP '22: 11th ACM SIGPLAN International Workshop on the State Of the Art in Program Analysis, San Diego, CA, USA, 14 June 2022, pages 23-29. ACM, 2022. URL: https://doi.org/10.1145/3520313.3534658.
  37. Xavier Rival and Kwangkeun Yi. Introduction to static analysis: an abstract interpretation perspective. Mit Press, 2020. Google Scholar
  38. A. Sabelfeld and A.C. Myers. Language-based information-flow security. IEEE Journal on Selected Areas in Communications, 21(1):5-19, 2003. URL: https://doi.org/10.1109/JSAC.2002.806121.
  39. Micha Sharir, Amir Pnueli, et al. Two approaches to interprocedural data flow analysis. New York University. Courant Institute of Mathematical Sciences, 1978. Google Scholar
  40. sivachokkapu. Revivecc, 2021. Accessed: 01-12-2022. URL: https://github.com/sivachokkapu/revive-cc.
  41. Fausto Spoto. A Java Framework for Smart Contracts. In Financial Cryptography and Data Security - FC 2019 International Workshops, VOTING and WTSC, St. Kitts, St. Kitts and Nevis, February 18-22, 2019, Revised Selected Papers, volume 11599 of Lecture Notes in Computer Science, pages 122-137. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-43725-1_10.
  42. Fausto Spoto. Enforcing Determinism of Java Smart Contracts. In Financial Cryptography and Data Security - FC 2020 International Workshops, AsiaUSEC, CoDeFi, VOTING, and WTSC, Kota Kinabalu, Malaysia, February 14, 2020, Revised Selected Papers, volume 12063 of Lecture Notes in Computer Science, pages 568-583. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-54455-3_40.
  43. Omer Tripp, Marco Pistoia, Stephen J. Fink, Manu Sridharan, and Omri Weisman. TAJ: effective taint analysis of web applications. In Proceedings of the 2009 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2009, Dublin, Ireland, June 15-21, 2009, pages 87-97. ACM, 2009. URL: https://doi.org/10.1145/1542476.1542486.
  44. Shuai Wang, Chengyu Zhang, and Zhendong Su. Detecting nondeterministic payment bugs in ethereum smart contracts. Proc. ACM Program. Lang., 3(OOPSLA):189:1-189:29, 2019. URL: https://doi.org/10.1145/3360615.
  45. Kazuhiro Yamashita, Yoshihide Nomura, Ence Zhou, Bingfeng Pi, and Sun Jun. Potential Risks of Hyperledger Fabric Smart Contracts. In 2019 IEEE International Workshop on Blockchain Oriented Software Engineering (IWBOSE), pages 1-10, 2019. URL: https://doi.org/10.1109/IWBOSE.2019.8666486.
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
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact