VIP: Enable Dynamic Analysis/Symbolic Execution Checks

[pirapira]

Preamble

VIP: <to be assigned>
Title: assertions that should never-ever fail
Author: Yoichi Hirai <yoichi@ethereum.org>
Type: Standard Track
Status: Draft
Created: 2018-03-21

Simple Summary

Add a special type of assertion that should never ever fail. When a static analyzer can fire it, the program surely has a bug.

Abstract

Static analyzers can detect bugs, but only when the desired properties are specified. The easiest way is to insert a "never-to-fail" assertions in the program.

Motivation

Mythril has a feature to detect when 0xfe is somehow reachable. KEVM can soon do that.

assert in vyper is expected to fail sometimes, and it is compiled to REVERT. REVERT might indicate a mistake of the caller, a mistake of the programmer, or a mistake of the compiler. So, static analyzers cannot shout "this is a bug".

Instead, if Vyper has a never-to-fail assertion that translates to INVALID (0xfe), static analyzers can confidently shout "this is a bug. See, this execution reaches INVALID".

Alternatives are specially formatted comments like ACSL or JML, but they are hard to learn.

Specification

Add a additional custom constant to the assert statement:

    assert amount != 0, UNREACHABLE

as well as

    raise UNREACHABLE

Backwards Compatibility

A program containing a name assure will cause compillation errors.

Copyright

Copyright and related rights waived via CC0

[pirapira]

Pinging @daejunpark and @ehildenb.

[fubuloubu]

We were talking about this a few months back. The only difference is we were talking about a special comment type for analysis. I think everyone was on board with the concept, but this particular implementation is interesting.

I think a more succinct way to do it is to include valid Python syntax that basically won't compile to anything in "normal" mode, and in static analysis mode would add extra asserts to the bytecode used for analysis, throwing the special opcode as you pointed out.

We would love to leverage this kind of analysis as a tool for our compiler. Perhaps this specification can be leveraged as a standard for any EVM language, and we can build toolsets that make this kind of analysis easier within a language-agnostic framework?

I think with all of our langauges targeting the EVM, we should be thinking much more about toolsets that leverage that layer so we're not duplicating work in every compiler.

[pirapira]

Yes, a common convention would save work. Solidity took the approach "INVALID means never-to-be-executed-if-program-is-sane".

http://solidity.readthedocs.io/en/v0.4.21/control-structures.html#error-handling-assert-require-revert-and-exceptions

Properly functioning code should never reach a failing assert statement; if this happens there is a bug in your contract which you should fix.

[ehildenb]

I'm in favor of the INVALID opcode means "never to be executed, if so then program has bug". It might not be so with legacy contracts, but I think it makes sense moving forward.

Alternative is making some explicit ASSERTION_FAILURE opcode, but if it would have same runtime behaviour as INVALID I don't see the benefit. If we can think of a different runtime behaviour for it, then it should be considered.

Another alternative is using some unused opcode as the de-facto ASSERTION_FAILURE opcode. This will have the same runtime behaviour as INVALID though, and may not be future-proof.

[fubuloubu]

Yeah, that's a toughy.

Perhaps the code gets added when compiled for FV mode (in either language) and the json assests file contains a listing of those bytecode locations that should trigger analysis failures if reached.

That would start to get into the need to formalize the assets file spec to leverage in different tools (e.g. solc --standard-json/vyper -f json) so that bytecode and metadata could get imported into tools in a standard way.

[ehildenb]

What's wrong with just generating INVALID when the code has an assert ... (or sure ... as @pirapira has above)? I suppose you could only insert it when in FV mode, but I think you would actually want to always insert it, even in production mode. If an assert ... failure is triggered at runtime, you want the contract to throw because people may take advantage of the bug the assert ... is guarding from.

I don't see the need for reading extra metadata, the tools can just analyze "is INVALID ever reachable?", which is a fairly simple query to make for a symbolic execution engine, and I think most static analysis tools should also be able to do something for that style of query.

[pirapira]

(I saw assert was already taken, so I sidestepped.)

[fubuloubu]

@ehildenb It's a suggestion. Some peoople don't want extra code to pollute their contracts, hence having a separate FV-only statement that would get dropped in normal compilation because you've "proved" it's not possible. We could definitely argue whether to give the person the option to include them in their final bytecode.

As far as metadata, it's more a UI thing. Yes the execution engine can tell when it hits a certain statement, but "there's a problem" is more opaque than "there's a problem L17, C40" or "your FVassert statement on line 17 failed"

[pirapira]

@fubuloubu well, programmers have the choice whether or not to use the new sure statements.

[pirapira]

If some programmers go for

    # @static-assert balance > 0

that's their choice.

sure x --> INVALID is just one way, very easy for static analyzers to understand.

[fubuloubu]

Well, in that case, wouldn't it make sense to have assure use the ASSERT under the hood and additionally generate the @static-assert for FV. That way we have three options:

1. assert -> always check
2. assure -> always in bytecode, should never happen, FV mode switches this to INVALID for analysis
3. #@static-assert -> never check, FV only, FV mode adds INVALID for analysis

[pirapira]

@fubuloubu well, #@static-assert is a comment, so it should never translate to any instruction. However, #@static-assert x can be translated into some sort of metadata, which is out of scope of my proposal. My point is that designing a common format of such metadata is hard, while it's easy to set up tools to detect INVALID.

[pirapira]

@fubuloubu I won't believe that the FV mode and non-FV mode behave the same, so if I analyze the FV mode code, I would just deploy the FV mode code.

[pirapira]

@fubuloubu so, I think it's safer to have assure or not to have assure. disable assure keyword in the non-FV mode. The compiler should error out ("error: assure keyword is only available in the FV-mode").

[fubuloubu]

Then you have two copies of the same code (one with the statement and one without), and that's a no-no to me. I think maybe make it more obvious that they're different, and that @assure will be removed in non-FV mode.