Merge branch 'master' into native-arb-cf-redirect-detector

* master: Improve performance of bulk read/writes to memory (#1509) Fixes ConstraintSet.new_bitvec size check (#1511) Fix operators.ORD for BitVecs of size > 8 (#1512) Removed redeclared smtlibv2 tests (#1513) Update manticore.py (#1508) Improve smemory tests (#1506) Manticore 0.3.1 (#1503) Optimize repeated division in CMPXCHG8B (#1501) Detecting the use of BALANCE in a strict comparison (#1481) Initial master merge into experimental state merging for native (#1482) Update crackme example to match the description (#1502) Add SHL/SHR/SAR (#1498) Add deprecation warnings for outdated API members (#1500) Patching STAICCALL (#1494) WIP: Support lsr.w on ARMv7 THUMB (#1363) Update evm examples (#1486) Logic Bomb Bugfixes (#1485) Add error for unsupported solc versions (#1488) Fix documentation typo in ManticoreBase (#1492) Add crytic-compile support (#1406)
trailofbits · Aug 27, 2019 · 806bbfa · 806bbfa
2 parents c45c56b + 6171924
commit 806bbfa
Show file tree

Hide file tree

Showing 46 changed files with 2,108 additions and 413 deletions.
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -1,6 +1,32 @@
 # Change Log
 
-## [Unreleased](https://github.com/trailofbits/manticore/compare/0.3.0...HEAD)
+## [Unreleased](https://github.com/trailofbits/manticore/compare/0.3.1...HEAD)
+
+## 0.3.1 - 2019-08-06
+
+Thanks to our external contributors!
+
+ - [arcz](https://github.com/trailofbits/manticore/commits?author=arcz)
+
+### Ethereum
+* Smart contracts are now compiled using [Crytic-Compile](https://github.com/crytic/crytic-compile) [#1406](https://github.com/trailofbits/manticore/pull/1406)
+* Added detector for strict comparisons to BALANCE [#1481](https://github.com/trailofbits/manticore/pull/1481)
+* Added bitshift instructions [#1498](https://github.com/trailofbits/manticore/pull/1498)
+* Added stub for STATICCALL (does not enforce static nature) [#1494](https://github.com/trailofbits/manticore/pull/1494)
+* Updated EVM Examples [#1486](https://github.com/trailofbits/manticore/pull/1486)
+
+### Native
+* Fixed `getdents` syscall [#1472](https://github.com/trailofbits/manticore/pull/1472)
+* Fixed state merging examples [#1482](https://github.com/trailofbits/manticore/pull/1482)
+* Support LSR.W on ARMV7 [#1363](https://github.com/trailofbits/manticore/pull/1363)
+* Fixed CrackMe Example [#1502](https://github.com/trailofbits/manticore/pull/1502)
+* Optimize CMPXCHG8B [#1501](https://github.com/trailofbits/manticore/pull/1501)
+* Added `fast_crash` configuration setting that causes Manticore to immediately produce a finding on memory unsafety [#1485](https://github.com/trailofbits/manticore/pull/1485)
+
+### Other
+* **[changed API]** Moved `issymbolic` into SMTLib to improve performance [#1456](https://github.com/trailofbits/manticore/pull/1456)
+* Refactored API Docs [#1469](https://github.com/trailofbits/manticore/pull/1469)
+* Fixed `FileNotFound` Error on state loading [#1480](https://github.com/trailofbits/manticore/pull/1480)
 
 ## 0.3.0 - 2019-06-06
 

diff --git a/README.md b/README.md
@@ -76,7 +76,7 @@ value = m.make_symbolic_value()
 
 contract_account.incremented(value)
 
-for state in m.running_states:
+for state in m.ready_states:
     print("can value be 1? {}".format(state.can_be_true(value == 1)))
     print("can value be 200? {}".format(state.can_be_true(value == 200)))
 ```
@@ -98,7 +98,7 @@ def hook(state):
   print('eax', cpu.EAX)
   print(cpu.read_int(cpu.ESP))
 
-  m.terminate()  # tell Manticore to stop
+  m.kill()  # tell Manticore to stop
 
 m.run()
 ```
@@ -215,6 +215,10 @@ brew install unicorn
 UNICORN_QEMU_FLAGS="--python=`whereis python`" pip install unicorn
 ```
 
+### Solidity Versions
+Note that we're still in the process of implementing full support for the EVM Constantinople instruction semantics, so certain opcodes may not be supported.
+You may want to consider using a version of `solc` that's less likely to generate these opcodes (eg pre-0.5.0).
+
 ## Getting Help
 
 Feel free to stop by our #manticore slack channel in [Empire Hacking](https://empireslacking.herokuapp.com/) for help using or extending Manticore.

diff --git a/docs/conf.py b/docs/conf.py
@@ -54,9 +54,9 @@
 # built documents.
 #
 # The short X.Y version.
-version = "0.3.0"
+version = "0.3.1"
 # The full version, including alpha/beta/rc tags.
-release = "0.3.0"
+release = "0.3.1"
 
 # The language for content autogenerated by Sphinx. Refer to documentation
 # for a list of supported languages.

diff --git a/examples/evm/complete.py b/examples/evm/complete.py
@@ -37,7 +37,7 @@
 )
 
 print("[+] Resulting balances are:")
-for state in m.running_states:
+for state in m.all_states:
     balance = state.platform.get_balance(int(user_account))
     print(state.solve_one(balance))
 

diff --git a/examples/evm/coverage.py b/examples/evm/coverage.py
@@ -29,7 +29,7 @@
 )
 
 print(f"[+] There are {m.count_terminated_states()} reverted states now")
-print(f"[+] There are {m.count_running_states()} alive states now")
+print(f"[+] There are {m.count_busy_states()} alive states now")
 # for state_id in m.running_state_ids:
 #     print(m.report(state_id))
 

diff --git a/examples/evm/reentrancy_concrete.py b/examples/evm/reentrancy_concrete.py
@@ -10,14 +10,14 @@
 
 contract Reentrance {
     mapping (address => uint) userBalance;
-   
+
     function getBalance(address u) constant returns(uint){
         return userBalance[u];
     }
 
     function addToBalance() payable{
         userBalance[msg.sender] += msg.value;
-    }   
+    }
 
     function withdrawBalance(){
         // send userBalance[msg.sender] ethers to msg.sender
@@ -26,9 +26,9 @@
            revert();
         }
         userBalance[msg.sender] = 0;
-    }   
+    }
 }
-//Function signatures: 
+//Function signatures:
 //c0e317fb: addToBalance()
 //f8b2cb4f: getBalance(address)
 //5fd8c710: withdrawBalance()
@@ -38,7 +38,7 @@
 pragma solidity ^0.4.15;
 
 contract GenericReentranceExploit {
-    int reentry_reps=10; 
+    int reentry_reps=10;
     address vulnerable_contract;
     address owner;
     bytes reentry_attack_string;
@@ -87,7 +87,8 @@
 contract_account = m.solidity_create_contract(
     contract_source_code, owner=user_account
 )  # Not payable
-m.world.set_balance(contract_account, 1000000000000000000)  # give it some ether
+for i in m.all_states:
+    i.platform.set_balance(contract_account, 1000000000000000000)  # give it some ether
 
 exploit_account = m.solidity_create_contract(exploit_source_code, owner=attacker_account)
 
@@ -101,16 +102,18 @@
 exploit_account.set_reentry_attack_string(reentry_string)
 
 print("[+] Initial world state")
-print(
-    f" attacker_account {attacker_account.address:x} balance: {m.get_balance(attacker_account.address)}"
-)
-print(
-    f" exploit_account {exploit_account.address} balance: {m.get_balance(exploit_account.address)}"
-)
-print(f" user_account {user_account.address:x} balance: {m.get_balance(user_account.address)}")
-print(
-    f" contract_account {contract_account.address:x} balance: {m.get_balance(contract_account.address)}"
-)
+for i in m.all_states:
+    i = i.platform
+    print(
+        f" attacker_account {attacker_account.address:x} balance: {i.get_balance(attacker_account.address)}"
+    )
+    print(
+        f" exploit_account {exploit_account.address} balance: {i.get_balance(exploit_account.address)}"
+    )
+    print(f" user_account {user_account.address:x} balance: {i.get_balance(user_account.address)}")
+    print(
+        f" contract_account {contract_account.address:x} balance: {i.get_balance(contract_account.address)}"
+    )
 
 
 # User deposits all in contract
@@ -127,13 +130,15 @@
 print("[+] Let attacker destroy the exploit contract and profit")
 exploit_account.get_money()
 
-print(
-    f" attacker_account {attacker_account.address:x} balance: {m.get_balance(attacker_account.address)}"
-)
-print(f" user_account {user_account.address:x} balance: {m.get_balance(user_account.address)}")
-print(
-    f" contract_account {contract_account.address:x} balance: {m.get_balance(contract_account.address)}"
-)
+for i in m.all_states:
+    i = i.platform
+    print(
+        f" attacker_account {attacker_account.address:x} balance: {i.get_balance(attacker_account.address)}"
+    )
+    print(f" user_account {user_account.address:x} balance: {i.get_balance(user_account.address)}")
+    print(
+        f" contract_account {contract_account.address:x} balance: {i.get_balance(contract_account.address)}"
+    )
 
 m.finalize()
 print(f"[+] Look for results in {m.workspace}")
diff --git a/examples/evm/use_def.py b/examples/evm/use_def.py
@@ -5,7 +5,6 @@
 ################ Script #######################
 
 m = ManticoreEVM()
-m.verbosity(0)
 # And now make the contract account to analyze
 # cat  | solc --bin
 source_code = """
@@ -18,80 +17,63 @@
         c =0;
         enabled = false;
         i = false;
-        
+
     }
     function f1() public {
         c+=1;
     }
     function f2() public {
         if(c>100)
             enabled=true;
-        
+
     }
     function f3() public{
-        if (!enabled) 
+        if (!enabled)
             return;
         i = true;
-        
+
     }
 }
 """
 print(source_code)
 
 
 class EVMUseDef(Plugin):
-    def _get_concrete_hex(self, state, array):
-        r = ""
-        for i in array:
-            l = state.solve_n(i, 2)
-            if len(l) == 1:
-                r += "%02x" % l[0]
-        if len(r) != 8:
-            return
-        return r
-
     def did_evm_write_storage_callback(self, state, address, offset, value):
         m = self.manticore
         world = state.platform
         tx = world.all_transactions[-1]
         md = m.get_metadata(tx.address)
-
-        r = self._get_concrete_hex(state, tx.data[0:4])
-        if r is None:
-            return
-
-        offsets = state.solve_n(offset, 3000)
-        with self.locked_context("storage_writes", dict) as storage_writes:
-            contract_function = (md.name, md.get_func_name(r))
-            if contract_function not in storage_writes:
-                storage_writes[contract_function] = set()
-            for off in offsets:
-                storage_writes[contract_function].add(off)
+        if md:
+            offsets = state.solve_n(offset, 3000)
+            with self.locked_context("storage_writes", dict) as storage_writes:
+                contract_function = (md.name, md.get_func_name(state.solve_one(tx.data[0:4])))
+                if contract_function not in storage_writes:
+                    storage_writes[contract_function] = set()
+                for off in offsets:
+                    storage_writes[contract_function].add(off)
 
     def did_evm_read_storage_callback(self, state, address, offset, value):
         m = self.manticore
         world = state.platform
         tx = world.all_transactions[-1]
         md = m.get_metadata(tx.address)
+        if md:
+            offsets = state.solve_n(offset, 3000)
+            with self.locked_context("storage_reads", dict) as storage_reads:
+                contract_function = (md.name, md.get_func_name(state.solve_one(tx.data[0:4])))
+                if contract_function not in storage_reads:
+                    storage_reads[contract_function] = set()
+                for off in offsets:
+                    storage_reads[contract_function].add(off)
 
-        r = self._get_concrete_hex(state, tx.data[0:4])
-        if r is None:
-            return
-
-        offsets = state.solve_n(offset, 3000)
-        with self.locked_context("storage_reads", dict) as storage_reads:
-            contract_function = (md.name, md.get_func_name(r))
-            if contract_function not in storage_reads:
-                storage_reads[contract_function] = set()
-            for off in offsets:
-                storage_reads[contract_function].add(off)
 
+p = EVMUseDef()
+m.register_plugin(p)
 
 # Initialize accounts
 user_account = m.create_account(balance=1000)
 contract_account = m.solidity_create_contract(source_code, owner=user_account)
-p = EVMUseDef()
-m.register_plugin(p)
 
 symbolic_data = m.make_symbolic_buffer(320)
 symbolic_value = m.make_symbolic_value()

diff --git a/examples/linux/Makefile b/examples/linux/Makefile
@@ -6,7 +6,7 @@ PYTHON=python3
 EXAMPLES=basic sindex  strncmp  arguments ibranch sendmail crackme indexhell  helloworld simple_copy simpleassert
 OTHER_EXAMPLES=nostdlib
 
-all: $(EXAMPLES) $(OTHER_EXAMPLES) 
+all: $(EXAMPLES) $(OTHER_EXAMPLES)
 
 arm: CC=arm-linux-gnueabi-gcc
 arm: $(EXAMPLES)
@@ -21,7 +21,7 @@ clean:
 % : %.c
 	$(CC) $(CFLAGS) $< -o $@
 
-nostdlib: nostdlib.c 
+nostdlib: nostdlib.c
 	$(CC) -m32 $(NOSTDLIBFLAGS) $< -o $@
 
 # simpleassert needs -O0
@@ -32,3 +32,5 @@ simpleassert: simpleassert.c
 crackme.c: crackme.py
 	$(PYTHON) crackme.py > $@
 
+crackme: crackme.c
+	$(CC) $(CFLAGS) -O0 $< -o $@
diff --git a/examples/linux/basic_state_merging.c b/examples/linux/basic_state_merging.c
@@ -0,0 +1,63 @@
+/**
+ * Symbolic values are read from stdin using standard libc calls.
+ * Program compares if two binary packed integers at the input with 0x41.
+ *
+ * Compile with :
+ *   $ gcc -static -Os basic_statemerging.c -o basic_statemerging
+ *
+ * Analyze it with:
+ *   $ python examples/script/basic_statemerging.py examples/linux/basic_statemerging
+ *
+ *   The Merger plugin used in basic_statemerging.py will find two states with state IDs 2, 4 to be at the same program
+ *   location (0x40060d) and merge their CPU states which should only require the value for RDI to be merged.
+ *
+ * Expected output:
+ *  $ python /Users/vaibhav/git_repos/manticore/examples/script/basic_statemerging.py examples/linux/basic_statemerging-Os
+      about to load state_id = 0
+      loaded state_id = 0 at cpu = 0x4008e0
+      about to load state_id = 1
+      loaded state_id = 1 at cpu = 0x400604
+      about to load state_id = 2
+      Merged registers:
+      RDI
+      at PC = 0x40060d, merge succeeded for state id = 2 and 4
+      loaded state_id = 2 at cpu = 0x40060d
+      about to load state_id = 3
+      loaded state_id = 3 at cpu = 0x400612
+ *
+*/
+
+#include <stdio.h>
+#include <stdlib.h>
+#include <unistd.h>
+#include <stdbool.h>
+
+ int main(int argc, char* argv[], char* envp[]){
+    unsigned int cmd1, cmd2;
+    unsigned int cmdChanged = 0;
+
+     if (read(0, &cmd1, sizeof(cmd1)) != sizeof(cmd1))
+    {
+        printf("Error reading stdin!");
+        exit(-1);
+    }
+    if (read(0, &cmd2, sizeof(cmd2)) != sizeof(cmd2))
+    {
+        printf("Error reading stdin!");
+        exit(-1);
+    }
+
+     if (cmd1 > 0x41)
+    {
+        cmdChanged = cmd1 - 0x42;
+    }
+    if (cmd2 < 0x41)
+    {
+        cmdChanged = cmd2 + 0x42;
+    }
+
+     if (cmdChanged == 0) printf("equal\n");
+    else printf("not equal\n");
+
+     return 0;
+}