From 7aa85f13bbe5f0b340f7177a77b39c87ebcc1f08 Mon Sep 17 00:00:00 2001 From: Mark Mossberg Date: Fri, 22 Dec 2017 12:23:17 -0500 Subject: [PATCH] Clean examples/evm (#661) * Clean examples/evm, add a new one integer_overflow.py -> simple_int_overflow.sol simple_functions.py -> simple_multi_func.sol simple_transaction.py -> simple_value_check.sol * Add umd example --- examples/evm/integer_overflow.py | 37 ------------------------ examples/evm/simple_functions.py | 37 ------------------------ examples/evm/simple_int_overflow.sol | 11 +++++++ examples/evm/simple_multi_func.sol | 13 +++++++++ examples/evm/simple_transaction.py | 43 ---------------------------- examples/evm/simple_value_check.sol | 14 +++++++++ examples/evm/two_tx_ovf.sol | 28 ++++++++++++++++++ examples/evm/umd_example.sol | 30 +++++++++++++++++++ 8 files changed, 96 insertions(+), 117 deletions(-) delete mode 100644 examples/evm/integer_overflow.py delete mode 100644 examples/evm/simple_functions.py create mode 100644 examples/evm/simple_int_overflow.sol create mode 100644 examples/evm/simple_multi_func.sol delete mode 100644 examples/evm/simple_transaction.py create mode 100644 examples/evm/simple_value_check.sol create mode 100644 examples/evm/two_tx_ovf.sol create mode 100644 examples/evm/umd_example.sol diff --git a/examples/evm/integer_overflow.py b/examples/evm/integer_overflow.py deleted file mode 100644 index b1e477a..0000000 --- a/examples/evm/integer_overflow.py +++ /dev/null @@ -1,37 +0,0 @@ -from manticore.seth import ManticoreEVM, IntegerOverflow -m = ManticoreEVM() -m.register_detector(IntegerOverflow()) - -#And now make the contract account to analyze -source_code = ''' -pragma solidity ^0.4.15; -contract Overflow { - uint private sellerBalance=0; - - function add(uint value) returns (uint){ - sellerBalance += value; // complicated math with possible overflow - - // possible auditor assert - assert(sellerBalance >= value); - return sellerBalance; - } -} -''' -#Initialize user and contracts -user_account = m.create_account(balance=1000) -contract_account = m.solidity_create_contract(source_code, owner=user_account, balance=0) - -#First add won't overflow uint256 representation -contract_account.add(m.make_symbolic_value()) - -#Potential overflow -contract_account.add(m.make_symbolic_value()) - -#Let seth know we are not sending more transactions so it can output -# info about running states and global statistics -m.finalize() -print "[+] Look for results in %s"% m.workspace - - - - diff --git a/examples/evm/simple_functions.py b/examples/evm/simple_functions.py deleted file mode 100644 index fabd27a..0000000 --- a/examples/evm/simple_functions.py +++ /dev/null @@ -1,37 +0,0 @@ -from manticore.seth import ManticoreEVM -################ Script ####################### - -m = ManticoreEVM() -m.verbosity(2) -#And now make the contract account to analyze -# cat | solc --bin -source_code = ''' -pragma solidity ^0.4.13; - -contract Test { - event Log(string); - mapping(address => uint) private balances; - - function Test() {} - function target1() public {} - function target2() internal {} - function target3() private {} - function() {} - -} -''' -#Initialize accounts -user_account = m.create_account(balance=1000) -contract_account = m.solidity_create_contract(source_code, owner=user_account) - -symbolic_data = m.make_symbolic_buffer(4) -symbolic_value = None -m.transaction( caller=user_account, - address=contract_account, - value=symbolic_value, - data=symbolic_data - ) - -m.finalize() -print "[+] Look for results in %s"% m.workspace - diff --git a/examples/evm/simple_int_overflow.sol b/examples/evm/simple_int_overflow.sol new file mode 100644 index 0000000..9933cf7 --- /dev/null +++ b/examples/evm/simple_int_overflow.sol @@ -0,0 +1,11 @@ +pragma solidity ^0.4.15; +contract Overflow { + uint private sellerBalance=0; + + function add(uint value) returns (bool, uint){ + sellerBalance += value; // complicated math with possible overflow + + // possible auditor assert + assert(sellerBalance >= value); + } +} diff --git a/examples/evm/simple_multi_func.sol b/examples/evm/simple_multi_func.sol new file mode 100644 index 0000000..22d6549 --- /dev/null +++ b/examples/evm/simple_multi_func.sol @@ -0,0 +1,13 @@ +pragma solidity ^0.4.13; + +contract Test { + event Log(string); + mapping(address => uint) private balances; + + function Test() {} + function target1() public {} + function target2() internal {} + function target3() private {} + function() {} + +} diff --git a/examples/evm/simple_transaction.py b/examples/evm/simple_transaction.py deleted file mode 100644 index 7425a20..0000000 --- a/examples/evm/simple_transaction.py +++ /dev/null @@ -1,43 +0,0 @@ -from manticore.seth import ManticoreEVM -################ Script ####################### - -m = ManticoreEVM() -m.verbosity(0) -#And now make the contract account to analyze -# cat | solc --bin -source_code = ''' -pragma solidity ^0.4.13; - -contract Test { - event Log(string); - - function target() payable public { - if (msg.value > 10) - Log("Value greater than 10"); - else - Log("Value less or equal than 10"); - - } - -} -''' -#Initialize accounts -user_account = m.create_account(balance=1000) -contract_account = m.solidity_create_contract(source_code, owner=user_account) - - -contract_account.target(value=m.SValue) - - -print "[+] There are %d reverted states now"% len(m.final_state_ids) -for state_id in m.final_state_ids: - print m.report(state_id) - -print "[+] There are %d alive states now"% len(m.running_state_ids) -for state_id in m.running_state_ids: - print m.report(state_id) - -print "[+] Global coverage:" -print m.coverage(contract_account) - - diff --git a/examples/evm/simple_value_check.sol b/examples/evm/simple_value_check.sol new file mode 100644 index 0000000..0a0b92e --- /dev/null +++ b/examples/evm/simple_value_check.sol @@ -0,0 +1,14 @@ +pragma solidity ^0.4.13; + +contract Test { + event Log(string); + + function target() payable public { + if (msg.value > 10) + Log("Value greater than 10"); + else + Log("Value less or equal than 10"); + + } + +} diff --git a/examples/evm/two_tx_ovf.sol b/examples/evm/two_tx_ovf.sol new file mode 100644 index 0000000..8808c2a --- /dev/null +++ b/examples/evm/two_tx_ovf.sol @@ -0,0 +1,28 @@ +pragma solidity ^0.4.15; + +contract SymExExample { + uint did_init = 0; + + event Log(string); + + // function id: 0x13371337 + function test_me(int input) { + if (did_init == 0) { + did_init = 1; + Log("initialized"); + return; + } + + if (input < 42) { + // safe + Log("safe"); + return; + } else { + // overflow possibly! + int could_overflow = input + 1; + Log("overflow"); + } + + } +} + diff --git a/examples/evm/umd_example.sol b/examples/evm/umd_example.sol new file mode 100644 index 0000000..25ff1cd --- /dev/null +++ b/examples/evm/umd_example.sol @@ -0,0 +1,30 @@ +// Smart contract based on a classic symbolic execution example from slides +// by Michael Hicks, University of Maryland. +// https://www.cs.umd.edu/~mwh/se-tutorial/symbolic-exec.pdf + +pragma solidity ^0.4.15; + +contract SymExExample { + + + function test_me(int a, int b, int c) public pure { + int x = 0; + int y = 0; + int z = 0; + + if (a != 0) { + x = -2; + } + + if (b < 5) { + if (a == 0 && c != 0) { + y = 1; + } + z = 2; + } + + // will fail when: a == 0 && b < 5 && c != 0 + assert(x + y + z != 3); + } + +}