When do classical zero-knowledge protocols remain secure against quantum attacks? In this work, we develop the techniques, tools, and abstractions necessary to answer this question for foundational protocols:1)We prove that the Goldreich-Micali-Wigderson protocol for graph non-isomorphism and the Feige-Shamir protocol for NP remain zero-knowledge against quantum adversaries. At the heart of our proof is a new quantum rewinding technique that enables extracting information from multiple invocations of a quantum adversary without disturbing its state.2)We prove that the Goldreich-Kahan protocol for NP is post-quantum zero knowledge using a simulator that can be seen as a natural quantum extension of the classical simulator.Our results achieve negligible simulation error, appearing to contradict a recent impossibility result due to Chia-Chung-Liu-Yamakawa (FOCS 2021). This brings us to our final contribution:3.We introduce coherent-runtime expected quantum polynomial time, a simulation notion that (a) precisely captures all of our zero-knowledge simulators, (b) cannot break any polynomial hardness assumptions, (c) implies strict polynomial-time ε-simulation and (d) is not subject to the CCLY impossibility. In light of our positive results and the CCLY negative results, we propose coherent-runtime simulation to be the appropriate quantum analogue of classical expected polynomial-time simulation.
Mujeeb A. Shittu, Ibukun Olaoluwa Adeniji, Habeeb Shittu, Ifeanyi Simon Opara
This study presents a comprehensive and critical examination of blockchain-assisted secure data exchange within SCADA-controlled power systems, motivated by the growing cybersecurity risks and trust deficits associated with increasingly digitalised and decentralised electricity infrastructures. The primary purpose of the study is to evaluate the extent to which blockchain technologies can enhance the security, integrity, and resilience of SCADA data exchange while remaining compatible with the stringent performance and safety requirements of power system operations. A structured review methodology was adopted to synthesise peer-reviewed literature from power system engineering, cybersecurity, distributed ledger technologies, and related cyber-physical system domains. The analysis systematically examined SCADA communication architectures, data exchange models, blockchain fundamentals, integration paradigms, consensus mechanisms, privacy and access control strategies, interoperability challenges, and empirical pilot implementations across both developed and developing contexts. The findings reveal that conventional SCADA architectures, largely built on centralised trust and legacy protocols, are increasingly inadequate for addressing modern threat landscapes and multi-stakeholder data sharing requirements. Blockchain-assisted architectures—particularly permissioned and hybrid on-chain/off-chain models—demonstrate strong potential to improve data integrity, auditability, non-repudiation, and cross-organisational trust without disrupting real-time control functions. However, the study also identifies persistent challenges related to scalability, interoperability, governance complexity, and human capacity, which constrain large-scale deployment. Empirical evidence from pilot projects further indicates that blockchain is most effective when applied selectively at supervisory and coordination layers rather than within time-critical control loops. The study concludes that blockchain-assisted secure data exchange represents a strategically valuable complement to existing SCADA security mechanisms rather than a standalone solution. It recommends future research on performance-optimised consensus protocols, standardised integration frameworks, and the convergence of blockchain with advanced analytics and artificial intelligence. Policy alignment, capacity development, and context-aware implementation strategies are also essential to support sustainable adoption, particularly in developing power system environments.
These days, businesses, in both online and offline, have started accepting cryptocurrencies as payment methods. Even in countries like <italic>El Salvador</italic>, cryptocurrencies are recognized as fiat currencies. Meanwhile, publicly known, but not patched software vulnerabilities are security threats to not only software users but also to our society in general. As the status of cryptocurrencies has gradually increased, the impact of security vulnerabilities related to cryptocurrencies on our society has increased as well. In this paper, we first analyze vulnerabilities from the two major cryptocurrency vendors of Bitcoin and Ethereum in a quantitative manner with the respect to the CVSS, to see how the vulnerabilities are roughly structured in those systems. Then we introduce a modified AML vulnerability discovery model for the vulnerability datasets from the two vendors, after showing the original AML dose not accurately represent the vulnerability discovery trends on the datasets. The analysis shows that the modified model performs better than the original AML model for the vulnerability datasets from the major cryptocurrencies.
Smart contracts are the key software components to realize blockchain applications, from single encrypted digital currency to various fields. Due to the immutable nature of blockchain, any bugs or errors will become permanent once published and could lead to huge economic losses. Recently, a great number of security problems have been exposed in smart contracts. It is important to verify the correctness of smart contracts before they are deployed on the blockchain. This paper aims to verify the correctness of smart contracts in Ethereum transactions, and the model checker Spin is adopted for the formal verification of smart contracts in order to ensure their execution with respect to parties’ willingness, as well as their reliable interaction with clients. In this direction, we propose a formal method to construct the models for smart contracts. Then, the method is applied to a study case in the Ethereum commodity market. Finally, a case model is implemented in Spin, which can simulate the process’s execution and verify the properties that are abstracted from the requirements. Compared with existing techniques, formal analysis can verify whether smart contracts comply with the specifications for given behaviors and strengthen the credibility of smart contracts in the transaction.
Francesco D’Amato, Joachim Neu, Ertem Nusret Tas, David Tse
The LMD GHOST consensus protocol is a critical component of proof-of-stake Ethereum. In its current form, this protocol is brittle, as evidenced by recent attacks and patching attempts. We propose Goldfish, a new protocol that satisfies key properties required of a drop-in replacement for LMD GHOST: Goldfish is secure in the sleepy model, assuming a majority of the validators follows the protocol. Goldfish is reorg resilient so that honestly produced blocks are guaranteed inclusion in the ledger, and it supports fast confirmation with expected confirmation latency independent of the desired security level. Subsampling validators can improve the communication efficiency of Goldfish, and Goldfish is composable with finality/accountability gadgets. Crucially, Goldfish is structurally similar to LMD GHOST, providing a credible path to adoption in Ethereum. Attacks on LMD GHOST exploit lack of coordination among honest validators, typically provided by a locking mechanism in classical BFT protocols. However, locking requires votes from a quorum of all participants and is not compatible with fluctuating participation. Goldfish is powered by a novel coordination mechanism to synchronize the honest validators' actions. Experiments with our prototype implementation of Goldfish suggest practicality.
Many of today's companies use Smart Contracts to represent and execute their business processes. Smart contracts are self-executed programs running over blockchain. In this context, composite smart contracts are used to represent collaborative business processes. A composite smart contract is a smart contract that needs to execute other contracts using external calls to achieve its tasks. Composite smart contracts, through the use of external calls and the execution of other smart contracts that might belong to other owners or companies, bring many challenges with regard to security requirements. As a result, special efforts must be done to ensure composite smart contracts security verification. In this paper, we propose a novel approach to verify the security and the correctness of the composite smart contracts written in solidity in Ethereum blockchain. This approach is based on the finite state machine models and model checking method for modeling and verifying the composite smart contracts respectively. We consider seven security properties as well as the security issues that depend on the contract context to be checked in the composite smart contract. For this, we provide two different yet complementary types of verification. The first type of verification is applied to all smart contracts with properties called in our approach “standard properties” that represent the generic ones, while the second type considers the context-dependent properties that we called “specific properties” varying from one smart contract to another. Finally, we express all properties using computation tree logic formulae and we use the nuXmv symbolic model checker to verify the model against all properties. This approach is validated using a different set of solidity smart contracts.
With the rapid development of physical networks, tens of billions of Internet of Things (IoT) devices have been deployed worldwide. Access control is essential in the IoT system, which manages user access to vital IoT data. However, access control for the IoT is mainly based on centralized trusted servers, which face problems such as a single point of failure and data leakage. To tackle these challenges, we propose an access control framework for the IoT by combining blockchain and Intel software guard extension (SGX) technology. A blockchain validates both IoT devices and edge servers added to the network. The access control contract is deployed on the blockchain, which can manage attribute-based access control policies in a fine-grained manner and make access control decisions flexibly. SGX technology is introduced into the edge computing server to realize the confidentiality of data processing. Finally, we implemented the prototype of the framework on Quorum and conducted extensive experiments and theoretical analyses on the performance of the blockchain. The results of the experimental tests and theoretical analyses show that our framework has more advantages in computing costs and on-chain storage costs.
Norine Coenen, Bernd Finkbeiner, Jana Hofmann, Julia Tillman
Smart contracts are small but highly security-critical programs that implement wallets, token systems, auctions, crowd funding systems, elections, and other multi-party transactions on the blockchain. A broad range of methods has been developed to ensure that a smart contract is functionally correct. However, smart contracts often additionally need to satisfy certain hyperproperties, such as symmetry, determinism, or an information flow policy. In this paper, we show how a synthesis method for smart contracts can ensure that the contract satisfies its desired hyperproperties. We build on top of a recently developed synthesis approach from specifications in the temporal logic TSL. We present HyperTSL, an extension of TSL for the specification of hyperproperties of infinite-state software. As a preprocessing step, we show how to detect if a hyperproperty has an equivalent formulation as a (simpler) trace property. Finally, we describe how to refine a synthesized contract to adhere to its HyperTSL specification.
Blockchain systems based on a reusable resource, such as proof-of-stake (PoS), provide weaker security guarantees than those based on proof-of-work. Specifically, they are vulnerable to long-range attacks, where an adversary can corrupt prior participants in order to rewrite the full history of the chain. To prevent this attack on a PoS chain, we propose a protocol that checkpoints the state of the PoS chain to a proof-of-work blockchain such as Bitcoin. Our checkpointing protocol hence does not rely on any central authority. Our work uses Schnorr signatures and leverages Bitcoin recent Taproot upgrade, allowing us to create a checkpointing transaction of constant size. We argue for the security of our protocol and present an open-source implementation that was tested on the Bitcoin testnet.
Fausto Spoto, Sara Migliorini, Mauro Gambini, Andrea Benini
Abstract This paper shows that generic types ( generics ) are useful for writing more abstract and more general smart contracts, but this comes with some security risks, reporting a concrete security issue found while using generics for writing smart contracts that implement shared entities for the Hotmoka blockchain. That issue can be used to steal the remuneration of validator nodes. This paper proposes a patch based on appropriate code rewriting. Namely, smart contracts are pieces of code that are deployed and executed in the context of a blockchain infrastructure in order to automatically enforce some effects when particular events occur. The writing of smart contracts is a complex and critical activity that can benefit from the use of high-level features of programming languages, and generics is one of them. In many programming languages, such as Java, generics are implemented by erasure , i.e. replaced by their upper bound type during compilation into bytecode. This is safe at source level, since the compiler takes care of checking that types are correct, before erasure. However, the erased types of the generated bytecode are consequently weaker. In a permissionless blockchain, where every user can call the bytecode of smart contracts installed by other users, these weaker types pose a risk of attack.
Yang Yang, Shangbin Han, Ping Xie, Yan Zhu · 8 authors
With the increasing demand for privacy protection in the blockchain, the universal zero-knowledge proof protocol has been developed and widely used. Because hash function is an important cryptographic primitive in a blockchain, the zero-knowledge proof of hash preimage has a wide range of application scenarios. However, it is hard to implement it due to the transformation of efficiency and execution complexity. Currently, there are only zero-knowledge proof circuits of some widely used hash functions that have been implemented, such as SHA256. SM3 is a Chinese hash function standard published by the Chinese Commercial Cryptography Administration Office for the use of electronic authentication service systems, and hence might be used in several cryptographic applications in China. As the national cryptographic hash function standard, the zero-knowledge proof circuit of SM3 (Chinese Commercial Cryptography) has not been implemented. Therefore, this paper analyzed the SM3 algorithm process, designed a new layered circuit structure, and implemented the SM3 hash preimage zero-knowledge proof circuit with a circuit size reduced by half compared to the automatic generator. Moreover, we proposed several extended practical protocols based on the SM3 zero-knowledge proof circuit, which is widely used in blockchain.
This paper proposes a protocol for Proof of As-sets of a bitcoin exchange using the Zero-Knowledge Succinct Non-Interactive Argument of Knowledge (ZK-SNARK) without revealing either the bitcoin addresses of the exchange or balances associated with those addresses. The proof of assets is a mech-anism to prove the total value of bitcoins the exchange has the authority to spend using its private keys. We construct a privacy-preserving ZK-SNARK proof system to prove the knowledge of the private keys corresponding to the bitcoin assets of an exchange. The ZK-SNARK toolchain helps to convert an NP-Statement for proving the knowledge of the private keys (known to the exchange) into a circuit satisfiability problem. In this protocol, the exchange creates a Pedersen commitment to the value of bitcoins associated with each address without revealing the balance. The simulation results show that the proof generation time, size, and verification time are efficient in practice.
Haoxian Chen, Gerald Whitters, Mohammad Javad Amiri, Yuepeng Wang · 5 authors
This paper presents DeCon, a declarative programming language for implementing smart contracts and specifying contract-level properties. Driven by the observation that smart contract operations and contract-level properties can be naturally expressed as relational constraints, DeCon models each smart contract as a set of relational tables that store transaction records. This relational representation of smart contracts enables convenient specification of contract properties, facilitates run-time monitoring of potential property violations, and brings clarity to contract debugging via data provenance. Specifically, a DeCon program consists of a set of declarative rules and violation query rules over the relational representation, describing the smart contract implementation and contract-level properties, respectively. We have developed a tool that can compile DeCon programs into executable Solidity programs, with instrumentation for run-time property monitoring. Our case studies demonstrate that DeCon can implement realistic smart contracts such as ERC20 and ERC721 digital tokens. Our evaluation results reveal the marginal overhead of DeCon compared to the open-source reference implementation, incurring 14% median gas overhead for execution, and another 16% median gas overhead for run-time verification.
By using zkSNARKs to prove that values have specific dependent types, it is possible to provably assure compatibility and correctness without revealing sensitive information and extend our trusted computing base well beyond our own system. The approach we developed expands the scope of what non-interactive zero-knowledge proofs can capture to include properties about both the execution and correctness of programs.
Ilya Grishkov, Roland Kromes, Thanassis Giannetsos, Kaitai Liang
This paper offers a prototype of a Hyperledger Fabric-IPFS based network architecture including a smart contract based encryption scheme that meant to improve the security of user's data that is being uploaded to the distributed ledger. A new extension to the self-encryption scheme was deployed by integrating data owner's identity into the encryption process. Such integration allows to permanently preserve ownership of the original file and link it to the person/entity who originally uploaded it. Moreover, self-encryption provides strong security guarantees that decryption of a file is computationally not feasible under the condition that the encrypted file and the key are safely stored.
Cong Yue, Tien Tuan Anh Dinh, Zhongle Xie, Meihui Zhang · 7 authors
Verifiable ledger databases protect data history against malicious tampering. Existing systems, such as blockchains and certificate transparency, are based on transparency logs --- a simple abstraction allowing users to verify that a log maintained by an untrusted server is append-only. They expose a simple key-value interface without transactions. Building a practical database from transparency logs, on the other hand, remains a challenge. In this paper, we explore the design space of verifiable ledger databases along three dimensions: abstraction, threat model, and performance. We survey existing systems and identify their two limitations, namely, the lack of transaction support and the inferior efficiency. We then present GlassDB, a distributed database system that addresses these limitations under a practical threat model. GlassDB inherits the verifiability of transparency logs, but supports transactions and offers high performance. It extends a ledgerlike key-value store with a data structure for efficient proofs, and adds a concurrency control mechanism for transactions. GlassDB batches independent operations from concurrent transactions when updating the core data structures. In addition, we design a new benchmark for evaluating verifiable ledger databases, by extending YCSB and TPC-C benchmarks. Using this benchmark, we compare GlassDB against four baselines: reimplemented versions of three verifiable databases, and a verifiable map backed by a transparency log. Experimental results demonstrate that GlassDB is an efficient, transactional, and verifiable ledger database system.
In decentralized finance (DeFi), lenders can offer flash loans to borrowers, i.e., loans that are only valid within a blockchain transaction and must be repaid with fees by the end of that transaction. Unlike normal loans, flash loans allow borrowers to borrow large assets without upfront collaterals deposits. Malicious adversaries use flash loans to gather large assets to exploit vulnerable DeFi protocols. In this paper, we introduce a new framework for automated synthesis of adversarial transactions that exploit DeFi protocols using flash loans. To bypass the complexity of a DeFi protocol, we propose a new technique to approximate the DeFi protocol functional behaviors using numerical methods (polynomial linear regression and nearest-neighbor interpolation). We then construct an optimization query using the approximated functions of the DeFi protocol to find an adversarial attack constituted of a sequence of functions invocations with optimal parameters that gives the maximum profit. To improve the accuracy of the approximation, we propose a novel counterexample driven approximation refinement technique. We implement our framework in a tool named FlashSyn. We evaluate FlashSyn on 16 DeFi protocols that were victims to flash loan attacks and 2 DeFi protocols from Damn Vulnerable DeFi challenges. FlashSyn automatically synthesizes an adversarial attack for 16 of the 18 benchmarks. Among the 16 successful cases, FlashSyn identifies attack vectors yielding higher profits than those employed by historical hackers in 3 cases, and also discovers multiple distinct attack vectors in 10 cases, demonstrating its effectiveness in finding possible flash loan attacks.
Smart contracts are self-executing programs that run on the blockchain and make it possible for peers to enforce agreements without a third-party guarantee. The smart contract on Ethereum is the fundamental element of decentralized finance with billions of US dollars in value. Smart contracts cannot be changed after deployment and hence the code needs to be verified for potential vulnerabilities. However, smart contracts are far from being secure and attacks exploiting vulnerabilities that have led to losses valued in the millions. In this work, we explore the current state of smart contracts security, prevalent vulnerabilities, and security-analysis tool support, through reviewing the latest advancement and research published in the past five years. We study 13 vulnerabilities in Ethereum smart contracts and their countermeasures, and investigate nine security-analysis tools. Our findings indicate that a uniform set of smart contract vulnerability definitions does not exist in research work and bugs pertaining to the same mechanisms sometimes appear with different names. This inconsistency makes it difficult to identify, categorize, and analyze vulnerabilities. We explain some safeguarding approaches and best practices. However, as technology improves new vulnerabilities may emerge. Regarding tool support, SmartCheck, DefectChecker, contractWard, and sFuzz tools are better choices in terms of more coverage of vulnerabilities; however, tools such as NPChecker, MadMax, Osiris, and Sereum target some specific categories of vulnerabilities if required. While contractWard is relatively fast and more accurate, it can only detect pre-defined vulnerabilities. The NPChecker is slower, however, can find new vulnerability patterns.
Kunjian Song, Nedas Matulevicius, Eddie B. de Lima Filho, Lucas C. Cordeiro
Smart contracts written in Solidity are programs used in blockchain networks, such as Etherium, for performing transactions. However, as with any piece of software, they are prone to errors and may present vulnerabilities, which malicious attackers could then use. This paper proposes a solidity frontend for the efficient SMT-based context-bounded model checker (ESBMC), named ESBMC-Solidity, which provides a way of verifying such contracts with its framework. A benchmark suite with vulnerable smart contracts was also developed for evaluation and comparison with other verification tools. The experiments performed here showed that ESBMC-Solidity detected all vulnerabilities, was the fastest tool and provided a counterexample for each benchmark. A demonstration is available at https://youtu.be/3UH8_1QAVN0.
Blockchain technologies have found important and concrete applications in the real world. Active solutions leverage Smart Contracts for the management of cryptocurrencies, sensitive data, and other valuable assets. One of the core objectives of blockchain-oriented software engineering (BOSE) is ensuring that Smart Contracts receive adequate pre-release testing to guarantee the deployment of reliable code. However, the novelty and the complexity of the blockchain environment pose new challenges to the validation and verification of Smart Contract based software. In this paper, we analyze the aforementioned challenges to foster the discussion on the specific topic of Smart Contract testing and identify relevant research directions.
Bernd Finkbeiner, Jana Hofmann, Florian Kohn, Noemi Passing
Smart contracts are small but highly error-prone programs that implement agreements between multiple parties. We present a reactive synthesis approach for the automatic construction of smart contract state machines. Towards this end, we extend temporal stream logic (TSL) with universally quantified parameters over infinite domains. Parameterized TSL is a convenient logic to specify the temporal control flow, i.e., the correct order of transactions, as well as the data flow of the contract's fields. We develop a two-step approach that 1) synthesizes a finite representation of the - in general - infinite-state system and 2) splits the system into a compact hierarchical architecture that enables the implementation of the state machine in Solidity. We implement the approach in our prototype tool SCSynt, which - within seconds - automatically constructs Solidity code that realizes the specified control flow.
Smart contracts are usually financial-related, which makes them attractive attack targets. Many static analysis tools have been developed to facilitate the contract audit process, but not all of them take account of two special features of smart contracts: (1) The external variables, like time, are constrained by real-world factors; (2) The internal variables persist between executions. Since these features import implicit constraints into contracts, they significantly affect the performance of static tools, such as causing errors in reachability analysis and resulting in false positives. In this paper, we conduct a systematic study on implicit constraints from three aspects. First, we summarize the implicit constraints in smart contracts. Second, we evaluate the impact of such constraints on the state-of-the-art static tools. Third, we propose a lightweight but effective mitigation method named ConSym to deal with such constraints and integrate it into OSIRIS. The evaluation result shows that ConSym can filter out 96% of false positives and reduce false negatives by two-thirds.
Smart cities deploy large numbers of sensors and collect a tremendous amount of data from them. For example, Advanced Metering Infrastructures (AMIs), which consist of physical meters that collect usage data about public utilities such as power and water, are an important building block in a smart city. In a typical sensor network, the measurement devices are connected through a computer network, which exposes them to cyber attacks. Furthermore, the data is centrally managed at the operator's servers, making it vulnerable to insider threats. Our goal is to protect the integrity of data collected by large-scale sensor networks and the firmware in measurement devices from cyber attacks and insider threats. To this end, we first develop a comprehensive threat model for attacks against data and firmware integrity, which can target any of the stakeholders in the operation of the sensor network. Next, we use our threat model to analyze existing defense mechanisms, including signature checks, remote firmware attestation, anomaly detection, and blockchain-based secure logs. However, the large size of the Trusted Computing Base and a lack of scalability limit the applicability of these existing mechanisms. We propose the Feather-Light Blockchain Infrastructure (FLBI) framework to address these limitations. Our framework leverages a two-layer architecture and cryptographic threshold signature chains to support large networks of low-capacity devices such as meters and data aggregators. We have fully implemented the FLBI's end-to-end functionality on the Hyperledger Fabric and private Ethereum blockchain platforms. Our experiments show that the FLBI is able to support millions of end devices.
This document provides a clear description of the COLLABS level-2 security components. In particular, it describes fine-grained authorization for constrained environments, relying on distributed ledger technologies for exchanges between different involved mechanisms. We show how COLLABS ledger-based security modules can secure inter-device communications and enhance the trust level in inter-<br> The project COLLABS has received funding from the European Union’s Horizon 2020 research and innovation programme under grant agreement No 871518.<br> device collaboration, on several aspects of the Smart Factory lifecycle. We describe how COLLABS ensures that all the data collected from connected objects, and all the actions are authorized following an effective security policy. This document also illustrates the main data flows with sequence diagrams, describing and visualizing processes involving each component, as well as mapping of COLLABS level-2 security components to the use case scenarios.