Understand the output of Securify when analyzing runtime bin

[ireneGP]

Hello, I am writing to ask a quick question regarding how to interpret the output of Security.

For instance when executing the following command and getting the output:

➜  securify git:(master) java -jar build/libs/securify.jar -fh src/test/resources/solidity/transaction-reordering.bin.hex
  Attempt to decompile the contract with methods...
  Success. Inlining methods...
  Propagating constants...
  Verifying patterns...

So what does that mean? Where can I find the corresponding results, something like whether this is vulnerable towards reentracy attack, towards TOD attack (violation or not).

I tried to append the --json option to the command but nothing happens.

Also, I tried to run a run-time EVM bytecode on my local machine and got the following output::

➜  securify git:(master) java -jar build/libs/securify.jar -fh /opt/wangshua/work/evm_analyzer_folder/evm_analyzer_1/scripts/contract_bins/0x068abd01efff87943c6853abff3d20edfa9f9a18.bin
  Attempt to decompile the contract with methods...
  Failed to decompile methods. Attempt to decompile the contract without identifying methods...
  Propagating constants...
  Verifying patterns...

Somehow the "function" is not recognized. Is it still OK to use Securify, for such cases? Thanks!

[ritzdorf]

Hi @ireneGP ,

thanks a lot for your question. This was unclear indeed. Please use:

java -jar build/libs/securify.jar -fh src/test/resources/solidity/transaction-reordering.bin.hex --livestatusfile /tmp/result.json

We also modified the usage message to clarify this.
Please let us know if it shouldn't work for you.

[ireneGP]

@ritzdorf Thank you so much for your prompt reply! I appreciate it very much.

Just one followup question to understand the json output. So basically I got the following output by analyzing my contract (a local EVM runtime bytecode):

{
  "decompiled": true,
  "securifyErrors": {
    "errors": []
  },
  "finished": true,
  "patternResults": {
    "DAO": {
      "completed": true,
      "hasViolations": false,
      "hasWarnings": false,
      "hasSafe": false,
      "hasConflicts": false,
      "violations": [],
      "warnings": [],
      "safe": [],
      "conflicts": []
    },
    "DAOConstantGas": {
      "completed": true,
      "hasViolations": true,
      "hasWarnings": false,
      "hasSafe": false,
      "hasConflicts": false,
      "violations": [
        354,
        866,
        831,
        777
      ],
      "warnings": [],
      "safe": [],
      "conflicts": []
    },
    "LockedEther": {
      "completed": true,
      "hasViolations": false,
      "hasWarnings": false,
      "hasSafe": true,
      "hasConflicts": false,
      "violations": [],
      "warnings": [],
      "safe": [
        1
      ],
      "conflicts": []
    },
    "MissingInputValidation": {
      "completed": true,
      "error": "not supported",
      "hasViolations": false,
      "hasWarnings": false,
      "hasSafe": false,
      "hasConflicts": false,
      "violations": [],
      "warnings": [],
      "safe": [],
      "conflicts": []
    },
    "RepeatedCall": {
      "completed": true,
      "hasViolations": false,
      "hasWarnings": false,
      "hasSafe": false,
      "hasConflicts": false,
      "violations": [],
      "warnings": [],
      "safe": [],
      "conflicts": []
    },
    "TODAmount": {
      "completed": true,
      "hasViolations": true,
      "hasWarnings": true,
      "hasSafe": false,
      "hasConflicts": false,
      "violations": [
        866,
        831
      ],
      "warnings": [
        354,
        777
      ],
      "safe": [],
      "conflicts": []
    },
    "TODReceiver": {
      "completed": true,
      "hasViolations": true,
      "hasWarnings": true,
      "hasSafe": false,
      "hasConflicts": false,
      "violations": [
        866,
        831
      ],
      "warnings": [
        354,
        777
      ],
      "safe": [],
      "conflicts": []
    },
    "UnhandledException": {
      "completed": true,
      "hasViolations": true,
      "hasWarnings": false,
      "hasSafe": false,
      "hasConflicts": false,
      "violations": [
        354,
        866,
        831,
        777
      ],
      "warnings": [],
      "safe": [],
      "conflicts": []
    },
    "UnrestrictedEtherFlow": {
      "completed": true,
      "hasViolations": false,
      "hasWarnings": true,
      "hasSafe": true,
      "hasConflicts": false,
      "violations": [],
      "warnings": [
        354,
        777
      ],
      "safe": [
        866,
        831
      ],
      "conflicts": []
    },
    "UnrestrictedWrite": {
      "completed": true,
      "hasViolations": true,
      "hasWarnings": true,
      "hasSafe": true,
      "hasConflicts": false,
      "violations": [
        251,
        365,
        374,
        454,
        464,
        473,
        523,
        532,
        615,
        669,
        698
      ],
      "warnings": [
        788,
        797
      ],
      "safe": [
        104,
        115,
        202,
        411,
        871,
        836
      ],
      "conflicts": []
    }
  }
}

My questions are:

1. what does it mean for "errors": [] in the "securifyErrors"? Does it mean this contract is safe?
   Note that I found that DAOConstantGas and TODAmount has some "violations"..

2. Where are the "bad randomness/dependence on system properties" issue and "reentrancy issue"?

Thanks a lot! I look forward to hearing from you!

[ritzdorf]

1. "errors" will report internal securify errors, e.g. failed decompilation. Obviously we try to minimize those. Let us know if you encounter some of those.
2. You can add --descriptions to get more information, e.g. the patterns DAO and DAOConstantGas check for reentrancy-related issues.

[ireneGP]

@ritzdorf Thank you! Then may I ask what about the dependence on timestamp or other system properties? I somehow got the impression that Securify would also capture that.

[ritzdorf]

@ireneGP We are working on such patterns. And will release them once they are stable enough. You can try out some initial version under https://securify.ch

[ireneGP]

@ritzdorf Thank you! One followup question on the "violation patterns" vs. "warning patterns". How should I interpret this? In case I encountered a "warning pattern", can I interpret it as "vulnerable" or so?

[ptsankov]

@ireneGP violation implies that the security property is violated, while warning indicates that it may be a false positive. For full details on that you can see Fig 2 in the tech report: https://files.sri.inf.ethz.ch/website/papers/ccs18-securify.pdf

[ireneGP]

@ptsankov @ritzdorf Thank you for the clarification. I am still a bit confused about the vulnerability pattern here, say, can Securify pinpoint DoS with (Unexpected) revert style vulnerability? I don't think the Handled Exception (HE) is what I am looking for here. Thanks!