No real intercontract concolic execution

[konradweiss]

https://github.com/b-mueller/laser-ethereum/blob/4465fe4697af6fe45902a061e07518b826215175/laser/ethereum/svm.py#L1145

This comment suggests that the return value is always symbolic and values are not taken in consideration. Is the return value at least some constraint symbolic value? Above when handling the CALL* instructions, several calls to _sym_exec(...) look like they carry on the symbolic/concolic execution in an intercontract manner. Is that so, what are the limitations of the current intercontract analysis and do you have any written documentation or papers on that subject?

[muellerberndt]

Hi @LoCorVin, we're currently discussing possible solutions for this. Here is an example I posted on Gitter yesterday and the resulting control flow graph.

pragma solidity ^0.4.17;

contract Callee {
	
    function theFunction(uint value) public returns(bool retval) {

    	if (value == 1){
    		return true;
    	} else {
    		return false;
    	}
        
    }
}

contract Caller {

	Callee callee = new Callee();

    function start(uint value) {
    	callee.theFunction(value) ;

    }
}

In laser, all three possible returns from the callee converge into a single state in the caller. Return values are always symbolic and any changes to the world state (such as one contracts sending funds to another) are lost.

To resolve this, IMO the call stack needs to be moved into global state. However we're also brainstorming foundational changes to the engine, such as restructuring the recursive _sym_exec to as an explicit worklist algorithm. Here a few more resources:

• Mythril core dev Gitter channel
• HITB paper p.46-49