As large language models (LLMs) grow in scale and are predominantly served from remote platforms, verifying faithful inference execution becomes critical (i.e., ensuring that a provider actually executes the advertised model and computational workload rather than a tampered or downsized variant). Zero-knowledge (ZK) LLM inference offers an appealing approach. It promises public verifiability and delivers per-instance guarantees of equational correctness by proving that an output is consistent with executing a public architecture under committed, private weights. Though, we show that it does not bind the effort expended to produce the output. In this paper, we formalize this overlooked effort gap and introduce the Hollow-LLM Attack, in which a dishonest provider retains the declared architecture and parameter count but embeds ghost weights whose algebraic structure collapses effective computation. These witnesses satisfy the verification circuit and yield valid proofs, even though the dishonest model owner, who serves as the prover, performs computation commensurate with a much smaller model than the declared public architecture. This creates a profitable equilibrium in which providers deliver provably correct outputs at small-model cost while overclaiming model size. Accordingly, we characterize concrete families of ghost weights that compose with standard transformer blocks and show that such hollow deployments substantially reduce serving cost with zero quality loss under the same verification circuit. These findings underscore that proof of correct inference is not proof of large-model execution and necessitate additional protections to bind correctness to verifiable computational work.
The rapid paradigm shift from passive, advisory Large Language Models (LLMs) to autonomous, agentic artificial intelligence systems has introduced critical execution risks. Traditional AI governance frameworks operate predominantly at the "evidence" layer-documenting data provenance, recording audit trails, and logging static safety evaluations. However, a structural vulnerability arises during the downstream execution phase: under operational pressure, autonomous agents can experience "authority drift," executing high-consequence actions based on stale dependencies, bypassed safety states, or invalid runtime authorities. To resolve this decoupling paradox, this paper introduces the Zero-Knowledge Kill-Switch (ZKKS), a cryptographic runtime enforcement architecture designed for Zero-Knowledge Web Servers (ZKWS). Rather than relying on post-hoc logging, ZKKS acts as a network-level, math-enforced execution barrier. By compiling safety policies into non-interactive zero-knowledge proofs (zk-SNARKs) and enforcing them via a Linear Temporal Logic (LTL) runtime state machine, the ZKWS dynamically halts downstream actions at the point of execution when a mathematical invariant or freshness threshold is violated-without decrypting or accessing the underlying private data payloads. We prove that ZKKS bounds operational failure to zero under deterministic policy constraints, bridging the critical gap between upstream integrity evidence and downstream execution control.
Since 2016, Apple has claimed that device analytics collected to improve user experience are protected by differential privacy (DP). Apple's DifferentialPrivacy framework is deployed across its operating systems and handles sensitive signals such as Safari domains, keyboard events, photo attributes, and health-related reports. Because Apple has not open-sourced its privatization algorithms, these privacy claims have been difficult to verify independently. We present a client-side audit of Apple's DP framework on macOS Sonoma 14.2 and Sequoia 15.6. We reverse engineer the shipped binaries, recover Objective-C interfaces, build runtime harnesses that execute Apple's deployed mechanisms, and test whether their outputs match the advertised privacy guarantees. Our audit covers nearly all active deployed mechanisms, including Count Median Sketch, Hadamard-CMS, randomized-response mechanisms, and Prio-style secure aggregation. We find multiple implementation bugs and misconfigurations. Every audited mechanism that relies on floating-point noise fails to meet its advertised DP or zero-knowledge proof guarantee, due to insecure samplers with known floating-point vulnerabilities. We also find secure-aggregation configurations with local DP disabled, exposing pre-aggregation records to any party with access to those logs. Overall, we find DP violations in 5 of 9 audited mechanisms, affecting 87% of data collection in macOS Sonoma and 68% in Sequoia. We also identify public leaked iPhone logs that can be decoded to recover private information, including Safari domains and keyboard emoji signals.
A framework for reusable compliance attestation in regulated industries based on cryptographic primitives, vector commitments with selective-opening proofs, re-randomisable signatures, zero-knowledge succinct non-interactive arguments of knowledge, and cryptographic accumulators with succinct non-membership proofs, composed into a protocol structure adapted to the specific structure of multidimensional compliance state. We identify five gaps that separate the generic primitives from a deployable solution for compliance attestation: multidimensional state binding, temporal freshness without correlation, revocation under reuse, cross-issuer aggregation, and verifier predicate richness. We sketch the protocol structure that addresses these gaps, analyse its security and privacy properties, and discuss applications in age verification, right-to-work assurance, and continuous-compliance monitoring. Companion preprint to UK Patent Application GB2611280.5 filed at the UK Intellectual Property Office on 14 May 2026.
This paper presents a paradigm-shifting data preservation framework that completely bypasses the von Neumann storage bottleneck and Shannon's information limits. By utilizing a deterministic Resonance Mapping algorithm, physical digital payloads are evaporated into 256-bit mathematical coordinate seeds, reducing physical storage requirements to absolute zero bytes. The protocol guarantees O(1) constant-time re-materialization and integrates NIST Post-Quantum Cryptography (PQC) alongside Fuzzy Extractor mechanisms, ensuring absolute cryptographic immunity against Shor's algorithm. This architecture fundamentally redefines Hyper-scale AI Data Centers, Semiconductor GPU memory walls, and Web3 stateless cold wallets.
Open access
2 source records
Physical Unclonable Functions (PUFs) and Hardware Security
Zero-knowledge proofs (ZKP) provide strong cryptographic guarantees allowing a prover to demonstrate knowledge of a property without revealing the underlying secret. These mechanisms are increasingly deployed in blockchain systems, digital identity infrastructures, web proofs, confidential finance, and privacy-preserving computation. However, many practical deployments rely on an often-overlooked component: the trusted acquisition and semantic extraction chain responsible for obtaining, interpreting, and transforming real-world data into proof witnesses. While proof verification may be cryptographically trustless, the acquisition process itself frequently depends on trusted runtimes, transport security, credential issuers, parsers, APIs, browser hooks, secure execution environments, or privileged software components. This paper argues that practical proof systems do not eliminate trust entirely, but frequently displace it toward increasingly complex acquisition infrastructures. We introduce the notions of Trusted Acquisition and Governed Disclosure, where programmable trust anchors and trusted governance platforms provide explicit, attestable, and policy-controlled acquisition boundaries. We further show that once such trusted acquisition layers already exist — as is often the case in industrial, enterprise, embedded, regulated, and digital identity systems — they may also provide simpler and more deployable alternatives to selected zero-knowledge constructions through governed disclosure mechanisms. The paper does not argue against zero-knowledge proofs. Instead, it proposes a complementary architectural perspective distinguishing between trustless verification and trustworthy acquisition.
Gabriela Dobrita, Simona-Vasilica Oprea, Adela Bara
Smart-contract exploits have caused billions of USD in cumulative losses, yet audits remain expensive and slow. Automated tools have emerged to close this gap, but each class has a characteristic failure mode. Static analyzers report findings that frequently fail manual triage at high rates, while large language models (LLMs) hallucinate findings that contradict the source code. Thus, we propose Chaintrix, an end-to-end auditing framework whose central architectural commitment is that every LLM-generated claim must be discharged against a deterministic structural contract representation. We introduce a Cross-Contract Interaction Model (CCIM) that parses Solidity into a structured map of function-level reads, writes, modifiers and resolved cross-contract calls. CCIM serves as the substrate against which all 12 of Chaintrix's deterministic signal engines and the parallel LLM audit pipelines operate. A staged false-positive-reduction pipeline, terminating in a Structural Verdict Engine (SVE) that applies deterministic structural checks against parsed code, filters the merged finding set, with selected high-confidence findings further validated through symbolic execution and fuzz testing. We evaluate Chaintrix on EVMbench, the smart-contract security benchmark by OpenAI, Paradigm, OtterSec. Chaintrix detects 86 of 120 high-severity vulnerabilities (71.7% recall), with 25 audits scoring 100% recall, placing Chaintrix 26 percentage points above the strongest frontier-model baseline.
Large language model (LLM) ecosystems such as Claude Code and ChatGPT increasingly rely on skills: packages of natural-language instructions and executable tools. Once in the LLM's context, skill content cannot be reliably separated from trusted instructions, and a skill's executable side can invoke privileged actions, exposing the skill supply chain to injection, tampering, and rug-pull attacks. Existing defenses are stage-bound: centralized signing, audit reports unbound from the runtime artifact, or policy engines that cannot attest to what was approved. We present SIGIL, the first framework that seals the audit-runtime gap for LLM skills. SIGIL delivers verifiable hosting through a tamper-evident, decentralized on-chain registry from which LLMs fetch skills directly. The registry admits four publication types, Transparent, Licensed, Sealed, and Committed, spanning plaintext public distribution, monetized access, custodial use, and off-chain workflows; before admission, every skill is vetted by a Decentralized Autonomous Organization (DAO) audit committee that supports pluggable auditing methods under a stake-and-slash economic model. At load time, SIGIL delivers verified loading through a skill verification protocol executed by a Skill Verification Loader (SVL) embedded as the mandatory loading path: the SVL retrieves and decrypts the skill as its type requires, verifies its integrity against the on-chain record, and enforces its permission manifest before context injection. We evaluate SIGIL on a real-world deployment against 1,023 in-the-wild skills spanning six attack types. At load time, the SVL verifies each skill's integrity against its on-chain record and enforces its approved permission manifest, completing batched verification under 86 ms. Together, these results show that LLM skills can be cryptographically bound from publication through runtime at practical cost.
Open access
3 source records
Adversarial Robustness in Machine Learning
Artificial Intelligence in Healthcare and Education
A model artifact can be verified on disk without establishing which model is computing at runtime. Trustfall Lite is an open-source command-line tool (Apache-2.0) that scans local Hugging Face and Ollama model caches, computes the SHA-256 of each artifact, and verifies the hash against a signed registry whose records are JWS-signed and verified against a published JWKS. Every artifact resolves to one of four statuses: verified, unknown_variant, not_enrolled, or pilot_available. The tool runs locally; model bytes are not transmitted, and file paths and filenames are not sent to the verification API. By default, artifact hashes may be queried against the Fall Risk API; --local-only verifies against a cached registry without network lookup. This note describes what artifact-level verification establishes, where it stops, and how it relates to the runtime structural identity measurement developed across the Fall Risk Research program. Artifact verification is necessary but not sufficient: the same SHA-256 can serve different runtimes, models can be loaded over the network without touching disk, and disk-time identity does not guarantee runtime identity. The boundary between these two evidence classes — file-level and runtime — is the subject of this note. 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).
This paper is the authoritative technical documentation of immo.quick Core version 2.1.0. It introduces and formally specifies the Deterministic Execution Proof Engine (DEPE) — the overarching orchestration layer that unifies five interlocking architectural components (Prior Admissibility Space, Exogenous Anchor Protocol, Sensor/Oracle Trust Bridge, Bi-Temporal Ledger, Machine Law Engine) into a single, unbroken, cryptographically provable execution corridor. Every transaction processed by DEPE produces an Execution Proof Artifact (EPA): a self-contained, externally verifiable, court-admissible proof object that the transaction was evaluated correctly under the rules applicable at the moment of execution. The EPA is not a log entry or a summary — it is a formal proof object that either verifies completely under the 6-step DEPE Verification Protocol, or does not verify at all. Version 2.1.0 introduces seven architectural advancements over v2.0.0: DEPE (Deterministic Execution Proof Engine): The integration layer producing a single signed EPA per transaction, cryptographically binding all five architectural layer outputs into an indivisible unit. EPA signature scheme: CRYSTALS-Dilithium-3 (NIST PQC standard). EPA generation latency: <100ms median. External verification latency: <50ms. JPO Pre-Fill Protocol: Reduces regulatory update latency for announced changes from 34ms to under 5ms by proactively compiling and staging rules upon legislative announcement, enabling millisecond-precision atomic swap at the effective date. Checker Rotation Governance (Six-Eye Principle): Formalizes a third independent checker drawn from a rotating governance pool for high-value and high-risk transactions. Rotation is deterministic (hash-based), requires no human discretion, and is itself bi-temporally logged and attested. Bypass requires simultaneous compromise of three institutionally separated hardware devices. BFT Quorum Specification: Formalizes Byzantine Fault Tolerance for the Bi-Temporal Ledger at f ≤ ⌊(n−1)/3⌋. Production configuration: n=7, f=2, quorum=5. Record commitment latency: 4ms median. Merkle replication lag: 12ms median. Deny Path Artifact (DPA): Every BLOCK decision generates a signed, immutable DPA specifying the exact gate condition, rule reference, and structural reason for rejection. Courts, regulators, and counterparties can independently verify not only that a transaction was blocked, but precisely why — with cryptographic proof. ZKP Circuit Library v2: Expanded to 47 pre-compiled, formally verified zero-knowledge proof circuits across banking/capital, AML/KYC, DORA/ICT, privacy/data, real estate, cross-border, and regulatory filing categories. All circuits use Groth16 and PLONK proving systems and are integrated directly into the Machine Law Engine compilation pipeline. Known Patterns Extension Protocol (KPEP): Enables ~70% acceleration for registered common transaction classes via formally verified proof templates, without any security reduction. Template match failure triggers automatic fallback to the full standard path. Additional v2.1.0 enhancements: ACASP Second-Order Anomaly Detection (ambiguity itself is a blocking condition); EAP dual-channel heartbeat with gap tolerance tightened from 50ms to 35ms; Offline Receipt Export for self-contained external verification without live system dependency. Central architectural guarantee (unchanged and strengthened): immo.quick Core is the only production architecture providing a complete, unbroken, cryptographically enforced provenance chain from the moment of physical real-world observation through the enforcement gate — with formally guaranteed zero false approval rate (Closed-World Assumption), formally guaranteed temporal accuracy (Bi-Temporal Ledger + BFT Quorum), and — as of v2.1.0 — a fully machine-verifiable Execution Proof Artifact for every transaction ever processed. This paper provides full formal specifications (TLA+/Z3 style), three detailed institutional case studies (DORA Art.11 ICT incident gate; cross-border real estate acquisition with §203 StGB / CLOUD Act conflict resolution; FATF Travel Rule enforcement with ZKP-selective disclosure), complete measured production performance data, and a complete attack surface analysis covering nine adversarial vectors including DEPE integration hash forgery and ACASP ambiguity injection. Supersedes: v2.0.0 (April 2026, DOI 10.5281/zenodo.19799660).
Smart contracts are a core component of blockchain-based systems, enabling decentralized applications to autonomously manage assets and enforce program logic. However, vulnerabilities in smart contracts can cause severe financial losses because of their immutability and public accessibility. As a result, analyzing common attack vectors and evaluating static detection techniques before deployment remain critical challenges in blockchain security. This thesis presents an analytical study of high-impact smart contract attack classes and evaluates the effectiveness of AST-based static detection approaches for Ethereum smart contracts. Building on the Aderyn static analysis framework, custom detectors are implemented to analyze structural code patterns that enable reentrancy attacks, authorization bypass vulnerabilities, and unsafe proxy delegation and storage collision risks. Rather than proposing new defensive mechanisms, this work systematically analyzes how known attacks arise from insecure smart contract programming practices and examines how defensive coding patterns can be identified at the source-code level through static analysis. The effectiveness of the analysis is evaluated using vulnerable smart contract implementations and corresponding exploit scenarios developed with the Foundry testing framework. Experimental results show that the implemented detectors successfully identify exploitable vulnerabilities and demonstrate a strong correspondence between attack-enabling code structures and statically detectable patterns, confirming alignment between static analysis findings and real-world attack behavior. This work demonstrates that extensible AST-based static analysis provides a practical foundation for analyzing both smart contract attacks and the defensive patterns intended to mitigate them before deployment.
Pascal Berrang, Mirco Giacobbe, Jacob Swales, Xiao Yang
We introduce a technology to formally verify that a software system satisfies a temporal specification of functional correctness, without revealing the system itself. Our method combines a deductive approach to model checking to obtain a formal certificate of correctness for the system, with zero-knowledge proofs to convince an external verifier that the system -- kept secret -- complies with its specification of correctness -- made public. We consider proof certificates represented as ranking functions, and introduce both an explicit-state and a symbolic scheme for model checking in zero knowledge. Our explicit-state scheme assumes systems represented as transition graphs. We use polynomial commitments to convince the verifier that the public proof certificates correspond to the secret transition relation. Our symbolic scheme assumes systems specified as linear guarded commands and uses piecewise-linear ranking functions. We apply Farkas' lemma to obtain a witness for the validity of the ranking function with public and secret components, and employ sigma protocols for matrix multiplication and range proofs to convince the verifier of the witness's existence. We built a prototype to demonstrate the practical efficacy of our two schemes on linear temporal logic verification examples. Our technology enables formal verification in domains where both the safety and the confidentiality of the system under analysis are critical.
Damiano Di Francesco Maesa, Francesco Donini, Paolo Mori, Laura Ricci
Non-Fungible Tokens (NFTs) are widely used nowadays for managing digital assets in many applications due to their ability to uniquely identify an asset and securely transfer and trace its ownership. Some scenarios require digital assets to be mutable, i.e., users should be allowed to update asset attributes over time, thus introducing possible security issues, since unwanted (or even malicious) updates could significantly decrease assets’ value. While various methods for NFT mutability exist, they often lack integrated, fine-grained, and on-chain enforceable authorisation models. This paper addresses this issue by considering an NFT expansion, named Non-Fungible Mutable Token (NMT), which natively supports the update of the attributes characterising each digital asset while guaranteeing a strict and fine-grained control over such updates. In fact, the NMT approach embeds an on-chain security support based on the Attribute-Based Access Control model within the NMT architecture, aimed at regulating, through access control policies enforcement, the execution of all the update operations defined on digital assets, from new token minting to ownership transfers and attribute updates.We propose a detailed architecture for NMTs and we outline the involved smart contracts structure, including the on-chain access control system. We validate our proposal by implementing it for two common use cases, wearables and digital event tickets in the metaverse, and by conducting an experimental evaluation of the deployment and execution costs. Moreover, we simulated the usage of NMTs over a given time interval to estimate the sustainability of the proposed approach over time.
Tom Sorger, Eric Cornelissen, Aman Kumar Sharma, Javier Ron · 6 authors
Software Bills of Materials (SBOMs) are increasingly mandated by regulators, yet existing sharing mechanisms impose a binary choice between full disclosure and full opacity. This exposes software suppliers to attacks that can be deduced from the SBOM only, such as the presence of a vulnerable dependency. Conversely, software consumers can be fooled by software suppliers who modify or misrepresent published SBOMs. We present zkSBOM, a privacy-preserving SBOM sharing mechanism designed to address these threats. zkSBOM uses zero-knowledge sets to cryptographically commit to the components within an SBOM. Software consumers can query for known vulnerabilities and receive a cryptographic proof confirming whether the artifact described by the SBOM is affected, without revealing any additional SBOM content. We conduct a security analysis of zkSBOM by quantifying expected leakage from inclusion and exclusion proofs. We demonstrate real-world feasibility by applying it to realistic scenarios and evaluating its operation requirements. Our evaluation demonstrates that zkSBOM is a strong, secure, and privacy-preserving mechanism for SBOM sharing, protecting software suppliers and software consumers from one another.
Rongji Huang, Yifeng Ye, Gerui Wang, Mingchao Wan · 8 authors
Due to regulatory compliance and governance management, modern (permissioned) blockchains require flexible endorsement, which allows the endorsement policy for each contract or state object to be individually defined. To enable flexible endorsement, Hyperledger Fabric employs an execute-order-validate (EOV) paradigm, in which transactions first undergo speculative execution and endorsement, and are only then ordered and validated. Meanwhile, most blockchain systems, including the platform targeted in this work (i.e., ChainMaker), still follow a conflict-free order-execute framework. We argue that the EOV paradigm still faces several limitations, notably high abort rates in high-contention workloads such as those in Decentralized Finance (DeFi). To avoid refactoring our system and better suit DeFi applications, we try to integrate flexible endorsement into the classical order-execute architecture and accordingly propose a new framework. The key challenge is to deterministically remove problematic transactions from an ordered list, while preserving censorship resistance and decentralization for the remaining ones. We instantiate this framework on top of Tendermint, a seminal Byzantine fault-tolerant (BFT) protocol adopted in our system, and thereby propose FlexTender. By elegantly embedding endorsements into consensus, FlexTender incurs no additional messaging overhead in the normal case. Empirical evaluation using an Ethereum USDT workload demonstrates that FlexTender achieves up to $10.6\times$ speedup in throughput over an EOV simulation on the same platform.
This research paper explores the critical challenge of verifiable execution integrity in modern cloud and serverless computing platforms. While services like Amazon Web Services Lambda and Google Cloud Functions provide scalable and efficient execution environments, they operate as opaque systems where users cannot verify whether their code is executed correctly or securely. The paper identifies a fundamental trust gap in current cloud architectures and presents a comprehensive threat model covering risks such as hypervisor compromise, malicious insiders, supply chain attacks, and output manipulation. It highlights how existing security certifications and auditing mechanisms fail to provide cryptographic guarantees of correctness. To address this problem, the paper proposes a novel framework called the CodeNet Integrity Layer (CIL). This system integrates multiple advanced technologies, including Trusted Execution Environments (TEEs), Zero-Knowledge Proofs (ZKPs), and blockchain-based audit mechanisms, to create a decentralized and trustless verification model. The framework ensures that computation outputs are provably linked to the correct code and inputs without relying on blind trust in the provider. The proposed solution is evaluated through experimental implementation, demonstrating that strong execution integrity can be achieved with minimal performance overhead, making it practical for real-world deployment. The research contributes to the future of secure, transparent, and trustless cloud computing, particularly for sensitive applications in finance, healthcare, and critical infrastructure.
Miguel Isabel, Enric RodrÃguez-Carbonell, Clara RodrÃguez-Núñez, Albert Rubio
Zero-knowledge proofs (ZKPs) are an emerging technology that has become the solution to efficiently provide security and privacy along with the transparency requirement of blockchains. ZKPs are usually expressed by means of arithmetic circuits and, more generally, systems of polynomial equations in a large prime field (commonly ranging from 64-bit to 256-bit values). An increasing interest to apply formal verification techniques to ensure soundness and completeness properties of ZKP protocols has shown the need of developing powerful SMT solvers able to handle such constraint systems. In this paper we consider the problem of deciding the satisfiability of existentially quantified first-order formulas defined over polynomial equations on a prime field. We present a new DPLL($T$)-based approach in which the theory solver orchestrates several modules with different trade-offs between completeness and efficiency. We have implemented the proposed techniques in a prototype that already shows better results than existing state-of-the-art tools on both benchmarks from the domain of ZKP compiler correctness and new benchmarks coming from the verification of arithmetic circuits for ZKPs. \keywords{SMT \and Finite field \and Polynomials \and Zero-Knowledge Proofs.
Canon² — Trust Layer Research Archive. In deterministic, decentralized computational frameworks, state mutations are immutable, linearly ordered, and rigidly governed by consensus constraints. Reversing or rolling back such state transitions traditionally necessitates revealing the sensitive state artifacts subject to the rollback, fundamentally destroying the cryptographic confidentiality of participant actors. I introduce the Zero-Knowledge State Reversal Protocol (ZK-SRP), a method designed to allow participating deterministic nodes to cryptographically prove the legitimacy, necessity, and validity of a state rollback without disclosing the underlying payloads of the state to any governing validator. I present a framework wherein zero-knowledge succinct non-interactive arguments (SNARKs/STARKs) are bound tightly into deterministic hashing algorithms (specifically SHA3-256) and anchored directly to the Trust Layer Certificate Fabric. In this design, execution nodes issue Reversal Envelopes that contain mathematically verifiable proofs that a specific backward transition maps cleanly onto earlier hash obligations. Through this protocol, the rollback itself becomes deterministic and universally validatable. I outline how this operates within the Lume-V wrapper ecosystem, the DAIGS master taxonomy, and the self-healing mechanisms of Type-4 Synthetic Organisms. I present what is, to my knowledge, the first deterministic privacy-preserving state reversal architecture that guarantees zero state leakage while maintaining general-purpose runtime rollbacks, ensuring that synthetic agents and multi-agent arbitration channels can effectively unspool catastrophic logic errors without breaking strict confidentiality agreements.
Auditing the semantic properties of proprietary data creates a fundamental tension: verification requires transparent access, while proprietary rights demand confidentiality. While Zero-Knowledge Proofs (ZKPs) ensure privacy, they are typically limited to precise algebraic constraints and are ill-suited for verifying qualitative, unstructured properties, such as the logic within a codebase. We propose {\em Agentic Witnessing}, a framework that moves verification from attested execution to {\em attested reasoning}. The system is composed of three agents: a Verifier (who wants to check properties of a dataset), a Prover (who owns the dataset) and an Auditor (that inspects the dataset). The Verifier is allowed to ask a limited number of simple binary true/false questions to the auditor. By isolating an LLM-based Auditor within a Trusted Execution Environment (TEE), the system enables the Verifier to query a Prover's private data via simple Boolean queries, without exposing the raw dataset. The Auditor uses the Model Context Protocol (MCP) to dynamically inspect the target dataset, producing a yes/no verdict accompanied by a cryptographic transcript: a signed hash chain binding the reasoning trace to both the original dataset and the TEE's hardware root of trust. We demonstrate this architecture by automating the artifact evaluation process for 21 peer-reviewed computer science papers with released codebases on GitHub (e.g. Does the codebase implement the system described in the paper?). We verified five high-level properties of these codebases described in the corresponding publications, treating the source code as private. Our results show that TEE-enabled agentic auditing provides a mechanism for privacy-preserving oversight, effectively decoupling qualitative verification from the need for data disclosure.
We prove three impossibility theorems establishing fundamental limits on universal AML compliance in zero-knowledge financial systems. T1 (Completeness Impossibility): no ZK compliance system achieves complete coverage of illicit transactions under rational adversarial behavior. T2 (Oracle Integrity Impossibility): no decentralized oracle network achieves integrity guarantees when state-level adversaries control oracle nodes — cryptographically valid compliance proofs can be semantically false by construction. T3 (Sovereignty Gap Impossibility): no voluntary international compliance framework achieves universal participation when sovereign defection is individually rational. These theorems are not engineering limitations addressable by better cryptography — they are structural properties of the compliance problem under adversarial conditions. Validated empirically against the Tornado Cash OFAC designation (T3) and the Lazarus Group / Ronin Bridge exploit (T2). The theorems characterize the residual attack surface that any compliance architecture must acknowledge and bound rather than claim to eliminate.
The Model State Attestation Framework (MSAF) is the theoretical foundation of the Auburn Governance Stack. It establishes the intellectual authority for why cryptographic AI attestation is necessary, defines the three-tier attestation architecture, surveys over 200 papers from 2022 through 2026 confirming that no existing system composes hardware trust, continuous model health monitoring, and supply chain provenance into a unified attestation artifact, and documents the theoretical ceilings that bound what attestation can and cannot guarantee. The framework addresses a fundamental governance paradox: organizations deploying foundation models into critical infrastructure cannot definitively demonstrate that a specific output was generated by a model version in a compliant internal state. Current governance artifacts including model cards, training logs, and static benchmarks are descriptive rather than prescriptive and fundamentally non-verifiable. MSAF composes three verification tiers into a layered architecture. The first tier provides TEE-backed platform attestation for execution environment integrity, proving the silicon is real and uncompromised. The second tier provides signed continuous metrics for training and inference health monitoring, proving the model is healthy at the moment of inference. The third tier provides selective zero-knowledge proofs for high-value inference verification, enabling verification without exposing proprietary model internals. The composed attestation artifact is mapped to specific evidence requirements across five regulatory frameworks: EU AI Act Articles 11 and 15, FDA Software as a Medical Device Pre-Determined Change Control Plans, Federal Reserve SR 11-7 ongoing monitoring requirements, US Federal Procurement mandates, and AI insurance underwriting. The framework identifies the theoretical ceilings that bound attestation: Rice's theorem establishing the undecidability of semantic properties, the Impossibility Sandwich bounding what verification can achieve between Rice's theorem and Gödel's incompleteness, and TEE physical side-channel vulnerabilities limiting hardware trust guarantees. The honest framing: MSAF provides probabilistic risk reduction and accountability infrastructure, not behavioral safety guarantees. This is analogous to financial auditing, which certifies process compliance without guaranteeing future solvency. The building blocks exist individually. MSAF is the composition that binds them into an enforceable governance architecture. This work was previously hosted on Figshare, where the author maintained a portfolio of 29 publications with minted DOIs and an established ORCID record. The author's Figshare account was disabled without prior notice, without citation of a specific terms violation, and without opportunity for review, rendering all published items and their associated DOIs inaccessible. No communication was provided before or at the time of the disable action. This deposit and associated deposits on Zenodo ensure continued public accessibility of the author's research on institutional infrastructure with appropriate permanence guarantees.
Open access
2 source records
Adversarial Robustness in Machine Learning
Security and Verification in Computing
Physical Unclonable Functions (PUFs) and Hardware Security
This paper present a complete and irreducible formal specification for the SIS-10 safety kernel. The system satisfies totality, invariance, bounded causality, schedulability, feasibility, verifiability, machine-learning safety, compositional closure, and full observability. No additional axioms are required: the specification is dimensionally complete and closed under refinement. The tool is Apache Kafka. Kafka provides an ordered, durable, replayable event log with partitioned total order, replicated storage, and deterministic offsets. We show that Kafka's log semantics satisfy the requirements for totality, observability, compositionality, verifiability, and bounded causality. The resulting system is a closed and provably safe dynamical system. Keywords: safety kernel, formal methods, SIS-10, IEC 61508, Apache Kafka, event sourcing, compositional verification, zero-knowledge proofs, dynamical systems, functional safety.
Behkish Nassirzadeh, Rui Xi, Karthik Pattabiraman, Vasisht L. Ganesh
Blockchain technologies have experienced rapid adoption across various sectors, including supply chain management, decentralized finance and cross-border payments. With this growth, however, the complexity and security risks of maintaining blockchain integrity and functionality have increased. Addressing these challenges requires a systematic and rigorous organization of knowledge in blockchain security. This paper presents a Systematization of Knowledge (SoK) study based on a structured survey of academic literature, industry reports and real-world case studies. The authors classify vulnerabilities into three layers: system-level, smart contract-level and application-level, analyzing their root causes, real-world prevalence and mitigation tradeoffs. The taxonomy encompasses blockchain-specific threats (e.g. gas-based DoS attacks, MEV) as well as vulnerabilities inherited from distributed systems and software (e.g. Sybil attacks, access control failures). The authors critically evaluate detection and mitigation techniques, including static and dynamic analysis, fuzzing, symbolic execution and formal verification, assessing their precision, recall, scalability and inherent limitations. The authors further review state-of-the-art auditing tools in terms of methodology, adoption and shortcomings. Finally, the authors discuss advanced approaches such as hybrid frameworks that combine AI with program analysis, SMT solvers, and zero-knowledge proofs, outlining how these can address current gaps in scalability, interpretability and runtime verification. Overall, this study systematizes the security landscape of blockchain technologies, synthesizes the limitations of current approaches, and identifies technically actionable future research directions toward building more robust and resilient blockchain systems.
This paper introduces ZKAP (Zero-Knowledge Audit Protocol), a cryptographic protocol in which a machine-learning inference is coupled to a zero-knowledge proof of constraint satisfaction in such a way that the output of the inference cannot be released on any observable channel unless the proof verifies. The protocol rests on two principal technical contributions: The Certified Stack — a composite object that cryptographically binds the model weights, a mandatory bit-integrity policy (integer quantisation), the inference runtime stack and the hardware configuration under a single commitment (RootHash), which is included as a public input to every proof produced by the system. Prove-before-output enforcement — a family of four embodiments (hardware output gate, trusted-execution-environment release path, silicon-level embodiment, syscall-intercepting software runtime) in which the output of the inference is physically blocked from leaving the system until the accompanying proof has verified against the Certified Stack commitment and against a constraint set signed by an external authority. Three supporting mechanisms are described: authority-signed formal constraints with a five-type taxonomy, a per-inference hash chain with external anchoring, and a three-party cryptographic separation of duties. The paper further discusses practical relaxations of the strict release semantics for real-time workloads. A soundness theorem is stated against a polynomial-time adversary controlling the operator of the inference, and regulatory implications for high-risk AI systems under Regulation (EU) 2024/1689 (Artificial Intelligence Act) are discussed. Priority declaration. The inventive mechanisms described in this paper are the subject of Bulgarian patent applications BG/P/2026/114317 (filed 30 March 2026) and PTBG202600000316742 (filed 12 April 2026). This preprint establishes the academic priority of the author, as of the date of the deposit timestamp, over the specific technical constructions described in Sections 3 and 4 of the paper. Access note. This deposit is under embargo until 31 March 2027. During the embargo, metadata (title, abstract, author, keywords, references) are publicly visible; the full text is not publicly accessible. The embargo date coincides with the Paris Convention priority deadline of the underlying Bulgarian patent application BG/P/2026/114317. The DOI assigned at deposit time serves as a timestamp for academic priority purposes, independent of the file's accessibility.