Jie Cai, Bin Li, Jiale Zhang, Xiaobing Sun · 5 authors
Smart contract security has drawn extensive attention in recent years because of the enormous economic losses caused by vulnerabilities. Even worse, fixing bugs in a deployed smart contract is difficult, so developers must detect security vulnerabilities in a smart contract before deployment. Existing smart contract vulnerability detection efforts heavily rely on fixed rules defined by experts, which are inefficient and inflexible.To overcome the limitations of existing vulnerability detection approaches, we propose a GNN based approach for smart contract vulnerability detection. First, we construct a graph representation for a smart contract function with syntactic and semantic features by combining abstract syntax tree (AST), control flow graph (CFG), and program dependency graph (PDG). To further strengthen the presentation ability of our approach, we perform program slicing to normalize the graph and eliminate the redundant information unrelated to vulnerabilities. Then, we use a Bidirectional Gated Graph Neural-Network model with hybrid attention pooling to identify potential vulnerabilities in smart contract functions.
Blockchain technology and its applications are gaining popularity day by day. It is a ground-breaking technology that allows users to communicate without the need of a trusted middleman. A smart contract (self-executable code) is deployed on the blockchain and auto executes due to a triggering condition. In a no-trust contracting environment, smart contracts can establish trust among parties. Terms and conditions embedded in smart contracts will be imposed immediately when specified criteria have been fulfilled. Due to this, the malicious assailants have a special interest in smart contracts. Blockchains are immutable means if some transaction is deployed or recorded on the blockchain, it becomes unalterable. Thus, smart contracts must be analyzed to ensure zero security vulnerabilities or flaws before deploying the same on the blockchain because a single vulnerability can lead to the loss of millions. For analyzing the security vulnerabilities of smart contracts, various analysis tools have been developed to create safe and secure smart contracts. This paper presents a systematic review on Ethereum smart contracts analysis tools. Initially, these tools are categorized into static and dynamic analysis tools. Thereafter, different sources code analysis techniques are studied such as taint analysis, symbolic execution, and fuzzing techniques. In total, 86 security analysis tools developed for Ethereum blockchain smart contract are analyzed regardless of tool type and analysis approach. Finally, the paper highlights some challenges and future recommendations in the field of Ethereum smart contracts.
A smart public transport system is expected to be an integral part of our human lives to improve our mobility and reduce the effect of our carbon footprint. The safety and ongoing maintenance of the smart public transport system from cyberattacks are vitally important. To provide more comprehensive protection against potential cyberattacks, we propose a novel approach that combines blockchain technology and a deep learning method that can better protect the smart public transport system. By the creation of signed and verified blockchain blocks and chaining of hashed blocks, the blockchain in our proposal can withstand unauthorized integrity attack that tries to forge sensitive transport maintenance data and transactions associated with it. A hybrid deep learning-based method, which combines autoencoder (AE) and multi-layer perceptron (MLP), in our proposal can effectively detect distributed denial of service (DDoS) attempts that can halt or block the urgent and critical exchange of transport maintenance data across the stakeholders. The experimental results of the hybrid deep learning evaluated on three different datasets (i.e., CICDDoS2019, CIC-IDS2017, and BoT-IoT) show that our deep learning model is effective to detect a wide range of DDoS attacks achieving more than 95% F1-score across all three datasets in average. The comparison of our approach with other similar methods confirms that our approach covers a more comprehensive range of security properties for the smart public transport system.
Kai Wang, Jun Pang, Ding-Jie Chen, Yu Zhao · 7 authors
Exploiting the anonymous mechanism of Bitcoin, ransomware activities demanding ransom in bitcoins have become rampant in recent years. Several existing studies quantify the impact of ransomware activities, mostly focusing on the amount of ransom. However, victims’ reactions in Bitcoin that can well reflect the impact of ransomware activities are somehow largely neglected. Besides, existing studies track ransom transfers at the Bitcoin address level, making it difficult for them to uncover the patterns of ransom transfers from a macro perspective beyond Bitcoin addresses. In this article, we conduct a large-scale analysis of ransom payments, ransom transfers, and victim migrations in Bitcoin from 2012 to 2021. First, we develop a fine-grained address clustering method to cluster Bitcoin addresses into users, which enables us to identify more addresses controlled by ransomware criminals. Second, motivated by the fact that Bitcoin activities and their participants already formed stable industries, such as Darknet and Miner , we train a multi-label classification model to identify the industry identifiers of users. Third, we identify ransom payment transactions and then quantify the amount of ransom and the number of victims in 63 ransomware activities. Finally, after we analyze the trajectories of ransom transferred across different industries and track victims’ migrations across industries, we find out that to obscure the purposes of their transfer trajectories, most ransomware criminals (e.g., operators of Locky and Wannacry) prefer to spread ransom into multiple industries instead of utilizing the services of Bitcoin mixers. Compared with other industries, Investment is highly resilient to ransomware activities in the sense that the number of users in Investment remains relatively stable. Moreover, we also observe that a few victims become active in the Darknet after paying ransom. Our findings in this work can help authorities deeply understand ransomware activities in Bitcoin. While our study focuses on ransomware, our methods are potentially applicable to other cybercriminal activities that have similarly adopted bitcoins as their payments.
Abdul Razaque, Bandar Alotaibi, Munif Alotaibi, Fathi Amsaad · 8 authors
When people use social networks, they often fall prey to a clickbait scam. The scammer attempts to create a striking headline that attracts the majority of users and attaches a link. The user follows the link and can be redirected to a fraudulent resource where the user easily loses personal data. To solve this problem, a Blockchain-enabled deep recurrent neural network (BDRNN) is proposed to detect the nature safe and malicious clickbait from the contents. The proposed BDRNN consists of three phases: analysis of clickbait and source rating, clickbait search process and multi-layered clickbait detection. The analysis of clickbait and source rating phase helps to analyze different sources to detect the clickbait and also rating the content-sources. To achieve the clickbait analysis and source rating, the detection of blocklisted/allowlisted source and source rating check algorithms are introduced. The clickbait search process is accomplished by incorporating the binary search features for a faster and more efficient search process for malicious content-detection. The multi-layered clickbait detection is main phase of the proposed BDRNN that consists of three models: content-to-vector model (layer-1), deep neural network model(layer-2), and Blockchain-enabled malicious content detection model (layer-3). These models collectively detect the malicious and safe clickbait from the contents. The extensive experiments are conducted to determine the effectiveness of the proposed BDRNN model and compared with the existing state-of-the-art neural network models designed for clickbait detection, and the result demonstrates that the proposed BDRNN model outperforms the counterparts from the, accuracy, link detection, memory usage, analogous perspectives, and attacker’s successful content capturing rate.
What is the funniest number in cryptography (Episode 2)? 0 [1]. The reason is that $\forall x, x \cdot 0 = 0$, i.e., the equation is satisfied no matter what $x$ is. We'll use zero to attack zero-knowledge proof (ZKP). In particular, we'll discuss a critical issue in a cutting-edge ZKP PLONK [2] C++ implementation which allows an attacker to create a forged proof that all verifiers will accept. We'll show how theory guides the attack's direction. In practice, the attack works like a charm and we'll show how the attack falls through a chain of perfectly aligned software cracks. In the same codebase, there is an independent critical ECDSA bug where (r, s) = (0, 0) is a valid signature for arbitrary keys and messages, but we won't discuss it further because it's a known ECDSA attack vector in the Google Wycheproof cryptanalysis project [3] that I worked on a few years ago. All bugs have been responsibly disclosed through the vendor's bug bounty program with total reward $\sim \$15,000$ (thank you).
In recent years Industrial Control Systems (ICS) have been targeted increasingly by sophisticated cyberattacks. Improving ICS security has drawn significant attention in the literature that emphasises the importance of Cyber Threat Intelligence (CTI) sharing in accelerating detection, mitigation, and prevention of cyberattacks. However, organisations are reluctant to exchange CTI due to fear of exposure, reputational damage, and lack of incentives. Furthermore, there has been limited discussion about the factors influencing participation in sharing CTI about ICS. The existing CTI-sharing platforms rely on centralised trusted architectures that suffer from a single point of failure and risk companies' privacy as the central node maintains CTI details. In this paper, we address the needs of organisations involved in the management and protection of ICS and present a novel framework that facilitates secure, private, and incentivised exchange of CTI related to ICS using blockchain. We propose a new blockchain-enabled framework that facilitates the secure dissemination of CTI data among multiple stakeholders in ICS. We provide the framework design, technical development and evaluate the framework's feasibility in a real-world application environment using practical use-case scenarios. Our proposed design shows a more practical and efficient framework for a CTI sharing network for ICS, including the bestowal and acknowledgment of data privacy, trust barriers, and security issues ingrained in this domain.
Bo Gao, Siyuan Shen, Ling Shi, Jiaying Li · 6 authors
Smart contracts are computerized transaction protocols built on top of blockchain networks. Users are charged with fees, a.k.a. gas in Ethereum, when they create, deploy or execute smart contracts. Since smart contracts may contain vulnerabilities which may result in huge financial loss, developers and smart contract compilers often insert codes for security checks. The trouble is that those codes consume gas every time they are executed. Many of the inserted codes are however redundant. In this work, we present sOptimize, a tool that optimizes smart contract gas consumption automatically without compromising functionality or security. sOptimize works on smart contract bytecode, statically identifies 3 kinds of code patterns, and further removes them through verification-assisted techniques. The resulting code is guaranteed to be equivalent to the original one and can be directly deployed on blockchain. We evaluate sOptimize on a collection of 1,152 real-world smart contracts and show that it optimizes 43% of them, and the reduction on gas consumption is about 2.0% while in deployment and 1.2% in transactions, the amount can be as high as 954,201 gas units per contract.
Semantic code search technology allows searching for existing code snippets through natural language, which can greatly improve programming efficiency. Smart contracts, programs that run on the blockchain, have a code reuse rate of more than 90%, which means developers have a great demand for semantic code search tools. However, the existing code search models still have a semantic gap between code and query, and perform poorly on specialized queries of smart contracts. In this paper, we propose a Multi-Modal Smart contract Code Search (MM-SCS) model. Specifically, we construct a Contract Elements Dependency Graph (CEDG) for MM-SCS as an additional modality to capture the data-flow and control-flow information of the code. To make the model more focused on the key contextual information, we use a multi-head attention network to generate embeddings for code features. In addition, we use a fine-tuned pretrained model to ensure the model's effectiveness when the training data is small. We compared MM-SCS with four state-of-the-art models on a dataset with 470K (code, docstring) pairs collected from Github and Etherscan. Experimental results show that MM-SCS achieves an MRR (Mean Reciprocal Rank) of 0.572, outperforming four state-of-the-art models UNIF, DeepCS, CARLCS-CNN, and TAB-CS by 34.2%, 59.3%, 36.8%, and 14.1%, respectively. Additionally, the search speed of MM-SCS is second only to UNIF, reaching 0.34s/query.
Yinxing Xue, Jiaming Ye, Wei Zhang, Jun Sun · 7 authors
Smart contract transactions are increasingly interleaved by cross-contract calls. While many tools have been developed to identify a common set of vulnerabilities to guard smart contracts, the cross-contract vulnerability is however overlooked by existing tools. Cross-contract vulnerabilities are exploitable bugs that manifest in the presence of more than two interacting contracts. Existing methods are however limited to analyze a maximum of two contracts at the same time. Detecting cross-contract vulnerabilities is highly non-trivial. With multiple interacting contracts, the search space is much larger than that of a single contract. To address this problem, we present xFuzz, a machine learning guided smart contract fuzzing framework. The machine learning models are trained with novel features (e.g., word vectors and instructions) and are used to filter likely benign program paths. Comparing with existing static tools, machine learning model is proven to be more robust, avoiding directly adopting manually-defined rules in specific tools. We compare xFuzz with three state-of-the-art tools on 7,391 contracts. xFuzz detects 18 exploitable cross-contract vulnerabilities, of which 15 vulnerabilities are exposed for the first time. Furthermore, our approach is shown to be efficient in detecting non-cross-contract vulnerabilities as well-using less than 20% time as that of other fuzzing tools, xFuzz detects twice as many vulnerabilities.
Yinxing Xue, Jiaming Ye, Wei Zhang, Jun Sun · 7 authors
Smart contract transactions are increasingly interleaved by cross-contract calls. While many tools have been developed to identify a common set of vulnerabilities, the cross-contract vulnerability is overlooked by existing tools. Cross-contract vulnerabilities are exploitable bugs that manifest in the presence of more than two interacting contracts. Existing methods are however limited to analyze a maximum of two contracts at the same time. Detecting cross-contract vulnerabilities is highly non-trivial. With multiple interacting contracts, the search space is much larger than that of a single contract. To address this problem, we present xFuzz, a machine learning guided smart contract fuzzing framework. The machine learning models are trained with novel features (e.g., word vectors and instructions) and are used to filter likely benign program paths. Comparing with existing static tools, machine learning model is proven to be more robust, avoiding directly adopting manually-defined rules in specific tools. We compare xFuzz with three state-of-the-art tools on 7,391 contracts. xFuzz detects 18 exploitable cross-contract vulnerabilities, of which 15 vulnerabilities are exposed for the first time. Furthermore, our approach is shown to be efficient in detecting non-cross-contract vulnerabilities as well -- using less than 20% time as that of other fuzzing tools, xFuzz detects twice as many vulnerabilities.
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.
Mirko Staderini, András Pataricza, Andrea Bondavalli
Smart contracts are one of the most important innovations of the second generation of the Blockchain. They are widely used in various contexts, including financial, insurance, gaming, and betting. Once a smart contract is deployed on a Blockchain, due to its code immutability, residual vulnerabilities cannot be patched. Static analysis is an efficient method for vulnerability detection. This paper addresses the security evaluation and improvement of Solidity smart contracts through the use of static analysis tools, discussing: (i) the motivation and background, (ii) the evaluation of how good the tools are for improving security, (iii) their combination, and (iv) main results.
Smart contracts are programs stored on a blockchain that run when predetermined conditions are met. However, designing and implementing a smart contract is not trivial since upon deployment on a blockchain, it is no longer possible to modify it (neither for improving nor for bug fixing). It is only possible by deploying a new version of the smart contract which is costly (deployment cost for the new contract and destruction cost for the old contract). To this end, there are many solutions for testing the smart contracts before their deployment. Since realizing bug-free smart contracts increase the reliability, as well as reduce the cost, testing is an essential activity. In this paper, we group the existing solutions that attempt to tackle smart contract testing into following categories: public test networks, security analysis tools, blockchain emulators and blockchain simulators. Then, we analyze these solutions, categorize them and show what their pros and cons are.
Zhiyong Fang, David Darais, Joseph P. Near, Yupeng Zhang
Static program analysis tools can automatically prove many useful properties of programs. However, using static analysis to prove to a third party that a program satisfies a property requires revealing the program's source code. We introduce the concept of zero-knowledge static analysis, in which the prover constructs a zero-knowledge proof about the outcome of the static analysis without revealing the program. We present novel zero-knowledge proof schemes for intra- and inter-procedural abstract interpretation. Our schemes are significantly more efficient than the naive translation of the corresponding static analysis algorithms using existing schemes. We evaluate our approach empirically on real and synthetic programs; with a pairing-based zero knowledge proof scheme as the backend, we are able to prove the control flow analysis on a 2,000-line program in 1,738s. The proof is only 128 bytes and the verification time is 1.4ms. With a transparent zero knowledge proof scheme based on discrete-log, we generate the proof for the tainting analysis on a 12,800-line program in 406 seconds, the proof size is 282 kilobytes, and the verification time is 66 seconds.
Andrea Lisi, Prateeti Mukherjee, Laura De Santis, Lei Wu · 6 authors
The disclosure of security vulnerabilities plays an important role in notifying vendors and the public about flaws in digital systems. Among the proposed disclosure approaches, the most utilized is Responsible Disclosure, which unfortunately suffers from several disadvantages such as fostering a false sense of security among the end-users, allowing arbitrary delays in the disclosure process, and forcing the party reporting a vulnerability to identify themselves, which has been exploited by vendors in the past through intimidation and malpractice. To address these issues, this paper presents an improved version of the Responsible Disclosure approach called Automated Responsible Disclosure (ARD) - a solution that leverages distributed ledgers and interledger technologies to automate the disclosure process while offering increased security, privacy, and transparency. A prototype implementation has been released as open-source software, and the evaluation of the solution shows that ARD is capable of addressing the key shortcomings in existing solutions and fostering more transparent vulnerability disclosure practices.
As the largest blockchain platform supporting smart contracts,millions of smart contracts have been deployed on Ethereum.Since the deployed smart contracts cannot be modified even if the contracts contain bugs,it is critical for developers to eliminate bugs prior to the deployment.Many smart contract analysis tools have been proposed.These tools either use bytecode-based symbolic execution to detect bugs,or convert the source code to an intermediate representation and then detect bugs.The tools based on symbolic execution usually cannot cover many types of bugs in source code.Converting the source code to an intermediate representation negatively impacts the detection speed.Moreover,these tools are bug detectors,which cannot automatically fix bugs based on analysis results.To address these limitations,we propose an approach named SolidityCheck,which employs regular expressions,program instrumentation and statement replacement in source code to quickly detect bugs and fix certain types of bugs.We conduct extensive experiments to evaluate SolidityCheck.The experimental results show that,compared with existing approaches,SolidityCheck demonstrates excellent performances on multiple indicators.
Smart contracts have gained popularity with the emergence of blockchain technology, although the concept behind them has been studied since the 1990s. The automation of contracts signed in real life is an interdisciplinary subject and draws attention not only in the scope of technology but also in areas like business area and legal area. With the aim of providing clear understanding, accuracy and security of information in the process of creating a smart contract, many tools have been developed, either to avoid vulnerabilities or to allow anyone to contribute in writing a contract. In view of this scenario and seeking to further facilitate the general understanding of a smart contract, this paper aims to study the representation of smart contracts as state diagrams. It summarizes, through a systematic mapping, the many ways to visually represent smart contracts as state diagrams, emphasizing their states and transitions. An experiment was also carried out in order to show how state diagrams can facilitate the understanding of a contract. The results show that state diagrams do help understanding smart contracts.
Henry Vargas, Carlos Lozano-Garzón, Germán A. Montoya, Yezid Donoso
Internet of Things (IoT) networks have been integrated into industrial infrastructure schemes, positioning themselves as devices that communicate highly classified information for the most critical companies of world nations. Currently, and in order to look for alternatives to mitigate this risk, solutions based on Blockchain algorithms and Machine Learning techniques have been implemented separately with the aim of mitigating potential threats in IIoT networks. In this paper, we sought to integrate the previous solutions to create an integral protection mechanism for IoT device networks, which would allow the identification of threats, activate secure information transfer mechanisms, and it would be adapted to the computational capabilities of industrial IoT. The proposed solution achieved the proposed objectives and is presented as a viable mechanism for detecting and containing intruders in an IoT network. In some cases, it overcomes traditional detection mechanisms such as an IDS.
Štefan Balogh, Ondrej Gallo, Roderik Ploszek, Peter Špaček · 5 authors
Internet of Things connects the physical and cybernetic world. As such, security issues of IoT devices are especially damaging and need to be addressed. In this treatise, we overview current security issues of IoT with the perspective of future threats. We identify three main trends that need to be specifically addressed: security issues of the integration of IoT with cloud and blockchains, the rapid changes in cryptography due to quantum computing, and finally the rise of artificial intelligence and evolution methods in the scope of security of IoT. We give an overview of the identified threats and propose solutions for securing the IoT in the future.
Detection of unknown malware and its variants remains both an operational and a research challenge in the Internet of Things (IoT). The Internet of Medical Things (IoMT) is a particular type of IoT network which deals with communication through smart healthcare (medical) devices. One of the prevailing problems currently facing IoMT solutions is security and privacy vulnerability. Previous malware detection methods have failed to provide security and privacy. In order to overcome this issue, the current study introduces a novel technique called biserial correlative Miyaguchi-Preneel blockchain-based Ruzicka-index deep multilayer perceptive learning (BCMPB-RIDMPL). The present research aims to improve the accuracy of malware detection and minimizes time consumption. The current study combines the advantages of machine-learning techniques and blockchain technology. The BCMPB-RIDMPL technique consists of one input layer, three hidden layers, and one output layer to detect the malware. The input layer receives the number of applications and malware features as input. After that, the malware features are sent to the hidden layer 1, in which feature selection is carried out using point biserial correlation, which reduces the time required to detect the malware. Then, the selected features and applications are sent to the hidden layer 2. In that layer, Miyaguchi-Preneel cryptographic hash-based blockchain is applied to generate the hash value for each selected feature. The generated hash values are stored in the blockchain, after which the classification is performed in the third hidden layer. The BCMPB-RIDMPL technique uses the Ruzicka index to verify the hash values of the training and testing malware features. If the hash is valid, then the application is classified as malware, otherwise it is classified as benign. This method improves the accuracy of malware detection. Experiments have been carried out on factors such as malware detection accuracy, Matthews's correlation coefficient, and malware detection time with respect to a number of applications. The observed quantitative results show that our proposed BCMPB-RIDMPL method provides superior performance compared with state-of-the-art methods.
Hai Jin, Zeli Wang, Ming Wen, Weiqi Dai · 6 authors
Ongoing smart contract attack events have seriously impeded the practical application of blockchain. Although lots of researches have been conducted, they mostly focus on off-chain vulnerability detection. However, smart contracts cannot be modified once they have been deployed on-chain, thus existing techniques cannot protect those deployed contracts from being attacked. To mitigate this problem, we propose a general smart contract repairer named Aroc, which can automatically patch vulnerable deployed contracts without changing the contract codes. The core insight of Aroc is to generate patch contracts to abort malicious transactions in advance. Taking the three most serious bug types (i.e., reentrancy, arithmetic bugs, and unchecked low-level checks) as examples, we present how Aroc automatically repairs them on-chain. We conduct abundant evaluations on four kinds of datasets to evaluate the effectiveness and efficiency of Aroc. In particular, Aroc can repair 95.95% of the vulnerable contracts with an average correctness ratio of 93.32%. Meanwhile, Aroc introduces acceptable additional overheads to smart contract users and blockchain miners. When compared with the state-of-the-art techniques, Aroc introduces either fewer execution overheads or contract codes.
Blockchain, as a distributed ledger technology, becomes increasingly popular, especially for enabling valuable cryptocurrencies and smart contracts. However, the blockchain software systems inevitably have many bugs. Although bugs in smart contracts have been extensively investigated, security bugs of the underlying blockchain systems are much less explored. In this paper, we conduct an empirical study on blockchain's system vulnerabilities from four representative blockchains, Bitcoin, Ethereum, Monero, and Stellar. Specifically, we first design a systematic filtering process to effectively identify 1,037 vulnerabilities and their 2,317 patches from 34,245 issues/PRs (pull requests) and 85,164 commits on GitHub. We thus build the first blockchain vulnerability dataset. We then perform unique analyses of this dataset at three levels, including (i) file-level vulnerable module categorization by identifying and correlating module paths across projects, (ii) text-level vulnerability type clustering by natural language processing and similarity-based sentence clustering, and (iii) code-level vulnerability pattern analysis by generating and clustering code change signatures that capture both syntactic and semantic information of patch code fragments. Our analyses reveal three key findings: (i) some blockchain modules are more susceptible than the others; notably, each of the modules related to consensus, wallet, and networking has over 200 issues; (ii) about 70% of blockchain vulnerabilities are of traditional types, but we also identify four new types specific to blockchains; and (iii) we obtain 21 blockchain-specific vulnerability patterns that capture unique blockchain attributes and statuses, and demonstrate that they can be used to detect similar vulnerabilities in other popular blockchains, such as Dogecoin, Bitcoin SV, and Zcash.
Abstract We report our experience in the formal verification of the reference implementation of the Beacon Chain. The Beacon Chain is the backbone component of the new Proof-of-Stake Ethereum 2.0 network: it is in charge of tracking information about the validators , their stakes , their attestations (votes) and if some validators are found to be dishonest, to slash them (they lose some of their stakes). The Beacon Chain is mission-critical and any bug in it could compromise the whole network. The Beacon Chain reference implementation developed by the Ethereum Foundation is written in Python, and provides a detailed operational description of the state machine each Beacon Chain’s network participant (node) must implement. We have formally specified and verified the absence of runtime errors in (a large and critical part of) the Beacon Chain reference implementation using the verification-friendly language Dafny. During the course of this work, we have uncovered several issues, proposed verified fixes. We have also synthesised functional correctness specifications that enable us to provide guarantees beyond runtime errors. Our software artefact with the code and proofs in Dafny is available at https://github.com/ConsenSys/eth2.0-dafny .