Skip to content

lisa-analyzer/go-lisa

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

813 Commits
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

logo


GoLiSA — Go Frontend of LiSA (Library for Static Analysis)

GitHub license Built on LiSA

GoLiSA is a static analysis tool for Go programs, built on top of the LiSA (Library for Static Analysis) framework. It provides a front-end that translates Go source files into LiSA's control flow graph (CFG) representation, enriches it with the semantics of a subset of the Go standard library, and runs configurable abstract interpretation analyses to detect bugs and verify program properties.


Blockchains and Smart Contracts Verification

GoLiSA provides several static analyses for detecting issues in blockchain software written in Go, supporting the semantics of a subset of instructions and functions from Hyperledger Fabric, Cosmos SDK, and Tendermint frameworks.


Table of Contents


Overview

GoLiSA translates Go source code into LiSA's intermediate representation and runs abstract interpretation analyses over the resulting program model. The analysis configuration is fully customizable — abstract domains, interprocedural strategy, and semantic checkers can all be selected independently.


Installation

Prerequisites: Java 17+, Gradle (wrapper included), GitHub credentials for the LiSA dependency.

LiSA Dependency

LiSA packages are hosted on GitHub Packages. Add your credentials to ~/.gradle/gradle.properties:

gpr.user=<your-github-username>
gpr.key=<your-github-personal-access-token>

Or export the environment variables USERNAME and TOKEN.

Build

git clone https://github.com/lisa-analyzer/go-lisa.git
cd go-lisa/go-lisa
./gradlew build

The archive containing the tool is written to build/distributions/golisa-0.1.zip.


<<<<<<< hf-checks

Usage

After building the distribution, run GoLiSA directly:

./build/distributions/go-lisa-0.1/bin/go-lisa --help

The command run the tool printing the help message


Command-Line Options

Option Long Option Argument Description
-i --input file Go source file to analyze (multiple files can be analyzed using multiple input options)
-ci --contractinfo name channel Deployment name and channel of the contract to analyze (hyperledger-fabric framework only)
-o --outdir directory Output directory for analysis results
-f --framework framework Framework used by the input files: hyperledger-fabric, cosmos-sdk, tendermint-core
-a --analysis analysis Analysis to perform : non-determinism, non-determinism-ni, phantom-read, ucci, cchi, read-write, unhandled-errors, var-numerical-overflow, div-by-zero
-xc --crosscontract Enable cross-contract analysis
-d --dumpAnalysis Dump the analysis
-h --help Print the help message

Supported Analysis

=======

Building GoLiSA

Compiling GoLiSA requires:

git clone https://github.com/lisa-analyzer/go-lisa
cd go-lisa/go-lisa
./gradlew build

In order to bundle GoLiSA as a distribution:

./gradlew distZip`
unzip build/distributions/go-lisa-0.1 

Finally, to run GoLiSA:

./build/distributions/go-lisa-0.1/bin/go-lisa

Building GoLiSA with snapshots

It is possible that GoLiSA refers to a snapshot release of LiSA to exploit unreleased features, and, when building, you get the following error message:

> Could not resolve io.github.lisa-analyzer:lisa-project:ver-SNAPSHOT.
  > Could not get resource 'https://maven.pkg.github.com/lisa-analyzer/lisa/io/github/lisa-analyzer/lisa-project/ver-SNAPSHOT/maven-metadata.xml'.
    > Could not GET 'https://maven.pkg.github.com/lisa-analyzer/lisa/io/github/lisa-analyzer/lisa-project/ver-SNAPSHOT/maven-metadata.xml'. Received status code 401 from server: Unauthorized

In this case, you need to perform the following steps:

  • create a GitHub Personal Access Token following this guide and grant read:packages permission
  • create a gradle.properties file at go-lisa/go-lisa (where the gradlew scripts are located) with the following content:
gpr.user=your-github-username
gpr.key=github-access-token

Finally, re-execute the build to have the snapshot dependencies downloaded.

Development with Eclipse

GoLiSA comes as a Gradle 6.0 project. For development with Eclipse, please install the Gradle IDE Pack plugin from the Eclipse marketplace, and make sure to import the project into the Eclipse workspace as a Gradle project.

Running GoLiSA

The entry point is the GoLiSA class, expecting four parameters:

  • -i <path>: the Go input file to be analyzed
  • -o <path>: the output directory
  • -f <framework>: the blockchain framework used in the Go input file (hyperledger-fabric, cosmos-sdk, tendermint-core)
  • -a <analysis>: the analysis to perform to detect issues of non-determinism (taint, non-interference)

Example

go-lisa -i mycontract.go -o output_dir -f hyperledger-fabric -a taint

master

Analysis Description
non-determinism performs an analysis to detect explicit flows that lead to issues related to non-determinism in blockchain software
non-determinism-ni performs an analysis to detect explicit and implicit flows that lead to issues related to non-determinism in blockchain software
phantom-read performs an analysis to detect phantom reads in blockchain software for hyperledger-fabric framework
ucci performs an analysis to detect untrusted cross-contract invocations in blockchain software for hyperledger-fabric framework
cchi performs an analysis to detect issues related to cross-channel invocations in blockchain software for hyperledger-fabric framework
read-write performs an analysis to detect read-after-write and over-write issues in blockchain software for hyperledger-fabric framework
unhandled-errors performs an analysis to detect unhandled errors in blockchain software
var-numerical-overflow performs an analysis to detect the integer overflow/underflow of program variables in Go software
div-by-zero performs an analysis to detect divison by zero in Go software

Publications

GoLiSA and its analyses

  • Luca Olivieri, Luca Negrini: Don’t Panic: Error Handling Patterns in Go Smart Contracts and Blockchain Software, in Proceedings of 7th Conference on Blockchain Research & Applications for Innovative Networks and Services (BRAINS), 2025 (link)
  • Luca Olivieri: Detection of Cross-Channel Invocation Risks in Hyperledger Fabric, in Proceedings of 36th International Symposium on Software Reliability Engineering (ISSRE), 2025 (link)
  • Luca Olivieri, Luca Negrini, Vincenzo Arceri, Pietro Ferrara, Agostino Cortesi: Detection of Read-Write Issues in Hyperledger Fabric Smart Contracts, in Proceedings of The 40th ACM/SIGAPP Symposium On Applied Computing (SAC), 2025 (link)
  • Luca Olivieri, Luca Negrini, Vincenzo Arceri, Pietro Ferrara, Agostino Cortesi, Fausto Spoto: Static Detection of Untrusted Cross-Contract Invocations in Go Smart Contracts in Proceedings of The 40th ACM/SIGAPP Symposium On Applied Computing (SAC), 2025 (link)
  • Luca Olivieri, Luca Negrini, Vincenzo Arceri, Badar Chachar, Pietro Ferrara, Agostino Cortesi: Detection of Phantom Reads in Hyperledger Fabric, in IEEE Access, vol. 12, pp. 80687-80697, 2024 (link)
  • Luca Olivieri, Luca Negrini, Vincenzo Arceri, Fabio Tagliaferro, Pietro Ferrara, Agostino Cortesi, Fausto Spoto: Information Flow Analysis for Detecting Non-Determinism in Blockchain. ECOOP 2023: 23:1-23:25 (link) <<<<<<< hf-checks
  • Luca Olivieri, Fabio Tagliaferro, Vincenzo Arceri, Marco Ruaro, Luca Negrini, Agostino Cortesi, Pietro Ferrara, Fausto Spoto, Enrico Talin: Ensuring determinism in blockchain software with GoLiSA: an industrial experience report. SOAP@PLDI 2022: 23-29 (link)

Other publications involving GoLiSA

  • Luca Olivieri, David Beste, Luca Negrini, Lea Schönherr, Antonio Emanuele Cinà, Pietro Ferrara: Code Generation of Smart Contracts with LLMs: A Case Study on Hyperledger Fabric, in Proceedings of 36th International Symposium on Software Reliability Engineering (ISSRE), 2025 (link)
  • Luca Negrini, Vincenzo Arceri, Agostino Cortesi, Pietro Ferrara: Tarsis: An effective automata-based abstract domain for string analysis, in Journal of Software: Evolution and Process, 2024 (link)

Awards, Honors, and Honorable Mentions

  • Best Artifact Award. Static Detection of Cross-Channel Invocation Issues in Hyperledger Fabric. IEEE 36th International Symposium on Software Reliability Engineering (ISSRE'25), 2025. Artifact: (link)
  • Candidate for Best Paper Award. Don't Panic: Error Handling Patterns in Go Smart Contracts and Blockchain Software. 7th Conference on Blockchain Research & Applications for Innovative Networks and Services (BRAINS'25), 2025.

Experimental Evaluations

The code in this branch is under development. Please look at the specific artifacts or branches cited in the corresponding research papers to reproduce experimental evaluations and results.


Analysis Examples

Non-determinism Analysis

./build/distributions/go-lisa-0.1/bin/go-lisa -i code.go -o output -f hyperledger-fabric -a non-determinism
./build/distributions/go-lisa-0.1/bin/go-lisa -i code.go -o output -f hyperledger-fabric -a non-determinism-ni

Phantom Read Analysis

./build/distributions/go-lisa-0.1/bin/go-lisa -i code.go -o output -f hyperledger-fabric -a phantom-read

Untrusted Cross-Contract Invocations Analysis

./build/distributions/go-lisa-0.1/bin/go-lisa -i code.go -o output -f hyperledger-fabric -a ucci

Cross-Channel Invocations Analysis

./build/distributions/go-lisa-0.1/bin/go-lisa -i codeA.go -o output -f hyperledger-fabric -a cchi
./build/distributions/go-lisa-0.1/bin/go-lisa -i codeA.go  -ci "contractA" "otherchannel" -i codeB.go -ci "contractB" "mychannel" -o output -f hyperledger-fabric -a cchi -xc

Read-after-write and Over-write Analysis

./build/distributions/go-lisa-0.1/bin/go-lisa -i code.go -o output -f hyperledger-fabric -a read-write

Unhandled Errors Analysis

./build/distributions/go-lisa-0.1/bin/go-lisa -i code.go -o output -f hyperledger-fabric -a unhandled-errors

Numerical Issues Analysis

./build/distributions/go-lisa-0.1/bin/go-lisa -i code.go -o output -f hyperledger-fabric -a numerical-issues

Other Licences

Logo

The Go gopher was designed by the Renee French. The design is licensed under the Creative Commons 4.0 Attributions license. Read link1 and link2 for more details.

  • Luca Olivieri, Fabio Tagliaferro, Vincenzo Arceri, Marco Ruaro, Luca Negrini, Agostino Cortesi, Pietro Ferrara, Fausto Spoto, Enrico Talin: Ensuring determinism in blockchain software with GoLiSA: an industrial experience report. SOAP@PLDI 2022: 23-29 (link)

master