Kamil Ježek, Seongho Jeong, Yeonsoo Kim, Bernhard Scholz · 5 authors
Ethereum’s smart contracts operate on directly addressable storage that is represented as tries. The performance of the Ethereum Virtual Machine (EVM) suffers from slow storage access due to trie encoding, which hampers transaction throughput and scalability. To mitigate the Ethereum storage performance bottleneck, we propose a new storage representation for the EVM that supports asynchronous trie construction. Without changing the Ethereum protocol, we add a flat representation called Storage Replica to improve performance. Storage Replica provides a fast lookup of values in the program’s main thread, while a worker thread prepares the tries for subsequent cryptographic calculations. With a storage overhead of less than 5% (i.e., 10 GB), we achieve up to a 6× speedup in processing smart contracts and a 4× speedup in block commits for the initial 9 M blocks of the Ethereum blockchain.
Smart contracts deployed on the Ethereum blockchain execute on the Ethereum Virtual Machine (EVM) and handle financial operations such as payments, asset transfers, and auctions. Given the high value they control, correctness in these contracts is critical, as errors and vulnerabilities have led to losses totalling hundreds of millions of dollars. To address this problem, we develop a novel formalization of the EVM. Compared to existing formalizations, our formalization is in Isabelle/HOL, covers all current EVM opcodes, and formalizes cross-contract execution. Thus, it allows us to express properties which are out of scope for other formalizations. To allow for the execution of our formalization, we implement a code generator, allowing it to be exported as a stand-alone Haskell program. We then validate the semantics by executing νmprint{25000} test cases from the official Ethereum test suite. Our formalization can be used to verify concrete smart contracts but also to reason about the correctness of tools and techniques which manipulate bytecode, such as compilers or optimizers.
K501 is a deterministic temporal-structural integration framework designed to provide append-only state anchoring, canonical serialization, and hash-bound integrity across heterogeneous systems. The framework does not replace existing infrastructures such as databases, version control systems, or distributed ledgers. Instead, it operates as an optional structural overlay layer that encapsulates states in a formally defined frame model with explicit time anchoring (UTC + Unix Epoch). K501 focuses on: Deterministic canonical serialization Append-only historical discipline Explicit temporal positioning Snapshot-based integrity Cross-system structural interoperability The specification defines minimal compliance requirements for structural integration without modifying internal operational semantics of integrated systems. K501 is intended as a neutral structural discipline for temporal knowledge stabilization and reproducible state documentation. Peace 🕊️ Frames stehen nicht isoliert! Das ist eine formal belastbare Beschreibung. Keine Überhöhung.Kein AGI.Keine Spekulation.Aber diese hier ist solide. 🕊️
K501 is a deterministic temporal-structural integration framework designed to provide append-only state anchoring, canonical serialization, and hash-bound integrity across heterogeneous systems. The framework does not replace existing infrastructures such as databases, version control systems, or distributed ledgers. Instead, it operates as an optional structural overlay layer that encapsulates states in a formally defined frame model with explicit time anchoring (UTC + Unix Epoch). K501 focuses on: Deterministic canonical serialization Append-only historical discipline Explicit temporal positioning Snapshot-based integrity Cross-system structural interoperability The specification defines minimal compliance requirements for structural integration without modifying internal operational semantics of integrated systems. K501 is intended as a neutral structural discipline for temporal knowledge stabilization and reproducible state documentation. Peace 🕊️ Frames stehen nicht isoliert! Das ist eine formal belastbare Beschreibung. Keine Überhöhung.Kein AGI.Keine Spekulation.Aber diese hier ist solide. 🕊️
Yinhao Xiao, Chih-Chung Liu, Mingshu Cong, Le Yang
DeFi smart-contract vulnerabilities often arise from protocol-level financial semantics rather than syntactic Solidity patterns. Direct LLM prompting can generate plausible patches that compile but leave oracle, vault, lending, or AMM invariants unresolved. We aim to make LLM-based smart-contract repair more reliable by separating patch generation from domain-specific judgment and requiring accepted patches to improve check-visible semantic obligations. We present DeFiSent, a check-guided repair framework. It normalizes contract code, infers protocol roles, routes vulnerability-family checks, emits structured findings and violated invariants, and prompts an LLM with this evidence. Candidate patches are accepted only after compilation, tests, interface preservation, non-increasing semantic severity, and invariant-specific gates. We evaluate DeFiSent on a coverage-aware corpus from DeFiHackLabs, EVMbench, LISA-Bench, SmartBugs Curated, and BCCC-SCsVuls-2024. The DeepSeek campaign contains 40,452 paired tasks and 80,904 model-mode runs, including a 41,332-row code-level shard. On the unified 6,000-task DeepSeek subset, check guidance improves dynamic pass rate from 54.82\% to 79.95\%, semantic-improvement rate from 40.42\% to 53.92\%, and total severity reduction from 8,733 to 24,084. On a 2,000-task SiliconFlow matrix, aggregate semantic-improvement rate increases from 27.0\% to 57.8\%. Structured findings and gate-based validation substantially improve LLM repair behavior for DeFi contracts. DeFiSent does not replace expert auditing, but it provides a reproducible path for aligning LLM-generated patches with financial-semantic proof obligations.
Smart contracts are self-executing programs deployed on blockchain networks, automating trust-based operations in decentralized applications (DApps). At the same time, their transparency and immutability offer significant advantages; these characteristics make them vulnerable to security flaws that, once deployed, cannot be rectified without substantial consequences. Existing verification tools such as Mythril, Slither, Oyente, and Zeus primarily target Solidity contracts using static or symbolic analysis. However, they fall short in supporting diverse blockchain languages like Rust (used in Solana), Michelson (Tezos), and Move (Aptos/Sui). Additionally, these tools lack formal specification using temporal logic, provide limited scalability for large and complex contracts, and often yield high false favorable rates. This paper presents an enhanced SmartScan framework for formally verifying smart contracts across multiple blockchain ecosystems to address these gaps. The framework introduces language-specific parsers and FSM/BIP model generation pipelines for Solidity, Vyper, Rust, Michelson, and Move. These models are translated into SMV format for symbolic model checking using nuXmv. The proposed algorithms incorporate CTL-based specifications to verify key properties such as fund safety, reentrancy prevention, access control compliance, and arithmetic safety. Scalability is achieved through symbolic abstraction, partial-order reduction, and multi-threaded execution, with optional support for distributed verification using cloud platforms. Experimental evaluation on diverse real-world contracts demonstrated a verification accuracy of over 94%, a 40–50% reduction in FSM states after optimization, and speedups of up to 3.2× with parallel execution. The case study on a cross-chain DeFi contract confirmed consistent vulnerability detection across all supported languages. The proposed framework offers a scalable, secure, and language-agnostic solution for trustworthy, intelligent contract verification.
Reentrancy remains one of the most persistent and damaging vulnerabilities in Ethereum smart contracts, enabling adversaries to recursively drain funds despite the presence of static and runtime defenses. Existing studies mainly focus on detection or program analysis, but they do not explain why and under what conditions attackers decide to exploit. In this work, we introduce a decision-theoretic framework that models reentrancy as a profit-maximizing problem under gas, risk, and atomicity constraints. Our framework derives the conditions under which reentrancy attacks are economically viable and provides an algorithm for computing optimal exploit strategies. We further extend the analysis to multi-contract attacks, capturing sequential, parallel, and optimized execution strategies. A simulation environment evaluates profitability across varying balances and gas configurations, highlighting thresholds where attacks become infeasible. Finally, we translate attacker decision profiles into practical defense recommendations for developers, auditors, and DeFi system designers. This framework bridges the gap between exploit detection and adversarial economics, offering a rigorous basis for strengthening smart contract security. This framework establishes a theoretical baseline for adversarial economics in smart contract security, forming a foundation for future MEV-aware exploitability models and Layer-2 risk analysis.
Traditional digital trust architectures suffer from the “Library Problem”: dependency on pre-compiled, static lookup tables or binaries that must be trusted blindly, creating supply-chain vulnerabilities. This paper proposes a paradigm shift to Intrinsic Trust, where encoding infrastructure is mathematically regenerated at runtime rather than distributed. We introduce the 0MXI Calculus, a deterministic lattice system anchored on universal transcendental constants:the golden ratio Φ ≈ 1.618033988749895 and π ≈ 3.141592653589793, with a contraction ratio λ ≈ 0.339949771344778. Operations on a quantized F15 lattice ensure cross-platform determinism, bounded by a Prime Boundary Horizon (N = 23) that guarantees injective reversibility (Theorems 1 and 2).This framework underpins TreeOS, an operating system that bootstraps from a “Math Root-of-Trust” via autogenesis, regenerating a bijective Tick Table for byte encoding without stored dependencies. TreeBABEL, the verifiable data transport protocol, packages data as JSON artifacts with mathematical manifests for independent receiver validation. Extending this, the VMEM Node Architecture transforms online repositories into externalized memory banks, enabling AI models to scrape and derive OS state on demand, eliminating internal weight bloat and static knowledge cutoffs.We demonstrate adaptability to constrained ledgers (e.g., 280-character limits) for efficient chunking. Through rigorous proofs and a Python reference implementation, we show that trust can be calculated, not stored, decoupling systems from physical hardware and fostering entropy-neutral, zero-trust computation.
The smart contracts facilitated by blockchains allow the decentralized and automated implementation of digital contracts, yet the current security measures in this space are mostly geared towards vulnerability detection and post-implementation functionality, which do not provide much defence against runtime attacks. The paper analyses the concept of smart contracts as a unified approach to cybersecurity, and provides a Hardened Smart Contract Model (HSCM) as a proactive and runtime security quotient model. The suggested model places policy-conscious logic, formal safety requirements, risk aversive execution, upgradability under control by governance, and unchangeable auditability directly in the design of contracts. The framework guarantees the elimination of unauthorized access, re-entrancy and logic abuse by providing runtime verification and automated response measures that avert such violations even before state transitions take place. A fair amount of experimental confirmation on an Ethereum-compatible system proves that there is a high security guarantee with tolerable load overhead, the deployed smart contracts could be hardened.
Abstract Program verification provides stronger guarantees of correctness than standard testing. The verification process takes a program as input and derives a mathematical formula. Proving that a program is correct then reduces to establishing that this derived formula is unsatisfiable. Traditionally, automated reasoning tools can be used to determine unsatisfiability automatically. Furthermore, modern solvers can also produce a proof of unsatisfiability. However, these techniques typically rely on the proof and the underlying code being publicly available, which may not be desirable for certain applications. This work shows how to address this problem. Our team initially developed a protocol for validating the unsatisfiability of Boolean formulas in privacy-preserving settings. Building on these initial results, we devised ZKSMT, a virtual machine for validating unsatisfiability results produced by SMT solvers in zero-knowledge settings. In this paper we describe the theoretical foundations of such virtual machines and demonstrate how they can be applied to the theories of uninterpreted functions and linear integer arithmetic, two of the most widely used theories in verification. We conclude by outlining how the full formal verification workflow can be adapted to operate in privacy-preserving settings.
Leanne Ngo, Tran Tien Nhat, anon anon, Triet Huynh Minh Le · 7 authors
Smart contracts underpin modern blockchain ecosystems, enabling decentralized applications in DeFi and digital asset management. However, their immutability exacerbates programming errors and vulnerabilities, leading to unpatchable flaws and significant financial losses, as seen in high-profile exploits. Current vulnerability detection methods including static and dynamic analysis—face critical limitations: (1) static analysis suffers from state-space explosion, control-flow complexity, over-approximation, and high false positives; (2) dynamic fuzzing relies on syntactic/random mutations lacking semantic awareness, inefficiently exploring deep state-dependent paths and complex transaction sequences; (3) both static and dynamic approaches overlook semantic-structural gaps, such as execution order semantics in reentrancy vulnerabilities; (4) fuzzing reports lack explainability, hindering practical auditing. To address these challenges, we propose MAESFuzz1, a multi-agent semantic-guided smart contract fuzzing framework that integrates static structural analysis, dynamic execution feedback, and Large Language Model (LLM)–assisted reasoning within a closed-loop architecture. MAESFuzz employs LLMs as semantic advisors to guide seed generation, transaction sequence construction, and mutation refinement, enabling effective exploration of deep state-dependent behaviors and complex multi-transaction vulnerabilities. Extensive evaluation on the SoliAudit benchmark and a real-world dataset of deployed Ethereum contracts shows that MAESFuzz improves vulnerability detection by up to 28.7% relative to state-of-the-art (SOTA) smart contract fuzzers on SoliAudit. On real-world contracts, MAESFuzz uncovers 25 more expert-validated vulnerabilities than the strongest SOTA baseline while maintaining 94.38% precision and competitive execution coverage. In addition, MAESFuzz generates structured, execution-grounded audit reports to enhance interpretability and support practical security auditing.
This registration documents the creation, structure, and validation workflow of SARMF-Bench, a minimal reproducible benchmark dataset for smart contract vulnerability analysis. SARMF-Bench consists of five intentionally engineered Solidity contracts representing canonical vulnerability classes: Reentrancy, Arithmetic Overflow Behavior, Access Control Weakness, Unchecked External Call, and Denial-of-Service Pattern. Each contract is paired with machine-readable static analysis outputs generated using Slither v0.11.5. The objective of this dataset is to provide a controlled experimental baseline for evaluating static analyzers, symbolic execution engines, fuzzers, and AI-assisted smart contract security tools. All artifacts were created in a controlled Linux environment and validated for reproducibility through consistent detector metadata (impact and confidence levels). No synthetic mutation frameworks or automated vulnerability generators were used. This registration serves as a timestamped, immutable research record documenting dataset structure, methodology, and reproducibility protocol.
The rapid growth of IoT devices has increased security risks, particularly in firmware updates and device authentication. Traditional approaches are vulnerable to attacks such as unauthorised access and data breaches. This study proposes a blockchain-based framework using smart contracts and a proof-of-authority (PoA) consensus mechanism to ensure secure firmware verification and decentralised authentication. The system leverages distributed ledger technology to enhance integrity, trust, and scalability in IoT environments. Experimental results demonstrate reduced latency, improved throughput, and strong resistance to common cyber threats, making the framework suitable for large-scale IoT deployments.
We present Processual Memory Architecture (PMA), a computational framework that unifies data storage and computation by representing all information as transformation functions rather than static state, rendering the traditional ontological distinction between them architecturally unnecessary. In PMA, storing information means encoding it as a mathematical transformation that produces the data when applied to a standardized canonical input; reading means applying the transformation; and computing means composing transformations. This inversion of the conventional von Neumann paradigm yields five emergent architectural properties—structural auditability, transparent reasoning, enforced constraints, tamper evidence, and reversibility—that collectively enable verifiable computation: systems that can mathematically verify the integrity and correctness of their own reasoning chains. We provide a complete mathematical specification of PMA over Galois fields GF(2k) with roundtrip exactness guarantees, constructive algorithms for both invertible and non-invertible encoding modes, and a reference permutation-based embodiment with explicit bit-level storage formats. We analyze thermodynamic properties under reversible logic implementation, demonstrating that PMA operations on adiabatic substrates can approach within 10× of the Landauer limit at the localnode level. We then present the integration architecture for PMA with artificial general intelligence (AGI) safety frameworks, showing how transformation-based reasoning enables safety constraints that are structural rather than advisory—creating systems where unsafe behavior is computationally undefined rather than merely prohibited. We discuss applications to financial auditing, medical AI verification, and autonomous systems governance, and compare PMA's approach to verifiable computation with existing paradigms including blockchain, zero-knowledge proofs, and mechanistic interpretability.
<b><i>Liquidity Exit Drain</i></b>, also referred to as a <b><i>Rug Stream</i></b>, describes a class of gradual capital extraction attacks in decentralized finance (DeFi) and stablecoin ecosystems. Unlike abrupt rug pulls or discrete exploit-based failures, Liquidity Exit Drains operate through prolonged, cumulative actions that remain within protocol-defined operational and governance boundaries. By exploiting trust persistence, governance opacity, and parameter flexibility, these attacks systematically siphon liquidity over extended time horizons while evading conventional audits and user detection. This paper formalizes <b><i>Liquidity Exit Drain</i></b> as a distinct economic attack class, examines its structural enablers and execution patterns, and outlines why existing security, audit, and monitoring frameworks frequently fail to detect it. The analysis highlights the need for longitudinal economic oversight and governance-aware risk assessment beyond static code correctness.
SARMF-Bench is a structured and reproducible benchmark dataset for smart contract vulnerability analysis. It consists of five minimal Solidity contracts representing canonical vulnerability classes: • Reentrancy • Arithmetic Overflow Behavior • Access Control Weakness • Unchecked External Call • Denial-of-Service Pattern Each contract is paired with machine-readable static analysis outputs generated using Slither v0.11.5. The dataset is designed to support controlled benchmarking experiments for: - Static analyzers - Symbolic execution engines - Fuzzers - AI-assisted smart contract security tools Related assets: GitHub repository: https://github.com/profmohit-edu/sarmf-framework Zenodo software DOI: https://doi.org/10.5281/zenodo.18754015 Reproducibility protocol: https://doi.org/10.17504/protocols.io.bp216eyxdgqe/v1 Mendeley dataset DOI (pending moderation): https://doi.org/10.17632/kd3vcpnn9v.1 HAL record: https://hal.science
Decentralized systems are increasingly required to operate across heterogeneous environments involving human presence, real-world assets, regulatory constraints, and adversarial network conditions. Traditional execution models, which assume static infrastructure, context-free computation, and pre-authorized identities, are insufficient for these emerging requirements. This paper introduces a Presence-Centric execution architecture that binds computational validity to verifiable environmental state at execution time. The proposed system is structured around two core components: the Crystal Validator, a context-aware validation layer, and an AI Feedback Loop, which enables adaptive policy enforcement based on observed outcomes. Central to this architecture is <b><i>Environment-Coupled Execution</i></b>, a model in which identity, intent, policy, and environment are jointly evaluated to determine execution validity. By treating environment as a first-class execution dependency, the system enables contextual non-repudiation, replay resistance, regulatory determinism, and post-execution auditability. The proposed approach is applicable to decentralized finance, stablecoins, real-world asset tokenization, governance systems, and presence-driven digital platforms.
<b><i>Governance Voter Loop Reuse</i></b> is a strategic exploit in decentralized finance (DeFi) governance systems whereby the same economic capital is repeatedly reused to exert voting influence across multiple proposals, epochs, or governance venues without maintaining sustained economic exposure. By exploiting snapshot-based voting, token mobility, and weak binding between voting power and duration of risk, attackers can artificially amplify governance influence while avoiding long-term commitment. This paper formalizes the exploit, analyzes its structural enablers and execution mechanisms, and evaluates its systemic impact on DAO legitimacy and protocol security. We further propose mitigation requirements centered on time-weighted exposure, continuity-aware governance models, and behavioral detection mechanisms.