pith. sign in

arxiv: 2606.18064 · v1 · pith:VJW2SPHEnew · submitted 2026-06-16 · 💻 cs.PL

Defense-in-Depth Runtime Safety in Move

Victor Gao , Wolfgang Grieskamp , Vineeth Kashyap , George Mitenkov , Teng Zhang , Runtian Zhou , Andrea Cappa , Marco Ilardi This is my paper

Pith reviewed 2026-06-26 21:51 UTC · model grok-4.3

classification 💻 cs.PL
keywords MoveAptosruntime safety checksdefense-in-depthsmart contractsverifier bugsbytecode verificationblockchain security
0
0 comments X

The pith

Aptos adds runtime safety checks to Move execution that independently verify invariants and protect against static verifier bugs or malicious bytecode.

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

Move programs on Aptos run as typed bytecode in a sandboxed VM that performs static verification of type safety and reference safety at load time. The static verifier is complex and evolving, so it can contain bugs that would allow asset loss, forged authority, or state corruption in a live blockchain. Aptos therefore runs independent runtime checks during execution that re-verify the same critical invariants. These checks supply defense-in-depth protection even when the static verifier misses a violation or when malicious bytecode is supplied. A sympathetic reader cares because the design directly addresses the high-stakes reality that a single missed rule violation can cause irreversible on-chain damage.

Core claim

The paper establishes that defense-in-depth runtime safety checks, performed during Move bytecode execution on Aptos, independently verify the critical invariants that the static verifier is intended to enforce, thereby protecting the blockchain against latent bugs in the verifier and against malicious bytecode that would otherwise evade detection.

What carries the argument

Defense-in-depth runtime safety checks that independently verify the critical invariants during execution.

If this is right

  • A missed static-verifier bug no longer directly translates into on-chain asset loss or corruption.
  • The verifier can continue to evolve without immediately exposing the chain to new rule violations.
  • Malicious or hand-crafted bytecode is still rejected at execution time even if it passes load-time checks.
  • The overall system maintains safety guarantees even when the static verification logic is incomplete or incorrect.

Where Pith is reading between the lines

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

  • Similar runtime re-checking could be added to other languages whose static analyzers are large and change frequently.
  • The runtime checks could themselves become a source of performance overhead that future work would need to measure and reduce.
  • Independent testing or fuzzing of the runtime checks against the static verifier could serve as an ongoing validation method.
  • The approach illustrates a general pattern for high-value execution environments where static analysis alone is considered insufficient.

Load-bearing premise

The runtime checks are correctly implemented, cover the same critical invariants as the static verifier, and do not introduce new exploitable bugs themselves.

What would settle it

A concrete transaction that violates a critical invariant, passes both the static verifier and the runtime checks, and causes asset loss or state corruption would show that the runtime layer does not provide the claimed protection.

Figures

Figures reproduced from arXiv: 2606.18064 by Andrea Cappa, George Mitenkov, Marco Ilardi, Runtian Zhou, Teng Zhang, Victor Gao, Vineeth Kashyap, Wolfgang Grieskamp.

Figure 1
Figure 1. Figure 1: A dotted line links each bytecode operation (left) to the access-path-tree [PITH_FULL_IMAGE:figures/full_fig_p005_1.png] view at source ↗
read the original abstract

Move is a smart-contract language used to execute transactions on the Aptos blockchain. Move programs execute in a sandboxed VM as typed bytecode. The VM statically verifies foundational safety properties like type safety and reference safety at code loading time. In principle, this design gives strong guarantees for Move. However, the static verification logic is complex and continually evolving with the language; like any software, it is not immune to bugs. In a live blockchain setting, a missed rule violation can translate directly into loss of assets, forged authority, or unrecoverable corruption of on-chain state. For this reason, Aptos relies on defense-in-depth runtime safety checks that independently verify the critical invariants during execution, providing protection against latent verifier bugs and malicious bytecode. This paper motivates and describes the runtime safety checks for Move on Aptos.

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

1 major / 0 minor

Summary. The paper motivates the use of defense-in-depth runtime safety checks in the Move VM on Aptos to protect against latent bugs in the static verifier for properties such as type safety and reference safety. It describes selected runtime checks that independently verify critical invariants during execution, arguing this provides protection against malicious bytecode in a live blockchain setting.

Significance. If the runtime checks are shown to cover the same invariants as the static verifier without gaps or new vulnerabilities, the work would be significant for practical security in resource-constrained blockchain VMs, where static analysis alone is insufficient due to verifier complexity. The description of concrete checks in a production system is a strength for systems-oriented PL research.

major comments (1)
  1. [Description of runtime checks (throughout)] The central claim that runtime checks 'independently verify the critical invariants' requires a systematic correspondence between static verifier rules and runtime checks, yet the manuscript provides only selected descriptions without an enumeration or completeness argument. This is load-bearing for the defense-in-depth motivation.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the constructive feedback on the central claim of the paper. We address the major comment below and will revise the manuscript to strengthen the defense-in-depth argument.

read point-by-point responses

  1. Referee: The central claim that runtime checks 'independently verify the critical invariants' requires a systematic correspondence between static verifier rules and runtime checks, yet the manuscript provides only selected descriptions without an enumeration or completeness argument. This is load-bearing for the defense-in-depth motivation.

    Authors: We agree that the manuscript would benefit from a more explicit mapping. The current version describes selected runtime checks that target critical invariants (type safety, reference safety, and resource linearity) as implemented in the Aptos Move VM. In revision we will add a new subsection that enumerates the primary static verifier rules for these properties and provides a direct correspondence to the runtime checks that independently re-verify them at execution time. We will also include a brief argument explaining why these checks address the invariants most relevant to asset safety in a live blockchain setting. A exhaustive formal completeness proof for every possible verifier rule is outside the scope of this systems paper, given the verifier's ongoing evolution, but the added mapping will make the independence claim more systematic and address the load-bearing concern. revision: yes

Circularity Check

0 steps flagged

No circularity; purely descriptive design paper with no derivations or fitted claims

full rationale

The manuscript motivates and describes runtime safety checks for Move on Aptos but contains no equations, derivations, predictions, or parameter fits. The central claim—that runtime checks independently verify critical invariants—is presented as an engineering design decision rather than derived from any self-referential construction, self-citation chain, or ansatz. No load-bearing step reduces to its own inputs by construction, and the text supplies no uniqueness theorems or renamed empirical patterns. This is the normal case of a self-contained descriptive paper.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

Abstract-only review; no technical derivations, parameters, or new entities are present in the provided text.

pith-pipeline@v0.9.1-grok · 5683 in / 969 out tokens · 15318 ms · 2026-06-26T21:51:07.038230+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

26 extracted references · 7 canonical work pages · 1 internal anchor

  1. [1]

    https://developers.libra.org/docs/the-libra-blockchain-paper (2019)

    Amsden, Z., Arora, R., Bano, S., Baudet, M., Blackshear, S., Bothra, A., Cabrera, G., Catalini, C., Chalkias, K., Cheng, E., Ching, A., Chursin, A., Danezis, G., Giacomo, G.D., Dill, D.L., Ding, H., Doudchenko, N., Gao, V., Gao, Z., Garillot, F., Gorven, M., Hayes, P., Hou, J.M., Hu, Y., Hurley, K., Lewi, K., Li, C., Li, Z., Malkhi, D., Margulis, S., Maur...

    2019

  2. [2]

    https://aptos-labs.github.io/framewor k-book/ (2023), accessed: 2026-05-09

    Aptos Labs: The Aptos Framework Book. https://aptos-labs.github.io/framewor k-book/ (2023), accessed: 2026-05-09

    2023

  3. [3]

    https://aptos-labs.github.io/move-book/ (2023), accessed: 2026-05-09

    Aptos Labs: The Move on Aptos Book. https://aptos-labs.github.io/move-book/ (2023), accessed: 2026-05-09

    2023

  4. [4]

    https://github.com/aptos-labs/aptos-core (2026), accessed: 2026-06-14

    Aptos Labs: Aptos Core. https://github.com/aptos-labs/aptos-core (2026), accessed: 2026-06-14

    2026

  5. [5]

    https://aptosnetwork.com/ (2026), accessed: 2026-06- 13

    Aptos Labs: Aptos Network. https://aptosnetwork.com/ (2026), accessed: 2026-06- 13

    2026

  6. [6]

    In: Lectures on Runtime Verification, Lecture Notes in Computer Science, vol

    Bartocci, E., Falcone, Y., Francalanza, A., Reger, G.: Introduction to runtime verification. In: Lectures on Runtime Verification, Lecture Notes in Computer Science, vol. 10457, pp. 1–33. Springer (2018)

    2018

  7. [7]

    Blackshear, S., Cheng, E., Dill, D.L., Gao, V., Maurer, B., Nowacki, T., Pott, A., Qadeer, S., Rain, Russi, D., Sezer, S., Zakian, T., Zho, R.: Move: A Language With Programmable Resources (2019), https://developers.libra.org/docs/move-paper

    2019

  8. [8]

    org/abs/2004.05106

    Blackshear, S., Dill, D.L., Qadeer, S., Barrett, C.W., Mitchell, J.C., Padon, O., Zohar, Y.: Resources: A safe language abstraction for money (2020), https://arxiv. org/abs/2004.05106

    work page arXiv 2020

  9. [9]

    CoRRabs/2205.05181(2022), https://arxiv.org/abs/2205.05181

    Blackshear, S., Mitchell, J.C., Nowacki, T., Qadeer, S.: The Move borrow checker. CoRRabs/2205.05181(2022), https://arxiv.org/abs/2205.05181

    work page arXiv 2022

  10. [10]

    In: USENIX Annual Technical Conference (USENIX ATC)

    Chow, J., Garfinkel, T., Chen, P.M.: Decoupling dynamic program analysis from execution in virtual environments. In: USENIX Annual Technical Conference (USENIX ATC). pp. 1–14 (2008)

    2008

  11. [11]

    https://decibel.trade/ (2026), accessed: 2026-06-14

    Decibel trading engine. https://decibel.trade/ (2026), accessed: 2026-06-14

    2026

  12. [12]

    In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2022)

    Dill, D.L., Grieskamp, W., Park, J., Qadeer, S., Xu, M., Zhong, J.E.: Fast and reliable formal verification of smart contracts with the move prover. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2022). Lecture Notes in Computer Science, vol. 13243, pp. 183–200. Springer (2022). https://doi.org/10.1007/978-3-030-99524-9_10

    work page doi:10.1007/978-3-030-99524-9_10 2022

  13. [13]

    In: Proceedings of the 28th ACM SIGPLAN Annual Symposium on Principles and Practice of Parallel Programming (PPoPP 2023)

    Gelashvili, R., Spiegelman, A., Xiang, Z., Danezis, G., Li, Z., Malkhi, D., Xia, Y., Zhou, R.: Block-STM: Scaling blockchain execution by turning ordering curse to a performance blessing. In: Proceedings of the 28th ACM SIGPLAN Annual Symposium on Principles and Practice of Parallel Programming (PPoPP 2023). pp. 232–244. ACM (2023). https://doi.org/10.114...

    work page doi:10.1145/3572848.3577524 2023

  14. [14]

    Formal Verification of Imperative First-Class Functions in Move

    Grieskamp, W., Zhang, T., Kashyap, V., Silverman, J.: Formal verification of imperative first-class functions in Move. CoRRabs/2605.10007(2026), https: //arxiv.org/abs/2605.10007

    work page internal anchor Pith review Pith/arXiv arXiv 2026

  15. [15]

    Hildenbrandt, E., Saxena, M., Rodrigues, N., Zhu, X., Daian, P., Guth, D., Moore, B.M., Park, D., Zhang, Y., Stefanescu, A., Rosu, G.: KEVM: A complete formal semantics of the ethereum virtual machine. In: CSF. pp. 204–217. IEEE Computer Society (2018) 10 V. Gao et al

    2018

  16. [16]

    In: ACM SIGSAC Conference on Computer and Communications Security (CCS)

    Jee, K., Kemerlis, V.P., Keromytis, A.D., Portokalidis, G.: ShadowReplica: Efficient parallelization of dynamic data flow tracking. In: ACM SIGSAC Conference on Computer and Communications Security (CCS). pp. 235–246 (2013)

    2013

  17. [17]

    Jung, R., Dang, H.H., Kang, J., Dreyer, D.: Stacked borrows: An aliasing model for Rust. Proc. ACM Program. Lang.4(POPL), 41:1–41:32 (2020)

    2020

  18. [18]

    Jung, R., Jourdan, J.H., Krebbers, R., Dreyer, D.: RustBelt: Securing the founda- tions of the Rust programming language. Proc. ACM Program. Lang.2(POPL), 66:1–66:34 (2018)

    2018

  19. [19]

    Addison-Wesley (1997)

    Lindholm, T., Yellin, F.: The Java Virtual Machine Specification. Addison-Wesley (1997)

    1997

  20. [20]

    Matsakis and Felix S

    Matsakis, N.D., Klock, II, F.S.: The Rust Language, nourl = http://doi.acm.org/10.1145/2692956.2663188. Ada Lett.34(3), 103–104 (Oct 2014). https://doi.org/10.1145/2692956.2663188

    work page doi:10.1145/2692956.2663188 2014

  21. [21]

    Meijer, E., Wa, R., Gough, J.: Technical overview of the common language runtime (2000)

    2000

  22. [22]

    In: 31st IEEE/ACM International Conference on Automated Software Engineering (ASE)

    Ming, J., Wu, D., Wang, J., Xiao, G., Liu, P.: StraightTaint: Decoupled offline symbolic taint analysis. In: 31st IEEE/ACM International Conference on Automated Software Engineering (ASE). pp. 308–319 (2016)

    2016

  23. [23]

    In: 5th International Workshop on Formal Methods for Blockchains (FMBC 2024)

    Park, J., Zhang, T., Grieskamp, W., Xu, M., Giacomo, G.D., Chen, K., Lu, Y., Chen, R.: Securing Aptos Framework with Formal Verification. In: 5th International Workshop on Formal Methods for Blockchains (FMBC 2024). Open Access Series in Informatics (OASIcs), vol. 118, pp. 9:1–9:16. Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024). https://doi.org...

    work page doi:10.4230/oasics.fmbc.2024.9 2024

  24. [24]

    MIT Press, Cambridge, MA, USA (2002)

    Pierce, B.C.: Types and Programming Languages. MIT Press, Cambridge, MA, USA (2002)

    2002

  25. [25]

    Villani, N., Dang, H.H., Jourdan, J.H., Jung, R., Dreyer, D.: Tree borrows. Proc. ACM Program. Lang.9(PLDI) (2025)

    2025

  26. [26]

    Wood, G.: Ethereum: A secure decentralised generalised transaction ledger (2014), https://ethereum.github.io/yellowpaper/paper.pdf

    2014