This is the repository hosting the code that implements an approach to making symbolic execution on Ethereum smart contracts more scalable. The code is built on top of Mythril and Slither
This is the repository containing the code to prepare for data for Singularity containerization based experiments and the code to extract experiment results.
A bibliography of papers on security and testing of Ethereum smart contracts.
This repository is for collecting and grouping the symbolic execution papers and open source tools in recent years.
The Smart Contract Weakness Classification Registry (SWC Registry) is an implementation of the weakness classification scheme proposed in EIP-1470. It is loosely aligned to the terminologies and structure used in the Common Weakness Enumeration (CWE) while overlaying a wide range of weakness variants that are specific to smart contracts.
The goals of this project are as follows:
Provide a straightforward way to classify security issues in smart contract systems. Define a common language for describing security issues in smart contract systems' architecture, design, or code. Serve as a way to train and increase performance for smart contract security analysis tools.
This is the very first iteration of the Decentralized Application Security Project (or DASP) Top 10 of 2018
This project is an initiative of NCC Group. It is an open and collaborative project to join efforts in discovering smart contract vulnerabilities within the security community. To get involved, join the Github page.
This is the benchmark used in the paper SGUARD: Towards Fixing Vulnerable Smart Contracts Automatically. It contains 5000 contracts whose verified source code are collected from EtherScan. The dataset can be downloaded from this link.
SB Curated is a dataset for research in automated reasoning and testing of smart contracts written in Solidity, the primary language used in Ethereum. It is part of the executional framework SmartBugs, which allows the possibility to integrate tools easily, so that they can be automatically compared (and their results reproduced). To the best of our knowledge, SmartBugs is the largest dataset of its kind.
This repository contains 47,398 smart contracts extracted from the Ethereum network. SmartBugs was used to analyze this dataset. The results are available, please see the ICSE 2020 paper.
SolidiFI-benchmark repository contains a dataset of buggy contracts injected by 9369 bugs from 7 different bug types, namely, reentrancy, timestamp dependency, uhnadeled exceptions, unchecked send, TOD, integer overflow/underflow, and use of tx.origin. The bugs have been injected in the contracts using SolidiFI.
The predominant approach to deciding the bit-vector theory is via eager reduction to propositional logic. While this often works well in practice, it does not scale well as the bit-width and number of operations increase. The first part of this thesis seeks to fill this gap, by exploring efficient techniques of solving bit-vector constraints that leverage the word-level structure. We propose two complementary approaches: an eager approach that takes full advantage of the solving power of off the shelf propositional logic solvers, and a lazy approach that combines on-the-fly algebraic reasoning with efficient propositional logic solvers. In the second part of the thesis, we propose a proof system for encoding automatically checkable refutation proofs in the theory of bit-vectors. These proofs can be automatically generated by the SMT solver, and act as a certificate for the correctness of the result.