Ethereum 2.0 is a major upgrade to improve its scalability, throughput, and security. In this version, RANDAO is the scheme to randomly select the users who propose, confirm blocks, and get rewards. However, a vulnerability, referred to as the `Last Revealer Attack' (LRA), compromises the randomness of this scheme by introducing bias to the Random Number Generator (RNG) process. This vulnerability is first clarified again in this study. After that, we propose a Shamir's Secret Sharing (SSS)-based RANDAO scheme to mitigate the LRA. Through our analysis, the proposed method can prevent the LRA under favorable network conditions.
Abstract Ethereum smart contracts are a special type of computer programs. Once deployed on the blockchain, they cannot be modified. This presents a significant challenge to the security of smart contracts. Previous research has proposed static and dynamic detection tools to identify vulnerabilities in smart contracts. These tools check contract vulnerabilities based on predefined rules, and the accuracy of detection strongly depends on the design of the rules. However, the constant emergence of new vulnerability types and strategies for vulnerability protection leads to numerous false positives and false negatives by tools. To address this problem, we analyze the characteristics of vulnerabilities in smart contracts and the corresponding protection strategies. We convert the contracts' bytecode into an intermediate representation to extract semantic information of the contracts. Based on this semantic information, we establish a set of detection rules based on semantic facts and implement a vulnerability detection tool SafeCheck using static program analysis methods. The tool is used to detect six common types of vulnerabilities in smart contracts. We have extensively evaluated SafeCheck on real Ethereum smart contracts and compared it to other tools. The experimental results show that SafeCheck performs better in smart contract vulnerability detection compared to other typical tools, with a high F‐measure (up to 83.1%) for its entire dataset.
Smart contracts, as a key component of blockchain technology, play a crucial role in ensuring the automation of transactions and adherence to protocol rules. However, smart contracts are susceptible to security vulnerabilities, which, if exploited, can lead to significant asset losses. This study explores the potential of enhancing smart contract security audits using the GPT-4 model. We utilized a dataset of 35 smart contracts from the SolidiFI-benchmark vulnerability library, containing 732 vulnerabilities, and compared it with five other vulnerability detection tools to evaluate GPT-4's ability to identify seven common types of vulnerabilities. Moreover, we assessed GPT-4's performance in code parsing and vulnerability capture by simulating a professional auditor's auditing process using CoT(Chain of Thought) prompts based on the audit reports of eight groups of smart contracts. We also evaluated GPT-4's ability to write Solidity Proof of Concepts (PoCs). Through experimentation, we found that GPT-4 performed poorly in detecting smart contract vulnerabilities, with a high Precision of 96.6%, but a low Recall of 37.8%, and an F1-score of 41.1%, indicating a tendency to miss vulnerabilities during detection. Meanwhile, it demonstrated good contract code parsing capabilities, with an average comprehensive score of 6.5, capable of identifying the background information and functional relationships of smart contracts; in 60% of the cases, it could write usable PoCs, suggesting GPT-4 has significant potential application in PoC writing. These experimental results indicate that GPT-4 lacks the ability to detect smart contract vulnerabilities effectively, but its performance in contract code parsing and PoC writing demonstrates its significant potential as an auxiliary tool in enhancing the efficiency and effectiveness of smart contract security audits.
Once deployed in blockchain, smart contracts become immutable: Attackers can exploit bugs and vulnerabilities in their code that cannot be replaced with a bug-free version. For this reason, the verification of smart contracts before they are deployed in blockchain is important. However, the development of verification tools is not easy, especially if one wants to obtain guarantees by using formal methods. This article describes the development, from scratch, of a static analyzer based on abstract interpretation for the verification of real-world Tezos smart contracts. The analyzer is generic with respect to the property under analysis. This article shows taint analysis as a concrete instantiation of the analyzer, at different levels of precision, to detect untrusted cross-contract invocations.
Xun Deng, Sidi Mohamed Beillahi, Cyrus Minwalla, Han Du · 6 authors
This paper presents OVer, a framework designed to automatically analyze the behavior of decentralized finance (DeFi) protocols when subjected to a "skewed" oracle input. OVer firstly performs symbolic analysis on the given contract and constructs a model of constraints. Then, the framework leverages an SMT solver to identify parameters that allow its secure operation. Furthermore, guard statements may be generated for smart contracts that may use the oracle values, thus effectively preventing oracle manipulation attacks. Empirical results show that OVer can successfully analyze all 10 benchmarks collected, which encompass a diverse range of DeFi protocols. Additionally, this paper illustrates that current parameters utilized in the majority of benchmarks are inadequate to ensure safety when confronted with significant oracle deviations. It shows that existing ad-hoc control mechanisms such as introducing delays are often in-sufficient or even detrimental to protect the DeFi protocols against the oracle deviation in the real-world.
The concept of smart contracts (SCs) is becoming more prevalent, and their application is gaining traction across many diverse scenarios. However, producing poorly constructed contracts carries significant risks, including the potential for substantial financial loss, a lack of trust in the technology, and the risk of exposure to cyber-attacks. Several tools exist to assist in developing SCs, but their limited functionality increases development complexity. Expert knowledge is required to ensure contract reliability, resilience, and scalability. To overcome these risks and challenges, tools and services based on modeling and formal techniques are required that offer a robust methodology for SC verification and life-cycle management. This study proposes an engineering framework for the generation of a robust and verifiable smart contract (GRV-SC) framework that covers the entire SC life-cycle from design to deployment stages. It adopts SC modeling and automated formal verification methodologies to detect security vulnerabilities and improve resilience, extensibility, and code optimization to mitigate risks associated with SC development. Initially, the framework includes the implementation of a formal approach, using colored Petri nets (CPNs), to model cross-platform Digital Asset Modeling Language (DAML) SCs. It also incorporates a specialized type safety dynamic verifier, which is designed to detect and address new vulnerabilities that can arise in DAML contracts, such as access control and insecure direct object reference (Idor) vulnerabilities. The proposed GRV-SC framework provides a holistic approach to SC life-cycle management and aims to enhance the security, reliability, and adoption of SCs.
Fernando Román-García, Juan Hernández‐Serrano, Óscar Esparza
This article introduces the Non-Repudiable Data Exchange (NoRDEx) protocol, designed to ensure non-repudiation in data exchanges. Unlike traditional non-repudiation and fair exchange protocols, NoRDEx can be considered decentralized as it eliminates the need for a centralized Trusted Third Party (TTP) by using a Distributed Ledger Technology (DLT) to store cryptographic proofs without revealing the exchanged message. NoRDEx is an optimistic non-repudiation protocol, as it only uses the DLT in case of a dispute. The protocol has been implemented and tested in real-world environments, with performance assessments covering cost, overhead, and execution time. A formal security analysis using the Syverson Van Oorschot (SVO) logical model demonstrates NoRDEx’s ability to resolve disputes securely.
Remote attestation (RA) protocols have been widely used to evaluate the integrity of software on remote devices.Currently, the state-of-the-art RA protocols lack a crucial feature: transparency.This means that the details of the final attestation verification are not openly accessible or verifiable by the public.Furthermore, the interactivity of these protocols often limits attestation to trusted parties who possess privileged access to confidential device data, such as pre-shared keys and initial measurements.These constraints impede the widespread adoption of these protocols in various applications.In this paper, we introduce zRA, a non-interactive, transparent, and publicly provable RA protocol based on zkSNARKs.zRA enables verification of device attestations without the need for pre-shared keys or access to confidential data, ensuring a trustless and open attestation process.This eliminates the reliance on online services or secure storage on the verifier side.Moreover, zRA does not impose any additional security assumptions beyond the fundamental cryptographic schemes and the essential trust anchor components on the prover side (i.e., ROM and MPU).The zero-knowledge attestation proofs generated by devices have constant size regardless of the network complexity and number of attestations.Moreover, these proofs do not reveal sensitive information regarding internal states of the device, allowing verification by anyone in a public and auditable manner.We conduct an extensive security analysis and demonstrate scalability of zRA compared to prior work.Our analysis suggests that zRA excels especially in peer-to-peer and Pub/Sub network structures.To validate the practicality, we implement an open-source prototype of zRA using the Circom language.We show that zRA can be securely deployed on public permissionless blockchains, serving as an archival platform for attestation data to achieve resilience against DoS attacks.
Data-driven landscape across finance, government, and healthcare, the continuous generation of information demands robust solutions for secure storage, efficient dissemination, and fine-grained access control. Blockchain technology emerges as a significant tool, offering decentralized storage while upholding the tenets of data security and accessibility. However, on-chain and off-chain strategies are still confronted with issues such as untrusted off-chain data storage, absence of data ownership, limited access control policy for clients, and a deficiency in data privacy and auditability. To solve these challenges, we propose a permissioned blockchain-based privacy-preserving fine-grained access control on-chain and off-chain system, namely FACOS. We applied three fine-grained access control solutions and comprehensively analyzed them in different aspects, which provides an intuitive perspective for system designers and clients to choose the appropriate access control method for their systems. Compared to similar work that only stores encrypted data in centralized or non-fault-tolerant IPFS systems, we enhanced off-chain data storage security and robustness by utilizing a highly efficient and secure asynchronous Byzantine fault tolerance (BFT) protocol in the off-chain environment. As each of the clients needs to be verified and authorized before accessing the data, we involved the Trusted Execution Environment (TEE)-based solution to verify the credentials of clients. Additionally, our evaluation results demonstrated that our system (https://github.com/cliu717/AsynchronousStorage) offers better scalability and practicality than other state-of-the-art designs. We deployed our system on Alibaba Cloud and Tencent Cloud and conducted multiple evaluations. The results indicate that it takes about 2.79 seconds for a client to execute the protocol for uploading and about 0.96 seconds for downloading. Compared to other decentralized systems, our system exhibits efficient latency for both download and upload operations.
Francesca Stabile, Walter Lúcia, Amr Youssef, Giuseppe Franzè
The proliferation of cloud computing technologies has paved the way for deploying networked encrypted control systems, offering high performance, remote accessibility and privacy. However, in scenarios where the control algorithms run on third-party cloud service providers, the control’s logic might be changed by a malicious agent on the cloud. Consequently, it is imperative to verify the correctness of the control signals received from the cloud. Traditional verification methods, like zero-knowledge proof techniques, are computationally demanding in both proof generation and verification, may require several rounds of interactions between the prover and verifier and, consequently, are inapplicable in real-time control system applications. In this paper, we present a novel computationally inexpensive verifiable computing solution inspired by the probabilistic cut-and-choose approach. The proposed scheme allows the plant’s actuator to validate the computations accomplished by the encrypted cloud-based networked controller without compromising the control scheme’s performance. We showcase the effectiveness and real-time applicability of the proposed verifiable computation scheme using a remotely controlled Khepera-IV differential-drive robot.
Smart contracts are programs stored on a blockchain ledger, thus being immutable after deployment, which makes assessment of their correctness before deployment vital. Extended finite state machines (EFSM) offer a structured framework for modeling complex systems, thus providing a systematic approach to scrutinize smart contract functionalities. This paper describes a methodology to automatically convert from the abstract syntax tree of a smart contract to an EFSM model. A smart contract implementing a casino is the specific use case, and verification of the EFSM model reveals it to be blocking. This blocking represents that a malicious player can lock the funds of the casino so that they can never be retrieved.
Decentralized Autonomous Organizations (DAOs) are blockchain-based organizations that facilitate decentralized governance. Today, DAOs not only hold billions of dollars in their treasury but also govern many of the most popular Decentralized Finance (DeFi) protocols. This paper systematically analyses security threats to DAOs, focusing on the types of attacks they face. We study attacks on DAOs that took place in the past, attacks that have been theorized to be possible, and potential attacks that were uncovered and prevented in audits. For each of these (potential) attacks, we describe and categorize the attack vectors utilized into four categories. This reveals that while many attacks on DAOs take advantage of the less tangible and more complex human nature involved in governance, audits tend to focus on code and protocol vulnerabilities. Thus, additionally, the paper examines empirical data on DAO vulnerabilities, outlines risk factors contributing to these attacks, and suggests mitigation strategies to safeguard against such vulnerabilities.
Seonghwan Park, Hayoung Kang, Shangze Han, Jonghee M. Youn · 5 authors
A smart contract is a program executed on a blockchain. However, once the smart contract is deployed on the blockchain, it becomes visible to all participants and remains immutable. Thus, any sensitive information or vulnerabilities in smart contracts can be exposed to potential attackers. To protect the confidentiality of smart contracts, existing studies execute smart contracts in a trusted execution environment (TEE). However, they still suffer from vulnerabilities in smart contracts and potential memory-vulnerability problems. If an attack such as privilege escalation occurs by exploiting this vulnerability, the TEE can have a detrimental effect on the entire system as it has the most privileges in the system. To mitigate the memory vulnerability of the smart contracts in TEE, we propose MECAT, a prototype for memory-safe confidential smart contracts. In essence, MECAT runs smart contracts written in Rust, a memory-safe language, in ARM TrustZone. And MECAT is developed as a software library, allowing developers to easily apply MECAT to their smart contracts. According to our evaluation, MECAT only incurs a 1.36x performance overhead and 0.3% power overhead in single-node environments and can process the 16 clients concurrently in the network made with 8 peer nodes.
Ethereum is the dominant blockchain ecosystem capable of executing Turing-complete smart contracts. Rollups gained significant traction as the primary layer 2 (L2) solution meant to bring horizontal scalability to the main Ethereum network (L1). A core component of any rollup is the sequencer, which creates new L2 blocks to be submitted in rollup batches to L1. In most of the current rollup architectures, this component is centralised. As a result, these designs are prone to inconspicuous censorship practices by the sequencer. Trusted execution environments (TEEs) can guarantee the integrity of various sequencer components, which is instrumental in addressing censorship. However, the reaction of the system design to censorship attempts depends on where a TEE is integrated and which components it protects. In particular, this reaction is limited in the case of a monolithic TEE-protected sequencer design. Proposer-Builder Separation (PBS) is a non-monolithic paradigm adopted on L1, which separates the production of blocks from proposing them for inclusion in the blockchain. Recently, PBS has been considered for integration with L2 sequencers, with an impact on alleviating censorship. In this paper, we explore the design space of TEE-integrating PBS and non-PBS sequencer variants. First, we introduce a formal framework for the censorship actions that captures the specificity of the L2 sequencer. Then, we analyse to what extent the different designs address these censorship actions. Our main contribution is a novel design variation that allows for a precise observation of censored transactions. In the presence of TEEs, in a PBS setting, we demonstrate this precise observability, which is necessary to enable resilience to censorship.
Smart contracts are computer programs running on blockchains to automate the transaction execution between users. The absence of contract specifications poses a real challenge to the correctness verification of smart contracts. Program invariants are properties that are always preserved throughout the execution, which characterize an important aspect of the program behaviors. In this paper, we propose a novel invariant generation framework, INVCON+, for Solidity smart contracts. INVCON+ extends the existing invariant detector, InvCon, to automatically produce verified contract invariants based on both dynamic inference and static verification. Unlike INVCON+, InvCon only produces likely invariants, which have a high probability to hold, yet are still not verified against the contract code. Particularly, INVCON+ is able to infer more expressive invariants that capture richer semantic relations of contract code. We evaluate INVCON+ on 361 ERC20 and 10 ERC721 real-world contracts, as well as common ERC20 vulnerability benchmarks. The experimental results indicate that INVCON+ efficiently produces high-quality invariant specifications, achieving a recall of 80%, which can be used to secure smart contracts from 17 types of common vulnerabilities.
Samson Kahsay Gebresilassie, Joseph Rafferty, Mamun Abu-Tair, Aftab Ali · 6 authors
The Internet of Things (IoT) is a technology paradigm that has transformed several domains including manufacturing, agriculture, healthcare, power grids, travel, and retail. Despite the enormous advantages that IoT offers to organizations and transforming individuals’ everyday lives in a wide range of domains, it comes with potential cyber risks that can negatively impact, harm, or damage them. Security is the most challenging issue in IoT systems due to insecure devices, inadequate IDMS, lack of data security and privacy, lack of trust, lack of risk analysis on network traffic, various vulnerabilities and attacks, lack of physical security, and many other risk factors. Although several security architectures have been developed, they fail to properly and fully address these IoT security challenges and an urgent demand awaits for a robust IoT security architecture. Thus, this work investigates state-of-the-art solutions and proposes a holistic novel IoT security architecture called SHIELD: Secure Holistic IoT Environment with Ledger-based Defense with core security capabilities of decentralized Identity Management System (IDMS), Network Traffic Monitoring, Analysis, and dataset generation, deep learning-based Intrusion Detection System (IDS), and Distributed Ledger Technology (DLT)-based Trust Management System (TMS). The proposed architecture is qualitatively compared with existing solutions using key features like a single point of failure, risk/attack-aware, trust, real-time traffic behavior monitoring, up-to-date dataset, cross-platform functionality, and availability among others. As a result of this comparison, SHIELD architecture provides a holistic and robust solution with multiple core security features to overcome some of the key security challenges IoT environment.
Abstract Blockchains are decentralized systems that provide trustable execution guarantees through the use of programs called smart contracts. Smart contracts are programs written in domain-specific programming languages running on blockchains that govern how tokens and cryptocurrency are sent and received. Smart contracts can invoke other smart contracts during the execution of transactions initiated by external users. Once deployed, smart contracts running code cannot be modified, so techniques like runtime verification are very appealing for improving their reliability. Moreover, the conventional model of computation of smart contracts is transactional: once operations commit, their effects are permanent and cannot be undone. Therefore, errors in smart contracts may lead to millionaire losses of money. In this paper, we present the concept of future monitors which allows monitors to remain waiting for future transactions to occur before committing or aborting. This is inspired by optimistic rollups, which are modern blockchain implementations that increase efficiency (and reduce cost) by delaying transaction effects. We exploit this delay to propose a model of computation that allows bounded future monitors. We show our monitors correct respect with legacy transactions, how they implement bounded future monitors and how they guarantee progress. We illustrate the use of bounded future monitors by implementing correctly multi-transaction flash loans.
Hamra Afzaal, Nazir Ahmad Zafar, Aqsa Tehseen, Shaheen Kousar · 5 authors
In recent years, Beacon Chain known as the core of Ethereum 2.0, has gained considerable attention since its launch. Many validators have staked billions of Ether in the Proof of Stake (PoS) network. It is a mission critical system and its security and stability rely on the justification and finalization of checkpoints. These are essential elements of the Casper FFG consensus algorithm utilized by the Beacon Chain. This process is critical for establishing a trustworthy foundation and finalizing proposed blocks by confirming agreed upon checkpoints. Hence, ensuring the correctness of checkpoints in the Beacon Chain has significant importance because any bug in it can cause serious implications. To address this challenge, we employ formal methods, a popular mathematical approach used for verifying the correctness of such critical systems. In this work, we have done formal verification of the processes of Beacon Chain state initialization, justification and finalization of checkpoints using the Process Analysis Toolkit (PAT) model checker. The adoption of model checking through the PAT model checker presents a novel contribution of our work, as this approach is not previously utilized in the formal verification of Beacon Chain. The presented work is specified through the Communicating Sequential Programs, formal specification language, and the properties are described through Linear Temporal Logic. The PAT model checker takes the specified formal model and properties as input to assess whether the properties are satisfied. The properties are analyzed with respect to the verification time, visited states, total transitions, and memory used. Through this research, we aim to increase confidence in the correctness and reliability of the Beacon Chain.
Pradeep Gupta, Nusrat Nigar, Roma Paswan, Rajat Kumar Singh · 5 authors
The advent of non-fungible tokens (NFTs) has revolutionized the digital landscape, providing creators and brands with unprecedented avenues to engage their communities and explore innovative monetization methods. Beyond their origins in digital art and collectibles, NFTs have catalyzed diverse applications, reshaping the way digital assets are perceived and utilized. One such innovation is the concept of NFT-gated websites, which has gained substantial momentum. These platforms facilitate community engagement by granting exclusive access to content and experiences, all while generating new revenue streams. NFT-gated websites operate by mandating users to connect their crypto wallets and prove ownership of specific NFTs or crypto tokens, thereby creating a unique layer of restricted access. This novel approach empowers creators and brands to nurture exclusive communities and deliver distinct experiences to their audience. In the rapidly evolving Web3 ecosystem, this transformative technology stands poised to redefine digital interactions, enabling creators and brands to thrive in this new era.
This paper presents a trustworthy architecture for Web3 service that establishes self-sovereign services. This architecture leverages decentralized identifiers (DID) and resource access control based on user trust scores and policies. By transitioning from centrally managed ID to DID, it will be possible to move towards ID management that does not rely on service providers. Trust scores are calculated by analyzing the social network generated from the history of past transactions between users stored in the blockchain. The degree of trust is quantified using measures of centrality and similarity. Centrality is measured by the number of user achievements and the extent of their connections. Similarity is calculated by estimating the communities they belong to using node embedding. These trust scores are clustered to generate policy based on role-based access control (RBAC). The authorization function is programmatically realized based on user credibility by comparing the results of the distribution of accessible resources by policy. In addition, a Web3 service broker acts as an intermediary between multiple service providers and users to provide optimal services through smart contracts. A Web3 service broker programmatically select services without intermediary agencies. A trustworthy architecture for Web3 service is shown as a case study of a home delivery service. In this scenario, Web3 service brokers offer optimal services for private companies and small and medium-sized businesses. This paper is an extended version of ”A Web3 Service Architecture with Self-Sovereign Identity” presented at iDECON/MS2023.