Search Results

Documents authored by Ferrara, Pietro

Document
DOI: 10.4230/DagRep.15.10.37
Sound Static Program Analysis in Modern Software Engineering (Dagstuhl Seminar 25421)

Authors: Pietro Ferrara, Liana Hadarean, Jorge A. Navas, Caterina Urban, and Greta Dolcetti

Published in: Dagstuhl Reports, Volume 15, Issue 10 (2026)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 25421 "Sound Static Program Analysis in Modern Software Engineering". Sound Static Program Analysis (SSPA) has historically been effective in proving the absence of runtime errors and security vulnerabilities, notably in safety-critical embedded software. However, it has seen limited adoption in desktop applications until its revival for Web application security (e.g., to prove the absence of SQL injection vulnerabilities). Modern software development, characterized by architectures like microservices, serverless computing, and the increasing use of scripting languages, presents challenges to SSPA due to the integration of multiple languages and complex semantics, while also posing new problems related to soundness, precision, and scalability stemming from the machine learning revolution in code development. Despite these new opportunities for SSPA to offer structured feedback and address serious flaws often overlooked by the shallow analyses currently favored by the industry, there has not been a significant resurgence in its industrial application. This Dagstuhl Seminar aimed to bridge the SSPA and software engineering communities to extend existing theories to these new trends, foster integration with modern practices like DevOps, and discuss the formal methods challenges arising from contemporary software architectures.
Cite as

Pietro Ferrara, Liana Hadarean, Jorge A. Navas, Caterina Urban, and Greta Dolcetti. Sound Static Program Analysis in Modern Software Engineering (Dagstuhl Seminar 25421). In Dagstuhl Reports, Volume 15, Issue 10, pp. 37-74, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@Article{ferrara_et_al:DagRep.15.10.37,
  author =	{Ferrara, Pietro and Hadarean, Liana and Navas, Jorge A. and Urban, Caterina and Dolcetti, Greta},
  title =	{{Sound Static Program Analysis in Modern Software Engineering (Dagstuhl Seminar 25421)}},
  pages =	{37--74},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2026},
  volume =	{15},
  number =	{10},
  editor =	{Ferrara, Pietro and Hadarean, Liana and Navas, Jorge A. and Urban, Caterina and Dolcetti, Greta},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.15.10.37},
  URN =		{urn:nbn:de:0030-drops-254154},
  doi =		{10.4230/DagRep.15.10.37},
  annote =	{Keywords: Abstract interpretation, Formal methods, Software engineering, Software verification, Sound static program analysis}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2023.23
Information Flow Analysis for Detecting Non-Determinism in Blockchain

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

Published in: LIPIcs, Volume 263, 37th European Conference on Object-Oriented Programming (ECOOP 2023)

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.
Cite as

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)

Copy BibTex To Clipboard

@InProceedings{olivieri_et_al:LIPIcs.ECOOP.2023.23,
  author =	{Olivieri, Luca and Negrini, Luca and Arceri, Vincenzo and Tagliaferro, Fabio and Ferrara, Pietro and Cortesi, Agostino and Spoto, Fausto},
  title =	{{Information Flow Analysis for Detecting Non-Determinism in Blockchain}},
  booktitle =	{37th European Conference on Object-Oriented Programming (ECOOP 2023)},
  pages =	{23:1--23:25},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-281-5},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{263},
  editor =	{Ali, Karim and Salvaneschi, Guido},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2023.23},
  URN =		{urn:nbn:de:0030-drops-182167},
  doi =		{10.4230/LIPIcs.ECOOP.2023.23},
  annote =	{Keywords: Static Analysis, Program Verification, Non-determinism, Blockchain, Smart contracts, DApps, Go language}
}
Document
Artifact
DOI: 10.4230/DARTS.9.2.23
Information Flow Analysis for Detecting Non-Determinism in Blockchain (Artifact)

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

Published in: DARTS, Volume 9, Issue 2, Special Issue of the 37th European Conference on Object-Oriented Programming (ECOOP 2023)

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.
Cite as

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)

Copy BibTex To Clipboard

@Article{olivieri_et_al:DARTS.9.2.23,
  author =	{Olivieri, Luca and Negrini, Luca and Arceri, Vincenzo and Tagliaferro, Fabio and Ferrara, Pietro and Cortesi, Agostino and Spoto, Fausto},
  title =	{{Information Flow Analysis for Detecting Non-Determinism in Blockchain (Artifact)}},
  pages =	{23:1--23:3},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2023},
  volume =	{9},
  number =	{2},
  editor =	{Olivieri, Luca and Negrini, Luca and Arceri, Vincenzo and Tagliaferro, Fabio and Ferrara, Pietro and Cortesi, Agostino and Spoto, Fausto},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.9.2.23},
  URN =		{urn:nbn:de:0030-drops-182633},
  doi =		{10.4230/DARTS.9.2.23},
  annote =	{Keywords: Static Analysis, Program Verification, Non-determinism, Blockchain, Smart contracts, DApps, Go language}
}
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact