How can I test a byte-code contract file with Securify?

[eth-sri]

How can I test a byte-code contract file with Securify?

[ptsankov]

Hi Lukas, Securify v2 analyzes Solidity source code, not EVM bytecode. Of course, one can build a tool that analyzes EVM bytecode (in fact, Securify v1 analyzes bytecode: https://github.com/eth-sri/securify). You to either decompile the bytecode to Solidity and then try Securify v2, or use Securify v1.

Petar

[lukasdenk]

OK, thank you.
Does this mean that Securify v2 also does not analyse byte-code internally? Is the core logic much different to Securify v1? And if so, is there a documentation or paper which explains how Securify v2 works?

[ptsankov]

Does this mean that Securify v2 also does not analyse byte-code internally?

Yes.

Is the core logic much different to Securify v1?

Yes.

And if so, is there a documentation or paper which explains how Securify v2 works?

For the intermediate representation of Securify v2, you can check out this thesis: https://www.research-collection.ethz.ch/bitstream/handle/20.500.11850/343039/1/Vogel_Frederic.pdf

The documentation for the static analysis is currently not available.

[lukasdenk]

OK, thank you!