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.
Roadside edge infrastructure is becoming an active execution layer in connected transportation. Roadside units, edge servers, and vehicular gateways not only relay safety messages, but also run local services and support traffic-control decisions. Once these nodes are compromised, data authentication, blockchain logging, or forensic evidence management cannot by itself guarantee service trustworthiness, because the node that senses, signs, forwards, or processes the information may already be running an unauthorized software stack. This paper presents RISE-CT, a runtime-integrity assurance and self-healing recovery framework for roadside edge infrastructure. RISE-CT models each node through a layered security-state graph covering hardware roots, boot chains, firmware images, runtime processes, key usage, and service status. It combines boot-time, periodic, and event-triggered attestation with runtime drift diagnosis to detect firmware deviation, process injection, abnormal key access, replayed evidence, and service-behavior changes. When the risk score exceeds policy thresholds, a risk-aware admission state machine moves the affected node into degraded, quarantined, or recovering states, and coordinates service migration, key renewal, firmware rollback, and re-attestation before safe re-admission. Seed-controlled emulation under firmware tampering, malicious OTA updates, runtime injection, key misuse, replayed attestation, and roadside-service hijacking shows that, under the evaluated emulation settings, RISE-CT reduces the representative detection delay to 0.98 s and service interruption to 0.82 s, while achieving a 0.94 re-admission success rate with controlled attestation overhead. The results suggest that runtime node integrity can provide a potential security mechanism for improving the trustworthiness of roadside infrastructure under the evaluated conditions.
This paper proposes a Non-Fungible Token (NFT) soft pairing framework for Bluetooth service access control. Unlike conventional Bluetooth systems where pairing implicitly grants persistent service access, the proposed approach decouples native Bluetooth pairing from authorization without modifying the underlying protocol stack. The framework introduces a three-layer architecture consisting of a Bluetooth layer for connectivity, a blockchain layer for trusted execution and on-chain state verification, and an application layer where NFT soft pairing defines the authorization logic. In this design, Non-Fungible Bluetooth Tokens (NFBTs) represent user-side access credentials, while Non-Fungible Device Tokens (NFDTs) represent device identities. Their bidirectional on-chain binding forms a revocable and verifiable NFT soft pairing relationship. During access, users prove ownership of valid NFBTs through challenge-response signatures, and devices verify the corresponding on-chain state before granting service access. A prototype implemented with MetaMask and Ethereum demonstrates secure authentication, dynamic revocation, acceptable latency, and gas-efficient credential issuance based on ERC1155.
With the transparency of the Ethereum platform, deployed smart contracts remain permanently public, exposing their virtual machine code to risks such as reverse engineering, control-flow analysis and malicious behavior identification. Although several obfuscation approaches for the EVM have been proposed, existing solutions often suffer from limited resistance against advanced analysis techniques, insufficient structural transformation capability or excessive execution overhead. In this work, we propose a novel obfuscation framework for EVM bytecode that enhances security by combining semantic-aware transformations with control-flow perturbation techniques. The proposed framework significantly increases structural complexity, hinders Control Flow Graph (CFG) recovery and alters discriminative virtual machine code characteristics while preserving the semantic correctness of smart contracts. Experimental results demonstrate that the proposed framework achieves a 100% obfuscation success rate with an average cyclomatic complexity of 90.80. Across all 15 evaluated transformation combinations, the framework introduces an overall mean virtual machine code size increase of 15.99% and a mean gas overhead of 7.04%. Notably, the complete multi-layer pipeline (T1+T2+T3+T4) exhibits overheads of 29.73% for virtual machine code size and 12.58% for gas, which remain acceptable considering the achieved robust resistance against reverse engineering and automated static analysis.
Open access
Advanced Malware Detection Techniques
Security and Verification in Computing
Physical Unclonable Functions (PUFs) and Hardware Security
Decentralized finance failures frequently arise not from a single obviously unsafe function, but from valid operations composed into an invalid state transition. Static analyzers and vulnerability checklists remain valuable, yet they often stop before answering the question that determines real risk: can an adversary control the preconditions, sequence, capital, ordering, and external dependencies required to turn a defect into impact? This working paper presents the Invariant-to-Exploit (I2E) framework, a practitioner-oriented method for connecting architecture assumptions to executable invariants, stateful counterexamples, exploitability evidence, and remediation regression tests. I2E consists of six linked activities: system scoping, invariant-ledger construction, adversarial controllability analysis, stateful sequence generation, exploitability tracing, and fix validation. The framework is applied retrospectively to three publicly documented incidents: KyberSwap Elastic, Euler, and the Curve sDOLA LlamaLend market. These analyses do not claim prospective vulnerability discovery; instead, they demonstrate the test signals that reviewers can derive from public root-cause information. The principal contribution is a reproducible audit worksheet that preserves the chain from protocol assumption to broken property, realistic exploitability, observable impact, and regression-tested remediation. The method is designed to remain usable by independent security researchers who cannot publish confidential client evidence. A benchmark design is proposed for future controlled comparison against checklist-only security review.
IoT sensor deployments increasingly export measurement streams to edge gateways and content-addressed storage such as IPFS, but access control decisions must be enforced without disclosing sensor owner policies, requester attributes, or stale data versions. Existing blockchain, CP-ABE, and zero-knowledge approaches reduce parts of this leakage, yet they can still expose public policy structure, accept stale Merkle proofs after sensor stream updates, overload provers when policies grow, or leave IPFS gateways vulnerable to bandwidth abuse. This paper proposes zk-Guard-R, a policy-hidden and replay-safe zk-SNARK access control framework for privacy-preserving IoT sensor data sharing. zk-Guard-R replaces public sparse policy matrices with MiMC-Merkle policy commitments verified inside the proof, separates long-lived logical sensor policy roots from frequently updated physical IPFS data roots, binds every proof to an on-chain nonce, and decouples attribute possession from policy interpretation through a bounded stack-based policy interpreter. Numeric sensor-access predicates are represented through committed values and range check gadgets, while an off-chain verification gateway couples accepted proofs with payment channel vouchers before releasing encrypted IPFS chunks. The design contribution is separated from the measured prototype: the full protocol specifies a bounded policy interpreter, whereas the present gnark prototype evaluates the core committed policy, committed attribute, range check, data root, nonce, Solidity verifier, and gateway-metering mechanisms. We implement a gnark BN254/Groth16 research prototype and benchmark it against a matrix-public zk-Guard prototype, a blockchain ABAC baseline, an IoT token/HMAC baseline, and a CP-ABE-style cryptographic-work proxy. For 128 attributes, the zk-Guard-R prototype with MiMC-Merkle commitments uses 425,574 R1CS constraints, generates proofs in 3.12 s, verifies in 0.73 ms, and uses 641 MB peak Go heap allocation. A three-run repeat of the 128-attribute configuration gives a proof-generation mean of 2.80 s with a 0.54 s standard deviation on the same local host, illustrating the runtime variability of prover measurements. We also deploy the generated Solidity verifier on a local Anvil EVM and measure 241,942 gas for a successful verification transaction, and we evaluate a local Kubo/IPFS gateway under valid, replayed, and voucher-limited flood requests. The results show that zk-Guard-R shifts substantial but measurable work to the prover while improving policy confidentiality, freshness, and gateway metering for IPFS-backed IoT sensor data sharing.
Multi-cloud adoption has widened the enterprise attack surface to a degree that perimeter-based defence can no longer address. Traffic is now flowing continuously across AWS, Azure, and GCP, and the majority of deployed Zero Trust Architecture (ZTA) systems are still using static rule tables, with no ability to provide an audit trail of the reasoning behind decisions, and with logs stored in datastores that can be modified by an insider without detection. This paper proposes ZT-ChainGuard, a framework that overcomes these three limitations in one architecture that integrates an ensemble machine learning trust-scoring engine, ZTA policy enforcement and a blockchain-based audit trail. The trust-scoring engine is a two-layer stacking ensemble, with XGBoost and Random Forest as base learners, and Logistic Regression as a meta-learner, and it returns a continuous trust score, P(Attack | flow), for each network flow, which is then used to trigger the ZT policy decision at a threshold of 0.5. The explanation of each decision is provided by SHAP values at both the global and per-flow level, and each decision is stored as an immutable, SHA-256 hash-chained block. On CICIDS2017 (2.83 million flows, 14 attack classes) the framework achieves 99.90% accuracy, 99.71% F1-score, and 99.99% ROC-AUC; on ToN-IoT (2.23 million IoT records, 9 attack types) it achieves 99.81% accuracy, 99.88% F1-score, and 100% ROC-AUC. The latency of inferences is 0.006ms per sample, and the overhead of auditing the blockchain is 0.019ms per block. This performance is not just a quirk of a particular split, as it is shown to be stable across the three folds of three-fold cross validation.
Abstract—As Autonomous AI Agents transition from conversational prototypes to enterprise-grade execution agents, currentsecurity architectures face a fundamental breakdown. Enterprise deployment demands unequivocal answers to six core trust questions: Principal (who does the agent represent?), Authorization (what is it allowed to do?), Tool/Action Bound (which API calls are safe?), Policy Gate (how are high-risk actions controlled?), Audit Log (how are actions traced immutably?), and Expiry/Revocation (how is authorization revoked instantly?). Existing enterprise solutions address at best one or two boundaries: IAM frameworks resolve identity but fail at granular tool execution; prompt guardrails handle basic content filtering but lack real-time authorization or cryptographic auditability; SIEM platforms store logs post-hoc without real-time interception capabilities. This paper introduces DROS-6P, a unified, deterministic runtime governance kernel designed to enforce all six fundamental trust boundaries within a single C-ABI and eBPF in-band execution layer. To prevent the security control plane from becoming a throughput bottleneck or a single point of failure under high-frequency system calls (Syscalls) generated by enterprise, third-party, or malicious agents—thereby mitigating self-induced Denial-of-Service (DDoS) degradation—runtime governance requires microsecondlevel evaluation capability. Empirical benchmark evaluations demonstrate that the DROS-6P in-band kernel achieves an average decision latency of approximately 26.1 μs. Specifically, DROS-6P enforces: (1) Principal via 3-tier PKI-signed DROS Identity Tokens (DIT); (2) Authorization via Capability Bitmaps mapping roles to deterministic execution vectors; (3) Tool/Action Bound via in-band C-ABI interceptors at the FFI boundary; (4) Policy Gate via dynamic data redaction, Human-In-The-Loop (HITL) suspension, and ZKP-Lite zero-knowledge proofs; (5) Audit Log via tamper-evident SHA-256 Merkle Hash Chains and Ed25519 signatures; and (6) Expiry/Revocation via O(1) Read-Copy-Update (RCU) atomic pointer swaps providing instant HTTP 403 enforcement. We validate DROS-6P across six heterogeneous domain tracks (Carbon DPP, Fintech AML, HIPAA Healthcare, Government Proxy Services, Inclusive Migrant Finance, and RBA Supply Chain Compliance), providing a fully reproducible testbed with 100% automated test assertions passed (0.004s), demonstrating that unified physical-layer governance is necessary and sufficient for safe enterprise AI agent deployment.Abstract—隨著自主AI Agent(自主智能體)從對話式原型走向企業級執行場景,傳統資安架構正面臨根本性的崩潰。企業部署AI Agent 時,必須對六大核心信任問題給出明確答案:Principal(Agent 代表誰?)、Authorization(被授權做什麼?)、Tool/Action Bound(哪些API 呼叫安全?)、Policy Gate(高風險動作如何控制?)、Audit Log(行動如何不可篡改地追溯?)以及Expiry/Revocation(授權何時失效且如何即時停止?)。然而,現有的企業安全處方最多只能回應一至兩個邊界:IAM 系統解決了身份認證,卻對動態Tool 呼叫束手無策;Prompt 防火牆(Guardrails)僅能處理文字層提示,缺乏執行期動態授權與密碼學稽核能力;SIEM 平台僅提供事後日誌紀錄,缺乏帶內即時攔截與防衛能力。本論文提出DROS-6P ——旨在單一C-ABI與 eBPF 帶內執行層中,同時強制執行這六大信任邊界之確定性執行期治理微內核。為確保安全控制面本身不會在企業內部、外部或惡意Agent 產生高頻系統呼叫(Syscalls)時成為效能瓶頸或單點故障點,進而防範自我引發的服務阻斷(Self-induced DDoS)與系統衰退,執行期治理必須具備「微秒級(μs)」的評估能力。實證基準測試顯示,DROS-6P 帶內微內核在測試環境中達到約26.1 μs 的平均決策延遲。具體而言,DROS-6P 強制執行:(1) Principal:透過3 階PKI 簽章之DROS 身份標籤(DIT);(2) Authorization:透過將角色精確映射至執行向量的確定性Capability Bitmaps;(3) Tool/Action Bound:透過FFI 邊界處的帶內C-ABI 攔截器;(4) Policy Gate:透過動態資料遮蔽(Redaction)、人工懸停審查(HITL) 與ZKP-Lite 零知識證明;(5) Audit Log:透過不可篡改的SHA-256 Merkle 雜湊鏈與Ed25519 數位簽章;以及(6) Expiry/Revocation:透過Read-Copy-Update (RCU) 原子指針交換實現O(1) 常數時間動態撤銷與秒級HTTP 403 阻斷。我們提供完全可重現的本地測試環境(test_verification_suite.py),100% 通過自動化斷言測試(耗時0.004s),並在六個異質產業賽道中驗證了DROS-6P,證明統合物理層治理是企業安全部署AI Agent 的充要條件。