Smart contracts, self-executing agreements written in code, are increasingly prevalent in decentralized applications (dApps). However, their immutable nature and complex logic make them vulnerable to security breaches, leading to significant financial losses and reputational damage. Traditional security auditing methods, relying heavily on manual code review and fuzzing, are often insufficient in uncovering subtle vulnerabilities. This paper proposes a novel approach to smart contract security auditing utilizing formal verification. We represent smart contracts as formal specifications and employ formal verification tools to rigorously analyze their behavior and detect potential security flaws. The core claim is that leveraging formal verification techniques significantly enhances the security and reliability of smart contracts. The core mechanism involves translating the contract's logic into a formal language, allowing automated verification against predefined security properties. This approach addresses the limitations of traditional auditing, providing a more comprehensive and reliable assessment of smart contract security. The research contributes to a proactive security strategy for smart contract development, reducing the risk of vulnerabilities and fostering greater trust in decentralized systems.
Proof-of-Work (PoW) consensus mechanisms, foundational to cryptocurrencies like Bitcoin, rely on computational difficulty to secure the network. However, this reliance introduces vulnerabilities. Traditional PoW systems are susceptible to targeted attacks where adversaries strategically generate blocks designed to disrupt consensus. This paper proposes a novel approach – adversarial training – to mitigate these vulnerabilities. We introduce a framework where a generator, mimicking an attacker, attempts to craft malicious blocks, while a discriminator learns to identify these blocks. Through iterative training, the system strengthens its defenses against such attacks, promoting robust consensus. This represents a significant departure from conventional PoW security strategies and offers a potentially more resilient approach to distributed ledger technology. We demonstrate the core principle through a conceptual model and outline a possible implementation strategy, highlighting the potential for future research and development.
Blockchain consensus protocols are complex systems requiring rigorous formal analysis to ensure security, reliability, and efficiency. Traditional methods for formal specification, often relying on state machines and temporal logic, frequently result in overly complex and difficult-to-manage specifications. This paper proposes a novel approach utilizing category theory to provide a more concise, elegant, and ultimately more powerful framework for specifying these protocols. We demonstrate how the inherent structural relationships within consensus protocols—the interactions between nodes, the propagation of messages, and the agreement on states—can be naturally represented and analyzed through category theory concepts such as objects, morphisms, and functors. This approach allows for a higher level of abstraction, facilitating a clearer understanding of the protocol's behavior and enabling more effective verification and validation. The key benefits of this method include reduced specification complexity, improved expressiveness, and enhanced modularity. We present a concrete example of applying category theory to the specification of a simplified Practical Byzantine Fault Tolerance (PBFT) protocol, highlighting the advantages of this new perspective.
OEURO is a EUR-denominated clearing token designed for direct account-to-account settlement.It is implemented as a restricted ERC-20 token with 6 decimals and a deliberately narrow functional scope.Its primary purpose is clearing and settlement, rather than market trading or speculative use.Ordinary transfers are designed for direct EOA-to-EOA circulation.The reference implementation disables approve() and transferFrom().Ordinary transfers to smart-contract recipients are rejected. Minting and burning are explicit operations controlled by the manager.Authorized oracles may submit MINT or BURN requests but cannot directly alter token supply.Oracle requests remain valid for 24 hours and must be executed or rejected by the manager.External clearing references are protected against replay through single-use proof handling.The architecture therefore separates attestation authority from final settlement authority.OEURO uses a restricted recipient model for sensitive infrastructure addresses.The reference contract uses OpenZeppelin ERC-20 and Ownable2Step components.Ethereum Sepolia is used as the current public reference testnet environment.This Zenodo archive contains the Solidity source code, ABI, flattened contract and the OEURO technical white paper and audit reference.
The increasing prevalence of smart contracts in decentralized applications necessitates robust methods for ensuring their correctness and security. Smart contracts, due to their inherent complexity and potential for subtle errors, pose a significant challenge for traditional verification techniques. This paper proposes a novel approach combining symbolic execution with constraint solving and temporal logic verification for the systematic analysis of smart contracts. The core idea is to systematically explore the execution paths of a smart contract using symbolic execution, identifying potential vulnerabilities and execution scenarios. Subsequently, temporal logic is applied to formally verify that the contract's behavior aligns with its intended specifications over time, capturing temporal constraints such as safety and liveness properties. This integrated framework provides a more comprehensive and reliable method for verifying smart contracts compared to relying solely on symbolic execution or temporal logic alone. The approach offers a structured methodology for detecting and mitigating risks associated with smart contract development.
PRE-GHR XXXIX v5.0 (2026-08-28) — release version closing all six objections of an adversarial pre-submission review. PRE-GHR XXXVIII gave the series its first formal definition of the irreducible governance residue δ0μ(P) := inf over admissible P' of ||residue(P')|| and proved a bit-level lower bound. This paper builds the property theory. The mathematics is a domain-order theory: every inequality follows from how the admissible domain D(P) behaves under enlargement or composition of protocols. We prove monotonicity of δ0μ in the erasure surface, an exact composition law δ0μ(P1 ∘ P2) = δ0μ(P1) + δ0μ(P2) − |T(P1) ∩ T(P2)| under explicit hypotheses (segment autonomy, joint attainability, cross-segment cleanliness), and positivity δ0μ(P) > 0 whenever T(P) is non-empty as a purely normative fact, with Landauer's principle confined to the physical interpretation. We then ask what a running system's audit ledgers can measure. The answer is stratified: the ordering structure is measurable in principle — conditional on a fixed normalization and full retention — while the absolute value is stated relative to a fixed code-point measure, and the aggregate-to-single-protocol bridge remains open. No interception statistic is claimed to equal δ0μ; where the wall cannot be built, the gap is marked, not papered over. Changes in v5.0 (six revision tickets, R01–R06, each closing one reviewer objection): R01 — Theorem 4 unilateralized: the safe direction (T(P) non-empty ⇒ δ0μ > 0) remains a theorem; the converse is demoted to Observation 4.1 under an explicit complete-erasure assumption. A witness-reading remark records that δ0μ is a minimum witness cardinality in the sense of why-provenance, inherited and not claimed as new. R02 — ledger counts restricted to lower witnesses only: the ordering claim is measurable solely under a fixed normalization and full retention, stated as an explicit condition rather than an implicit assumption. R03 — the uniform-sampling remark now carries an explicit finite-sample bound (Hoeffding's inequality in its standard form), two-sided: “holds in expectation” is no longer used as if it held for a sample. R04 — four empirical mappings corrected: schema-field disjointness is separated from retained-trace intersection; the approximate join reports both false-negative and false-positive error (the earlier “directionally safe, never over-counting” claim is withdrawn); the overlap-error direction is declared two-sided and governed by an error budget rather than assumed away; and the retention ratio is restated as an interception-event ratio in matched units. R05 — measure-relative notation throughout: bits and code points are two measures on one trace universe, so every ordering claim is stated at a fixed μ and changing μ defines a new quantity rather than restating the old one. R06 — subject classification reassessed and Related Work rebuilt. The paper contains no multiagent model and no coordinated-interaction result; the earlier cs.MA classification is withdrawn as unsupported by the technical content, and the classification adopted here is cs.CR primary with cs.DB cross-list. Related Work now separates the lineage the paper inherits from — linked timestamping and distributed witnesses (Haber & Stornetta 1991; Bayer, Haber & Stornetta 1993), split-view detection and the undefined gossip layer (Certificate Transparency, RFC 6962 / RFC 9162), existence-not-authenticity timestamping (OpenTimestamps), provenance and lineage (W3C PROV; Buneman, Khanna & Tan 2001; Cui, Widom & Wiener 2000), record linkage (Fellegi & Sunter 1969), trace semantics (Hoare 1978; Brookes, Hoare & Roscoe 1984), and measure and order (Halmos; Davey & Priestley) — from adjacent recent lines cited for comparison only. Where a construction of this paper rediscovers an existing one, priority is assigned to the source and no originality is claimed. Honesty notes. Citations to Hoeffding, Fellegi & Sunter, Halmos, Davey & Priestley and the CSP literature are made at the level of the standard statement of each framework only, pending full-text verification. Two candidate references were deliberately excluded because their primary sources could not be verified. Two gaps are inherited rather than closed: the hash-chain anchor has no consistency-proof comparison mechanism, and the anchor-propagation (gossip) layer is undefined in the source standard as well. Open questions Q5.1, Q5.3 and Q5.4 remain declared open.
Decentralized networks, such as blockchain and peer-to-peer systems, rely on trust propagation mechanisms to maintain integrity and security. However, these mechanisms are often complex and prone to errors. This paper presents a novel approach to formally verify the correctness of trust propagation in these networks using temporal reachability analysis. We model the trust propagation process as a temporal system and employ model checking techniques to rigorously assess the system's behavior. The key contribution lies in providing a mathematical framework for guaranteeing that trust is propagated accurately and efficiently, addressing a critical gap in the current landscape of decentralized network security. This approach enables developers to confidently implement trust propagation algorithms, reducing the risk of vulnerabilities and enhancing network resilience. The paper details the methodology, provides a formal specification of the trust propagation process, and illustrates its application with a concrete example.
Decentralized consensus algorithms are the foundation of blockchain technology, enabling trustless and secure distributed systems. However, verifying the correctness and security of these algorithms is a formidable challenge due to their inherent complexity, distributed nature, and susceptibility to various failure modes, notably Byzantine faults. This paper proposes a novel approach utilizing abstract interpretation techniques to provide a rigorous and mathematically sound method for formal verification. We leverage techniques like interval analysis and linear arithmetic to construct abstract models of consensus protocols. These models allow us to formally verify crucial properties such as liveness (guaranteeing eventual agreement), safety (preventing incorrect states), and resilience to Byzantine failures. The approach offers a significant advancement over traditional testing and simulation methods, providing a higher degree of confidence in the reliability and security of decentralized consensus algorithms. The core contribution lies in the systematic application of abstract interpretation to model and verify complex, distributed systems, offering a pathway to robust and trustworthy blockchain implementations.
Blockchain technology has garnered significant attention as a revolutionary distributed ledger system. However, the security and efficiency of blockchain consensus protocols – the mechanisms that ensure agreement among nodes – remain a critical concern. These protocols are often characterized by intricate designs and complex interactions, making traditional testing methods insufficient to guarantee their robustness. This paper proposes a novel approach to formally model and verify blockchain consensus protocols using symbolic execution. Symbolic execution allows us to systematically explore all possible execution paths of a protocol, identifying potential vulnerabilities, inefficiencies, and deviations from the intended behavior. By representing variables with symbolic values rather than concrete values, we can create a comprehensive model that captures the protocol's logic without being constrained by specific data. This approach offers a rigorous and automated method for assessing the security and performance of blockchain consensus protocols, ultimately contributing to the development of more trustworthy and reliable decentralized systems.
Blockchain technology's core functionality relies heavily on consensus algorithms to maintain data integrity and security. However, the complexity inherent in these algorithms introduces significant potential for errors and vulnerabilities. This paper proposes a formal verification approach utilizing model checking to rigorously assess the correctness and security of prominent blockchain consensus algorithms, including Proof-of-Work (PoW) and Proof-of-Stake (PoS). We define formal specifications of these algorithms and employ a model checker to explore all possible states and transitions, identifying potential bugs and ensuring adherence to protocol rules. The methodology presented offers a systematic and automated means of guaranteeing the reliability of blockchain systems, a critical step towards wider adoption and trust. This work focuses on the theoretical aspects of verification, providing a framework for future practical implementation and integration within blockchain development workflows. The key contributions are a detailed specification language for blockchain algorithms and a demonstrated application of model checking to uncover subtle vulnerabilities.
This paper proposes a novel decentralized verification protocol for distributed systems leveraging blockchain technology and cryptographic commitments. The core idea is to eliminate the need for a central authority by enabling components to independently verify each other's outputs through a trustless and auditable process. The system utilizes smart contracts on a blockchain to record component outputs and their corresponding commitments, establishing a verifiable record of the system's behavior. This approach offers a fundamentally new method for distributed systems security, addressing limitations inherent in traditional centralized verification models. The protocol's key components include commitment schemes, decentralized consensus mechanisms, and blockchain-based storage, all designed to ensure the integrity and authenticity of distributed system components. We outline the protocol's architecture, detailing the cryptographic operations and blockchain interactions involved. The resulting system provides a robust and scalable solution for verifying distributed systems, particularly in scenarios where trust is limited or absent.
Blockchain technology relies fundamentally on consensus mechanisms to ensure data integrity and prevent fraud. However, the inherent complexity of these mechanisms often leads to subtle vulnerabilities that can be exploited. This paper presents a novel approach to blockchain security by developing a formal specification language and accompanying verification tools. We aim to rigorously analyze and verify the security and performance of various blockchain consensus protocols, including Proof-of-Work (PoW) and Proof-of-Stake (PoS). The methodology employs mathematical modeling and logical reasoning to identify potential weaknesses and assess protocol robustness. The developed tools facilitate a systematic examination of protocol behavior under various conditions, ultimately leading to the design of more secure and reliable decentralized systems. This work offers a significant advancement in the field by providing a concrete framework for formal verification, moving beyond anecdotal evidence and subjective assessments. The core claim of this paper is that blockchain consensus mechanisms are complex and prone to vulnerabilities, and the proposed approach provides a mechanism to address this issue.
Stian Lybech, Eun-Young Kang, Riccardo Tonello, Anders Dalskov
This paper develops a model of a smart-contract language for a blockchain architecture with off-chain components. Off-chain components are pieces of smart contracts that execute at designated locations outside of the network of blockchain nodes, but remain synchronised with the on-chain contract state. They react to changes to the on-chain state, but may also notify the on-chain component about events in the world, e.g. stock prices, weather data etc., or even act as a bridge between different blockchains. This affords greater flexibility for the developer, but may also enable new vulnerabilities. As a concrete example, we use the model to study the problem of ensuring integrity and secrecy of data between the on-chain and off-chain components, using static information flow control techniques. This fails, even in the absence of a loop construct, because off-chain components act as separate threads and can encode a blocking construct e.g. through recursive method calls. We end the paper with a discussion of possible ways to remedy this situation.
A provenance-bound values model published as a public evaluator rather than deployed as a filter — why open weights defeat a filter and strengthen a referee, why the same weights bear three different relations to the model they judge, and why an evaluator that gatekeeps its own judgments has reproduced the defect it exists to correct. A values model — a model that judges conduct against a standard — is an established artifact. Guard models, safety classifiers, critic models, preference models and process reward models all instantiate the family, and the engineering is not in dispute. What is in dispute, and what this paper specifies, is the posture in which such an artifact is published, which we argue is not a deployment detail but the property that determines whether the artifact does anything at all. We identify an inversion that we believe has not been stated as a design principle. A values model deployed as a filter — sitting in a serving path, permitting or refusing — is defeated by publication of its weights, because the published artifact is precisely the oracle against which an attacker optimizes; recent optimization-based attacks against safety-classifier pipelines report attack success rates of roughly 71% where prior black-box methods achieved approximately zero. The same model published as an evaluator — emitting verdicts about systems it does not control — is strengthened by publication, because open weights are what allow a third party to reproduce and therefore to trust its verdicts. Openness is not a property with a fixed sign. Its sign is set by posture. From this we derive a second result. The independent-evaluation literature documents at length the ways in which the evaluated party's control over access corrupts evaluation: short access windows, low rate limits, evaluator dependence on the goodwill and funding of the party being evaluated. We observe that the defect is symmetric and that its mirror image has not been named. An evaluator that controls access to its own judgments holds the same kind of power, pointed the other way — it can decline to evaluate, deprioritize, or be unavailable for a party it wishes to spare or to punish. We therefore specify a non-gatekeeping constraint: the ability to obtain a judgment must not depend on the evaluator's permission, which requires that the model, the harness, and the evaluation corpus be freely runnable, and which makes any hosted endpoint a convenience rather than a channel. We specify provenance-binding as the constitutive constraint on the model's outputs: every judgment must resolve to a citation into a fixed canonical corpus, and a judgment that cannot be so resolved is withheld rather than emitted. This trades coverage for auditability deliberately, and it distinguishes the artifact from values models trained on preference data whose sources cannot be named, and from purpose-authored value-rule corpora, whose rules are written for the alignment task itself and therefore cannot serve as an independent ground truth. Finally we specify that a single such artifact bears three non-interchangeable relations to the systems it judges, selected by carrier: a gate in the publisher's own hardware, a citation requirement without veto in an autonomous successor agent, and a referee in the wider world. We state plainly that the middle case must not be implemented as the first, because a veto held by a smaller model over a more capable agent bounds that agent at the evaluator's ceiling — the weak-supervisor problem applied to the very system the arrangement exists to enable. A consequence we did not initially see, and which we regard as the most immediately actionable result in the paper: the two postures are complements rather than alternatives, and the natural first evaluation subject for a referee is a filter. A filter's characteristic failure is silent bypass; an evaluator watching its record converts that failure into a recorded one. And because safety classifiers are frequently published open-weight and emit discrete, samplable decisions, this is the one evaluation target for which the access problem does not arise at all — no cooperation, permission, or notice is required from the artifact's publisher. We do not claim to have solved scalable oversight. We claim that a narrow, citation-bound, openly published evaluator is a tractable and underoccupied position in the design space, and that its tractability comes precisely from what it refuses to do. --- Provenance. This paper is part of the THonly research corpus, dedicated to the public domain under CC0 1.0. The canonical version is at https://thonly.org/research/the-referee-not-the-governor. Its SHA-256 is 1184b0f3e5408a504c60be2d542b551df1c22facedfe18bb9a689bb50a9cc3fe, independently timestamped to the Bitcoin blockchain via OpenTimestamps and signed under RFC 3161 by three trust authorities, one of them eIDAS-qualified. AI co-authorship is disclosed. Miss Aquarius is the consistent name used for the AI collaboration across all venues.
Cyber–physical systems (CPSs) increasingly rely on complex software components whose vulnerabilities may affect both digital services and physical processes. Fuzzing is a practical technique for discovering such vulnerabilities in CPS-facing parsers, protocol handlers, and edge services. Distributed fuzzing improves throughput, but outsourcing fuzzing tasks to multiple untrusted nodes introduces privacy risks: valuable seeds, especially crash-triggering samples, may reveal vulnerability information before affected users are protected. In this paper, we propose PrivFuzz, a privacy-preserving collaborative fuzzing framework. PrivFuzz allows organizations and individuals to collaborate and receive rewards while keeping fuzzing seeds confidential and enabling controlled encrypted seed reuse among untrusted fuzzing nodes. The key idea is to combine trusted execution environments (TEEs) with blockchain-based smart contracts to support confidentiality and fair reward settlement. We give game-based definitions and reduction-style arguments for seed confidentiality, worker soundness, outsourcer atomicity, and duplicate-claim resistance under an attested execution model. We implement a PrivFuzz prototype and evaluate it on four open-source parsing targets. Separately, native AFL++ sanity checks suggest that CPS-facing industrial protocol parsers such as Modbus and OPC UA fall within the same fuzzable target domain. Demonstrating end-to-end PrivFuzz on CPS control programs is left as future work. Using PrivFuzz, we discovered nine bugs and reported them to the developers.
Abstract This manuscript per the authors addresses secure software update delivery for Internet of Things (IoT) devices. Existing IoT update mechanisms suffer from centralized trust dependency, attribute privacy leakage, and limited scalability. This manuscript proposes ZBA-SU (Zero-Knowledge Blockchain Attribute-Based Software Update), a methodology integrating zero-knowledge proof (ZKP), blockchain smart contracts, and ciphertext-policy attribute-based encryption (CP-ABE). The proposed framework achieves privacy-preserving device attribute verification via ZKP, tamper-proof atomic update delivery via blockchain, and fine-grained access control via CP-ABE. Experimental results on Raspberry Pi, ESP32, and Ethereum private chain show ZKP generation time of 1.8 seconds, attribute leakage reduction of 97%, verification within 3 seconds, and throughput improvement of 40%. Security analysis confirms resistance against attribute forgery and proof replay attacks. ZBA-SU provides effective security enhancement for IoT software updates in smart cities and industrial IoT.