Smart contracts extended blockchain functionality beyond simple transactions, powering complex applications like decentralized finance (DeFi). However, this complexity introduces serious security challenges, including price manipulation and inflation attacks. Despite the development of various security tools, the rapid rise in financially motivated exploits continues to pose a significant threat to the blockchain ecosystem. These financially motivated exploits often stem from Monetarily Exploitable Vulnerabilities (MEVuls), which refer to vulnerabilities arising from exploitable implementations in monetary transactions or value-transfer logic. Due to their complexity, intricate chains of function calls, multifaceted logic, and diverse manifestations across different smart contracts, MEVuls are particularly challenging for current security tools to identify. Instead of providing actionable insights, existing tools frequently generate excessive warnings that overwhelm developers without effectively mitigating risks. To address the challenge of recognizing MEVuls, we first formalize MEVuls based on common real-world financial exploits. Then, we introduce FAUDITOR, a specialized fuzzer designed to detect MEVuls in smart contracts. The key insight is that leveraging smart contracts' finance-related interfaces directly exposes critical vulnerabilities, making detection more targeted. We further integrate auditors' reports using NLP to extract valuable insights on exploitation patterns, enabling a more informed search strategy. Additionally, FAUDITOR employs a self-learning mechanism that refines its detection strategies over time, allowing it to improve based on prior fuzzing results. In our evaluation, FAUDITOR impressively reveals 220 zero-day MEVuls. Meanwhile, compared to existing fuzzers, FAUDITOR detects vulnerabilities faster and achieves better instruction coverage.
Rohith Singh, Mr. Charan Singh, Abdul Rashad, Md. Abdur Rasheed · 6 authors
Prompt injection is a foundational security vulnerability in large language models (LLMs) deployed as autonomous agents with tool access and multi-step reasoning capabilities. Existing defenses rely on heuristic filters that fail under obfuscation, indirect injection, and multi-agent propagation. We present a Unified Cryptographic-Control Architecture (UCCA), a principled framework that integrates five complementary guarantees: (1) information-theoretic leakage bounds derived via Fano's inequality, (2) certified robustness via randomized smoothing, (3) token-level rejection via erase-and-check, (4) runtime trajectory enforcement via control barrier functions (CBFs), and (5) verifiable inference via zero-knowledge proofs (ZK-SNARKs). We formally prove that any successful prompt injection attack must simultaneously bypass all five mechanisms, a condition we show has probability at most δ under stated assumptions. We evaluate UCCA on three real LLMs (GPT-4o, Claude 3.5 Sonnet, Mistral-7B) across four established attack benchmarks (INJECAGENT, TensorTrust, PromptBench, HarmBench), achieving attack success rates below 8% while maintaining median latency overhead under 340 ms. Our framework bridges formal security guarantees and deployable system architecture, establishing a foundation for provably secure autonomous AI. • Information-theoretic bounds on system prompt leakage using mutual information and Fano's inequality. • Certified robustness for safety-critical classification through randomized smoothing, where the robustness radius R is determined from output probability gaps. • Token-level rejection guarantees using an erase-and-check procedure capable of detecting adversarial subsets of size ≤ k. • Runtime safety enforcement through control barrier functions (CBFs), ensuring LLM outputs remain within a verified safe set. • Verifiable inference using ZK-SNARKs, allowing cryptographic attestation of model outputs without revealing model weights. • UCCA, a deployable system integrating all five mechanisms, evaluated on real LLMs and standard benchmarks.
Cross-chain bridges are critical for decentralized finance (DeFi) to enable asset interoperability across heterogeneous blockchains. They are based on a complex hybrid architecture that involves on-chain contracts and off-chain relayers. In the recent past, several major attacks exploited vulnerabilities in cross-chain bridges. However, existing analysis tools have limited detection effectiveness as they focus on individual contracts and do not capture the complex interaction chain in cross-chain bridges. In this paper, we present BridgeFuzz, the first fuzzing framework for cross-chain bridge developers capable of detecting vulnerabilities such as balance mismatches, protocol errors, and off-chain denial-of-service bugs. BridgeFuzz is the first step towards bridging the gap between smart contract vulnerability research and the holistic vulnerability analysis of cross-chain bridges.
Permission control vulnerabilities in Non-fungible token (NFT) contracts can result in significant financial losses, as attackers may exploit these weaknesses to gain unauthorized access or circumvent critical permission checks. In this paper, we propose NFTDELTA, a framework that leverages static analysis and multi-view learning to detect permission control vulnerabilities in NFT contracts. Specifically, we extract comprehensive function Control Flow Graph (CFG) information via two views: sequence features (representing execution paths) and graph features (capturing structural control flow). These two views are then integrated to create a unified code representation. We also define three specific categories of permission control vulnerabilities and employ a custom detector to identify defects through multi-view feature similarity analysis. Our evaluation of 795 popular NFT collections identified 241 confirmed permission control vulnerabilities, comprising 214 cases of Bypass Auth Reentrancy, 15 of Weak Auth Validation, and 12 of Loose Permission Management. Manual verification demonstrates the detector's high reliability, achieving an average precision of 97.92% and an F1-score of 81.09%. Furthermore, NFTDELTA demonstrates enhanced efficiency and scalability, proving its effectiveness in securing NFT ecosystems.
Smart contracts are a critical component of blockchain systems. Due to the large amount of digital assets carried by smart contracts, their security is of critical importance. Although numerous tools have been developed for detecting smart contract vulnerability, their effectiveness remains limited, particularly due to the high false positives included in the reported results. Therefore, developers and auditors are often overwhelmed with manually verifying the reported issues. A fundamental reason behind this is that while a reported vulnerability satisfies specific vulnerable patterns, it may not actually be exploitable, either because the vulnerable code cannot be triggered or it does not result in any financial loss. In this paper, we propose V2E, a new framework for validating whether a reported vulnerability is truly exploitable. The core idea of V2E is to automatically generate executable Proof-of-Concept Exploit (PoC for short), and then assess if the vulnerability could be triggered and incur any real damage (i.e., causing financial loss) by the PoC. While LLMs have shown proficiency in PoC generation, achieving our task is by no means trivial. In detail, it is difficult for LLM to: (1) generate and update PoC to trigger a specific vulnerability, (2) evaluate the PoC’s effectiveness to validate exploitable vulnerability. To this end, V2E automates the whole process through a novel combination of PoC generation, validation, and refinement: (1) Firstly, V2E generates targeted PoCs by analyzing potential vulnerability paths. (2) Then, V2E verifies the validity of PoCs through triggerability and profitability analysis. (3) In addition, V2E iteratively refines the generated PoC based on PoC execution feedback, therefore, increasing the chance to confirm the vulnerability. Evaluation on 264 manually labeled contracts shows that V2E outperforms the baseline approach. Particularly, V2E successfully identifies 102 out of 124 exploitable vulnerabilities, achieving a precision of 91.9% and a recall of 82.3%. In addition, it successfully eliminates 71 out of 140 false alarms (50.7%). Besides, V2E effectively enhances the performance of SOTA tools. It reduces the false positive rates of Slither by 76.9%, Mythril by 56.9% and Confuzzius by 65%.
Massimo Bartoletti, Angelo Ferrando, E. Lipparini, Vadim Malvone
Smart contracts deployed on blockchains such as Ethereum routinely manage large amounts of assets, making their security critical. Empirical studies show that real-world attacks often exploit flaws in the business logic of contracts that unfold across multiple transactions, such as liquidity or front-running attacks. Detecting these attacks requires reasoning about expressive temporal properties beyond the capabilities of existing analysis tools. In this paper, we present an automated approach to the formal verification of smart contracts, enabling the specification and verification of complex temporal properties. Our approach provides a fully automated encoding into Lustre -- the specification language supported by the Kind 2 model checker -- of an expressive subset of Solidity contracts and temporal specifications based on first-order Hennessy-Milner Logic. This encoding allows us to leverage Kind 2 to determine whether the contract respects the specification or not. We implement our approach in a toolchain that integrates the translation and verification steps, and we evaluate its effectiveness and performance on a benchmark of smart contracts and temporal properties capturing complex attack scenarios. Our results show that the proposed approach can effectively verify non-trivial temporal properties of smart contracts and detect violations that are beyond the reach of existing analysis tools.
With the help of pact technology, a program that has been developed, the smart contract can take place between two or more entities without any third-party actor. Although smart contracts provide transparency and efficiency, security flaws in smart contracts have resulted in costly attacks, including re-entrancy, integer overflows, and access control violations. Current tools for intelligent contract verification, such as Mythril, Oyente, and Securify, mainly apply symbolic execution, taint analysis, and pattern matching to identify vulnerabilities. However, these tools have many false positives, take a lot of time to execute, and don't scale efficiently with large numbers of contracts. In this context, the paper presents VeriChain. This formal verification framework combines Control Flow Graph (CFG) analysis, symbolic execution, and static analysis to improve vulnerability detection and tackle the challenges above. VeriChain systematically constructs the contract’s Control Flow Graph (CFG), explores CFG execution paths with symbolic execution, and employs a set of rules for performing rule-based static analysis that can uncover vulnerabilities. Using CFG-based dependency tracking, VeriChain achieves enhanced analysis of dependencies among functions and coverage of execution paths, thereby reducing the number of false positives while achieving accurate detection results. The experimental results show that VeriChain obtains 98.3% detection accuracy, higher than Mythril, Oyente, and Securify. Compared to existing tools, VeriChain has a much lower false-positive rate (1 false alarm) and a much faster execution time (Running in only 2.3 seconds). This framework gives a structured security assessment by categorizing the vulnerabilities according to severity and execution traces, ensuring that the smart contracts are accessed under heavy security verification pre-deployment. With its ability to accomplish highly accurate results efficiently whilst providing structured ways to report on security, VeriChain will be an influential component in delivering safe, innovative contract launches to decentralized applications for blockchain developers and security analysts.
WebAssembly linear memory is an untyped byte array shared across module boundaries. When independently compiled modules — potentially from different source languages — read and write the same memory regions, no existing type system covers the cross-module interface. We present typed-wasm, a type system that applies a 12-level progressive type safety framework, originally developed for database query languages, to Wasm linear memory. The system treats contiguous memory segments as typed region schemas and load/store operations as typed projections verified against those schemas at compile time. We formalise the system in Idris 2 using Quantitative Type Theory (QTT), providing proofs of bounds safety, aliasing freedom, effect purity, lifetime validity, linearity, cost boundedness, and epistemic freshness — all erased before code generation, yielding zero runtime overhead. Our principal contribution is multi-module schema agreement: a static verification that independently compiled Wasm modules agree on the layout, types, alignment, and invariants of shared memory regions — a property that no source-level type system, and no existing Wasm proposal, can express. We further extend the framework with two novel levels: tropical cost-tracking (Level 11), which proves that memory access patterns have bounded cost via a min-plus semiring, and epistemic safety (Level 12), which prevents modules from acting on stale knowledge of shared state.
Decentralized applications (DApps) represent a paradigm shift in software architecture, leveraging blockchain technology and distributed consensus mechanisms to eliminate single points of failure and centralized control. As the adoption of DApps accelerates across sectors such as finance, supply chain, healthcare, and governance, ensuring their functional correctness and behavioral reliability has become a critical engineering challenge. Unlike traditional software, DApps operate in adversarial, permissionless environments where smart contracts execute autonomously and immutably on distributed nodes, making post-deployment correction extremely costly or impossible. This review systematically examines the landscape of functional testing methodologies tailored for decentralized applications, analyzing their suitability, limitations, and practical applicability in modern DApp development workflows. We survey research spanning smart contract verification, consensus protocol testing, oracle interaction validation, cross-chain interoperability testing, and user-layer functional testing of Web3 interfaces. The review identifies four dominant testing paradigms: (1) unit testing of smart contract functions, (2) integration testing of DApp components, (3) property-based testing using formal specifications, and (4) end-to-end simulation on testnets. Through comparative analysis across 13 seminal studies, we evaluate each approach along dimensions of automation feasibility, coverage depth, gas efficiency awareness, and scalability to complex DApp ecosystems. Our findings indicate that while static analysis and symbolic execution tools such as Mythril, Slither, and Manticore offer strong vulnerability detection, they address security properties more than functional correctness. Conversely, framework-based testing tools like Hardhat, Truffle, and Foundry provide adequate unit-level coverage but struggle with cross-contract orchestration and event-driven logic verification. A critical gap exists in testing oracle-dependent and DAO governance workflows. This review concludes with a synthesis of best practices, open research challenges, and a directional roadmap for developing holistic functional testing frameworks suited to the evolving complexity of decentralized systems.
Money laundering enables malicious actors to integrate illegal profits into the legitimate economy and has long been a central concern in financial regulation. Blockchain systems introduce new channels for laundering through decentralized, pseudonymous, and cross-border asset transfers. In this context, blockchain exploiters often rely on laundering to conceal fund origins and enable cash-out.
Insider threats pose a persistent and evolving challenge to contemporary software ecosystems, where privileged users can exploit access for malicious purposes, often evading traditional perimeter-based defences. This paper introduces a novel hybrid framework that synergistically integrates zero-knowledge proofs (ZKPs) and behavioural analytics to detect and mitigate such threats with enhanced privacy and precision. ZKPs enable secure authentication and data verification without revealing sensitive information, ensuring compliance with privacy regulations like GDPR while thwarting unauthorized access. Complementarily, our behavioural analytics engine employs advanced machine learning models, including graph neural networks and unsupervised anomaly detection (e.g., isolation forests), to profile user behaviours across software pipelines, identifying deviations indicative of insider malice. The proposed architecture is deployed in a microservices-based ecosystem, demonstrating scalability via containerized components on Kubernetes. Extensive evaluations on benchmark datasets (e.g., CERT Insider Threat) and simulated enterprise environments yield a 95% detection accuracy, with 40% fewer false positives than state-of-the-art methods like UEBA systems. Latency remains under 50ms for real-time operations, preserving performance in high-throughput scenarios. Our framework outperforms baselines by 25% in F1-score, validated through rigorous ablation studies. By bridging cryptographic privacy with AI-driven intelligence, this work advances proactive security for modern software, offering deployable solutions against sophisticated insiders. Future extensions explore quantum-resistant ZKPs for post-quantum resilience.
Fine-tuning is the dominant paradigm for adapting large machine learning models, yet current deployment pipelines provide no way to verify how a released model was updated. In particular, a model provider or auditor cannot check whether a fine-tuned model adheres to a claimed update procedure without access to its parameters. We introduce \emph{fine-tuning integrity} (FTI), a cryptographic objective for verifying that a deployed model differs from a trusted base model only within a declared class of admissible updates. We construct \emph{succinct model difference proofs} (SMDPs), zero-knowledge protocols that certify structured parameter drift without revealing model weights. Our framework supports three fundamental update classes: norm-bounded, low-rank, and sparse drift, covering common fine-tuning methods such as regularized training, LoRA, and prefix tuning. In all cases, proof size and verification cost depend on the structure of the update rather than the number of parameters. We prove soundness, zero-knowledge, and succinctness for each construction, and establish a matching $Ω(n)$ lower bound showing that structural assumptions are necessary for succinct verification. A prototype evaluation on synthetic benchmarks and GPT-2 fine-tuning demonstrates that proofs remain compact and verification is efficient at realistic scales.
A zero-knowledge proximity proof certifies geometric nearness but carries no commitment to an application context. In stateful geo-content systems, where drops can share coordinates, policies evolve, and content has persistent identity, this gap can permit proof transfer between application objects unless extra operational invariants are maintained. We present a systems-security analysis of this deployment problem: a taxonomy of context-binding vulnerabilities, a formal off-circuit verification model for a transcript-adversary that holds a recorded proof but cannot obtain fresh coordinates, an assumption comparison across five binding strategy classes, and a concrete instantiation, Zairn-ZKP, that embeds drop identity, policy version, and session context as public circuit inputs. Compared with a strong off-circuit alternative based on stored-digest server checking, in-proof binding reduces operational invariants from four to two and adds no measurable proving cost relative to the sound geo-only baseline (-0.12 ms median in our setup). It also removes a correctness pitfall we identify empirically: a plausible off-circuit implementation that omits one server-side check remains vulnerable to cross-drop transfer. Measurements across six network conditions, seven venues in four countries, and an epoch-window simulation indicate that same-epoch transfer is realistic in dense urban deployments unless per-request nonces are maintained. Across five platforms and seven binding strategies, the results support a deployable methodology for reducing assumption surfaces in stateful ZK-backed verification workflows.
Java applications are prone to vulnerabilities stemming from the insecure use of security-sensitive APIs, such as file operations enabling path traversal or deserialization routines allowing remote code execution. These sink APIs encode critical information for vulnerability discovery: the program-specific constraints required to reach them and the exploitation conditions necessary to trigger security flaws. Despite this, existing fuzzers largely overlook such vulnerability-specific knowledge, limiting their effectiveness. We present GONDAR, a sink-centric fuzzing framework that systematically leverages sink API semantics for targeted vulnerability discovery. GONDAR first identifies reachable and exploitable sink call sites through CWE-specific scanning combined with LLM-assisted static filtering. It then deploys two specialized agents that work collaboratively with a coverage-guided fuzzer: an exploration agent generates inputs to reach target call sites by iteratively solving path constraints, while an exploitation agent synthesizes proof-of-concept exploits by reasoning about and satisfying vulnerability-triggering conditions. The agents and fuzzer continuously exchange seeds and runtime feedback, complementing each other. We evaluated GONDAR on real-world Java benchmarks, where it discovers four times more vulnerabilities than Jazzer, the state-of-the-art Java fuzzer. Notably, an earlier GONDAR version contributed to Team Atlanta's first-place CRS in the DARPA AI Cyber Challenge, and is integrated into OSS-CRS, a sandbox project in The Linux Foundation's OpenSSF, to analyze open-source Java projects, where it has already uncovered a zero-day vulnerability.
Smart contracts have become a cornerstone of modern blockchain ecosystems by enabling decentralized, transparent, and autonomous execution of digital agreements. Despite their widespread adoption, smart contracts continue to suffer from two persistent challenges: inefficient execution and critical security vulnerabilities. These limitations not only increase operational costs but also undermine trust in blockchain-based systems. This research paper presents a comprehensive and plagiarism-free investigation into smart contract optimization with a strong emphasis on security-driven design principles. The study analyzes execution inefficiencies, gas consumption patterns, and architectural constraints across major blockchain platforms, alongside prevalent vulnerabilities such as reentrancy attacks, integer overflows, access control flaws, and logic inconsistencies. Building upon this analysis, the paper proposes an integrated optimization–security framework that combines code-level optimization, modular design, formal verification, automated vulnerability detection, and hybrid on-chain/off-chain computation models. The proposed approach demonstrates how efficiency and security can be jointly enhanced rather than treated as isolated objectives. The findings aim to guide developers, researchers, and practitioners in designing smart contracts that are cost-effective, secure, and resilient within rapidly evolving blockchain environments.
We present HyperVerITAS, a new zero-knowledge proof (ZKP) system for image provenance that enables scalable, efficient, and privacy-preserving verification of image transformations. HyperVerITAS builds upon the same minimal trust model as VerITAS (IEEE S&P '25), requiring trust only in the image source device, while treating the editing software as untrusted. Unlike VerITAS, which relies on FFT-intensive SNARKs and suffers from high memory overhead (up to 120 GB), HyperVerITAS leverages multilinear polynomial encodings over the Boolean hypercube to dramatically reduce both proving time and memory usage. Our design cleanly separates signature verification from image transformation, supports modular integration of multiple polynomial commitment schemes (including post-quantum constructions) and naturally extends to a wide range of affine image transformations. We implement HyperVerITAS with two distinct commitment schemes (Brakedown and multilinear KZG) and evaluate it on full-system pipelines involving cropping and grayscaling. On commodity hardware (Apple M3, 36 GB RAM), HyperVerITAS generates proofs for 33 MP images using only 27 GB of RAM and 6.6 minutes of proving time, whereas VerITAS fails to scale beyond 4 MP. These results establish HyperVerITAS as a practical and scalable ZKP system for secure and efficient image provenance.
Traditional digital card games rely on centralized servers, introducing catastrophic single points of failure, while decentralized Web3 alternatives fail to achieve real-time viability due to prohibitive block latency. This paper introduces Panoptes, an optimized, hybrid cryptographic engine that enforces low-latency decentralized consensus for peer-to-peer state channels. Assuming a highly hostile user-space environment, Panoptes treats the host application space and its underlying managed runtime as fundamentally compromised.A bifurcated architecture is detailed utilizing a hardened native airgap and direct OS-level memory mapping to process ciphertexts, bypassing standard and predictable libc allocators. To mitigate automated memory scrapers and frustrate asynchronous Direct Memory Access (DMA) attacks, Panoptes implements a multiplexed decoy memory topology (The Vault). This architecture relies on strict virtual page guarding, offline decryption, and temporal starvation via millisecond-scale execution windows. The protocol replaces commutative encryption with a deterministic Hand Commitment Payload, utilizing X25519 KEM, XOR- based Secret Sharing, and ChaCha20-Poly1305 to enforce Strict Zero-Trust Consensus.
Traditional digital card games rely on centralized servers, introducing catastrophic single points of failure, while decentralized Web3 alternatives fail to achieve real-time viability due to prohibitive block latency. This paper introduces Panoptes, a highly optimized, hybrid Zero-Trust cryptographic engine that enforces microsecond-latency decentralized consensus for the CoronaPoker peer-to-peer network. Assuming a strict Ring-0 adversary model, Panoptes treats the host operating system and the Java Virtual Machine (JVM) as fundamentally compromised. We detail a bifurcated architecture utilizing a hardened native airgap that leverages OS-level stealth allocators to process ciphertexts without leaving plaintext residue in the managed heap. To mitigate OS-level memory scrapers and hardware-based Direct Memory Access (DMA) attacks, Panoptes implements a multiplexed decoy memory topology (The Vault). It is secured by strict virtual page guarding against software introspection, and heavily relies on offline decryption with immediate sub-millisecond zeroization to temporally starve asynchronous hardware-level carving. The protocol entirely replaces traditional commutative encryption with the deterministic Hand Commitment Megapacket, a flat-buffer payload leveraging X25519 KEM, Additive Secret Sharing, and ChaCha20-Poly1305 to ensure Byzantine fault tolerance without majority voting. We present formal implementations of our micro-architectural defenses, including Mixed Boolean-Arithmetic (MBA) for constant-time execution, direct cross-platform syscalls bypassing libc, OS-level DACL lockdowns, PEB cloaking, and asynchronous SipHash-2-4 binary attestation. Furthermore, we introduce a multithreaded Deadman Switch to detect CPU cycle drift via RDTSC. Evaluated under an exhaustive 42-point "Total Siege" adversarial framework, the engine demonstrates unparalleled resilience against hardware breakpoints, kernel introspection, inline hooking, and temporal drift attacks.
Three model substitution scenarios were executed against a live inference endpoint with real HTTP requests, signed attestation JWTs, and OPA policy enforcement. In each scenario, every tested workload, artifact, or API identity control relevant to that scenario — workload JWT validation, health checks, gateway process continuity, artifact manifest integrity, API key authentication — remained valid while the model changed. In each scenario, a structural identity measurement based on activation geometry during a standard forward pass detected the substitution and the enforcement layer denied the request. Three substitutions were tested and three were detected, with zero false accepts in this run. The warm-path verification latency was 5.7–6.7 seconds on a single A100 with the model already loaded. The complete evidence chain — before/after measurement results, attestation claim summaries, OPA policy evaluations, and HTTP response codes — is published alongside this note as machine-readable JSON. This is a technical note, not a numbered entry in the research series. Supplementary Material. This note is accompanied by three machine-readable evidence files: cat3_results.json (structured results for all three scenarios, including the full before/after evidence chain for Scenario A with signed attestation claims, OPA policy evaluations, and HTTP response codes), manifest_authorized.json (SHA-256 build manifest for the enrolled model, 10 files, all verified), and manifest_substituted.json (SHA-256 build manifest for the substituted model, 10 files, all verified). All three files are available for download as supplementary files attached to this record. The Neural Network Identity Series — Mathematical foundations, empirical validation, and governance frameworks for verifying which model is running Newest addition: Technical Note: The Disappearing Window — AI Logprob Access Withdrawal and the Structural Verifiability of Frontier Model Contracts (DOI: 10.5281/zenodo.20362098) Paper 1: The δ-Gene: Inference-Time Physical Unclonable Functions from Architecture-Invariant Output Geometry (DOI: 10.5281/zenodo.18704275) Paper 2: Template-Based Endpoint Verification via Logprob Order-Statistic Geometry (DOI: 10.5281/zenodo.18776711) Paper 3: The Geometry of Model Theft: Distillation Forensics, Adversarial Erasure, and the Illusion of Spoofing (DOI: 10.5281/zenodo.18818608) Paper 4: Provenance Generalization and Verification Scaling for Neural Network Forensics (DOI: 10.5281/zenodo.18872071) Paper 5: Beneath the Character: The Structural Identity of Neural Networks — Mathematical Evidence for a Non-Narrative Layer of AI Identity (DOI: 10.5281/zenodo.18907292) Paper 6: Which Model Is Running?: Structural Identity as a Prerequisite for Trustworthy Zero-Knowledge Machine Learning (DOI: 10.5281/zenodo.19008116) Paper 7: The Deformation Laws of Neural Identity (DOI: 10.5281/zenodo.19055966) Paper 8: What Counts as Proof? — Admissible Evidence for Neural Network Identity Claims (DOI: 10.5281/zenodo.19058540) Paper 9: Composable Model Identity — Formal Hardening of Structural Attestations in the Enterprise Identity Stack (DOI: 10.5281/zenodo.19099911) Paper 10:Where Identity Comes From: Path Sensitivity and Endpoint Underdetermination in Neural Network Training (DOI: 10.5281/zenodo.19118807) Paper 11: Post-Hoc Disclosure Is Not Runtime Proof: Model Identity at Frontier Scale (DOI: 10.5281/zenodo.19216634) Paper 12: Family-Dependent Response to Reasoning Distillation Across Structural and Functional Identity Layers (DOI: 10.5281/zenodo.19298857) Paper 13: Safety-Alignment Removal as a Model-Identity Failure — Structural Evidence from Published Weight-Level Mutation Checkpoints (DOI: 10.5281/zenodo.19383019) Technical Note: Agent Identity Is Not Model Identity (DOI: 10.5281/zenodo.19240883) Technical Note: Gap Invariance: Why PPP Measurements Are Domain-Independent by Construction (DOI: 10.5281/zenodo.19275524) Technical Note: Measured Model Substitution Under Valid Agent Credentials (DOI: 10.5281/zenodo.19342848) Technical Note: Artifact Identity Is Not Runtime Identity — Trustfall Lite and the Boundary of File-Level Model Verification (DOI: 10.5281/zenodo.20019127) Formal Verification Stack for Neural Network Structural Identity (IT-PUF Coq Proofs) (DOI: 10.5281/zenodo.18930621) Copyright (c) 2026 Anthony Ray Coslett / Fall Risk AI, LLC. All Rights Reserved. Confidential and Proprietary. Patent Pending (Applications 63/982,893, 63/990,487, 63/996,680, 64/003,244).
Contemporary cryptographic execution systems-particularly those employing zero-knowledge proofs-provide strong guarantees that a computation satisfies a given arithmetic circuit. However, satisfying a circuit is not equivalent to executing correctly with respect to the intended semantics of the system being proven. This paper identifies and formalizes the semantic gap: the class of failures in which execution is provably valid under a proof system yet provably invalid under the system's formal specification. We present the Verifiable Semantic Execution Layer (VSEL), a layered architecture that binds formal specification, execution, constraint derivation, proof generation, and verification into a single semantically coherent pipeline. VSEL models systems as deterministic labeled transition systems, defines explicit semantic mappings between concrete and formal artifacts, derives constraints mechanically from a semantic intermediate representation, and requires that every accepted proof attest not merely to constraint satisfaction but to membership in the formal language of valid execution traces. We define the proof obligations, invariant system, and refinement chain required for end-to-end semantic correctness; characterize the adversarial model including specification manipulation, underconstraint exploitation, and compositional failure; and establish the conditions under which composition of independently correct systems preserves global correctness. The architecture integrates hybrid post-quantum cryptography to ensure long-term validity of proofs and commitments, and introduces a formal economic invariant layer that elevates economic semantics from informal domain knowledge to enforceable first-class predicates over states and execution traces. We provide a complete formal treatment of the system model, semantic preservation theorems, constraint soundness and completeness conditions, witness uniqueness requirements, economic admissibility conditions, and the assume-guarantee framework for safe composition.
Open access
2 source records
Cryptographic Implementations and Security
Physical Unclonable Functions (PUFs) and Hardware Security
Cross-chain bridges represent one of the most critical yet vulnerable components of blockchain infrastructure, with over $2.5 billion lost to bridge exploits between 2022-2023 alone. MERIDIAN LINK introduces an architecture combining Light Protocol's ZK Compression on Solana with GrotH16 zero-knowledge proofs for verification on EVM chains, reducing trust assumptions compared to signature-based bridges while acknowledging explicit trade-offs. Key Properties: Cost reduction: 95%+ savings on Solana storage via compressed accounts (~15,000vs ~1,600,000 lamports per deposit record) Verification: GroTH16 proofs (~100-bit security on BN254) replace multisig attes-tation for withdrawal authorization Latency: ~20-25 seconds end-to-end (competitive with intent-based bridges) Replay protection: Poseidon-based nullifiers with on-chain tracking Explicit Limitations: Throughput: ~12-20 withdrawals per minute per direction (sequential IMT updates) EVM costs: Withdrawal verification costs ~$4-6 at 30 gwei, dominating total transfer cost Trust assumptions: GroTH16 trusted setup, Light Protocol implementation, Photon indexer availability, relayer liveness The protocol shifts the trust model from "honest majority of signers" to "cryptographic soundness plus infrastructure liveness." A compromised relayer cannot forge proofs or double-spend, but can censor transactions or extract MEV through reordering.
The integrity of distributed healthcare databases is continuously threatened by unauthorized modifications, hardware faults, software vulnerabilities, and increasingly sophisticated cyberattacks. Traditional relational and NoSQL database systems rely on centralized access-control mechanisms and periodic audit logs that cannot provide cryptographic proof of unaltered history or real-time anomaly detection. This paper presents ChainGuard, a novel middleware framework that integrates Ethereum-based smart contracts, a network of IoT integrity-sensing nodes, and an AI-powered anomaly classifier to provide end-to-end, tamper-evident integrity assurance for distributed healthcare information systems. ChainGuard records SHA-256 hash digests of critical database state snapshots onto a permissioned Ethereum ledger, while a constellation of lightweight IoT agents embedded at database server nodes continuously monitors system-level indicators—I/O throughput, memory bus activity, and cryptographic nonce validation—at ten-second intervals. Deviations from baseline behavior trigger smart-contract-enforced quarantine procedures that freeze suspect transactions and emit verifiable incident records onto the immutable ledger. A Random Forest classifier trained on 12,000 synthetic database-event logs achieves 96.4% accuracy in discriminating legitimate bulk insertions from covert data-tampering attempts. Evaluation across three clinical deployment scenarios demonstrates that ChainGuard reduces mean time to tamper detection from 47 minutes (baseline centralized audit) to 38 seconds, with a false-positive rate of 1.7%. The framework is deployable on existing PostgreSQL and MongoDB infrastructure without schema modification, making it an immediately practicable path toward regulatory compliance with HIPAA, GDPR, and the forthcoming NIS2 Directive.
EN — This paper introduces proof-object dissociation as an architectural principle for certification systems. In the major families of existing approaches reviewed here — including trusted timestamping, zero-knowledge proofs, token-based certification models, public key infrastructures, commitment schemes, and proof-of-existence mechanisms — the proof remains structurally tied to the object, secret, or entity whose validity is being established. This paper argues that such coupling should be understood as a dominant architectural convention rather than as a logical necessity. EN — Under proof-object dissociation, a certification reference structure may be generated, preserved, and anchored independently of any future certified object. Certification is then achieved through a controlled activation mechanism that associates an already valid reference structure with a specific object, user, or context. At the architectural level, this shift makes possible a set of properties that are difficult or unavailable in coupled models: pre-certification independent of the future object, deferred activation, mutation or transfer of activation rights without regeneration of the reference layer, and validation without disclosure of confidential source elements. EN — The paper positions this proposal relative to existing certification architectures, outlines a general implementation-agnostic framework, and identifies a further operational capability termed the Blind Pre-Certification Layer (BPCL). FR — Cet article introduit la dissociation preuve-objet comme principe architectural pour les systèmes de certification. Dans les principales familles d'approches existantes examinées ici — notamment l'horodatage de confiance, les preuves à divulgation nulle, les modèles de certification fondés sur des jetons, les infrastructures à clé publique, les schémas d'engagement et les mécanismes de preuve d'existence — la preuve demeure structurellement liée à l'objet, au secret ou à l'entité dont la validité est établie. L'article soutient que ce couplage doit être compris comme une convention architecturale dominante plutôt que comme une nécessité logique. FR — Sous dissociation preuve-objet, une structure de référence de certification peut être générée, conservée et ancrée indépendamment de tout objet futur certifié. La certification est ensuite réalisée par un mécanisme d'activation contrôlée qui associe une structure de référence déjà valide à un objet, un utilisateur ou un contexte spécifique. Au niveau architectural, ce déplacement rend possible un ensemble de propriétés difficiles à obtenir ou absentes dans les modèles couplés : pré-certification indépendante de l'objet futur, activation différée, mutation ou transfert des droits d'activation sans régénération de la couche de référence, et validation sans divulgation des éléments confidentiels sources. FR — L'article situe cette proposition par rapport aux architectures existantes de certification, présente un cadre général agnostique quant à l'implémentation, et identifie une capacité opérationnelle supplémentaire nommée Couche de Pré-Certification Aveugle (BPCL).