Broken Dataflow

[ritzdorf]

The mayFollow relation does not correctly capture dataflow dependencies.

Example:

contract A {
  	address a;
	function f() public view returns(address) {
    	    return a;
        }
}

contract B {
    mapping(address => bool) approved;
    mapping(address => bool) modified;

    function x(A a) internal returns(address){
        return address(a.f());
    }

    function g(A a) public {
        require(approved[x(a)]);
        modified[x(a)] = true;
     }
}

It does not identify that function x() may follow itself.

A test case is provided inside the broken_dataflow branch (https://github.com/eth-sri/securify/tree/broken_dataflow).

Simply run ./gradlew test to trigger.

[ptsankov]

The dataflow analysis is correct. The reason this does not get detected is that by default Securify would decompile methods and compute a local, per-method dataflow fixpoint. Disabling method decompilation results in computing a global dataflow fixpoint that passes this test.

[hiqua]

So shall I just remove the Decompiler and use the DecompilerFallback as default?

[ritzdorf]

Can you rerun the test cases with this change so that we can evaluate the difference?

[hiqua]

Rerunning now, one thing though is that the MissingInputValidation pattern depends on the method decompilation. We could also just have the method decompilation for this pattern and the fallback decompilation for the others.

[hiqua]

Difference available on comparison_decompiler_fallback.

[ritzdorf]

Thanks. Do we have an ordered diff somewhere, so it is easier to see what changed?

[hiqua]

Try with 2b72e5f and let me know if that works for you.

[ritzdorf]

When I rebase to the specified commit the issue is gone. ./gradlew test gets two new errors:

1. Is about MissingInputValidation. That is expected and we are fixing it elsewhere.
2. Is about this check

   securify/src/test/java/ch/securify/patterns/LockedEtherTest.java

   Line 34 in 689c872

   assertEquals(2, instructionPatternTest.pattern.violations.size());

The relevant code is: https://github.com/eth-sri/securify/blob/broken_dataflow/src/test/resources/solidity/LockedEther.sol

The returned result is 1 but the expected result is 2, but I find that 1 is the correct result, so overall it seems to fix things.