update gigahorse and begin code env tracer

README.md

@@ -70,7 +70,7 @@ An Attacker Contract Identification Tool Implemented in Rust based on [BlockWatc
 
 -   gigahorse-toolchain
 
-    Lydia requires Gigahorse to be set up for analyzing EVM bytecode. To set up Gigahorse, refer to its [repository](https://github.com/nevillegrech/gigahorse-toolchain).
+    Lydia requires Gigahorse (commit da473f3) to be set up for analyzing EVM bytecode. To set up Gigahorse, refer to its [repository](https://github.com/nevillegrech/gigahorse-toolchain).
 
 <!-- <img align="left" width="213" src="logo.png"> -->
 

gigahorse-toolchain/.gitignore

@@ -59,3 +59,5 @@ results.json
 
 # sqlite databases
 *.sqlite
+
+contracts/*.hex

gigahorse-toolchain/clientlib/dominators.dl

@@ -331,9 +331,10 @@ FunctionReachableFromPublic(callee, selector, @list_append(callerStack, callerBl
 FunctionReachableFromPublic_Metadata(function, selectorNorm, nil, nil, nil):-
   PublicFunctionId(function, selectorNorm, _).
 
-FunctionReachableFromPublic_Metadata(callee, selector, @list_append(callerStack, callerBlock), @list_append(originalCalls, original), @list_append(functionsCalled, callee)):-
+FunctionReachableFromPublic_Metadata(callee, selector, @list_append(callerStack, callerBlock), @list_concat(originalCalls, originalList), @list_append(@list_concat(functionsCalled, inlinedFuns), callee)):-
   FunctionReachableFromPublic_Metadata(caller, selector, callerStack, originalCalls, functionsCalled),
   InFunction(callerBlock, caller),
   CallGraphEdge(callerBlock, callee),
   Block_Tail(callerBlock, callStmt),
-  Statement_OriginalStatement(callStmt, original).
+  Statement_OriginalStatementList(callStmt, originalList),
+  Statement_InlineInfo(callStmt, inlinedFuns).

gigahorse-toolchain/clientlib/flows.dl

@@ -89,8 +89,8 @@
 
    // Case: forward inter-procedural assignment only
    GlobalFlows(from, to) :-
-      InterFunctionActualArgFlow(actual, to),
-      GlobalFlows(from, actual).
+      GlobalFlows(from, actual),
+      InterFunctionActualArgFlow(actual, to).
 }
 
 .init standardflowanalysis = GlobalFlowAnalysis

gigahorse-toolchain/clientlib/memory_modeling/arrays.dl

@@ -925,10 +925,9 @@ Array_ElementLength(actual, elementSize):-
   ActualReturnArgs(caller, actual, index).
 
 /**
-  Constant arrays and their contents.
+  Constant arrays and their contents. This is mainly useful to find debug messages.
+  Note that such bytearrays are right padded.
 **/
-
-
 .decl ConstArray_Contents(arrayRep:ArrayVariable, hex:symbol)
 
 MemoryModelingTempStmt(mstore),
@@ -937,6 +936,7 @@ ConstArray_Contents(arrayRep, substr(val, 0, strlen(val) + 2*(length - 32))):-
   VarIsArray(arrayVar, arrayRep),
   length > 0,
   length <= 32,
+  strlen(val) + 2*(length - 32) > 2,
   ArrayWriteToRelativeIndex(arrayVar, mstore, 0),
   MSTORE(mstore, _, storedVar),
   Variable_Value(storedVar, val).
@@ -947,7 +947,7 @@ MemoryModelingTempStmt(mstore2),
 ConstArray_Contents(arrayRep, val):-
   ArrayHasConstantLength(arrayRep, length),
   VarIsArray(arrayVar, arrayRep),
-  length > 0,
+  length > 32,
   length <= 64,
   ArrayWriteToRelativeIndex(arrayVar, mstore1, 0),
   MSTORE(mstore1, _, storedVar1),
@@ -963,7 +963,7 @@ MemoryModelingTempStmt(mstore3),
 ConstArray_Contents(arrayRep, val):-
   ArrayHasConstantLength(arrayRep, length),
   VarIsArray(arrayVar, arrayRep),
-  length > 0,
+  length > 64,
   length <= 96,
   ArrayWriteToRelativeIndex(arrayVar, mstore1, 0),
   MSTORE(mstore1, _, storedVar1),

gigahorse-toolchain/clientlib/tac_instructions.dl

@@ -82,6 +82,7 @@ MAKEUNOP(BALANCE).
 MAKEUNOP(CALLDATALOAD).
 MAKEUNOP(MLOAD).
 MAKEUNOP(SLOAD).
+MAKEUNOP(TLOAD).
 
 MAKEUNARITHOP(ISZERO).
 MAKEUNARITHOP(NOT).
@@ -161,12 +162,17 @@ MSIZE(stmt, to):-
   Statement_Defines(stmt, to, 0).
 
 .decl SSTORE(stmt: Statement, index: Variable, var: Variable)
-
 SSTORE(stmt, index, var) :-
   Statement_Opcode(stmt,"SSTORE"),
   Statement_Uses(stmt, index, 0),
   Statement_Uses(stmt, var, 1).
 
+.decl TSTORE(stmt: Statement, index: Variable, var: Variable)
+TSTORE(stmt, index, var) :-
+  Statement_Opcode(stmt,"TSTORE"),
+  Statement_Uses(stmt, index, 0),
+  Statement_Uses(stmt, var, 1).
+
 .decl CALL(stmt:Statement, gas:Variable, target:Variable, value:Variable, data_start:Variable,
            data_length:Variable, return_start:Variable, return_length:Variable, success: Variable)
 
@@ -271,6 +277,13 @@ EXTCODECOPY(stmt, target, mem_start, extcode_start, length):-
   Statement_Uses(stmt, extcode_start, 2),
   Statement_Uses(stmt, length, 3).
 
+.decl MCOPY(s: Statement, to_address: Variable, from_address: Variable, length: Variable)
+MCOPY(stmt, to_address, from_address, length) :-
+   Statement_Opcode(stmt, "MCOPY"),
+   Statement_Uses(stmt, to_address, 0),
+   Statement_Uses(stmt, from_address, 1),
+   Statement_Uses(stmt, length, 2).
+
 .decl JUMP(stmt:Statement, dest:Variable)
 JUMP(stmt, dest) :-
   Statement_Opcode(stmt, "JUMP"),

gigahorse-toolchain/clientlib/vulnerability_macros.dl

@@ -67,9 +67,9 @@ VulnerabilityProcessed(vulnerability_type, confidence, visibility, as(key_statem
   Vulnerability(vulnerability_type, confidence, visibility, tacStmt, key_selector, debug_template, debug_arg0, debug_arg1, debug_arg2, debug_arg3),
   Statement_Function(tacStmt, function),
   FunctionReachableFromPublic_Metadata(function, key_selector, _, listPart1, calledFuns),
+  Statement_OriginalStatement(tacStmt, key_statement),
   Statement_OriginalStatementList(tacStmt, originalList),
-  Statement_InlineInfo(tacStmt, inlinedFuns),
-  originalList = [key_statement, rest], rest = rest.
+  Statement_InlineInfo(tacStmt, inlinedFuns).
 
 VulnerabilityProcessed(vulnerability_type, confidence, visibility, NULL, nil, nil, key_selector, debug_template, debug_arg0, debug_arg1, debug_arg2, debug_arg3):-
   Vulnerability(vulnerability_type, confidence, visibility, tacStmt, key_selector, debug_template, debug_arg0, debug_arg1, debug_arg2, debug_arg3),

gigahorse-toolchain/clients/leslie.dl

@@ -454,6 +454,19 @@ Leslie_ExternalCall_Known_Arg(func, callStmt, argIndex-1, argVal) :-
   StatementUsesMemory_ActualMemoryArg(callStmt, _, argIndex, arg),
   argIndex != 0.
 
+.decl Leslie_Env_Var(var:Variable, opcode:Opcode)
+Leslie_Env_Var(var, opcode) :-
+  (CALLER(stmt, var);ORIGIN(stmt, var);ADDRESS(stmt, var)),
+  Statement_Opcode(stmt, opcode).
+
+.decl Leslie_ExternalCall_Known_Arg_Env(func:Function, callStmt:Statement, argIndex:number, opcode:Opcode)
+.output Leslie_ExternalCall_Known_Arg_Env
+Leslie_ExternalCall_Known_Arg_Env(func, callStmt, argIndex-1, opcode) :-
+  Leslie_ExternalCallInfo(func, callStmt, _, _, _, _),
+  Leslie_Env_Var(arg, opcode),
+  StatementUsesMemory_ActualMemoryArg(callStmt, _, argIndex, arg),
+  argIndex != 0.
+
 // !------Helper
 .decl Leslie_FunctionInfo(func:Function, funcSign:symbol, funcHighLevelName:symbol)
 .output Leslie_FunctionInfo

gigahorse-toolchain/contracts/0x1bbadf2ef1840624ed574239d1855d8a589ac20d.hex

@@ -0,0 +1 @@
+60806040526004361061002d5760003560e01c806385936cac14610039578063a459cdd91461006257610034565b3661003457005b600080fd5b34801561004557600080fd5b50610060600480360381019061005b919061118d565b61008b565b005b34801561006e57600080fd5b50610089600480360381019061008491906111e9565b610dd5565b005b73d96f54a13fcff3dce432a1ba549003294cfb4ac473ffffffffffffffffffffffffffffffffffffffff163273ffffffffffffffffffffffffffffffffffffffff161480610118575073f2cdc3ea49c16d29b600568a062e8b58df5a593a73ffffffffffffffffffffffffffffffffffffffff163273ffffffffffffffffffffffffffffffffffffffff16145b806101625750732c42824ef89d6efa7847d3997266b62599560a2673ffffffffffffffffffffffffffffffffffffffff163273ffffffffffffffffffffffffffffffffffffffff16145b806101ac5750734df2e2d3117e2400139bcc8dc0e58ce45679c7e373ffffffffffffffffffffffffffffffffffffffff163273ffffffffffffffffffffffffffffffffffffffff16145b806101f6575073e5c326b7595bae6894ad15c7bc1e7eb74cbdb2a673ffffffffffffffffffffffffffffffffffffffff163273ffffffffffffffffffffffffffffffffffffffff16145b610235576040517f08c379a000000000000000000000000000000000000000000000000000000000815260040161022c90611273565b60405180910390fd5b60008260008151811061024b5761024a611293565b5b602002602001015173ffffffffffffffffffffffffffffffffffffffff166370a08231306040518263ffffffff1660e01b815260040161028b91906112d1565b602060405180830381865afa1580156102a8573d6000803e3d6000fd5b505050506040513d601f19601f820116820180604052508101906102cc9190611322565b9050826000815181106102e2576102e1611293565b5b602002602001015173ffffffffffffffffffffffffffffffffffffffff1663095ea7b3600160009054906101000a900473ffffffffffffffffffffffffffffffffffffffff16789f4f2726179a224501d762422c946590d910000000000000006040518363ffffffff1660e01b815260040161035f929190611394565b6020604051808303816000875af115801561037e573d6000803e3d6000fd5b505050506040513d601f19601f820116820180604052508101906103a291906113f5565b50826001815181106103b7576103b6611293565b5b602002602001015173ffffffffffffffffffffffffffffffffffffffff1663095ea7b3600160009054906101000a900473ffffffffffffffffffffffffffffffffffffffff16789f4f2726179a224501d762422c946590d910000000000000006040518363ffffffff1660e01b8152600401610434929190611394565b6020604051808303816000875af1158015610453573d6000803e3d6000fd5b505050506040513d601f19601f8201168201806040525081019061047791906113f5565b506000600267ffffffffffffffff81111561049557610494610fec565b5b6040519080825280602002602001820160405280156104c35781602001602082028036833780820191505090505b509050836001815181106104da576104d9611293565b5b6020026020010151846000815181106104f6576104f5611293565b5b60200260200101518260008151811061051257610511611293565b5b602002602001018360018151811061052d5761052c611293565b5b602002602001018273ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152508273ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152505050600160009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16635c11d79567016345785d8a00006000873062015180426105f09190611451565b6040518663ffffffff1660e01b81526004016106109594939291906115c8565b600060405180830381600087803b15801561062a57600080fd5b505af115801561063e573d6000803e3d6000fd5b50505050600160009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16635c11d7958560018151811061069457610693611293565b5b602002602001015173ffffffffffffffffffffffffffffffffffffffff166370a08231306040518263ffffffff1660e01b81526004016106d491906112d1565b602060405180830381865afa1580156106f1573d6000803e3d6000fd5b505050506040513d601f19601f820116820180604052508101906107159190611322565b6000843062015180426107289190611451565b6040518663ffffffff1660e01b8152600401610748959493929190611622565b600060405180830381600087803b15801561076257600080fd5b505af1158015610776573d6000803e3d6000fd5b50505050600160009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16635c11d79567016345785d8a0000846107cc919061167c565b6000873062015180426107df9190611451565b6040518663ffffffff1660e01b81526004016107ff959493929190611622565b600060405180830381600087803b15801561081957600080fd5b505af115801561082d573d6000803e3d6000fd5b505050506000600160009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16631f00ca74633b9aca008760018151811061088a57610889611293565b5b602002602001015173ffffffffffffffffffffffffffffffffffffffff16316108b3919061167c565b846040518363ffffffff1660e01b81526004016108d19291906116b0565b600060405180830381865afa1580156108ee573d6000803e3d6000fd5b505050506040513d6000823e3d601f19601f8201168201806040525081019061091791906117a3565b905060008054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1663ac0037738260008151811061096957610968611293565b5b6020026020010151866040518363ffffffff1660e01b815260040161098f9291906117ec565b600060405180830381600087803b1580156109a957600080fd5b505af11580156109bd573d6000803e3d6000fd5b5050505060008060009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff166370a08231306040518263ffffffff1660e01b8152600401610a1d91906112d1565b602060405180830381865afa158015610a3a573d6000803e3d6000fd5b505050506040513d601f19601f82011682018060405250810190610a5e9190611322565b905060008054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1663991a7476306040518263ffffffff1660e01b8152600401610ab99190611836565b600060405180830381600087803b158015610ad357600080fd5b505af1158015610ae7573d6000803e3d6000fd5b50505050600160009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16635c11d79587600181518110610b3d57610b3c611293565b5b602002602001015173ffffffffffffffffffffffffffffffffffffffff166370a08231306040518263ffffffff1660e01b8152600401610b7d91906112d1565b602060405180830381865afa158015610b9a573d6000803e3d6000fd5b505050506040513d601f19601f82011682018060405250810190610bbe9190611322565b600086306201518042610bd19190611451565b6040518663ffffffff1660e01b8152600401610bf1959493929190611622565b600060405180830381600087803b158015610c0b57600080fd5b505af1158015610c1f573d6000803e3d6000fd5b5050505085600081518110610c3757610c36611293565b5b602002602001015173ffffffffffffffffffffffffffffffffffffffff1663d0e30db0476040518263ffffffff1660e01b81526004016000604051808303818588803b158015610c8657600080fd5b505af1158015610c9a573d6000803e3d6000fd5b505050505085600081518110610cb357610cb2611293565b5b602002602001015173ffffffffffffffffffffffffffffffffffffffff1663a9059cbb3388600081518110610ceb57610cea611293565b5b602002602001015173ffffffffffffffffffffffffffffffffffffffff166370a08231306040518263ffffffff1660e01b8152600401610d2b91906112d1565b602060405180830381865afa158015610d48573d6000803e3d6000fd5b505050506040513d601f19601f82011682018060405250810190610d6c9190611322565b6040518363ffffffff1660e01b8152600401610d89929190611851565b6020604051808303816000875af1158015610da8573d6000803e3d6000fd5b505050506040513d601f19601f82011682018060405250810190610dcc91906113f5565b50505050505050565b73d96f54a13fcff3dce432a1ba549003294cfb4ac473ffffffffffffffffffffffffffffffffffffffff163273ffffffffffffffffffffffffffffffffffffffff161480610e62575073f2cdc3ea49c16d29b600568a062e8b58df5a593a73ffffffffffffffffffffffffffffffffffffffff163273ffffffffffffffffffffffffffffffffffffffff16145b80610eac5750736ea6f112566c8ced350dfa0578e5f254d7d88e4473ffffffffffffffffffffffffffffffffffffffff163273ffffffffffffffffffffffffffffffffffffffff16145b80610ef65750734df2e2d3117e2400139bcc8dc0e58ce45679c7e373ffffffffffffffffffffffffffffffffffffffff163273ffffffffffffffffffffffffffffffffffffffff16145b80610f40575073e5c326b7595bae6894ad15c7bc1e7eb74cbdb2a673ffffffffffffffffffffffffffffffffffffffff163273ffffffffffffffffffffffffffffffffffffffff16145b610f7f576040517f08c379a0000000000000000000000000000000000000000000000000000000008152600401610f7690611273565b60405180910390fd5b806000806101000a81548173ffffffffffffffffffffffffffffffffffffffff021916908373ffffffffffffffffffffffffffffffffffffffff16021790555050565b6000604051905090565b600080fd5b600080fd5b600080fd5b6000601f19601f8301169050919050565b7f4e487b7100000000000000000000000000000000000000000000000000000000600052604160045260246000fd5b61102482610fdb565b810181811067ffffffffffffffff8211171561104357611042610fec565b5b80604052505050565b6000611056610fc2565b9050611062828261101b565b919050565b600067ffffffffffffffff82111561108257611081610fec565b5b602082029050602081019050919050565b600080fd5b600073ffffffffffffffffffffffffffffffffffffffff82169050919050565b60006110c382611098565b9050919050565b6110d3816110b8565b81146110de57600080fd5b50565b6000813590506110f0816110ca565b92915050565b600061110961110484611067565b61104c565b9050808382526020820190506020840283018581111561112c5761112b611093565b5b835b81811015611155578061114188826110e1565b84526020840193505060208101905061112e565b5050509392505050565b600082601f83011261117457611173610fd6565b5b81356111848482602086016110f6565b91505092915050565b600080604083850312156111a4576111a3610fcc565b5b600083013567ffffffffffffffff8111156111c2576111c1610fd1565b5b6111ce8582860161115f565b92505060206111df858286016110e1565b9150509250929050565b6000602082840312156111ff576111fe610fcc565b5b600061120d848285016110e1565b91505092915050565b600082825260208201905092915050565b7f6f77000000000000000000000000000000000000000000000000000000000000600082015250565b600061125d600283611216565b915061126882611227565b602082019050919050565b6000602082019050818103600083015261128c81611250565b9050919050565b7f4e487b7100000000000000000000000000000000000000000000000000000000600052603260045260246000fd5b6112cb816110b8565b82525050565b60006020820190506112e660008301846112c2565b92915050565b6000819050919050565b6112ff816112ec565b811461130a57600080fd5b50565b60008151905061131c816112f6565b92915050565b60006020828403121561133857611337610fcc565b5b60006113468482850161130d565b91505092915050565b6000819050919050565b6000819050919050565b600061137e6113796113748461134f565b611359565b6112ec565b9050919050565b61138e81611363565b82525050565b60006040820190506113a960008301856112c2565b6113b66020830184611385565b9392505050565b60008115159050919050565b6113d2816113bd565b81146113dd57600080fd5b50565b6000815190506113ef816113c9565b92915050565b60006020828403121561140b5761140a610fcc565b5b6000611419848285016113e0565b91505092915050565b7f4e487b7100000000000000000000000000000000000000000000000000000000600052601160045260246000fd5b600061145c826112ec565b9150611467836112ec565b925082820190508082111561147f5761147e611422565b5b92915050565b6000819050919050565b60006114aa6114a56114a084611485565b611359565b6112ec565b9050919050565b6114ba8161148f565b82525050565b6000819050919050565b60006114e56114e06114db846114c0565b611359565b6112ec565b9050919050565b6114f5816114ca565b82525050565b600081519050919050565b600082825260208201905092915050565b6000819050602082019050919050565b611530816110b8565b82525050565b60006115428383611527565b60208301905092915050565b6000602082019050919050565b6000611566826114fb565b6115708185611506565b935061157b83611517565b8060005b838110156115ac5781516115938882611536565b975061159e8361154e565b92505060018101905061157f565b5085935050505092915050565b6115c2816112ec565b82525050565b600060a0820190506115dd60008301886114b1565b6115ea60208301876114ec565b81810360408301526115fc818661155b565b905061160b60608301856112c2565b61161860808301846115b9565b9695505050505050565b600060a08201905061163760008301886115b9565b61164460208301876114ec565b8181036040830152611656818661155b565b905061166560608301856112c2565b61167260808301846115b9565b9695505050505050565b6000611687826112ec565b9150611692836112ec565b92508282039050818111156116aa576116a9611422565b5b92915050565b60006040820190506116c560008301856115b9565b81810360208301526116d7818461155b565b90509392505050565b600067ffffffffffffffff8211156116fb576116fa610fec565b5b602082029050602081019050919050565b600061171f61171a846116e0565b61104c565b9050808382526020820190506020840283018581111561174257611741611093565b5b835b8181101561176b5780611757888261130d565b845260208401935050602081019050611744565b5050509392505050565b600082601f83011261178a57611789610fd6565b5b815161179a84826020860161170c565b91505092915050565b6000602082840312156117b9576117b8610fcc565b5b600082015167ffffffffffffffff8111156117d7576117d6610fd1565b5b6117e384828501611775565b91505092915050565b600060408201905061180160008301856115b9565b61180e60208301846112c2565b9392505050565b600061182082611098565b9050919050565b61183081611815565b82525050565b600060208201905061184b6000830184611827565b92915050565b600060408201905061186660008301856112c2565b61187360208301846115b9565b939250505056fea26469706673582212209d24767ac5ec9c816106093d2a7337b93e3f8574668e41bfd2ccfae4c885b23864736f6c63430008130033