Order fairness in distributed ledgers refers to properties that relate the order in which transactions are sent or received to the order in which they are eventually finalized, i.e., totally ordered. The study of such properties is relatively new and has been especially stimulated by the rise of Maximal Extractable Value (MEV) attacks in blockchain environments. Indeed, in many classical blockchain protocols, leaders are responsible for selecting the transactions to be included in blocks, which creates a clear vulnerability and opportunity for transaction order manipulation. Unlike blockchains, DAG-based ledgers allow participants in the network to independently propose blocks, which are then arranged as vertices of a directed acyclic graph. Interestingly, leaders in DAG-based ledgers are elected only after the fact, once transactions are already part of the graph, to determine their total order. In other words, transactions are not chosen by single leaders; instead, they are collectively validated by the nodes, and leaders are only elected to establish an ordering. This approach intuitively reduces the risk of transaction manipulation and enhances fairness. In this paper, we aim to quantify the capability of DAG-based ledgers to achieve order fairness. To this end, we define new variants of order fairness adapted to DAG-based ledgers and evaluate the impact of an adversary capable of compromising a limited number of nodes (below the one-third threshold) to reorder transactions. We analyze how often our order fairness properties are violated under different network conditions and parameterizations of the DAG algorithm, depending on the adversary's power. Our study shows that DAG-based ledgers are still vulnerable to reordering attacks, as an adversary can coordinate a minority of Byzantine nodes to manipulate the DAG's structure.
The popularity of smart contracts has cemented their place in the Blockchain Ecosystem.This is because of the immense number of use cases smart contracts provide.They have become the go-to solution for improving transparency and security for all parties involved in the transaction.Furthermore, a smart contract is immutable after it is deployed.Thus optimization of the smart contract is very important before deployment.Sol-Repairer is a tool that provides the implementation for identifying dead code segments from solidity-written smart contracts and then repairing them.Extensive experiments show that Sol-Repairer optimizes dead code better than the solidity compiler.The study also demonstrates that optimizing dead code reduces gas consumption significantly for smart contracts. CCS Conceptsā¢ Software and its engineering ā Software testing and debugging.
We present the design and implementation of a fourth-year undergraduate computer science elective course on cryptocurrency. The course introduces the basics of cryptocurrencies and blockchains using Bitcoin. Programming distributed applications for blockchains is explored using Ethereum via the Solidity programming language. Advanced theoretical concepts are discussed, using different cryptocurrencies to demonstrate how they are implemented in practice. Cryptocurrency applications are presented, along with a responsible examination of present-day cryptocurrency scams. The assignments build upon each other, with the students implementing a web-based blockchain application by the end of the semester. The course was well received, and student feedback was positive. All of the course materials are available online under public copyright licenses.
Bo Gao, Yuan Wang, Qingsong Wei, Yong Liu Ā· 6 authors
Decentralized finance (DeFi) applications depend on accurate price oracles to ensure secure and fair transactions. However, poorly integrated oracles remain susceptible to manipulation, enabling attackers to exploit smart contract logic for unfair asset valuation and financial gain. While many such vulnerabilities are only detected after deployment, smart contracts are typically immutable once deployed, making post-hoc fixes costly or infeasible. This highlights the critical need for detecting oracle manipulation risks before deployment. In this paper, we propose$AiRacleX$, a novel LLM-driven framework that enables pre-deployment detection of price oracle manipulation vulnerabilities by leveraging the complementary strengths of multiple large language models (LLMs). Our approach begins with domain-specific knowledge extraction, where an LLM model synthesizes precise insights about price oracle vulnerabilities, eliminating the need for profound expertise from developers or auditors. This knowledge forms the foundation for a second LLM model to generate structured, context-aware Chain-of-Thought prompts, which guide a third LLM model in accurately identifying manipulation patterns in smart contracts. We evaluate$AiRacleX$on 60 known vulnerabilities from 44 real-world DeFi exploits and Code4rena projects spanning 2021-2023. The results show that$AiRacleX$achieves a 2.58 times improvement in recall over the state-of-the-art GPTScan, with comparable precision. Our framework also demonstrates strong extensibility and efficiency, and supports deployment with open-source LLMs to enhance security and reduce operational cost.
The trading of data is becoming increasingly important as it holds substantial value. A blockchain-based data marketplace can provide a secure and transparent platform for data exchange. To facilitate this, developing a fair data exchange protocol for digital goods has garnered considerable attention in recent decades. The Zero Knowledge Contingent Payment (ZKCP) protocol enables trustless fair exchanges with the aid of blockchain and zero-knowledge proofs. However, applying this protocol in a practical data marketplace is not trivial. In this paper, several potential attacks are identified when applying the ZKCP protocol in a practical public data marketplace. To address these issues, we propose SmartZKCP, an enhanced solution that offers improved security measures and increased performance. The protocol is formalized to ensure fairness and secure against potential attacks. Moreover, SmartZKCP offers efficiency optimizations and minimized communication costs. Evaluation results show that SmartZKCP is both practical and efficient, making it applicable in a data exchange marketplace.
Blockchain systems, such as Bitcoin and Ethereum, have evolved into essential platforms for a variety of applications. Smart contracts are small computer programs that represent a fundamental component of these systems, enabling self-executing tasks ranging from simple operations to complex workflows, all without the need for intermediaries. On Ethereum, smart contracts are permanently stored on-chain, making them immutable and transparent. However, these features also expose them to potential attacks if vulnerabilities exist in their code. To address this concern, the present thesis conducts a security analysis of real-world smart contracts to assess the vulnerability landscape of the Ethereum blockchain over a ten-year period from 2016 to 2025. This analysis leverages an Ethereum archive node, providing access to the full historical state of the blockchain. Using a custom-built vulnerability scanner in combination with established bytecode analysis tools such as Mythril and Oyente, the study focuses on a historical assessment of smart contract security. The system was designed to automatically retrieve bytecode from deployed contracts in a structured manner, perform static analysis, and classify detected issues based on vulnerability categories. The results were processed and visualised in a front-end web application, enabling clear interpretation of the findings. The analysis reveals that vulnerabilities in smart contracts were widespread during Ethereum's early years. In particular, reentrancy issues, call-related issues, and transaction issues were the most prevalent vulnerability categories, while the remaining categories were only detected sporadically. In contrast, the prevalence of such vulnerabilities has significantly declined in recent years, indicating substantial improvements in the overall security posture of Ethereum smart contracts.
Smart contracts are self-executing programs on the blockchain, representing the core of Decentralized Finance (DeFi). They can carry billions of dollars, making their correctness and security essential. However, like any other software application, smart contracts may contain vulnerabilities that can be exploited by malicious adversaries ā a concern that is further exacerbated by their immutability and transparent nature. Fuzzing is a widely adopted automated testing approach for assessing and ensuring smart contract quality. Although powerful, its effectiveness heavily depends on the quality of the initial inputs, also referred to as seeds. This thesis identifies a key limitation in traditional smart contract fuzzers, such as Echidna, which often rely on randomly generated seeds. It investigates how these fuzzers can be improved in exploring deep contract states, reaching hard-to-trigger conditional paths, and increasing the number of executed instructions by providing higher-quality initial seeds. This thesis proposes AutumnEchidna, a smart contract pre-processing tool that leverages static analysis to generate optimized initial seeds for fuzzing. The methodology involves generating transaction sequences based on state dependencies and producing arguments through constraint solving, aiming to guide execution toward critical contract states. Experiments are conducted on two datasets: a Motivation Dataset and a Maze Dataset, designed to simulate complex input constraints and deep state transitions. Performance is evaluated based on instruction coverage and execution time under consistent configurations for both baseline Echidna (with random seeds) and AutumnEchidna (with optimized seeds). The experiment results show that AutumnEchidna improves instruction coverage by 1.26% on the aggregated Motivation Dataset and by 4.45% on the aggregated Maze Dataset. Additionally, it also reduces the execution time to achieve comparable or higher coverage. These findings demonstrate that optimized seed generation can enhance both the effectiveness and efficiency of smart contract fuzzing. This thesis concludes that incorporating static analysis to generate high-quality initial seeds is a promising approach for enhancing the performance of fuzzing strategies.
This talk given at the 2025 MDIC CM&S Summit on "Credible Models in the AI Age" traces the evolution of trust mechanisms in computational systems, from traditional model validation approaches in mechanistic modeling to emerging cryptographic verification methods for AI. We'll explore how the credibility challenge for regulators has transformed as we've moved from deterministic simulations to probabilistic AI systems, and examine how cryptographic proofs, zero-knowledge techniques, and verifiable computation are creating new pathways for establishing trust in AI outputs. By understanding this historical progression, we can better appreciate both the continuity and fundamental shifts in how we ensure reliability in our computational approaches.
Computer programs control vital infrastructure, safeguard national security, and process all financialtransactions, making their correctness and security paramount. Formal verification is a key tool for program trust and assurance. However, as the complexity of computer systems grows, the complexity of their properties does as well. While traditional verification has focused on proving safety, the same techniques do not extend to other properties of interest, such as liveness, correct execution, and cryptographic properties, like zero-knowledge security. While these properties are valuable in cloud computing, where execution is outsourced to untrusted third-party providers, they remain understudied. This dissertation presents new languages, proof systems, and techniques targeting the verifica-tion of programs and their executions. Domain-specific languages (DSLs) are key in this effort. By restricting program syntax to a mathematically well-understood subset, we prove important proper- ties. This dissertation introduces four new languages and proof systems: Ticl, a structural temporal logic for modularly proving complex liveness specifications for infinite, nondeterministic programs; Reef, a system for verifiable regular expression matching that keeps matched text confidential; Otti, a framework for proving correct execution of optimization problems like machine learning training; and Zippel, a language for implementing and automatically verifying properties of non-interactive zero-knowledge protocols. Each one of those works shows that, by carefully designing languages and proof systems for specificdomains, we can have both expressive languages, and practical verification of complex properties which were previously difficult, or impossible to prove. We demonstrate this through case studies in distributed systems, secure computation, and cryptographic protocols.
Certified computer systems are becoming the key in the increasingly complex decision making activities of our modern society. Among others, error-free and secure solutions are indispensable within AI, Autonomous Systems, Big Data, Blockchain, Decentralized Finance (DeFi), or Cloud Computing. While the explosion in applications of computer systems leads to great increases in productivity, wealth, and convenience, it creates a paradoxical situation: we rely on computer systems despite that uncountable many scenarios showcase that computer systems are not (properly) certified and hence are error-prone. The area of automated reasoning provides computer-aided solutions to prove that computer systems are error-free, just like we prove theorems in mathematics. However, who can tell software developers which automated reasoning solutions should be used? Moreover, which reasoning method is best to be used during code review, for ensuring system safety and security? This talk will reflect on some challenges of automated reasoning and focus on concrete applications of system verification security. We will highlight aspects of open-source code development, allowing others to easily use our solutions in their technologies without the need of becoming experts in automated reasoning.
Eclipse attack is a major threat to the blockchain network layer, wherein an attacker isolates a target node by monopolizing all its connections, cutting it off from the rest of the network.Despite the attack's demonstrated effectiveness in Bitcoin (Usenix'15, SP'20, Usenix'21, CCS'21, SP'23) and partially in Ethereum (NDSS'23, SP'23), its applicability to a wider range of blockchain systems remains uncertain.In this paper, we investigate eclipse attacks against Monero, a blockchain system known for its strong anonymity and pioneering the use of Dandelion++ (the state-of-the-art blockchain network layer protocol for transaction privacy protection).Our analysis of Monero's connection management mechanism reveals that existing eclipse attacks are surprisingly ineffective against Monero.We accordingly introduce the first practical eclipse attack against Monero by proposing a connection reset approach, which forces the target node to drop all benign connections and reconnect with malicious nodes.Specifically, we outline two methods for executing such an attack.The first one exploits the private transaction mechanisms, while the second method leverages the differences in propagation between stem transactions and fluff transactions under Dandelion++.Our attack is not only applicable to Monero but to all blockchain systems utilizing Dandelion++ and similar connection management strategies.We conduct experiments on the Monero mainnet.Evaluation results confirm the feasibility of our attack.Unlike existing eclipse attacks, our connection reset-based approach does not require restarting the target node, significantly accelerating the attack process and making it more controllable.We also provide countermeasures to mitigate the proposed eclipse attack while minimizing the impact on Monero.In addition, we have ethically reported our investigation to Monero official team.
The implementation of Industrial Internet of Things (IIoT) is significantly constrained by the emergence of Data security. This paper examines the primary data security issues and protection mechanisms associated with IIoT, providing a comprehensive analysis of how security protection systems evolve across the stages of data collection, transmission, storage, and processing. The focus is directed towards advancements in edge computing and lightweight distributed ledger technologies, which significantly enhance data security. The paper begins with a review of the evolution and development of IIoT, highlighting the challenges that current technologies present in effectively addressing data privacy, integrity, real-time performance, and scalability. Following this, the analysis focuses on the efficacy of edge computing to mitigate data exposure while simultaneously improving computational efficiency. Additionally, the study examines the benefits of lightweight distributed ledger technologies for resource-constrained environments, highlighting their role in ensuring data immutability and enhancing data transparency. The paper concludes by analyzing potential trends in IIoT data security technologies, such as post-quantum cryptography, AI-driven security protections, and zero-trust architectures, and by offering perspectives on the future of technological advancements.
Microservices commonly rely on bearer tokens such as JSON Web Tokens (JWTs). Although fast, these tokens reveal user claims to every service and can be reused if stolen. This thesis designs and evaluates a privacy-preserving alternative based on zero-knowledge proofs (ZKPs) that verifies each request under a zero-trust model without disclosing identity attributes. The authentication prototype service is built with two implementations (TypeScript/NestJS and Rust) and compared with a JWT baseline in privacy, access control correctness, and performance. Across six concurrency levels (1, 10, 15, 20, 25, 30) over 15-second runs, CPU and memory usage were sampled every 250 ms, and means were reported across the concurrency points. The workflow achieves zero attribute disclosure while keeping verification practical: verification adds 1.8 ms per microservice hop with a native Rust verifier and ā¼130 ms with a NestJS verifier. Proof generation is the main computational cost (ā¼0.7s in NestJS; ā¼1.4s in Rust), with NestJS demonstrating superior performance due to efficient WASM witness generation and reuse of artefacts. These measurements were taken on the same host with an otherwise idle machine to control variance. Formal statistical significance would require multiple independent repetitions; the present analysis reports central tendencies and observed stability. Contributions are: (i) a working ZKP-based authentication workflow suitable for microservices, (ii) a dual-stack prototype and comparative evaluation against JWT, and (iii) evidence that privacy can be improved without prohibitive verification overhead.
This thesis explores the concept of zero-knowledge proofs and their application in zkVMs - virtual machines capable of generating proofs of correct computation without revealing private input. We begin by introducing fundamental cryptographic tools such as zk-SNARKs and zk-STARKs, along with supporting techniques such as lookup tables. We then analyze the architecture of two concrete zkVM implementations: RISC Zero and SP1. We describe their different approaches to proof systems, recursion mechanisms, and optimization strategies. In the final part, we present comparative benchmarks on various examples, highlighting their performance differences. The results show that RISC Zero produces smaller proofs and has faster verification, while SP1 is faster in proof generation and requires fewer computation cycles.
An important cryptographic mechanism that guarantees confidentiality (the zero-disclosure property) and ensures that it is impossible to prove a false statement to the verifier is zero-disclosure proofs. A popular implementation of zero-disclosure proofs is short, noninteractive proofs that can be quickly verified and that do not require interaction between the parties after the initial setup. The main direction in the development of modern proof systems is interactive proof, which is built in two steps. The first is sending a confirmation of the polynomial of an interactive oracle proof and the second is creating correct oracles of the polynomial commitment scheme using well-defined cryptographic methods for evaluating polynomials. Verifying the use of the same coefficients in each linear combination requires checking both polynomial consistency and variable consistency. To construct general schemes of concise non-interactive zerodisclosure knowledge argument, an interactive oracle proof polynomial was proposed that models messages as polynomial oracles. All tests are proved using polynomial commitment schemes and then evaluated with zero knowledge at a point specified by the person verifying the information. The reliability and confidentiality of all tests are based on three main categories of interactive oracle proof polynomials, namely polynomial commitment schemes with conjunction, with inner product argument and with code theory. The protocols of concise noninteractive zero-disclosure knowledge arguments are implemented through high-level programs (compilers), which are converted into an intermediate representation, i.e. a scheme defined by a system of constraints. The compilers used are divided into domain-oriented languages, embedded domain-oriented languages, and zero-knowledge virtual machines. Specialized domain-oriented hardware description languages or programming languages offer an adapted syntax for efficiently expressing constraints in arithmetic schemes. Embedded domain-oriented languages are implemented as functions in general-purpose programming languages and are oriented to the overhead schemes inherited from the embedded language. Zero-knowledge virtual machines process the opcode of the fetch-decodeexecute cycle, replicating the computation trace for general programs and generating corresponding zeroknowledge proofs. They are compatible with existing high-level programming languages and can use the features of existing compilers. Compilers are evaluated for cross- or syntactic compatibility. In general, the biggest obstacle to using non-interactive proof libraries is the lack of documentation. Standardization can help developers compare important features across libraries and establish a more consistent performance baseline. Library documentation for these core features is implicit, and developers need to understand the underlying cryptographic techniques to choose an appropriate scheme. Standardization of compiler options is important, making it difficult to reuse existing tools.
This paper introduces a novel framework for Zero-Knowledge Infrastructure Verification (ZKIV) that combines chaos engineering principles with security operations and zero-knowledge proofs to create a robust infrastructure verification system. By leveraging these technologies within a DevOps context, organizations can validate the integrity and security posture of their infrastructure without revealing sensitive configuration details or credentials. This approach, which we term ChaosSecOps, represents a significant advancement in infrastructure security verification, enabling teams to verify compliance, detect misconfigurations, and identify vulnerabilities without exposing sensitive information. Through a detailed AWS implementation case study, this paper demonstrates how ZKIV can be applied to modern cloud environments to enhance security, streamline compliance verification, and build resilient systems.Executive SummaryThis paper introduces Zero-Knowledge Infrastructure Verification (ZKIV), a novel framework for validating the security and compliance of complex, modern infrastructure (particularly cloud environments like AWS) without exposing sensitive configuration details or credentials. ZKIV achieves this by combining principles from:ā¢ Zero-Knowledge Proofs (ZKPs): While full cryptographic ZKPs are discussed, the paper focuses on "functional zero-knowledge" approaches practical for infrastructure. This means proving that security controls are in place and functioning correctly without revealing the underlying configurations themselves. Examples include black-box testing, output-only verification, and attestation.ā¢ Chaos Engineering: The deliberate introduction of controlled failures (like misconfigurations or simulated attacks) to test system resilience and the effectiveness of security controls.ā¢ Security Operations (SecOps): Continuous monitoring, threat response, and security automation practices.ā¢ DevOps: Leveraging automation, continuous integration/continuous delivery (CI/CD), and Infrastructure as Code (IaC). The integration of these disciplines is termed ChaosSecOps. Key Benefits of ZKIVā¢ Enhanced Security: Verification happens without needing to expose sensitive data, reducing the attack surface.ā¢ Improved Compliance: Continuous, automated verification ensures ongoing adherence to regulatory and internal security policies (e.g., PCI DSS, SOC 2). Evidence is collected in a zero-knowledge manner.ā¢ Reduced Operation Risk: Proactive identification of vulnerabilities and misconfigurations before they can be exploited.ā¢ Increased Confidence: Greater assurance in the security posture due to systematic and continuous testing.ā¢ Scalability: Verification is automated and can be used across many systems.ā¢ Efficiency: Verification can be done faster.ZKIV Framework ComponentsThe framework consists of several key components that work together:ā¢ Verification Orchestrator: The central control point for scheduling, executing, and managing verification tests.ā¢ Policy Engine: Defines and enforces security and compliance rules (using policy-as-code).ā¢ Test Agents: Ephemeral (short-lived) components deployed within the infrastructure to perform black-box testing.ā¢ Evidence Collection System: Gathers test results in a way that preserves zero-knowledge (no sensitive data revealed).ā¢ Remediation Framework: Automates the fixing of identified security issues.AWS Implementation Case StudyA detailed case study demonstrates ZKIV implementation within a financial services organization using AWS. Key AWS services used include AWS Organizations, Security Hub, Lambda, Step Functions, EventBridge, Systems Manager, S3, and Config. The case study shows practical application of zero-knowledge techniques like:ā¢ Least-Privilege IAM Roles: Verification agents have only the permissions needed to check configurations, not to access the data they protect.ā¢ Output-Only Verification: Validating database security settings without querying the database itself.ā¢ Black-Box Network Testing: Using isolated containers to test network segmentation without accessing internal network configurations.
Increasing attention to digital identity and self-sovereign identity (SSI) is gaining momentum. SSI brings various benefits to natural persons, such as owning controls; conversely, digital identity systems in the real world require Sybil-resistance to comply with anti-money laundering (AML) and other needs. CanDID by Maram et al. proposed that decentralized digital identity systems may achieve Sybil-resistance and preserve privacy by utilizing multi-party computation (MPC), assuming a distributed committee of trusted nodes. Pass et al. proposed the formal abstraction of attested execution secure processors (AESPs) while equipping hardware-assisted security in mobile devices has become the norm. We first describe our proposal to utilize AESPs for building secure Sybil-resistant SSI systems, the architecture with a set of system protocols$\Pi ^{{\mathcal {G}}_{\mathtt {att}}}$, which brings drastic flexibility and efficiency compared to existing systems. In addition, we propose a novel scheme that enables users (holders) to request verifiers to verify their credentials without AESPs, and it further achieves unlinkability among credentials created for public verification. Our scheme introduces a simplified format for computed claims and commitment-based anonymous identifiers. We also describe a technique to utilize zero-knowledge membership proofs, in particular, āOne-Out-of-Many Proofsā$\Sigma $-protocol by Groth and Kohlweiss, which can prove the existence of an expected credential without identifying it. Along with other techniques, such as utilizing the BBS+ signature scheme, we demonstrate how our scheme can achieve its goals with the extended anonymous and Sybil-resistant SSI system protocols$\Pi ^{{\mathcal {G}}_{\mathtt {att}}+}$. Entitling unlinkability among derived credentials in the anonymous Sybil-resistant SSI results in proper privacy preservation.