pith. sign in

arxiv: 1907.03868 · v1 · pith:TQLV3PA7new · submitted 2019-07-08 · 💻 cs.CR · cs.SC

Annotary: A Concolic Execution System for Developing Secure Smart Contracts

Konrad Weiss , Julian Sch\"utte This is my paper

Pith reviewed 2026-05-25 00:55 UTC · model grok-4.3

classification 💻 cs.CR cs.SC
keywords smart contractsconcolic executionsymbolic executionEthereumvulnerability detectionannotationsEVM bytecodeblockchain analysis
0
0 comments X

The pith

Annotary uses developer annotations in Solidity to analyze inter-contract and inter-transactional smart contract behaviors by mixing symbolic EVM execution with live blockchain values.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper presents Annotary as a concolic execution framework that lets developers add annotations directly to Solidity source to direct analysis of how contracts call one another across sequences of transactions. It executes EVM bytecode symbolically while resolving concrete values from the actual Ethereum blockchain, addressing the limitation that prior tools could only examine single contracts in isolation. A sympathetic reader would care because deployed contracts are immutable and can hold large sums, so catching vulnerabilities that span multiple contracts and transactions matters for preventing real financial losses. The system trades some soundness for precision by pruning unreachable states through its inter-transactional checks. It is implemented on the Laser symbolic machine and offered as an editor plugin.

Core claim

Annotary supports analysis of inter-transactional, inter-contract control flows by combining symbolic execution of EVM bytecode with resolution of concrete values from the public Ethereum blockchain, guided by annotations that developers write in the Solidity source code.

What carries the argument

Developer-written annotations in Solidity source code that guide concolic execution on the Laser symbolic virtual machine while pulling concrete blockchain storage values.

If this is right

  • Analysis can now cover sequences of transactions that cross contract boundaries instead of stopping at single-contract boundaries.
  • Unreachable states that would generate false positives in pure symbolic execution can be eliminated by consulting actual blockchain call chains.
  • Developers receive guidance inside their usual editor without needing separate formal-methods expertise.
  • Precision receives priority, so some paths may remain unexplored if annotations do not cover them.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The approach suggests that lightweight annotation-driven tools could complement heavier formal verifiers for day-to-day contract development.
  • Because the system already resolves live blockchain values, it could be extended to monitor deployed contracts for emerging interaction patterns after launch.
  • Wider adoption would depend on how easily annotations can be maintained as contracts evolve before deployment.

Load-bearing premise

The annotations written by developers are both accurate and complete enough to steer the analysis through complex inter-contract behaviors without missing paths or creating false guidance.

What would settle it

Apply Annotary to a collection of known vulnerable multi-contract Ethereum deployments and check whether the reported issues match the actual exploits or produce systematic misses traceable to annotation gaps.

Figures

Figures reproduced from arXiv: 1907.03868 by Julian Sch\"utte, Konrad Weiss.

Figure 1
Figure 1. Figure 1: Annotary’s architecture with Solidity files undergoing analysis and violations reported to the editor plugin. analysis component and receives found annotation violations for visualization. 3.1 Annotations Annotary specifies a set of annotations which developers can use to express invariants and restrictions directly in the Solidity source code. These annotations will then be translated into constraints or … view at source ↗
Figure 2
Figure 2. Figure 2: Backward strategy finding state independent sequence for both violations. [PITH_FULL_IMAGE:figures/full_fig_p007_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Annotary marks violated annotations and violating code. [PITH_FULL_IMAGE:figures/full_fig_p013_3.png] view at source ↗
read the original abstract

Ethereum smart contracts are executable programs, deployed on a peer-to-peer network and executed in a consensus-based fashion. Their bytecode is public, immutable and once deployed to the blockchain, cannot be patched anymore. As smart contracts may hold Ether worth of several million dollars, they are attractive targets for attackers and indeed some contracts have successfully been exploited in the recent past, resulting in tremendous financial losses. The correctness of smart contracts is thus of utmost importance. While first approaches on formal verification exist, they demand users to be well-versed in formal methods which are alien to many developers and are only able to analyze individual contracts, without considering their execution environment, i.e., calls to external contracts, sequences of transaction, and values from the actual blockchain storage. In this paper, we present Annotary, a concolic execution framework to analyze smart contracts for vulnerabilities, supported by annotations which developers write directly in the Solidity source code. In contrast to existing work, Annotary supports analysis of inter-transactional, inter-contract control flows and combines symbolic execution of EVM bytecode with a resolution of concrete values from the public Ethereum blockchain. While the analysis of Annotary tends to weight precision higher than soundness, we analyze inter-transactional call chains to eliminate false positives from unreachable states that traditional symbolic execution would not be able to handle. We present the annotation and analysis concepts of Annotary, explain its implementation on top of the Laser symbolic virtual machine, and demonstrate its usage as a plugin for the Sublime Text editor.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 1 minor

Summary. The paper presents Annotary, a concolic execution framework for detecting vulnerabilities in Ethereum smart contracts. It allows developers to write annotations directly in Solidity source code to guide analysis of inter-transactional and inter-contract control flows. The system combines symbolic execution of EVM bytecode (on top of the Laser VM) with concrete values resolved from the public Ethereum blockchain, and is provided as a Sublime Text plugin. The approach explicitly prioritizes precision over soundness.

Significance. If the inter-transactional analysis and annotation-guided path resolution deliver on the claimed reduction in false positives, the work would address a clear gap in existing single-contract symbolic execution tools for smart contracts. The combination of blockchain concrete values with symbolic analysis is a practical strength for real-world contract ecosystems.

major comments (2)
  1. [Abstract] Abstract: The central claim that 'analysis of inter-transactional call chains [eliminates] false positives from unreachable states' lacks any supporting evaluation data, case studies, or quantitative comparison to baseline symbolic execution; without such evidence the practical advantage over prior tools cannot be assessed.
  2. [Abstract] Abstract and implementation description: The framework relies on developer-written annotations being accurate and sufficient to guide inter-contract and inter-transactional analysis, yet provides no mechanism, validation procedure, or completeness argument for these annotations; incorrect annotations would directly undermine the inter-transactional benefit.
minor comments (1)
  1. The manuscript would benefit from a dedicated evaluation section even if preliminary, given that it is a tool paper.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the constructive feedback on our manuscript. The comments highlight important gaps in the presentation of claims and assumptions. We address each point below and indicate planned revisions.

read point-by-point responses

  1. Referee: [Abstract] Abstract: The central claim that 'analysis of inter-transactional call chains [eliminates] false positives from unreachable states' lacks any supporting evaluation data, case studies, or quantitative comparison to baseline symbolic execution; without such evidence the practical advantage over prior tools cannot be assessed.

    Authors: We agree that the manuscript provides no quantitative evaluation, case studies, or direct comparison demonstrating the reduction in false positives. The current version focuses on describing the framework, annotation mechanism, and implementation on Laser. In revision we will qualify the abstract claim to reflect that inter-transactional analysis is intended to reduce unreachable-state false positives in principle, and we will add a dedicated section with concrete examples drawn from the tool's usage to illustrate the effect where possible. revision: yes

  2. Referee: [Abstract] Abstract and implementation description: The framework relies on developer-written annotations being accurate and sufficient to guide inter-contract and inter-transactional analysis, yet provides no mechanism, validation procedure, or completeness argument for these annotations; incorrect annotations would directly undermine the inter-transactional benefit.

    Authors: The design intentionally treats annotations as developer-provided guidance rather than automatically verified specifications, consistent with the precision-over-soundness stance stated in the paper. We acknowledge that the manuscript does not discuss validation procedures or the impact of incorrect annotations. In the revision we will add a short subsection addressing annotation assumptions, potential failure modes, and simple mitigation practices such as annotation review or cross-checking against test transactions. revision: yes

Circularity Check

0 steps flagged

No circularity: tool implementation with no derivation chain

full rationale

The paper presents Annotary as a concolic execution framework and editor plugin. It contains no equations, fitted parameters, predictions, uniqueness theorems, or ansatzes. Claims about inter-transactional analysis rest on the described implementation and annotation mechanism rather than any reduction to prior fitted inputs or self-citations. This is a standard engineering/tool paper whose central contribution is the system itself; the derivation chain is absent and the work is self-contained against external benchmarks such as existing symbolic EVM tools.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

Review performed on abstract only; no free parameters, axioms, or invented entities are described in the available text.

pith-pipeline@v0.9.0 · 5800 in / 1169 out tokens · 19388 ms · 2026-05-25T00:55:06.746506+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

24 extracted references · 24 canonical work pages · 1 internal anchor

  1. [1]

    http://hackingdistributed.com/2016/06/18/analysis-of-the-dao-exploit/, (Accessed on 11/18/2018)

    Analysis of the dao exploit. http://hackingdistributed.com/2016/06/18/analysis-of-the-dao-exploit/, (Accessed on 11/18/2018)

    work page 2016

  2. [2]

    https://forum.ethereum.org/discussion/ 3779/formal-verification-for-solidity-contracts, (Accessed on 11/18/2018)

    Formal verification for solidity contracts - ethereum community forum. https://forum.ethereum.org/discussion/ 3779/formal-verification-for-solidity-contracts, (Accessed on 11/18/2018)

    work page 2018

  3. [3]

    http://hackingdistributed.com/2017/07/22/deep-dive-parity-bug/, (Accessed on 11/18/2018)

    An in-depth look at the parity multisig bug. http://hackingdistributed.com/2017/07/22/deep-dive-parity-bug/, (Accessed on 11/18/2018)

    work page 2017

  4. [4]

    https://github.com/pirapira/ eth-isabelle, (Accessed on 11/25/2018)

    pirapira/eth-isabelle: A lem formalization of evm and some isabelle/hol proofs. https://github.com/pirapira/ eth-isabelle, (Accessed on 11/25/2018)

    work page 2018

  5. [5]

    https://www.parity.io/ a-postmortem-on-the-parity-multi-sig-library-self-destruct/, (Accessed on 11/18/2018)

    A postmortem on the parity multi-sig library self-destruct. https://www.parity.io/ a-postmortem-on-the-parity-multi-sig-library-self-destruct/, (Accessed on 11/18/2018)

    work page 2018

  6. [6]

    https://github.com/ethereum/remix-ide/issues/543, (Ac- cessed on 11/25/2018)

    Remove why3 output - issue #543 - ethereum/remix-ide. https://github.com/ethereum/remix-ide/issues/543, (Ac- cessed on 11/25/2018)

    work page 2018

  7. [7]

    https://solidity.readthedocs.io/en/develop/ 050-breaking-changes.html, (Accessed on 11/20/2018)

    Solidity v0.5.0 breaking changes - solidity 0.5.1 documentation. https://solidity.readthedocs.io/en/develop/ 050-breaking-changes.html, (Accessed on 11/20/2018)

    work page 2018

  8. [8]

    Smt checker poc 1 (2017), https://github.com/ethereum/solidity/projects/8

    work page 2017

  9. [9]

    Fundamentals of Software Engineering (FSEN) (2019), https://git.io/fx6cn

    Ahrendt, W., Bubel, R., Ellul, J., Pace, G.J., Pardo, R., Rebiscoul, V ., Schneider, G.: Verification of Smart Contract Business Logic Exploiting a Java Source Code Verifier. Fundamentals of Software Engineering (FSEN) (2019), https://git.io/fx6cn

    work page 2019

  10. [10]

    In: Proceedings of the 2016 ACM Workshop on Programming Languages and Analysis for Security - PLAS’16 (2016)

    et al., B.: Formal Verification of Smart Contracts. In: Proceedings of the 2016 ACM Workshop on Programming Languages and Analysis for Security - PLAS’16 (2016). https://doi.org/10.1145/2993600.2993611

    work page doi:10.1145/2993600.2993611 2016

  11. [11]

    Vandal: A Scalable Security Analysis Framework for Smart Contracts

    Brent, L., Jurisevic, A., Kong, M., Liu, E., Gauthier, F., Gramoli, V ., Holz, R., Scholz, B.: Vandal: A scalable security analysis framework for smart contracts. arXiv preprint arXiv:1809.03981 (2018)

    work page internal anchor Pith review Pith/arXiv arXiv 2018

  12. [12]

    URL https://github

    Buterin, V ., et al.: Ethereum white paper, 2014. URL https://github. com/ethereum/wiki/wiki/White-Paper (2013)

    work page 2014

  13. [13]

    https://solidity.readthedocs.io/en/v0.4.24/, (Accessed on 11/20/2018)

    Ethereum: Solidity - solidity 0.4.24 documentation. https://solidity.readthedocs.io/en/v0.4.24/, (Accessed on 11/20/2018)

    work page 2018

  14. [14]

    In: European Symposium on Programming

    Filli ˆatre, J.C., Paskevich, A.: Why3 - where programs meet provers. In: European Symposium on Programming. pp. 125–128. Springer (2013)

    work page 2013

  15. [15]

    In: 2018 IEEE 31st Computer Security Foundations Symposium (CSF)

    Hildenbrandt, E., Saxena, M., Rodrigues, N., Zhu, X., Daian, P., Guth, D., Moore, B., Park, D., Zhang, Y ., Stefanescu, A., Rosu, G.: Kevm: A complete formal semantics of the ethereum virtual ma- chine. In: 2018 IEEE 31st Computer Security Foundations Symposium (CSF). pp. 204–217 (July 2018). https://doi.org/10.1109/CSF.2018.00022

    work page doi:10.1109/csf.2018.00022 2018

  16. [16]

    https://doi.org/10.14722/ndss.2018.23082

    Kalra, S., Goel, S., Dhawan, M., Sharma, S.: ZEUS: Analyzing Safety of Smart Contracts (2018). https://doi.org/10.14722/ndss.2018.23082

    work page doi:10.14722/ndss.2018.23082 2018

  17. [17]

    In: 27th {USENIX} Security Symposium ({USENIX} Security 18)

    Krupp, J., Rossow, C.: teether: Gnawing at ethereum to automatically exploit smart contracts. In: 27th {USENIX} Security Symposium ({USENIX} Security 18). pp. 1317–1333 (2018)

    work page 2018

  18. [18]

    In: Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security

    Luu, L., Chu, D.H., Olickel, H., Saxena, P., Hobor, A.: Making smart contracts smarter. In: Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security. pp. 254–269. CCS ’16, ACM, New York, NY , USA (2016). https://doi.org/10.1145/2976749.2978309, http://doi.acm.org/10.1145/2976749.2978309 11 Annotary: A Concolic Execution System...

    work page doi:10.1145/2976749.2978309 2016

  19. [19]

    In: Ramakrishnan, C.R., Rehof, J

    de Moura, L., Bjørner, N.: Z3: An efficient smt solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. pp. 337–340. Springer Berlin Heidelberg, Berlin, Heidelberg (2008)

    work page 2008

  20. [20]

    HITB SECCONF Amsterdam (2018)

    Mueller, B.: Smashing ethereum smart contracts for fun and real profit. HITB SECCONF Amsterdam (2018)

    work page 2018

  21. [21]

    In: Proceedings of the 34th Annual Computer Security Applications Conference

    Nikoli ´c, I., Kolluri, A., Sergey, I., Saxena, P., Hobor, A.: Finding the greedy, prodigal, and suicidal contracts at scale. In: Proceedings of the 34th Annual Computer Security Applications Conference. pp. 653–663. ACSAC ’18, ACM, New York, NY , USA (2018). https://doi.org/10.1145/3274694.3274743, http://doi.acm.org/10.1145/ 3274694.3274743

    work page doi:10.1145/3274694.3274743 2018

  22. [22]

    In: Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineer- ing Conference and Symposium on the Foundations of Software Engineering - ESEC/FSE 2018 (2018)

    Park, D., Zhang, Y ., Saxena, M., Daian, P., Rou, G.: A formal verification tool for Ethereum VM bytecode. In: Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineer- ing Conference and Symposium on the Foundations of Software Engineering - ESEC/FSE 2018 (2018). https://doi.org/10.1145/3236024.3264591

    work page doi:10.1145/3236024.3264591 2018

  23. [23]

    In: Proceedings of the 34th Annual Computer Security Applications Conference

    Torres, C.F., Sch ¨utte, J., State, R.: Osiris: Hunting for integer bugs in ethereum smart contracts. In: Proceedings of the 34th Annual Computer Security Applications Conference. pp. 664–676. ACSAC ’18, ACM, New York, NY , USA (2018). https://doi.org/10.1145/3274694.3274737, http://doi.acm.org/10.1145/3274694.3274737

    work page doi:10.1145/3274694.3274737 2018

  24. [24]

    Wood, G.: Ethereum: a secure decentralised generalised transaction ledger. ethereum project yellow paper 151 (2014) (2014) 12 Annotary: A Concolic Execution System for Developing Secure Smart Contracts A PREPRINT A Appendix A.1 Annotary IDE Plugin Figure 3: Annotary marks violated annotations and violating code. A.2 Code Rewritings Inline Checks at annota...

    work page 2014