Open ritzdorf opened 5 years ago
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.
So shall I just remove the Decompiler and use the DecompilerFallback as default?
Can you rerun the test cases with this change so that we can evaluate the difference?
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.
Difference available on comparison_decompiler_fallback
.
Thanks. Do we have an ordered diff somewhere, so it is easier to see what changed?
Try with 2b72e5f529d479e4e1a842be34aaf88ac5602576 and let me know if that works for you.
When I rebase to the specified commit the issue is gone. ./gradlew test
gets two new errors:
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.
The
mayFollow
relation does not correctly capture dataflow dependencies.Example:
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.