Practical Runtime Verification of Cross-Organizational Smart Contracts

Note

This README and the associated documentation in docs/ has been generated with AI assistance.

Reproduction artifact for the paper "Practical Runtime Verification of Cross-Organizational Smart Contracts". The work applies runtime assertion checking (RAC) to Hyperledger Fabric chaincode written in Java, using JML specifications enforced by OpenJML at runtime. The case study is a Java implementation of TPC-C that runs as Fabric chaincode (CCaaS).

Repository layout

Path	Contents
src/main/java/	Java chaincode (TPC-C contract API, business API, entities, middleware, registry helpers)
specs/	Sibling JML spec tree mirroring src/. 108 specifications across entities and transactions
libs/	Bundled hypernate jar (entity/registry layer used by the chaincode)
scripts/	Helper scripts: Fablo patcher, OpenJML local compile, cc.sh peer-CLI wrapper
Dockerfile	Three-stage build: shadowJar → OpenJML RAC recompile → runtime image
Dockerfile.norac	Baseline image with no RAC (used by the overhead benchmarks)
fablo-config.json	Fablo network topology (Fabric 3.1.0, BFT ordering, 2 peers, CCaaS chaincode)
fablo	Pinned Fablo 2.5.0 launcher
benchmarks/	Overhead benchmarks (chaincode-level + end-to-end), CSV results, reporting scripts
fault-injection/	Mutation-testing harness, mutant manifest, per-mutant artefacts and verdicts
figures/	UML class diagram (PlantUML source + rendered PNG)
docs/	Supplementary documentation (see below)
test_data/	Inputs used to seed the ledger

docs/ — supplementary documentation

• docs/spec-manifest.md — complete catalogue of all 108 JML specifications, organized by a two-level taxonomy (entity vs. transaction) with predicate text and ID for each clause.
• docs/new-specs.md — diff of the spec set against the originally submitted version (new preconditions, postconditions, and invariants added during revision), with TPC-C v5.11 references.
• docs/fablo-bugs.md — bugs encountered in the Fablo 2.5.0 + Fabric 3.1.0 + CCaaS toolchain and the patches applied automatically via scripts/patch-fablo.sh.

Prerequisites

• Linux, Docker, Docker Compose v2
• Java 21 (Temurin), Gradle wrapper bundled
• gawk, GNU coreutils, curl, unzip
• Python ≥ 3.11 with uv for the reporting scripts (they declare deps inline via PEP 723 and run with uv run)

OpenJML 21-0.23 is downloaded automatically by scripts/openjml-compile.sh and by the Docker build.

Building and running the chaincode

The end-to-end network is brought up with Fablo, which generates the Fabric artifacts and then triggers a docker build of the chaincode image as a post-generate hook.

./fablo up         # generate, patch, build, start
./fablo recreate   # tear down and rebuild from scratch
./fablo down       # stop and remove

The post-generate hook runs scripts/patch-fablo.sh (see docs/fablo-bugs.md for the rationale) and then builds the tpcc:0.1.0 image from the project root Dockerfile.

Invoking transactions

scripts/cc.sh wraps the peer CLI inside the running cli container.

./scripts/cc.sh invoke init
./scripts/cc.sh invoke newOrder '{"w_id":1,"d_id":1,"c_id":1,"o_entry_d":"2026-03-29","i_ids":[1,2,3,1,2],"i_w_ids":[1,1,1,1,1],"i_qtys":[1,1,1,1,1]}'
./scripts/cc.sh -v query readWarehouse 1

Building the chaincode locally (no Fabric)

./gradlew shadowJar delombok       # plain JAR + delombok'd sources
./scripts/openjml-compile.sh       # recompile with OpenJML RAC

Set -PwithoutOpenJML=true to skip OpenJML during IDE / Gradle development.

Reproducing the evaluation

Both experiments require a running Fablo network (./fablo up) and the scripts/cc.sh wrapper.

Mutation testing (fault detection capability)

./fault-injection/run-mutations.sh                # run the full manifest
./fault-injection/run-mutations.sh L1-06          # run a single mutant

Mutants are organized by a three-layer taxonomy (Avizienis et al. 2004): L1 implementation faults, L2 design faults, L3 specification faults. For each mutant the harness applies the patch, rebuilds the RAC image, swaps the CCaaS containers, re-initialises the ledger, invokes the target transaction, classifies the verdict (killed / survived / error), and reverts the source. Results land in fault-injection/results/run_<timestamp>/, alongside per-mutant build logs, diffs, invocation output, and chaincode container logs.

Overhead benchmarks

Two scopes are measured separately, then combined:

./benchmarks/chaincode/benchmark-chaincode.sh [WARMUP] [MEASURED] [RUNS]
./benchmarks/e2e/benchmark-e2e.sh             [WARMUP] [MEASURED] [RUNS]

• The chaincode-level benchmark extracts per-method timings from @Loggable log lines (Java method execution only, excluding the Fabric pipeline).
• The end-to-end benchmark wall-clocks each transaction through the peer CLI.

Both swap between RAC and noRAC images by replacing Dockerfile with Dockerfile.norac and calling ./fablo recreate between configurations.

Reporting scripts (in benchmarks/, benchmarks/chaincode/, benchmarks/e2e/) summarize the raw CSVs and emit the cross-scope overhead breakdown shown in the paper.

How to cite

Citation will be added once the article is published.

License

Source files are released under the Apache License 2.0 (see SPDX headers). The bundled hypernate jar in libs/ is third-party (Apache-2.0).