PaperlayerView exact revision on arXiv

Source-linked AI summary

SAILFISH: Vetting Smart Contract State-Inconsistency Bugs in Seconds

Priyanka Bose, Dipanjan Das, Yanju Chen, Yu Feng, Christopher Kruegel, Giovanni Vigna

arXiv:2104.08638v2cs.CRcs.PL

TL;DR

State-inconsistency bugs are difficult to detect scalably because evaluating all possible schedules is computationally infeasible. SAILFISH combines lightweight exploration with symbolic refinement guided by value-summary analysis, significantly outperforming five state-of-the-art analyzers and identifying 47 previously unknown vulnerable contracts.

  • Problem

    Detecting state-inconsistency bugs requires evaluating infeasibly many possible schedules, while symbolic execution also faces path explosion and complex summaries.

  • Method

    SAILFISH combines lightweight exploration and storage-dependency graph queries with symbolic refinement guided by value-summary analysis.

  • Results

    47 previously unknown vulnerable contracts were identified, while SAILFISH significantly outperformed five state-of-the-art analyzers in precision and performance.

  • Takeaways & Limitations

    SAILFISH provides scalable detection of state-inconsistency bugs in Ethereum smart contracts and identifies vulnerable contracts missed by other tools.

  • Takeaways & Limitations

    SAILFISH does not claim soundness for its reentrancy and transaction-order-dependence detection rules.

Abstract

from arXiv · show

This paper presents SAILFISH, a scalable system for automatically finding state-inconsistency bugs in smart contracts. To make the analysis tractable, we introduce a hybrid approach that includes (i) a light-weight exploration phase that dramatically reduces the number of instructions to analyze, and (ii) a precise refinement phase based on symbolic evaluation guided by our novel value-summary analysis, which generates extra constraints to over-approximate the side effects of whole-program execution, thereby ensuring the precision of the symbolic evaluation. We developed a prototype of SAILFISH and evaluated its ability to detect two state-inconsistency flaws, viz., reentrancy and transaction order dependence (TOD) in Ethereum smart contracts. Further, we present detection rules for other kinds of smart contract flaws that SAILFISH can be extended to detect. Our experiments demonstrate the efficiency of our hybrid approach as well as the benefit of the value summary analysis. In particular, we show that S SAILFISH outperforms five state-of-the-art smart contract analyzers (SECURITY, MYTHRIL, OYENTE, SEREUM and VANDAL ) in terms of performance, and precision. In total, SAILFISH discovered 47 previously unknown vulnerable smart contracts out of 89,853 smart contracts from ETHERSCAN .

I. INTRODUCTION

SAILFISH targets state-inconsistency bugs in smart contracts with a scalable hybrid analysis that combines lightweight exploration, value-summary-guided refinement, and symbolic evaluation. Evaluated on 89,853 Etherscan contracts, it outperformed five state-of-the-art analyzers in performance and precision and uncovered 47 previously unknown vulnerabilities.

  • Problem: State-inconsistency bugs let attackers manipulate contract storage by changing transaction order across transactions or control flow within a transaction.The paper identifies transaction order dependence and reentrancy as two root causes, including a new reentrancy pattern.
  • Motivation: Existing state-inconsistency analyzers either over-approximate execution and produce false alarms or enumerate traces precisely and fail to scale, while dynamic tools require active-attack evidence.These limitations motivate scalable static analysis for pre-deployment auditing.
  • Approach: SAILFISH combines a lightweight EXPLORE phase with value-summary-guided REFINE symbolic evaluation to scale static detection while reducing false alarms.Value summaries constrain storage-variable scope and provide preconditions for symbolic evaluation.
  • Approach: SAILFISH models detection as hazardous-access queries over a storage dependency graph summarizing storage-variable read-write dependencies and execution side effects.Queries return either no result or a potentially vulnerable subgraph matching the vulnerability pattern.
  • Evaluation: 47 previously unknown vulnerable contracts were uncovered by SAILFISH among 89,853 Etherscan contracts, while outperforming five state-of-the-art analyzers in runtime and precision.SAILFISH averaged 30.79 seconds per contract, 31 times faster than MYTHRIL.

II. BACKGROUND · III. MOTIVATION · A. Identifying the root causes of SI vulnerabilities

The paper frames state inconsistency as unpredictable contract-state evolution caused by execution nondeterminism, then identifies stale reads and delayed writes as root causes of reentrancy and TOD vulnerabilities. It motivates detection challenges by showing that existing tools can over-approximate delayed-write patterns and produce false alarms.

  • II. BACKGROUND: State inconsistency arises when execution nondeterminism makes a contract’s final state unpredictable, including transaction-order variation and control transfer through external calls.The paper models execution as a schedule acting on an initial state and reaching a potentially unpredictable final state.
  • II. BACKGROUND: Reentrancy occurs when a called contract reenters the caller before its original invocation updates internal state, enabling execution against an inconsistent state.The Ethereum protocol permits callbacks into public or external methods during the same transaction.
  • II. BACKGROUND: A withdraw implementation becomes vulnerable when it performs an external transfer before updating the account mapping, allowing repeated reentry to drain Ether.The attacker repeatedly reads a stale balance, so the balance check continues to pass; the illustrated contract structure is identified in Figure 1.
  • II. BACKGROUND: Reentrancy can also be cross-function, create-based, or delegate-based, extending the attack beyond a single victim function.A cross-function attack reenters through a different function after an untrusted external call transfers control to the attacker.
  • III. MOTIVATION: The motivating examples focus on reentrancy and transaction-order dependence as state-inconsistency vulnerabilities and examine why automated detection remains challenging.The motivation section introduces vulnerable examples, detection challenges, shortcomings of existing techniques, and the paper’s solution.
  • A. Identifying the root causes of SI vulnerabilities: An SI vulnerability requires two executions sharing storage and either a stale read or a delayed write that creates inconsistent state.The authors derive these preconditions by manually analyzing prior reentrancy and TOD bugs and warnings from existing analysis tools.
  • A. Identifying the root causes of SI vulnerabilities: Existing tools detect stale-read patterns with varying accuracy, but delayed-write reentrancy was previously unexplored and conservative analyses such as MYTHRIL generate false alarms.MYTHRIL flags state accesses after external calls without checking whether they actually create an inconsistent state.

B. Running examples · C. State of the vulnerability analyses

The running example illustrates a cross-function reentrancy caused by a destructive write, while the vulnerability-analysis review identifies limitations in existing tools and SAILFISH’s targeted solutions. SAILFISH addresses these limitations through paired-function analysis, hazardous-access reasoning, and value summaries that over-approximate whole-contract side effects.

  • B. Running examples: The example’s attacker reenters updateSplit and changes splits[id] to zero, enabling all funds to be transferred again to payee b.The attack crosses updateSplit and splitFunds through an external call.
  • C. State of the vulnerability analyses: Most existing techniques cannot detect cross-function attacks, and some raise false alarms because their conservative policies over-approximate reentrancy behavior.SEREUM also fails on the example because it does not set a lock without a control-flow decision variable.
  • C. State of the vulnerability analyses: Existing tools largely model reentrancy within a single function, leaving the cross-function attack spanning updateSplit and splitFunds out of scope.VANDAL and OYENTE check recursive reachability to the enclosing function, while SECURIFY and MYTHRIL use related post-call storage policies.
  • C. State of the vulnerability analyses: SAILFISH uses taint analysis to retain only attacker-controlled external calls and analyzes public functions in pairs to avoid unbounded exploit call chains.This design targets state-explosion and scalability problems in static analysis.
  • C. State of the vulnerability analyses: SAILFISH defines a hazardous access pair as two public-method-reachable operations on one state variable where at least one operation writes, unifying stale reads and destructive writes.The criterion distinguishes benign reentrancy from reentrancy that can induce state inconsistency.
  • C. State of the vulnerability analyses: SAILFISH’s symbolic verifier checks paths involving hazardous accesses, but whole-contract modeling of shared state would otherwise be prohibitively expensive.The verifier therefore needs summaries of public-method effects across executions.
  • C. State of the vulnerability analyses: SAILFISH augments symbolic verification with value summaries that over-approximate public methods’ side effects on state variables across all executions.These summaries support precise reasoning without explicitly performing whole-contract symbolic analysis.

D. SAILFISH overview · IV. STATE INCONSISTENCY BUGS

SAILFISH combines lightweight exploration with symbolic refinement to detect state-inconsistency vulnerabilities. It defines state inconsistency through divergent final states under equivalent schedules, encompassing reentrancy and transaction-order bugs.

  • D. SAILFISH overview: SAILFISH combines EXPLORER and REFINER modules, modeling state-inconsistency vulnerabilities as graph queries over a storage dependency graph.The SDG over-approximates storage-variable read-write accesses along possible execution paths.
  • D. SAILFISH overview: The EXPLORER conservatively flags potential state inconsistencies using counterexamples spanning public functions and hazardous storage writes and reads.Cross-function attacks are represented through detected hazardous accesses and corresponding counterexamples.
  • D. SAILFISH overview: The REFINER performs contract-wide value-summary analysis to compute storage-value preconditions and guide symbolic evaluation of path constraints.This addresses state changes caused by other public methods, including reentry after an external call.
  • IV. STATE INCONSISTENCY BUGS: A schedule is a valid sequence of externally invoked contract events whose ordered execution transforms an initial state ∆ into a final state ∆′.Events may be invoked directly by a transaction or through another contract, including reentrant invocations.
  • IV. STATE INCONSISTENCY BUGS: Equivalent schedules contain the same function invocations, while transformation functions preserve equivalence by changing reentry program counters or permuting events.These two strategies correspond to reentrancy and transaction ordering, respectively.
  • IV. STATE INCONSISTENCY BUGS: A contract has a state-inconsistency bug when equivalent schedules starting from the same state produce different final states.The definition compares execution under an original schedule with execution under its transformed schedule.
  • IV. STATE INCONSISTENCY BUGS: Reentrancy is state inconsistency caused by a transformed schedule containing a nonzero program-counter event, whereas generalized TOD is caused by permuting events.The work restricts TOD detection to cases where Ether transfer is affected by state inconsistency.

V. EXPLORER: LIGHTWEIGHT EXPLORATION OVER SDG · A. Storage dependency graph (SDG)

SAILFISH’s lightweight explorer represents attacker-subverted execution and storage interactions with a storage dependency graph (SDG), then detects state-inconsistency hazards through SDG queries. The SDG is constructed from interprocedural control-flow, data-flow, storage, access-control, and ordering information encoded with Datalog rules.

  • V. EXPLORER: LIGHTWEIGHT EXPLORATION OVER SDG: The SDG captures control- and data-flow relations between storage variables and critical instructions, enabling hazardous-access queries for detecting state-inconsistency bugs.Critical instructions include control-flow decisions and state-changing operations.
  • A. Storage dependency graph (SDG): SAILFISH models attacker-subverted execution by connecting public entry points, storage variables, and storage-operating statements to their effects on contract global state.Public methods are treated as attacker-callable entry points in the SDG.
  • A. Storage dependency graph (SDG): Datalog rules encode SDG construction from facts and predicates describing reachability, successors, external calls, entries, exits, storage, writes, dependencies, and owner-only execution.The rules are defined as conjunctions of predicates over program facts.
  • A. Storage dependency graph (SDG): SAILFISH derives SDG inputs from an interprocedural control-flow graph and uses static taint analysis to restrict external-call entries.The owner predicate marks statements executable only by contract owners, supporting precise modeling of state-inconsistency attacks.
  • A. Storage dependency graph (SDG): SDG edges distinguish writes, data dependencies, and execution order, respectively recording variable updates, statement dependence on storage, and ordering relations.These edge types are used to connect storage variables and instructions during graph construction.
  • A. Storage dependency graph (SDG): In the splitFunds/updateSplit example, the SDG links deposits and splits[id] to the relevant instructions and marks hazardous accesses on splits[id].Write edges represent updates to deposits, while data-dependency edges connect later instructions to both state variables.

B. Hazardous access

SAILFISH introduces hazardous access to avoid infeasible enumeration of all schedules and contract states. It statically identifies potentially conflicting accesses through the contract’s SDG, then uses symbolic evaluation to remove infeasible cases.

  • B. Hazardous access: Hazardous access makes scalable static detection possible by replacing infeasible enumeration of every schedule on every contract state with analysis of shared storage-variable operations.The concept is inspired by data races, where different execution paths operate on the same variable and at least one operation writes.
  • B. Hazardous access: Hazardous access is a tuple ⟨s1, s2, v⟩ where both statements operate on storage variable v and at least one statement writes.Data-flow dependencies include both direct and indirect dependencies; a statement operates on v when it assigns v or contains an expression that depends on it.
  • B. Hazardous access: SAILFISH identifies hazardous accesses by querying a path-condition-agnostic contract SDG, with any non-empty result indicating a potential hazard.Because conflicting path conditions may make accesses infeasible, REFINER uses symbolic evaluation to prune them.

C. State inconsistency bug detection · VI. REFINER: SYMBOLIC EVALUATION WITH VALUE SUMMARY · A. Value summary analysis (VSA)

SAILFISH detects state-inconsistency bugs by using hazardous accesses to avoid enumerating schedules, then refines feasible counterexamples with symbolic evaluation guided by value summaries. Its domain-specific value-summary analysis preserves branch conditions while scaling through conservative treatment of loops and external calls.

  • C. State inconsistency bug detection: SAILFISH uses hazardous access as a proxy for state-inconsistency bugs instead of statically enumerating all possible schedules.A bug exists when two schedules produce different storage-variable values; hazardous-access analysis targets the underlying cause more tractably.
  • C. State inconsistency bug detection: For reentrancy, SAILFISH checks whether hazardous-access pairs are reachable during reentrant execution, while TOD detection checks whether Ether transfers are reachable from such pairs.Reentrancy can change statement order, whereas transaction ordering can change the amount transferred.
  • C. State inconsistency bug detection: SAILFISH handles delegate-based reentrancy by modeling delegatecall according to destination taint and available delegated-contract source code, defaulting to unsafe external-call treatment when unavailable.For create-based attacks, the analysis applies corresponding attack-specific handling described in the implementation.
  • VI. REFINER: SYMBOLIC EVALUATION WITH VALUE SUMMARY: When exploration raises an alarm, SAILFISH refines the generated counterexample with symbolic evaluation because unconstrained storage variables can produce false positives.The alarm may indicate either a genuinely vulnerable contract or an infeasible counterexample subgraph.
  • A. Value summary analysis (VSA): VSA computes lifecycle invariants for storage variables, addressing precision loss from naive summaries and scalability barriers from path-by-path symbolic execution.A naive analysis may summarize a mutex as unconstrained, while path-by-path analysis must construct and disjoin summaries for every path.
  • A. Value summary analysis (VSA): The domain-specific VSA stitches branch conditions to symbolic variables at control-flow merge points, preserving precision beyond interval-based summaries.This design targets the precision challenge identified for smart-contract value summaries.
  • A. Value summary analysis (VSA): VSA represents values and path constraints explicitly, havocs external-call returns and loop-written variables, and merges uncertain conditional branches with their path conditions.External calls may return arbitrary values, while loop summarization is conservatively simplified for scalability.

B. Symbolic evaluation

SAILFISH checks candidate state-inconsistency paths through symbolic evaluation, using value summaries to constrain storage state and reduce false alarms. For TOD, it symbolically evaluates the subgraph under two preconditions and compares the resulting call amounts.

  • Symbolic evaluation: SAILFISH evaluates whether a valid path through the Explorer-returned subgraph satisfies the state-inconsistency query, reducing bug checking to reachability.The subgraph contains the queried statement pair, and symbolic checking determines whether a valid path exists.
  • Symbolic evaluation: Assuming unconstrained storage variables causes SAILFISH to fail to refute a significant amount of false alarms in the ablation study.This motivates constraining storage-variable ranges without sacrificing too much precision.
  • Symbolic evaluation: For TOD, SAILFISH symbolically evaluates the subgraph twice and reports a bug when the external-call Ether amounts a1 and a2 differ.The two executions use true and the value summary as their respective preconditions.
  • Value summary analysis: Value summaries are unioned into a global pre-condition enforced throughout symbolic evaluation to constrain storage variables.This addresses the loss of precision caused by assuming all storage variables are completely unconstrained.
  • Value summary analysis: SAILFISH discards a reentrancy report when the mutex = false pre-condition is unsatisfiable under the current state, refuting the false positive.Although callback-based re-entry is possible, re-entering the relevant branch and triggering the external call is impossible.

VII. IMPLEMENTATION … B. Vulnerability detection

SAILFISH combines lightweight exploration with symbolic refinement and evaluates vulnerability detection across 89,853 Ethereum contracts. It reports the fewest warnings, finds 47 zero-day vulnerabilities, and detects all vulnerabilities in the manually analyzed dataset with the lowest false-positive rate.

  • VII. IMPLEMENTATION: SAILFISH implements an Explorer that lifts Solidity into a system dependence graph through Slither and a Refiner that symbolically checks counterexample feasibility with Rosette.The Refiner uses symbolic evaluation to assess whether Explorer-generated counterexamples are feasible.
  • VIII. EVALUATION: The experiments compare SAILFISH with existing analyzers for vulnerability detection, scalability, and the Refiner’s ability to prune false alarms.These correspond to RQ1, RQ2, and RQ3.
  • A. Experimental setup: The evaluation crawled 91,921 Etherscan contracts, excluded 2,068 incompatible or Vyper contracts, and retained 89,853 deduplicated Solidity contracts.The dataset covers contracts available through October 31, 2020.
  • B. Vulnerability detection: SAILFISH reports potential reentrancy in 2.40% and potential TOD in 8.74% of contracts, versus higher reentrancy rates for SECURIFY, MYTHRIL, and VANDAL.TOD detection was supported by only SECURIFY, OYENTE, and SAILFISH among the compared tools.
  • B. Vulnerability detection: MYTHRIL timed out on 66.84% of contracts, while VANDAL timed out on 1.56% but flagged 52.27% for reentrancy, making its warnings difficult to triage.The authors attribute VANDAL’s warning volume to poor precision and note that symbolic-execution scalability is difficult to assess for OYENTE because of unsupported Solidity versions.
  • B. Vulnerability detection: The manual analysis identified 26 reentrancy and 110 TOD-vulnerable contracts, and SAILFISH detected all vulnerabilities in this ground-truth dataset.The ground truth was used to compare true, false, and missed detections across tools.
  • B. Vulnerability detection: Symbolic refinement eliminates some Explorer alerts by checking feasibility and accounting for hazardous state access, although imprecise static taint analysis still causes false positives.The paper gives examples where the Refiner removes alerts that symbolic evaluation shows are safe.
  • B. Vulnerability detection: SAILFISH emits the fewest warnings in the full dataset, finds 47 zero-day vulnerabilities, and achieves the lowest false-positive rate while detecting all manual-dataset vulnerabilities.These results answer RQ1 on vulnerability-detection effectiveness.

C. Performance analysis

SAILFISH achieves analysis times comparable to VANDAL while substantially outperforming SECURIFY, MYTHRIL, and OYENTE. Across tools, analysis time increases as dataset size grows, with MYTHRIL incurring especially high times and timeouts.

  • Performance comparison: Analysis time increases with dataset size for all evaluated tools.The performance analysis covers small, medium, large, and full datasets.
  • Performance comparison: SAILFISH is 6, 31, and 6 times faster than SECURIFY, MYTHRIL, and OYENTE, respectively, while remaining comparable to VANDAL.This comparison holds across the evaluated datasets.

D. Ablation study … XI. CONCLUSION

SAILFISH combines lightweight exploration with VSA-guided symbolic evaluation to identify state-inconsistency bugs accurately and scalably. The paper reports ablation evidence for this design, discusses limitations and related approaches, and concludes with strong ETHERSCAN results.

  • D. Ablation study: The ablation study finds that symbolic evaluation and value-summary analysis effectively prune false positives while supporting precision and scalability.SAILFISH is evaluated in static-only, static-plus-havoc, and full configurations to assess REFINE and VSA.
  • IX. LIMITATIONS: Although SAILFISH uses SLITHER and source code for developer-oriented debugging, its techniques do not depend on rich source semantics and could be ported to bytecode.The stated source-code choice facilitates debugging and introspection rather than supplying essential semantic information.
  • X. RELATED WORK: Pattern-based static analyzers can over-approximate program states, producing false positives and missed detections, whereas SAILFISH targets stale reads and destructive writes.The related-work discussion presents these two causes as complementary explanations for state-inconsistency bugs.
  • X. RELATED WORK: Traditional symbolic-execution tools face path explosion and poor scalability, while SAILFISH uses symbolic execution for validation with VSA-based over-approximation across executions.The approach under-constrains symbolic execution while over-approximating preconditions for state-variable updates.
  • X. RELATED WORK: Dynamic-analysis tools perform runtime or post-mortem checks, while SAILFISH generalizes callback-freedom reasoning through its hazardous-access notion for state inconsistency.The comparison includes SEREUM, SODA, TXSPECTOR, and ECFCHECKER.
  • X. RELATED WORK: SERIF detects reentrancy through trusted-untrusted computation and annotated information-flow labels, requiring semantic understanding of the contract.Its type-system approach enforces secure information flow using those trust labels.
  • XI. CONCLUSION: SAILFISH significantly outperforms state-of-the-art analyzers in precision and performance, identifying 47 previously unknown vulnerable and exploitable contracts on ETHERSCAN.The conclusion characterizes SAILFISH as a scalable hybrid tool combining lightweight exploration with VSA-aided symbolic evaluation.

APPENDIX I EXTENDED EVALUATION · APPENDIX II CASE STUDIES · A. Zero-day vulnerabilities

The extended evaluation shows that value-summary analysis substantially accelerates symbolic refinement, while the case studies document unique real-world reentrancy and transaction-order-dependence vulnerabilities found by SAILFISH.

  • APPENDIX I EXTENDED EVALUATION: 21.50% of contracts timed out with path-by-path summaries, while Figure 12 reports speedup-factor results for the 1,570 contracts terminating under both modes.The experiment compared value summaries with standard path-by-path function summaries on a randomly selected subset of 2,000 warned contracts.
  • APPENDIX I EXTENDED EVALUATION: The novel value-summary analysis is significantly faster than classic summary-based symbolic analysis.SAILFISH replaced value summaries with standard path-by-path function summaries in the comparison.
  • A. Zero-day vulnerabilities: SAILFISH identified unique vulnerabilities that no other evaluated tool detected, although anonymity and blockchain immutability hindered reporting and remediation.The case studies redacted code and masked program elements for anonymity and simplicity.
  • A. Zero-day vulnerabilities: The case studies include a real-world cross-function reentrancy vulnerability and a delegate-based reentrancy vulnerability.Figure 13 illustrates cross-function reentrancy, while Figure 14 presents delegatecall-based reentrancy.
  • A. Zero-day vulnerabilities: SAILFISH successfully flagged a simplified real-world delegatecall-based vulnerability after tuple-support limitations prevented running it as-is on the original contract.The contracts were simplified to remove syntactic complexity unrelated to the vulnerability while retaining the relevant inter-contract behavior.
  • A. Zero-day vulnerabilities: A real-world TOD bug lets front-running settleBet() invocations earn higher rewards because the reward depends on the increased total balance.Figure 15 illustrates the bug; the attacker benefits when two equal-value settleBet() calls race.

B. Advantage of value-summary analysis. · C. False positives for reentrancy and TOD

SAILFISH’s value-summary analysis improves precision by accounting for whole-program side effects, while its reentrancy and TOD detectors can still produce benign false positives. The examples show these false alarms arise from disregarded guards or harmless transaction-order effects.

  • B. Advantage of value-summary analysis.: The analysis uses value summaries to improve symbolic evaluation by accounting for side effects across the wrapped execution of a function.This is illustrated by the modifier’s placement of the underscore, which determines when the original function executes.
  • C. False positives for reentrancy and TOD: SAILFISH raises a reentrancy false alarm when static taint analysis ignores a require guard protecting the constructor-initialized bTken variable.The later balanceOf call on bTken is therefore treated as tainted even though the preceding guard constrains execution.
  • B. Advantage of value-summary analysis.: SAILFISH’s value-summary analysis demonstrates a concrete benefit on a real-world contract involving a nonReentrant modifier and reentrancy lock updates.The modifier sets the lock on entry and resets it after exit; the example motivates modeling hazardous accesses across wrapped function execution.
  • C. False positives for reentrancy and TOD: Figure 17 presents a real-world contract example of SAILFISH’s reentrancy false positive.The false positive results from disregarding the require clause that guards the relevant assignment.
  • C. False positives for reentrancy and TOD: The donation example is not a true TOD attack because transaction ordering changes the reward without harming functionality.If pay front-runs withdrawDonations, the recipient receives a greater donation rather than suffering a harmful inconsistency.
  • C. False positives for reentrancy and TOD: SAILFISH also flags a donation-collection contract as a TOD case because the transferred donation amount depends on transaction order.The contract’s pay and withdrawDonations functions can modify the relevant donation state before the recipient transfer.

APPENDIX III EXTENDED RELATED WORK … B. Detecting owner-only statements

SAILFISH combines static analysis, value summaries, and symbolic execution to improve scalability and precision when detecting smart-contract vulnerabilities. Its precision depends on resolving external-call targets and identifying owner-only statements, which can be challenging in practice.

  • APPENDIX III EXTENDED RELATED WORK: SAILFISH combines static analysis, path filtering, value-summary computation, and symbolic execution to achieve scalable and precise vulnerability analysis.The value summary is used in conjunction with symbolic execution to approximate whole-program side effects.
  • APPENDIX III EXTENDED RELATED WORK: Hybrid analyses use static analysis to prune uninteresting paths or selectively explore promising program regions before symbolic execution.SAILFISH applies this strategy to filter contracts and find potentially vulnerable paths.
  • APPENDIX IV EXTENDED DISCUSSION: SAILFISH loses precision when an external call’s destination is not statically known or its target source code is absent from the database.Such external calls are treated as untrusted.
  • A. Inter-contract analysis: Backward data-flow analysis resolves external-call destinations from source visibility, owner-set runtime values, or existing transaction data.Resolved targets are incorporated when their source is present in SAILFISH’s database; tainted or unavailable targets require no further analysis.
  • B. Detecting owner-only statements: Owner-only statements implement critical administrative functionalities, but determining them precisely requires reasoning about complex path conditions.Owners may be one or more addresses responsible for roles such as contract creation or destruction.
Loading 2104.08638v2…