Review of six smart contract audit automation tools
Smart contracts are becoming increasingly popular in the world of blockchain technology. They are self-executing contracts with the terms of the agreement between buyer and seller being directly written into lines of code. As such, they need to be carefully designed and tested to ensure that they work as intended and do not contain any security vulnerabilities. This is where smart contract audit automation tools come in, providing a streamlined approach to auditing and testing these contracts. In this article, we review six smart contract audit automation tools.
Mythril is a security analysis tool for EVM bytecode. It detects security vulnerabilities in smart contracts built for Ethereum, Hedera, Quorum, Vechain, Roostock, Tron and other EVM-compatible blockchains. It uses symbolic execution, SMT solving and taint analysis to detect a variety of security vulnerabilities.
Symbolic execution is a technique used in software testing and analysis that involves exploring all possible paths through a program by representing inputs and program states as symbolic expressions rather than concrete values. It is particularly useful in the context of smart contracts, where it can be used to identify potential security vulnerabilities and other issues.
When a program is executed symbolically, inputs and program states are represented as symbolic expressions rather than concrete values. The program is then executed using these symbolic expressions, allowing all possible execution paths to be explored. As the program is executed, the symbolic expressions are modified based on the values that the program encounters, allowing the exploration to continue.
Satisfiability modulo theories (SMT) solving is a technique used in automated theorem proving, software verification, and constraint satisfaction problems. It involves checking the satisfiability of logical formulas that use a combination of different theories, such as arithmetic, arrays, and bitvectors.
In the context of smart contract analysis, SMT solving is used to verify that a contract’s behavior is consistent with its intended design. For example, it can be used to verify that a contract implements a certain algorithm correctly or to check that the contract’s state cannot be manipulated in unintended ways.
Taint analysis is a technique used in software analysis and security to track the flow of data through a program and identify potential vulnerabilities. It works by labeling data that originates from an untrusted source (i.e., “tainted data”) and tracking how that data is propagated through the program.
In the context of smart contract analysis, tainted analysis can be used to identify potential security vulnerabilities by tracking the flow of data through a contract and identifying places where tainted data may be used in unexpected ways. For example, it can be used to identify places where user input is used to calculate a contract’s balance or to detect potential race conditions and reentrancy vulnerabilities
It also provides a user-friendly interface and integrates well with other Ethereum development tools. It’s also used (in combination with other tools and techniques) in the MythX security analysis platform.
Securify 2.0 is a security scanner for Ethereum smart contracts supported by the Ethereum Foundation and ChainSecurity. The core research behind Securify was conducted at the Secure, Reliable, and Intelligent Systems Lab (SRILAB) at ETH Zurich.
It is the successor of the popular Securify security scanner
The tool analyzes contracts written in Solidity >= 0.5.8
It is known to be fully automated, scalable and able to prove whether contract behaviors are safe by verifying the satisfaction of several properties. 37 known vulnerabilities are currently supported by Securify2.
Securify2 proceeds its analysis in several steps. It firstly extracts semantic information about each function of the contract. This process of semantic extraction may involve using natural language processing techniques or other methods to analyze the code and identify the meaning behind each function. This semantic information are composed of facts describing the relations between the variables, the control-flow and the data-flow in order to understand how the functions behave.
Securify2 verifies vulnerabilities into two types of patterns: Compliance and Violation patterns. Compliance patterns define rules that a program must follow to ensure that it behaves correctly and securely, while Violation patterns represent behavior that violates the rules.
By formalizing vulnerabilities into these two patterns, Securify2 can analyze the code to determine whether it complies with the rules or violates them. The tool can then provide feedback on any potential security issues, allowing developers to fix them before the code is deployed. A report containing all warnings and violations is provided to the user of the program.
Slither is a Solidity static analysis framework written in Python3. It does its analysis by using “Detectors” and “Printers”
The tool has a set of built-in checks or detectors that it uses to analyze the bytecode of a smart contract and identify potential vulnerabilities.
These detectors are essentially a set of algorithms that are designed to look for patterns in the code that could indicate security risks. Each detector is focused on a specific type of vulnerability or issue that commonly occurs in smart contracts.
Further, Slither allows printing contracts information through “Printers” which will print visual information about contract details. By providing visual information about contract details and potential issues, Slither helps developers understand the structure and behavior of their contracts and identify potential security risks. This information can be especially helpful for developers who are new to smart contract development or who are working with complex contracts that may have many interdependencies and potential issues.
And finally Slither provides an API to easily write custom analyses.
Manticore is a symbolic execution tool for the analysis of smart contracts and binaries. Manticore can execute a program with symbolic inputs and explore all the possible states it can reach. Manticore can detect crashes and other failure cases in binaries and smart contracts. Manticore provides fine-grained control of state exploration via event callbacks and instruction hooks. Manticore exposes programmatic access to its analysis engine via a Python API
Manticore can analyze the following types of programs:
- Ethereum smart contracts (EVM bytecode)
- Linux ELF binaries (x86, x86_64, aarch64, and ARMv7)
- WASM Modules
Manticore requires Python 3.7 or greater
Echidna is written in the Haskell programming language and is designed for fuzzing and property-based testing of Ethereum smart contracts.
Fuzzing is a technique where random or semi-random input data is generated and fed into a program to see how it responds. The goal of fuzzing is to find bugs or vulnerabilities in the program by generating unexpected or unusual input data. Fuzzing typically does not involve any formal specification of the program’s behavior or properties.
Property-based testing, on the other hand, is a technique where the correctness of a program is tested by specifying a set of properties that the program must satisfy, and then generating input data that satisfies these properties. The goal of property-based testing is to ensure that the program behaves correctly under all conditions by systematically testing it against a wide range of input data. Property-based testing typically involves a formal specification of the program’s behavior or properties.
While fuzzing and property-based testing are different techniques, they can be used together to provide comprehensive test coverage.
Osiris is A tool to detect integer bugs in Ethereum smart contracts. Osiris is based on Oyente. It is a framework that combines symbolic execution and taint analysis, in order to accurately find integer bugs in Ethereum smart contracts.
There are a multitude of different scenarios of integer operations that may result in bugs in Ethereum smart contracts. There are three main classes of integer bugs that may allow a malicious user to steal ether or modify the execution path of a smart contract: 1) arithmetic bugs, 2) truncation bugs and 3) signedness bugs
Arithmetic Bugs are bugs such as integer overflows and underflows and also bugs due to division by zero or modulo zero
Converting a value of one integral type to a narrower integral type which has a shorter range of values may introduce so-called truncation bugs
Converting a signed integer type to an unsigned type of the same width (or vice versa) may introduce signedness bugs
Osiris can take as input the bytecode or Solidity source code of a smart contract. The latter gets internally compiled to EVM bytecode. Osiris outputs whether a contract contains any integer bug (e.g. overflow, underflow, truncation, etc.).
Osiris consists of three main components: symbolic analysis, taint analysis and integer error detection. The symbolic analysis component constructs a Control Flow Graph (CFG) and symbolically executes the different paths of the contract. The symbolic analysis component passes the result of every executed instruction to the taint analysis component as well as to the integer error detection component. The taint analysis component introduces, propagates and checks for taint across stack, memory and storage. The integer error detection component checks whether an integer bug is possible within the executed instruction.
In conclusion, smart contract audit automation tools are crucial in ensuring the security of smart contracts. The six tools reviewed in this article are just a few examples of the many available tools that can help developers identify and address security vulnerabilities in their smart contracts. It is important to use these tools to ensure that smart contracts are secure and function as intended.