This paper explores the application of quantum error correction (QEC) codes to enhance the security and resilience of blockchain technology. Traditional blockchains are vulnerable to attacks that exploit vulnerabilities in their distributed ledger systems. The core challenge lies in the immutable nature of the blockchain, where a single compromised node can potentially disrupt the entire network. This research proposes leveraging the powerful error-correcting capabilities of QEC codes to safeguard blockchain data. Specifically, we examine the encoding and decoding processes using various QEC codes, focusing on their ability to detect and correct errors introduced by malicious actors. The integration of QEC codes into the blockchain architecture can significantly improve its tolerance to attacks, ensuring data integrity and maintaining the trust inherent in the blockchain system. We present a framework for implementing QEC within blockchain transactions and discuss the potential performance implications. The primary goal is to demonstrate that QEC codes offer a viable path towards a more robust and secure blockchain ecosystem.
This comprehensive 500-page architectural specification details the complete deployment framework for the CATECHON Hardware Inhibitor and its associated global ecosystem. The document establishes the definitive standard for sub-nanosecond deterministic control systems and is divided into three primary operational domains: 1. Physical Integration & Hardware Protocol (The "BOX"): Exact engineering specifications for the Active Plasma Stability Controller (FPGA-Based). Includes >100 MSPS ADC interfaces, full galvanic isolation, and sub-nanosecond deterministic mitigation of Magnetohydrodynamic (MHD) instabilities (e.g., VDEs) utilizing the K_0 metric engineering approach. This section defines the physical bridge between theoretical metrics and hardware-level Zero Trust execution. 2. Theoretical Foundations & AI Containment: Extension of the hardware-level inhibition architecture to cognitive trajectories, autonomous AI containment, and quantum entropy management (including the Cybernetic Zeno Effect and ChronoSphere modeling). 3. Decentralized Autonomous Organization (DAO) & Governance: The foundational legal, financial, and operational infrastructure required for the deployment of CATECHON technology. This section outlines the smart contract architecture, token annihilation mechanics, the Balance DevHub framework, and the non-negotiable architectural veto rights designed to ensure absolute system safety and integrity. RESTRICTION NOTICE: This archive contains proprietary hardware calibration offsets, integration keys, and closed governance protocols. Public access is strictly restricted.
Rong Fu, Jia Yee Tan, Ziyu Kong, Shuning Zhang · 8 authors
Zero-knowledge circuits enable privacy-preserving and scalable systems but are difficult to implement correctly due to the tight coupling between witness computation and circuit constraints. We present zkCraft, a practical framework that combines deterministic, R1CS-aware localization with proof-bearing search to detect semantic inconsistencies. zkCraft encodes candidate constraint edits into a single Row-Vortex polynomial and replaces repeated solver queries with a Violation IOP that certifies the existence of edits together with a succinct proof. Deterministic LLM-driven mutation templates bias exploration toward edge cases while preserving auditable algebraic verification. Evaluation on real Circom code shows that proof-bearing localization detects diverse under- and over-constrained faults with low false positives and reduces costly solver interaction. Our approach bridges formal verification and automated debugging, offering a scalable path for robust ZK circuit development.
Open access
2 source records
Physical Unclonable Functions (PUFs) and Hardware Security
Custom tokens are fundamental in decentralized applications (dApps) operating on Ethereum and other Blockchain platforms. Ethereum, in particular, relies on the ERC-20 standard as a widely accepted token interface, facilitating seamless integration with numerous pre-existing dApps, user interface platforms, and popular web applications like exchange services. A notable security challenge within the ERC-20 framework is the “lost token problem”. This problem arises because users occasionally send tokens to the wrong addresses, and it has caused more than $27 million in damage. In this paper, we evaluate three existing solutions to this issue. Through the utilization of formal modeling, property specification, and the TLC model checker. Most importantly, we propose a novel double-layer solution to remedy the ERC-20 vulnerability. Our formal verification and experimental results indicate our approach encompasses the protection of the already deployed smart contracts, which is a critical aspect that has never been addressed in the existing mitigation techniques.
Open access
Security and Verification in Computing
Radiation Effects in Electronics
Physical Unclonable Functions (PUFs) and Hardware Security
Decentralized and Connected Autonomous Vehicle (CAV) networks offer promising advances in safety, efficiency, and real-time decision-making. However, they face significant challenges in authentication, privacy, and scalability—especially in the face of quantum adversaries. This paper proposes a novel post-quantum secure framework that integrates lattice-based Zero-Knowledge Proofs (ZKPs), optimized Binius proofs, and Multi-Layer Compressed Counting Bloom Filters (ML-CCBF) to enable privacy-preserving authentication and model verification in decentralized CAV environments. Our lattice-based ZKP scheme achieves cryptographic commitments in under 5μs, while Binius proofs verify model integrity in less than 0.17 seconds per update. ML-CCBF ensures scalable membership filtering with 0% false positives across 1000 nodes. Experimental results confirm 100% ZKP soundness, strong resilience against simulated quantum and adaptive attacks, and stable latency under increasing network load. These findings demonstrate that our framework delivers quantum-resilient security, real-time efficiency, and robust scalability, offering a viable solution for trustworthy decentralized intelligence in next-generation vehicular systems.
Decentralized Finance (DeFi) on Ethereum has undergone significant transformations since its emergence during the DeFi summer of 2020. With the introduction of Proof of Stake (PoS) and Proposer-Builder Separation (PBS), the transaction supply chain on Ethereum has shifted from relying entirely on the public mempool for DeFi interactions to an astonishing 80% usage of private RPCs. These private RPCs submit transactions directly to builders, skipping the public mempool, while conducting Order Flow Auctions (OFAs) to capture MEV backrun rebates and gas rebates. Our findings reveal that not all RPCs OFAs produce the same outcomes. These insights underscore the significant implications of OFA design choices on transaction efficiency and execution quality, and thus why an order flow originators should pay close attention to which OFA they use.
Zero-knowledge proof (ZKP) systems have surged attention and held a fundamental role in contemporary cryptography. Zero-knowledge succinct non-interactive argument of knowledge (zk-SNARK) protocols dominate the ZKP usage, implemented through arithmetic circuit programming paradigm. However, underconstrained or overconstrained circuits may lead to bugs. The former refers to circuits that lack the necessary constraints, resulting in unexpected solutions and causing the verifier to accept a bogus witness, and the latter refers to circuits that are constrained excessively, resulting in lacking necessary solutions and causing the verifier to accept no witness. This paper introduces a novel approach for pinpointing two distinct types of bugs in ZKP circuits. The method involves encoding the arithmetic circuit constraints to polynomial equation systems and solving them over finite fields by the computer algebra system. The classification of verification results is refined, greatly enhancing the expressive power of the system. A tool, AC4, is proposed to represent the implementation of the method. Experiments show that AC4 demonstrates a increase in the solved rate, showing a 29% improvement over Picus and CIVER, and a slight improvement over halo2-analyzer, a checker for halo2 circuits. Within a solvable range, the checking time has also exhibited noticeable improvement, demonstrating a magnitude increase compared to previous efforts.
Vladimir Kukharenko, Kirill Ziborov, Rafael Faritovich Sadykov, Ruslan Rezin
The extent of formal verification methods applied in industrial projects has always been limited. The proliferation of distributed ledger systems (DLS), also known as blockchain , is rapidly changing the situation. Since the main area of DLSs’ application is the automation of financial transactions, the properties of predictability and reliability are critical for implementing such systems. The actual behavior of the DLS is largely determined by the chosen consensus protocol, which properties require strict specification and formal verification. Formal specification and verification of the consensus protocol is necessary but not sufficient. It is also required to ensure that the software implementation of the DLS nodes complies with this protocol. Finally, the verified software implementation of the protocol must run on a fairly reliable operating system. The financial focus of DLS application has also led to the emergence of the so-called smart contracts , which are an important part of the applied implementations of specific business processes based on DLSs. Therefore, the verifiability of smart contracts is also a critical requirement for industrial DLSs. In this paper, we describe an ongoing industrial project between a large Russian airline and three universities – Innopolis University (IU), Moscow Institute of Physics and Technology (MIPT) and Lomonosov Moscow State University (MSU). The main expected project result is a DLS for more flexible refueling of aircrafts, verified at least at the four technological levels described above. After brief project overview, we focus on our experience with the formal specification and verification of HotStuff, a leader-based fault-tolerant protocol that ensures reaching distributed consensus in the presence of Byzantine processes. The formal specification of the protocol is performed in the TLA+ language and then verified with a specialized TLC tool to verify models based on TLA+ specifications.
Recent years have witnessed a boom in blockchain systems written in Rust to utilize its efficiency and safety. Unfortunately, deadlock bugs have become one of the ubiquitous banes to these systems due to the heavy use of locks for parallelism and the misunderstanding of the lock mechanism in Rust. This paper analyzed the common lock-related pitfalls in blockchain systems written in Rust and proposed Stuck-me-not, the first MIR-based static deadlock detector, for the most common deadlock type: double-lock. We have discovered 29 previously unknown double-lock bugs in 11 popular blockchain-related projects. We believe our work can greatly improve the concurrency security of the current blockchain ecosystem.