Release of Securify v2.0
We are happy to announce Securify v2.0, the new release of the popular security scanner for Ethereum smart contracts.
Securify v2.0 outperforms state-of-the-art vulnerability scanners for smart contracts by bringing:
- High precision, thanks to a brand new intermediate representation (IR) for Solidity and fully declarative context-sensitive static analysis;
- Improved scalability, leveraging a fully declarative static analysis powered by the efficient Souffle Datalog engine;
- High vulnerability coverage, covering 37 distinct security properties adopted from the Smart Contract Weakness Classification Registry and classified by their severity.
Importantly, Securify v2.0 remains free and open-source. You can download Securify v2.0 for free on GitHub.
What does Securify v2.0 support?
- Ethereum smart contracts written in Solidity 0.5.* and 0.6.*
- 37 vulnerabilities classified by their severity (the full list of supported vulnerabilities is at the bottom of this article)
What is new in Securify v2.0?
We now discuss the key technical details and improvements added to Securify v2.0. These make Securify the most comprehensive and extensible static analyzer for Solidity.
1. Source code analysis with a new Intermediate Representation
In contrast to the first version of the tool, Securify v2.0 analyzes source code, not EVM bytecode. While analyzing Solidity source code is more difficult due to the richer structure of the language, it captures important semantic information that is missing in the bytecode. Importantly, Solidity precisely captures the storage model of a contract, allowing clear distinction between variables and mappings, information which is not present in the low-level hash-based storage model used in the bytecode.
To deal with the complexity of the Solidity language, Securify v2.0 compiles Solidity into a new clean and concise Intermediate Representation (IR) for Solidity. The new IR is based on the MLton compiler for Standard ML and features:
- Control-flow graph (CFG) over basic blocks;
- Basic blocks resemble continuations, usually seen in continuation-passing style, where each block accepts arguments and has a pointer to the next block in the form of a transfer that can pass arguments;
- Static single assignment (SSA) form for variables and three-address code style for statements.
To illustrate the IR, consider the following Solidity code:
contract ToyExample{ function inc(uint x) internal returns (uint){ return x+1; } function main() external{ uint res; for(uint i = 0; i < 42; i++){ res = inc(i); require(res > 0); } }}
Securify v2.0 uses the Solidity compiler to obtain the AST of the contract and to then transforms it into the following intermediate representation:
The code follows the single static assignment form (SSA) assigning the result of each operation to a fresh variable (identified by the statement’s label). The code is divided into multiple basic blocks. BLOCK00 corresponds to the definition of function inc and BLOCK01 to the definition of the main function. Variables are passed between the blocks in the form of arguments (see annotated edges). This representation is concise, with a limited number of node types, maintaining only the information necessary for the analysis. The IR is complete, in the sense that any Solidity smart contract can be mapped to it.
2. Higher precision via call-site sensitivity
Securify v2.0 achieves higher precision via call-site sensitivity. To get a better idea of what call-site sensitivity is and how it benefits our analysis, consider the following example:
contract CallSitesTest { mapping(address => uint) aMapping; function id(address x) public returns (address){ return x; } function unrestrictedStorage(address arbitraryAddress) external{ address a = id(arbitraryAddress); aMapping[a] = 1; } function restrictedStorage(address arbitraryAddress) external { address b = id(msg.sender); aMapping[b] = 1; }}
In the example above, functions unrestrictedStorage and restrictedStorage accept an arbitrary address as an argument from the user. Note that function unrestrictedStorage allows anyone to write to an arbitrary location in the storage, while function restrictedStorage allows a user can write only to aMapping[msg.sender] in the storage (where msg.sender is the user’s address). To identify this vulnerability, Securify v2.0 tags user-provided values as untrusted (in this example, it taints arbitraryAddress) and propagates the tag along the program’s dependency graph. A precise analysis would identify that address a is untrusted, reporting function unrestrictedStorage as vulnerable, while address b is trusted, reporting function restrictedStorage as safe.
The first version of Securify uses call-site insensitive analysis which tags the return value of function id as untrusted, because it returns the value of arbitraryAddress when function id is called by function unrestrictedStorage. In particular, the analysis does not differentiate whether the function id is called from function unrestrictedStorage or function restrictedStorage. As a result of this imprecision, the analysis reports the restrictedStorage function as vulnerable too.
In contrast, Securify v2.0 differentiates whether the function id is called from the function unrestrictedStorage or restrictedStorage (hence the name call-site sensitive). The additional precision correctly identifies that address b is not untrusted and, in turn, the function restrictedStorage is correctly marked as safe.
3. Improved scalability via fully declarative analysis
The first version of Securify implements deeper vulnerability checks in a combination of Java and Datalog. This slows down the analysis because it requires passing all intermediate Datalog results to Java.
In contrast, the analysis of Securify v2.0 is fully declarative and implemented in Datalog. This greatly improves the performance and scalability of the analysis. Moreover, the fully declarative analysis improves Securify’s maintenance and extensibility as the declarative patterns are easier to specify.
4. Higher vulnerability coverage
Securify v2.0 supports 37 known vulnerability patterns. It classifies them into five severity levels: critical, high, medium, low, and info. Similarly to the first version of the tool, Securify v2.0 reports violations, which are behaviors that are guaranteed to violate a given security property, and warnings, which behaviors that may violate the security property.
How to use Securify v2.0?
The easiest way to use Security v2.0 using its Docker image as follows:
docker run -it -v `pwd`:/share securify /share/myContract.solAn alternative method to install Securify v2.0 as python package following the instructions on GitHub:
securify myContract.solIn addition to analyzing a Solidity contract, Securify v2.0 can analyze any contract available on Etherscan.io:
securify -b <contractAddress> — key /path/to/api_key.txtUsers can control which severity levels should be reported by Securify using the -i argument:
securify myContract.sol -i CRITICAL HIGHFurther, users can specify which vulnerability to check for using the -p argument:
securify myContract.sol -p LockedEtherFor further help, you can check out the README instructions on GitHub.
Supported vulnerabilities
Securify v2.0 supports the following vulnerabilities:
|----|-----------------------------------| ---------|---------|
| ID | Pattern name | Severity | SWC ID |
|----|-----------------------------------| ---------|---------|
| 1 | TODAmount | Critical | SWC-114 |
| 2 | TODReceiver | Critical | SWC-114 |
| 3 | TODTransfer | Critical | SWC-114 |
| 4 | UnrestrictedWrite | Critical | SWC-124 |
| 5 | RightToLeftOverride | High | SWC-130 |
| 6 | ShadowedStateVariable | High | SWC-119 |
| 7 | UnrestrictedSelfdestruct | High | SWC-106 |
| 8 | UninitializedStateVariable | High | SWC-109 |
| 9 | UninitializedStorage | High | SWC-109 |
| 10 | UnrestrictedDelegateCall | High | SWC-112 |
| 11 | DAO | High | SWC-107 |
| 12 | ERC20Interface | Medium | - |
| 13 | ERC721Interface | Medium | - |
| 14 | IncorrectEquality | Medium | SWC-132 |
| 15 | LockedEther | Medium | - |
| 16 | ReentrancyNoETH | Medium | SWC-107 |
| 17 | TxOrigin | Medium | SWC-115 |
| 18 | UnhandledException | Medium | - |
| 19 | UnrestrictedEtherFlow | Medium | SWC-105 |
| 20 | UninitializedLocal | Medium | SWC-109 |
| 21 | UnusedReturn | Medium | SWC-104 |
| 22 | ShadowedBuiltin | Low | - |
| 23 | ShadowedLocalVariable | Low | - |
| 24 | CallToDefaultConstructor | Low | - |
| 25 | CallInLoop | Low | SWC-104 |
| 26 | ReentrancyBenign | Low | SWC-107 |
| 27 | Timestamp | Low | SWC-116 |
| 28 | AssemblyUsage | Info | - |
| 29 | ERC20Indexed | Info | - |
| 30 | LowLevelCalls | Info | - |
| 31 | NamingConvention | Info | - |
| 32 | SolcVersion | Info | SWC-103 |
| 33 | UnusedStateVariable | Info | - |
| 34 | TooManyDigits | Info | - |
| 35 | ConstableStates | Info | - |
| 36 | ExternalFunctions | Info | - |
| 37 | StateVariablesDefaultVisibility | Info | SWC-108 |
|----|-----------------------------------| ---------|---------|The following SWC vulnerabilities do not apply to Solidity contracts with pragma >=0.8 and are therefore not checked by Securify v2.0:
- SWC-118 (Incorrect Constructor Name)
- SWC-129 (Usage of +=)
How can I contribute?
Securify v2.0 is available on GitHub at https://github.com/eth-sri/securify2.
To contribute, please report any issues and bugs you have encountered while using the tool.
Acknowledgments
The following people have contributed to Securify v2.0:
- Ioannis Sachinoglou
- Lavrentios Frobeen
- Frederic Vogel
- Dimitar Dimitrov
- Petar Tsankov
The team would also like to thank the Ethereum Foundation, which partially funded the development of Securify v2.0.
