Solidity Static Analysis

Slither

slither contract.sol
slither .

Contract summary printer

Function summary printer

Inheritance printer

Authorization printer

Echidna

Property based testing

Solidity property based testing

Writing tests

  • Have no argument
  • Return true if it is successful
  • Have its name starting with echidna
  • 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)
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;
}
}
contract TestToken is Token {
function echidna_balance_under_1000() public view returns(bool) {
return balances[msg.sender] <= 1000;
}
}
  • 0x00a329c0648769A73afAc7F9381E08FB43dBEA72 which calls the constructor.
  • 0x10000, 0x20000, and 0x00a329C0648769a73afAC7F9381e08fb43DBEA70 which randomly calls the other functions.
$ echidna-test testtoken.sol --contract TestToken ... echidna_balance_under_1000: failed!💥 Call sequence, shrinking (1205/5000): airdrop() backdoor()

Manticore

Dynamic Symbolic Execution

  • 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.
function f(uint a) { if (a == 65) { // A bug is present } }

Solidity Dynamic Symbolic Execution

function unsafe_add(uint a, uint b) returns(uint c) {
c = a + b; // no overflow protection return c;
}
function safe_add(uint a, uint b) returns(uint c) {
c = a + b;
require(c >= a);
require(c >= b);
return c;
}
contract Simple {
function f(uint a) payable public {
if (a == 65) {
revert();
}
}
}
$ 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 ...
  • 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

Manipulate a smart contract through the API

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

--

--

--

Love podcasts or audiobooks? Learn on the go with our new app.

Get the Medium app

A button that says 'Download on the App Store', and if clicked it will lead you to the iOS App store
A button that says 'Get it on, Google Play', and if clicked it will lead you to the Google Play store
Victor Genin

Victor Genin

More from Medium

Detailed explanation of Ethereum smart contract vulnerabilities:On-chain recurring vulnerabilities

Re-entrancy — Still a significant problem ?

Ethernaut — Level 20— Denial

“Audit in progress”