Transaction selection in parallel or DAG-based distributed ledger technologies (DLTs) is a crucial challenge that directly impacts throughput, fairness, and validator incentives. In these systems, validators independently choose transactions to include in their blocks, often relying on naive heuristics like uniform or proportional selection. This can lead to inefficient outcomes when validators prioritize their own rewards without considering collective impacts. We analyze two fee allocation mechanisms used in practice: Random Fee Allocation (RFA), where transaction fees are randomly assigned to one validator, and Collaborative Fee Sharing (CFS), where fees are distributed equally among all validators. Using a single-shot game-theoretic framework, we derive symmetric Nash equilibria (NE) for selecting transactions for both mechanisms and propose an optimization-based method to compute these equilibria. Numerical simulations demonstrate that the NE of CFS consistently achieves higher throughput and rewards compared to the NE of RFA, particularly under skewed fee distributions. Additionally, we compare these equilibrium strategies to naive benchmarks (uniform and proportional selection), showing that the proportional strategy outperforms the NE of RSA in many situations. These findings may provide actionable insights into the design of transaction selection and incentive mechanisms, enabling more robust and high-performance DAG-based DLTs.
Sulyab Thottungal Valapu, John Heidemann, Mattijs Jonker, Raffaele Sommese
DNS integrations leverage the discovery, trust, and uniqueness of the global Domain Name System with a linkage to another naming ecosystem, so the DNS name can help identify resources such as a cryptocurrency wallet or software component. While DNS ownership is verified at linkage creation, many ecosystems do not track subsequent DNS changes. The result is zombie linkages, where the DNS ownership has expired or changed, but the mapping to the linked resource persists. We define a threat model for DNS integrations, identifying five classes of attacks that leverage or exploit zombie linkages. We measure zombie occurrence across three DNS integrations -- Web PKI; ENS, a blockchain naming system; and Maven Central, a Java software repository. We show that zombies exist in every ecosystem, but at very different fractions -- zombies make up roughly 3% of TLS certificates for new domains, 24% of ENS on-chain imports, and 15% of Maven Central namespaces. We evaluate how integration design choices affect outcomes, with validate-once integrations (ENS on-chain, Maven Central) accumulating long-lasting zombies, linkages with expiration (Web PKI) limiting damage, while integrations that validate on every use (ENS gasless) are zombie-free by design. We look for specific attacks, finding attacks actively available for exploitation in both Web PKI and Maven Central. Finally, we recommend steps to reduce zombie occurrence.
Keir Finlow-Bates, Markus Jakobsson, Hossein Siadati
The transition to post-quantum cryptography in blockchain systems such as Bitcoin and Ethereum is often framed as a purely cryptographic problem. In practice, it also presents significant economic and infrastructural challenges: in globally replicated networks, increases in transaction size and verification cost are multiplied across all participating nodes. Existing post-quantum signature schemes, including lattice-based constructions such as CRYSTALS-Dilithium and stateless hash-based schemes such as SPHINCS+, introduce substantial increases in signature size. At blockchain scale, these increases translate into higher storage, bandwidth, and validation requirements, potentially requiring multiple generations of hardware improvement to become operationally routine. Historical experience suggests that even moderate increases in data footprint can be contentious, as illustrated by the Bitcoin block size debates (2015--2017). We propose a hash-based commit--reveal construction that replaces a single signature-bearing transaction with two lightweight transactions, each containing a fixed-size (32-byte) hash output derived from well-established primitives such as SHA-256, BLAKE, or Keccak. This approach achieves post-quantum security under standard hash assumptions while increasing the effective transaction footprint by only approximately 1.5$\times$ to 2$\times$ per authorization event. These results indicate that practical post-quantum migration may benefit from rethinking transaction semantics rather than directly adopting larger signature schemes, and that viable designs for decentralized systems must account for system-wide cost amplification.
Maryam Bahrani, Michael Neuder, S. Matthew Weinberg
An emerging blockchain protocol design pattern leverages the asymmetry between the computational effort in performing versus verifying tasks. For example, cryptographic validity proofs (e.g., SNARKS) require the prover to expend significant effort demonstrating the correctness of their claim, while the verifiers benefit from extremely easy validation. The operationalization of this paradigm requires efficiently soliciting the performance of expensive tasks in pseudonymous, adversarial environments. We formalize this as a mechanism design question. The protocol balances the economic cost of a liveness fault, where the work is not completed, with the payments required to incentivize specific behavior from candidate suppliers. We show that the loss of the optimal protocol scales logarithmically in the cost of a liveness fault, scaled up by the adversarial fraction of the network. Further, we find that the optimal equilibria have an intuitive structure, allowing us to provide concrete advice to practitioners. Specifically, in many regimes, the optimum designates a single, random node as the primary worker and a committee as a fallback, which is reminiscent of leader-based consensus mechanisms. We also characterize the asymptotic regimes where having negative payments (i.e., slashing in blockchain parlance) is especially helpful.
This study investigates the rapid centralization of the Ethereum builder market under the Proposer-Builder Separation (PBS) architecture. We argue that existing research, by focusing predominantly on influential order flows, lacks a comprehensive evaluation of order flow behavioral patterns and economic purposes. To address this gap, we analyze Ethereum transactions from September 2023 to August 2025 to characterize Exclusive Order Flows (EOFs) and non-atomic Maximal Extractable Value (MEV) -- the missing components corresponding to these behavioral and economic dimensions, respectively. We introduce a novel exclusivity metric based on Kullback-Leibler divergence and employ supervised learning to identify 75 EOFs and 322 non-atomic MEV flows, which account for 71\% and 23\% of trading-related builder revenue. A longitudinal analysis of builder strategies across these dimensions delineates the market's evolution into four distinct eras, revealing that while EOFs were instrumental in establishing early dominance, incumbents have since decoupled market share from immediate EOF dependency by leveraging entrenched network effects. Ultimately, we conclude that builder centralization is an emergent property of the PBS framework itself, as the architecture systematically violates the fundamental prerequisites of a competitive market.
Paul Gerhart, Jay Taylor, Sri Aravinda Krishnan Thyagarajan
Atomic swaps are a fundamental primitive for the trustless exchange of digital assets across blockchains: they guarantee that either both parties receive the agreed assets or neither party transfers. While this all-or-nothing guarantee is powerful, it also imposes an inherent determinism that rules out exchanges whose intended outcome is probabilistic. As a result, existing atomic swaps cannot realize trustless exchanges in which one party pays for a fixed chance of receiving a larger asset or reward, as in lotteries, randomized allocation mechanisms, and probabilistic cross-chain trades. We introduce probabilistic swaps, a new cryptographic primitive that extends atomic swaps to the probabilistic setting. In a probabilistic swap, one party's transfer is executed with a fixed, publicly specified probability embedded in the protocol and cannot be biased by either party. This yields a trustless mechanism for randomized exchange with verifiable odds and no trusted intermediary. Our construction combines adaptor signatures with oblivious pseudorandom functions (OPRFs) to realize the desired probabilistic outcome while ensuring that neither party can predict or bias it in advance. Along the way, we introduce a new mechanism for the atomic exchange of OPRF evaluations for payments, which may be of independent interest. A key feature of our approach is that it preserves the minimal on-chain footprint of modern atomic-swap protocols. The protocol relies only on standard Bitcoin scripts, such as digital signatures and timelocks, and is deployable on any blockchain that already supports atomic swaps. Consequently, probabilistic swaps are indistinguishable from ordinary on-chain transactions, which helps preserve privacy and fungibility. We provide formal security foundations and demonstrate practicality through a probabilistic swap in the Bitcoin testnet and in the Lightning Network.
Decentralized finance (DeFi) protocols now intermediate over USD 100 billion in value, including regulated stablecoins and tokenized assets deployed as collateral, yet no widely adopted framework operationalizes risk assessment at the rigor institutional adoption demands. Existing approaches emphasize protocol-specific parameter optimization or conceptual taxonomies without providing explainable, composability-aware, and structurally independent assessment methodologies. We propose a nine-dimension DeFi risk assessment framework extending the six-dimension taxonomy introduced by Moody's Analytics and Gauntlet with three novel dimensions: composability risk, comprehension debt, and temporal risk dynamics. We additionally introduce a transparency confidence modifier separating assessment reliability from risk severity. The framework is grounded in structural analysis of protocol dependencies conducted through an ontology-based protocol intelligence infrastructure covering more than 8,000 DeFi protocols. We retrospectively analyze 12 major DeFi-related incidents from 2024-2026 representing approximately USD 2.5 billion in direct losses. Five of the 12 incidents require at least one novel dimension for complete root-cause characterization, including the two highest-systemic-impact events in the dataset.
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
Blockchain-based IoT data sharing systems increasingly adopt a hybrid architecture in which a permissioned ledger stores tamper-evident metadata while encrypted payloads are placed in content-addressed storage. In such systems, a central security bottleneck is key access control: enforcing dynamic, multi-user authorization for releasing or using bulk-data decryption keys. Existing designs often rely on always-online RBAC or smart-contract gates that return keys to authorized users, reintroducing a trusted online policy enforcement point and weakening auditability. This paper presents a revocation-ready key management layer that replaces online key release with ciphertext key publication: the ledger records metadata of the form (CID, CK, PolicyID, epoch), where CK is a CP-ABE ciphertext encapsulating an AES-GCM key. Users retrieve CK from the ledger and decrypt locally if their attributes satisfy the policy. To support forward revocation and policy evolution without re-encrypting large files, the design introduces an epoch/time-bound attribute and a lightweight CK-rotation protocol that updates only small ciphertext keys and ledger entries. We implement a minimal end-to-end prototype using a local content-addressed store, a hash-chained ledger, and a CP-ABE backend, with the goal of isolating key-management costs rather than benchmarking production blockchain throughput. Experiments on a commodity MacBook show that CP-ABE encryption dominates store latency, with approximately 186 ms for a k=6 mixed-Boolean policy, while ledger and storage operations remain around 1-2 ms. Epoch-based revocation amortizes key update cost under churn, gateway-assisted mode reduces median client-side decryption time by more than 4x under a simulated 4x client slow-down, and ledger growth scales with the number of shared assets rather than the number of readers.
Pierre Pouliquen, Hadrien Barral, David Naccache, Thibaut Heckmann · 5 authors
ASIC cryptocurrency miners are a core component of blockchain infrastructures, directly converting computation and energy into monetary value. Despite their economic importance, their security is rarely evaluated in a structured manner. In this paper, we show that the firmware distribution ecosystem of mining devices fundamentally challenges existing trust assumptions. We introduce a scalable methodology based on the collection and static analysis of publicly distributed firmware artifacts, requiring neither device access nor runtime interaction. Applying this approach, we reconstruct and analyze 134 firmware images spanning manufacturers that account for over 99% of deployed miners (Bitmain, MicroBT, Canaan, Iceriver). Our results reveal that firmware artifacts alone are sufficient to recover internal architecture, identify security weaknesses, and reconstruct complete attack paths leading to high-impact adversarial objectives. In particular, our analysis reveals vulnerabilities that enable realistic large-scale attack scenarios, including firmware phishing and the exploitation of miners still operating over Stratum V1. Validation on two real devices confirms that publicly distributed artifacts closely reflect deployed software and that these weaknesses translate into attack capabilities. Overall, our study shows that firmware distribution mechanisms themselves constitute a primary attack surface, significantly lowering the barrier to compromise in the ASIC mining ecosystem.
Karolina Gorna, Nicolas Iooss, Yannick Seurin, Rida Khatoun · 5 authors
Zorya is a concolic execution framework that lifts compiled binaries to Ghidra's P-Code intermediate representation and uses the Z3 SMT solver to detect vulnerabilities by reasoning over both concrete and symbolic values. Previous versions supported only single-threaded TinyGo binaries. In this paper, we extend Zorya to multi-threaded binaries produced by Go's standard gc compiler. This is achieved by restoring OS thread states from gdb dumps, neutralizing runtime preemption, and introducing overlay path analysis with copy-on-write semantics to detect silent vulnerabilities on untaken branches. We rigorously assess Zorya on 11 real-world vulnerabilities from production Go projects such as Kubernetes, Go-Ethereum, and CoreDNS. Our evaluation shows that Zorya detects seven bugs at the binary level, including a silent integer overflow detects no other evaluated tool finds without a manually written oracle.
Smart contracts on blockchains are prone to diverse security vulnerabilities that can lead to significant financial losses due to their immutable nature. Existing detection approaches often lack flexibility across vulnerability types and rely heavily on manually crafted expert rules. In this paper, we present an LLM-based framework for practical smart contract vulnerability detection. We construct and release a large-scale dataset comprising 31,165 professionally annotated vulnerability instances collected from over 3,200 real-world projects across 15 major blockchain platforms. Our approach leverages precise AST-based context extraction and vulnerability-specific prompt design to instantiate customized detectors for 13 prevalent vulnerability categories. Experimental results demonstrate strong effectiveness, achieving an average positive recall of 0.92 and an average negative recall of 0.85, highlighting the potential of carefully engineered contextual prompting for scalable and high-precision smart contract security analysis.
Data valuation is a foundational task in data marketplaces, where a Shapley-value attribution determines how a buyer's payment is distributed among data providers. Typically, the marketplace operator runs this attribution alone, requiring participants and external auditors to trust scores they cannot independently recompute on the underlying private data. While zero-knowledge proofs (ZKPs) can theoretically reconcile this conflict between privacy and verifiability, existing ZK valuation systems fail to scale to real-world marketplace demands due to prohibitive proving times or the requirement to disclose validation cohorts. We present ZK-Value, a practical, end-to-end ZK data-valuation system. Our solution bridges the scalability gap through a fully co-designed architecture: (1) LSH-Shapley, a locality-based valuation primitive that replaces expensive pairwise distance metrics with per-bucket collision counts; (2) ZK-LSH-Shapley, a tailored ZKP protocol that drastically reduces witness size by encoding these counts into bucket-level histograms rather than naive per-pair tensors; and (3) structural proof-system optimizations, specifically super-oracle batching and sparsity skipping. Evaluated across 12 standard datasets, ZK-Value delivers valuation quality on par with state-of-the-art baselines (within 0.033 AUROC of exact KNN-Shapley), while generating proofs in seconds to minutes and outperforming specialized ZK baselines by 12.6x to 68.1x in proving time, with verification in under 4.6 s.
SILMARILS is built from a minimal algebraic core over $\mathbb{F}_p$ using true randomness and perfect $2$-out-of-$2$ Shamir secret sharing. The framework supports both two-party and three-party modes. In the two-party setting, SILMARILS realizes a transferable designated-verifier (TDV) signature scheme. The designated verifier can simulate accepting transcripts indistinguishable from real ones, achieving Jakobsson-Sako-Impagliazzo DV security. The verifier may publish a receipt $r$ enabling public verification, yet even with $r$, no external party can tell whether a transcript was signed or simulated. As DV signatures permit simulation, standard EUF-CMA cannot hold for the designated verifier; instead, we prove $\mathsf{EUF\text{-}CMA}^{\neg\mathsf{DV}}$ security for all non-designated verifiers in both the random oracle model (ROM) and quantum random oracle model (QROM). In the three-party mode, adopting the broadcast model of Fitzi et al., we obtain a statistically secure signature protocol with simulation-based security and error $1/p$. We analyze security in the Pure IT model, the IT+ROM, and the QROM, extending the Fitzi et al. framework to quantum adversaries with classical I/O. Correctness, secrecy, transferability, and unforgeability for non-designated parties remain equivalent to simulation-based security. Thanks to its simple algebraic structure, SILMARILS offers very compact keys and signatures for the blockchain settings we target, where standardized PQC schemes are already more than sufficient. Our goal is not to compare SILMARILS with PQC, but to highlight its suitability for lightweight TDV authentication. A fair comparison with other DV schemes is omitted due to space and the complexity of aligning models.
This paper presents InsureConnect, a blockchain-based system for improving transparency, authentication, and auditability in property-insurance workflows after natural disasters. The system combines Self-Sovereign Identity (SSI), Decentralized Identifiers (DIDs), Verifiable Credentials (VCs), satellite imagery, Hyperledger Fabric, and IPFS to register identities, insurance contracts, and damage claims. Property images are stored off-chain in IPFS, while content hashes and signed records are maintained on a permissioned blockchain. Users interact with the system through a desktop application, while chaincode enforces role-based access control and validates digital signatures. The prototype was evaluated under concurrent request loads from 50 to 3000 requests, measuring latency, throughput, and dropped connections. The results indicate that the system sustains increasing throughput under load, although latency rises and dropped connections appear at higher concurrency levels.
Smart contract vulnerabilities in Decentralized Finance caused over billions of dollars losses every year, yet the security community faces a critical bottleneck: identifying a vulnerability is not the same as proving it is exploitable. Manual PoC construction is prohibitively labor-intensive, leaving most disclosed vulnerabilities unverified and protocols exposed long before mitigation is applied. In this paper, we propose \sys, a knowledge-driven agentic system for end-to-end contract vulnerability detection and exploit synthesis. Our core insight is that exploit synthesis is not a code generation task but a \emph{structured reasoning problem} that requires grounded knowledge of protocol semantics, failure root cause, and exploit primitives. \sys organizes this knowledge into a \emph{Hierarchical Knowledge Graph} (HKG) that serves as structured memory for LLM-guided multi-hop reasoning. To validate exploit feasibility beyond code synthesis, \sys employs a two-stage validation framework that checks exploit-path reachability via SMT solving and profit realizability via asset-level state simulation, ensuring generated PoCs satisfy both logical and economic viability constraints. Evaluated on 88 real-world DeFi attacks and 72 audited projects (2,573 contracts), \sys achieves 98\% recall and 0.9 F1-score in detection, and a 96.6\% exploit success rate (ESR), reproducing 85 historical exploits and recovering over \$116.2M revenue. \sys outperforms SOTA fuzzers (\textsc{Verite}, \textsc{ItyFuzz}) by up to $5\times$ in ESR and $300\times$ in recoverable value, and the LLM-based exploit generator \textsc{A1} by $2\times$ and $8.5\times$ respectively. In bug bounty evaluation, \sys identified 16 confirmed 0-day vulnerabilities, helping secure over \$70.6M and earning \$2,900 in bounties.
ECDSA signatures form the bedrock of blockchain transaction authentication, yet their security critically depends on proper nonce generation. We uncover a critical vulnerability in the Polygon MEV ecosystem: systematic nonce reuse that enables complete private key recovery. Analyzing on-chain data reveals that searchers, driven by the need for sub-second response times in sealed-bid auctions, employ predictable nonce patterns. These patterns create linear relationships between signatures, allowing passive attackers to recover private keys using elementary algebra. We provide a compact linear-system formulation for such attacks, including the dangerous case of cross-wallet nonce collisions, and present concrete evidence of exploitable patterns on Polygon. Our findings demonstrate how protocol-induced latency pressures can lead to catastrophic cryptographic failures in production blockchain systems, where a single implementation error compromises multiple accounts simultaneously.
While public blockchains provide transparent and auditable transaction histories, they inherently compromise user privacy. Existing privacy-enhancing protocols, such as those deployed on Ethereum, typically rely on succinct zero-knowledge proofs (zk-SNARKs) to obscure the transaction graph. However, implementing comparable cryptographic guarantees on high-throughput blockchains like Algorand is challenging due to strict per-call execution budgets and the state contention introduced by global Merkle accumulators. This paper presents Obscura, a decentralized, non-custodial privacy protocol tailored for constrained smart contract environments. Obscura achieves transaction anonymity using Linkable Spontaneous Anonymous Group (LSAG) signatures over the BN254 elliptic curve, verified entirely on-chain. To overcome limitations of the Algorand Virtual Machine (AVM), we introduce a novel state model that leverages Algorand's Box Storage for $O(1)$ commitment membership checks, eliminating the need for global Merkle accumulators, and a dynamic opcode-budget expansion mechanism via pooled inner application calls. Our implementation demonstrates that signer-ambiguous privacy is practical and efficient on Algorand without relying on trusted setups or succinct proofs. Obscura provides a robust privacy layer for transparent ledgers, bridging the gap between high-throughput blockchain architectures and the dual requirements of cryptographic privacy and selective auditability.
Blockchain and decentralized finance have revolutionized the financial ecosystem while simultaneously exposing it to cryptocurrency phishing attacks. Existing phishing detection methods primarily rely on graph learning, but they face significant limitations. Static graph learning approaches fail to account for the temporal evolution of phishing patterns, while semi-dynamic methods, such as those combining static GNNs with LSTM, struggle to capture the irregular and bursty nature of blockchain transactions. Moreover, these methods overlook the diversity of Ethereum transactions, treating them as homogeneous graphs, and heavily rely on supervised learning, which requires extensive labeled data that is not readily available. These limitations reduce their adaptability to emerging phishing threats. In this paper, we present PhishEye, a fully dynamic self-supervised system that monitors on-chain transactions to detect phishing activities. PhishEye formulates Ethereum transactions as a heterogeneous temporal attributed multi-graph and incorporates a novel temporal graph contrastive learning model, which captures both temporal patterns and heterogeneous transaction types. The evaluation on a dataset of 161,658 addresses and 416,541 transactions shows that PhishEye outperforms existing methods, achieving an F1 score of 87.23% and an AUC of 98.43% for phishing transaction detection, and an F1 score of 94.19% and an AUC of 98.03% for phishing account detection. In real-world deployment from May 1, 2023 to July 31, 2024, PhishEye identified 1,803 previously unknown phishing addresses, providing early alerts that helped prevent losses exceeding 2 billion USD.
An agent skill is a configuration package that equips an LLM-driven agent with a concrete capability, such as reading email, executing shell commands, or signing blockchain transactions. Each skill is a hybrid artifact-a structured half declares executable interfaces, while a prose half dictates when and how those interfaces fire-and the prose is reinterpreted probabilistically on every invocation. Conventional static analyzers parse the structured half but ignore the prose; LLM-based tools read the prose but cannot reproducibly prove that a tainted input reaches a high-impact sink. We present Semia, a static auditor for agent skills. Semia lifts each skill into the Skill Description Language (SDL), a Datalog fact base that captures LLM-triggered actions, prose-defined conditions, and human-in-the-loop checkpoints. Synthesizing a fact base that is both structurally sound and semantically faithful to the original prose is the central challenge; we address it with Constraint-Guided Representation Synthesis (CGRS), a propose-verify-evaluate loop that refines LLM candidates until convergence. Security properties (e.g., indirect injection, secret leakage, confused deputies, unguarded sinks, etc.) over an agent skill can then be reduced to Datalog reachability queries. We evaluate Semia on 13,728 real-world skills from public marketplaces. Semia renders all of them auditable and finds that more than half carry at least one critical semantic risk. On a stratified sample of 541 expert-labeled skills, Semia achieves 97.7% recall and an F1 of 90.6%, substantially outperforming signature-based scanners and LLM baselines.
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.
Renewed attention to the identity of Bitcoin's pseudonymous creator has revived an old worry: that the roughly 1.148 million BTC mined by Satoshi and never moved represent a major tail risk for bitcoin. This paper argues that the worry is overstated. The mechanical downside of selling the position is bounded well below the feared collapse, and the outcomes most consistent with sixteen years of observed behavior are not bearish for bitcoin's effective supply. We analyze the position in two ways. First, we model the case of a purely financial holder. Multiple sale scenarios, checked against both a square-root-law estimate and the historical record of large sales, suggest that bitcoin's current market liquidity could absorb a patient multi-year sale with a cumulative price impact centered around 10 to 13 percent relative to a no-sale case. The same arithmetic also links the downside from a surprise sale to the upside from a confirmed burn: both are bounded by the same effective-supply adjustment, so the doom case and the burn-rally case cannot both be large. Second, we consider the preferences implied by the sixteen-year record. Ideological restraint, privacy, already having enough, and preserving the myth all point toward further dormancy, permanent loss of access, or a deliberate burn. A sale or an act of sabotage remains possible, but the record supports it less strongly. Under both approaches, the mechanical bear case is bounded, and the likeliest outcomes are neutral to mildly positive for bitcoin's effective supply. The argument does not rule out transient overshoot or leverage-driven amplification; it bounds the durable repricing the coins themselves can cause.
Muhammet Anil Yagiz, Fahrettin Horasan, Ahmet Hasim Yurttakal
Integrity of audit logs produced by Internet of Things (IoT) devices is a prerequisite for post-incident forensics, regulatory compliance, and operational accountability. While blockchain-backed logging infrastructures can satisfy this requirement, they introduce consensus overhead, network dependencies, and deployment complexity that are often prohibitive at the IoT edge. This paper presents a lightweight and evaluated integrity verification pipeline that combines Merkle-tree commitments with resource-aware adaptive chunking to provide tamper evidence without relying on distributed ledger technologies. The proposed pipeline operates in three stages: (i) resource-aware batch ingestion via adaptive chunk sizing, (ii) Merkle-tree construction with O(logn) inclusion proof generation, and (iii) deterministic single-entry verification against a trusted root anchor. We further report an implementation audit that identified and corrected two evaluation defects: a double-counting bug in tampering metrics and a redundant full-tree reconstruction during batch appends. Using the corrected implementation, five-run benchmarks on synthetic IoT log datasets demonstrate throughput exceeding 130,000 logs/s for 100,000 records. The system achieves per-entry verification latency of approximately 22 ms, proof generation latency of 22 ms, an average proof size of 1,006 bytes, and peak memory usage below 5 MB. Tampering detection achieves perfect precision, recall, and F1-score (1.0) across corruption ratios ranging from 1% to 50%.
FlyClient is a lightweight blockchain verification protocol that enables proof-of-work validation using minimal data, making it ideal for resource-constrained environments like mobile wallets, Internet-of-Things devices or cross-chain bridges implemented with smart contracts. Despite its strong potential for enabling lightweight blockchain verification, FlyClient protocol is still in the experimental stages, with limited real-world deployments and performance evaluations under diverse conditions. In this paper we bridge the gap between theory and deployment, by addressing several technical challenges to advance FlyClient to a production-ready solution. Namely, our contribution is three-fold: (i) we formally introduce an adversary model alternative to the original FlyClient one, that allows us to parametrize a verifier under a concrete economic interpretation, while also saving some proof space; (ii) we provide the first practical FlyClient prover implementation for a production blockchain (Zcash), and we estimate its performance under different configurations; (iii) we introduce and evaluate two optimizations that minimize the size of FlyClient proofs, the first of which does not require any consensus change.