Solidity Static Analysis
A growing number of industries are using blockchain platforms to perform trustless computation using smart contracts. Applications ranging from financial services to supply chains, and from logistics to healthcare are being developed to rely on blockchain technologies. One of the most popular underlying technologies is the Ethereum smart contact, whitten in Solidity, which are then compiled to Ethereum Virtual Machine (EVM) assembly instructions for blockchain deployment. Often, or more likely usually, the deployed smart contract’s code is insecure: software vulnerabilities are regularly identified, and have been exploited by malicious actors, resulting in millions of dollars in damages and harm to the reputation of blockchain systems.
While modern compilers, offer various APIs on top of which third-party analyzers can be built, the Solidity compiler fails to offer the same features. However, there are several tools that you can use, of which the today's article will talk extensively. The creators of the tools decided to go for the mythological creature names, so here you go - one to rule them all:
Slither
Slither is the first open-source static analysis framework for Solidity. Slither is fast and precise; it can find real vulnerabilities in a few seconds without user intervention. It is highly customizable and provides a set of APIs to inspect and analyze Solidity code easily. If you are a smart-contract developer, a security expert, or an academic researcher, then you will find Slither invaluable. Slither can find real vulnerabilities in a few seconds with minimal or no user interaction. It should be your tool of use, when it comes to reviewing the Solidity code. You can also integrate Slither into your development process without any configuration and run it on each commit to check that you are not adding new bugs.
Slither has a simple command line interface. To run all of its detectors on a Solidity file, this is all you need:
slither contract.sol
or on the entire codebase:
slither .
The most powerful features of Slither, is its set of predefined “printers”, which show high-level information about the contract. There are several out-of-the-box ones to print essential security information: a contract summary, a function summary, a graph of inheritance, and an authorization overview.
Contract summary printer
Gives a quick summary of the contract, showing the functions and their visibility:
Function summary printer
Shows useful information for each function, such as the state variables read and written, or the functions called:
Inheritance printer
Outputs a graph highlighting the inheritance dependencies of all the contracts:
Authorization printer
Shows what a user with privileges can do on the contract:
Echidna
Property based testing
Property based testing frameworks check the truthfulness of properties. A property is a statement like: for all (x, y, ...) such that precondition(x, y, ...) holds predicate(x, y, ...) is true. It checks that a function, program or whatever system under test abides by a property. Property can be seen as a trait you expect to see in your output given the inputs. It does not have to be the expected result itself and most of the time it will not be. A property is just something like:
for all (x, y, ...) such that precondition(x, y, ...) holds predicate(x, y, ...) is true
For example, using properties you might state that:
for any strings a, b and c ;b is a substring of a + b + cProperty based testing frameworks will take this spell as an input and run the check on multiple generated random entries. In case of failure, it should provide both a counterexample and the seed causing the generation.
Solidity property based testing
Now that we know what property-based testing is, Echidna is a program designed for property-based testing of Ethereum smarts contracts. It uses sophisticated grammar-based fuzzing campaigns based on a contract ABI to falsify user-defined predicates or Solidity assertions.
The core Echidna functionality is an executable called echidna-test. echidna-test takes a contract and a list of invariants (properties that should always remain true) as input. For each invariant, it generates random sequences of calls to the contract and checks if the invariant holds. If it can find some way to falsify the invariant, it prints the call sequence that does so. If it can't, you have some assurance the contract is safe.
Writing tests
Echidna properties are Solidity functions. A property must:
- Have no argument
- Return true if it is successful
- Have its name starting with echidna
Echidna will:
- Automatically generate arbitrary transactions to test the property.
- Report any transactions leading a property to return false or throw an error.
- Discard side-effect when calling a property (i.e. if the property changes a state variable, it is discarded after the test)
For example, let's write some token contract and then test it:
contract Token{
mapping(address => uint) public balances;
function airdrop() public{
balances[msg.sender] = 1000;
}
function consume() public{
require(balances[msg.sender]>0);
balances[msg.sender] -= 1;
}
function backdoor() public{
balances[msg.sender] += 1;
}
}
It's better to use inheritance to separate your contract from your properties, so that the contract itself is not cluttered with all the tests:
contract TestToken is Token{
function echidna_balance_under_1000() public view returns(bool){
return balances[msg.sender] <= 1000;
}
}
Echidna needs a constructor without argument. If your contract needs a specific initialization, you need to do it in the constructor.
There are some specific addresses in Echidna:
- 0x00a329c0648769A73afAc7F9381E08FB43dBEA72 which calls the constructor.
- 0x10000, 0x20000, and 0x00a329C0648769a73afAC7F9381e08fb43DBEA70 which randomly calls the other functions.
We do not need any particular initialization in our current example, as a result our constructor is empty. Now let's run our testing:
$ echidna-test testtoken.sol --contract TestToken
...
echidna_balance_under_1000: failed!💥
Call sequence, shrinking (1205/5000):
airdrop()
backdoor()
What it did, was calling randomly the contract method, until it failed. As the backdoor method increases the balance, eventually it reached greater than 1000 and failed the echidna_balance_under_1000 test
Manticore
Dynamic Symbolic Execution
Dynamic symbolic execution (DSE) is a program analysis technique that explores a state space with a high degree of semantic awareness. This technique is based on the discovery of "program paths", represented as mathematical formulas called path predicates. Conceptually, this technique operates on path predicates in two steps:
- They are constructed using constraints on the program's input.
- They are used to generate program inputs that will cause the associated paths to execute.
This approach produces no false positives in the sense, that all identified program states can be triggered during concrete execution. For example, if the analysis finds an integer overflow, it is guaranteed to be reproducible.
Let's start with the path predicate example, to get an insigh of how DSE works:
function f(uint a) {
if (a == 65) {
// A bug is present
}
}
As f() contains two paths, a DSE will construct two differents path predicates:
- Path 1: a == 65
- Path 2: Not (a == 65)
Each path predicate is a mathematical formula that can be given to a so-called SMT solver, which will try to solve the equation. For Path 1, the solver will say that the path can be explored with a = 65. For Path 2, the solver can give a any value other than 65, for example a = 0.
Solidity Dynamic Symbolic Execution
Manticore is a symbolic execution tool for analysis of smart contracts and binaries. Using Manticore one can identify ‘interesting’ code locations and deduce inputs that reach them. This can generate inputs for improved test coverage, or quickly lead execution to a vulnerability.
Manticore allows a full control over all the execution of each path. As a result, it allows to add arbirtray contraints to almost anything. This control allows for the creation of properties on the contract. Consider the following example:
function unsafe_add(uint a, uint b) returns(uint c){
c = a + b; // no overflow protection
return c;
}
Here there is only one path to explore in the function: Path 1: c = a + b. Using Manticore, you can check for overflow, and add constraitns to the path predicate: c = a + b AND (c < a OR c < b). If it is possible to find a valuation of a and b for which the path predicate above is feasible, it means that you have found an overflow. For example the solver can generate the input a = 10 , b = MAXUINT256. If you consider a fixed version:
function safe_add(uint a, uint b) returns(uint c){
c = a + b;
require(c>=a);
require(c>=b);
return c;
}
The associated formula with overflow check would be: c = a + b AND (c >= a) AND (c=>b) AND (c < a OR c < b) This formula cannot be solved; in other world this is a proof that in safe_add, c will always increase. DSE is thereby a powerful tool, that can verify arbitrary constraints on your code.
We will see how to explore a smart contract with the Manticore API. The target is the following smart contract:
contract Simple {
function f(uint a) payable public{
if (a == 65) {
revert();
}
}
}
You can run Manticore directly on the smart contract by the following command (project can be a Solidity File, or a project directory) and will get the output of testcases:
$ manticore project ... ... m.c.manticore:INFO: Generated testcase No. 0 - STOP ... m.c.manticore:INFO: Generated testcase No. 1 - REVERT ... m.c.manticore:INFO: Generated testcase No. 2 - RETURN ... m.c.manticore:INFO: Generated testcase No. 3 - REVERT ... m.c.manticore:INFO: Generated testcase No. 4 - STOP ... m.c.manticore:INFO: Generated testcase No. 5 - REVERT ... m.c.manticore:INFO: Generated testcase No. 6 - REVERT ...
Manticore will explore the contract with new symbolic transactions until it does not explore new paths on the contract. Manticore does not run new transactions after a failing one (e.g: after a revert). Manticore will output the information in a mcore_* directory. Among other, you will find in this directory:
- global.summary: coverage and compiler warnings
- test_XXXXX.summary: coverage, last instruction, account balances per test case
- test_XXXXX.tx: detailed list of transactions per test case
Here Manticore founds 7 test cases, which correspond to:
| Transaction 0 | Transaction 1 | Transaction 2 | Result | |
| test_00000000.tx | Contract creation | f(!=65) | f(!=65) | STOP |
| test_00000001.tx | Contract creation | fallback function | REVERT | |
| test_00000002.tx | Contract creation | RETURN | ||
| test_00000003.tx | Contract creation | f(65) | REVERT | |
| test_00000004.tx | Contract creation | f(!=65) | STOP | |
| test_00000005.tx | Contract creation | f(!=65) | f(65) | REVERT |
| test_00000006.tx | Contract creation | f(!=65) | fallback function | REVERT |
Exploration summary f(!=65) denotes f called with any value different than 65. As you can notice, Manticore generates an unique test case for every successful or reverted transaction.
Manipulate a smart contract through the API
To explore the code further, let's assume that the documentation of f() states that the function is never called with a == 65, so any bug with a == 65 is not a real bug. We'll now use Manticore API to know if a constraint is still feasible. For example, the following will constraint symbolic_value to be different from 65 and check if the state is still feasible. Use state.constrain(constraint) to add a constraint to a specific state It can be used to constrain the state after its exploration to check some property on it.
from manticore.ethereum import ManticoreEVM
from manticore.core.smtlib.solver import Z3Solver
solver = Z3Solver.instance()
m = ManticoreEVM()
with open("example.sol") as f:
source_code = f.read()
user_account = m.create_account(balance=1*10**18)
contract_account = m.solidity_create_contract(source_code, owner=user_account)
symbolic_var = m.make_symbolic_value()
contract_account.f(symbolic_var)
no_bug_found = True
## Check if an execution ends with a REVERT or INVALID
for state in m.terminated_states:
last_tx = state.platform.transactions[-1]
if last_tx.result in ['REVERT', 'INVALID']:
# we do not consider the path were a == 65
condition = symbolic_var != 65
if m.generate_testcase(state, name="BugFound", only_if=condition):
print(f'Bug found, results are in {m.workspace}')
no_bug_found = False
if no_bug_found:
print(f'No bug found')
Conclusion
Doing code analysis is boring, annoying and not really rewarding - I mean, at most, you'll find a bug. But, if you have decided to workin the blockchain space, this should be a mandatory step in your software development life cycle (SDLC).
Comments
Post a Comment