FEATURE: Audit Module

[fubuloubu]

It would be really awesome if Viper had some sort of internal auditing capabilities that could warn you if/when/under what conditions certain methods could fail. Additionally, to be able to add rules to the source file (that do not get compiled) dictating what non-exceptional scenarios constitute a failure. Suggested keyword (from #370) is should, but I think #invariant or #assume would be better.

As an example, the company.v.py example has two different scenarios I could envision this working with:

def sell_stock(sell_order: currency_value):
    assert self.holding[msg.sender] >= sell_order
    assert self.balance >= (sell_order * self.price)
    self.holdings[msg.sender] -= sell_order
    self.holdings[self.company] += sell_order
    send(msg.sender, sell_order * self.price)

might produce something like this:

AuditWarning: A value for 'sell_order' in the range '[-2**127, 0)'
              would cause an exception 'NegativeWeiTransfer'
              when executing 'send(msg.sender, sell_order * self.price)'
              in method 'sell_stock()'

Adding a #invariant should check if that condition is ever possible

# Part of the audit assertions (that don't get compiled)
#invariant holding[any(address)] >= 0 # Should never have negative stock

def transfer_stock(receiver: address, transfer_order: currency_value):
    assert self.holding[msg.sender] >= transfer_order
    self.holdings[msg.sender] -= transfer_order
    self.holdings[receiver] += transfer_order
    should self.holdings[receiver] + transfer_order == self.holdings[msg.sender]

which might produce something like:

AuditWarning: A value for 'transfer_order' in the range '[-2**127, 0)'
              would fail invariant 'holding[any(address)] >= 0'
              given 'self.holdings[receiver] = 0'
              in method 'transfer_stock()'

Alerting you to the fact that you should add an assertion to transfer_stock() to ensure transfer_order is never negative, which has the additional side effect of allowing someone to steal stock from another person (this is not necessarily caught in this example, but the fact the Audit Module caught one weird scenario can help alert you to the bigger problem).

While this is not a good substitute for an audit by a human for potential functional issues (like being able to steal stock), it does provide a cool guarentee that you can audit code written in variable against commonly employed attacks (basically whatever we build in to the Audit Module). Viper is currently simple enough (no inheritance, limited support for arrays, limited types, etc.) that this is possible to implement, and it can also help alert us to issues in the underlying compiler over time.

[DustinWehr]

+1 for #invariant

[vbuterin]

I support this. Examples of things that this could be useful for:

1. In a currency, verify that balances cannot go below zero.
2. In a currency, verify that no function except for issue affects the total supply
3. In an on-chain market maker, verify that the invariant of holdings of asset A vs holdings of asset B holds true (useful for Bancor or things like this)
4. Verify that the balance of address x can only decrease in a function call if msg.sender = x
5. Verify that there always exists some sequence of transactions through which the set of participants in a contract could collude to take the money out
6. Verify that taking any funds out of a multisig actually requires 3/5 permission

I'd love to see a longer list of motivating examples put together to help point anyone trying to make fuzz testing, model checking, symbolic execution or formal verification tools in the right direction.

[fubuloubu]

For 4. (balance can only decrease in a function call for a given address x) how does a syntax like this look? #invariant self.balance[x] >= funName(sender=x) then self.balance[x], where x = any(address)

[fubuloubu]

5. seems very hard to reason about, but maybe revise that to something like "only participants x, y, z can get money out of this contract's balance using any one method" e.g. #invariant a.balance < any(method) then a.balance, where a not in [x, y, z]

Where any(method) just means any callable function inside the contract, and assume a is the sender.

[DustinWehr]

I think 5 and 6 would be a job for an interactive theorem prover. @pirapira you're interested in proving dapp level correctness properties, right? Or are you focused on compiler correctness?

@fubuloubu is this the issue you suggested making for the should keyword? It seems to have expanded to a larger scope.

As I imagined it, should is a very user friendly and easy to implement, but relatively limited way of communicating intent to any theorem prover. The syntax is exactly the same as assert, except you restrict the expression to be side effect free. To a theorem prover it is a goal and, once proved, a lemma.

A major use would be to express some complex precondition on a private helper function that can't be expressed using the type system.

Could also be used for optimization. A concrete (but trivial) example from one of the few contracts I've written, our suggested fix for the delegating voting example (still untested): the function forward_weight gets called both internally/privately (by delegate) and externally/publicly (forgive me for not knowing the Solidity terminology). For the internal call, the two assert statements could be skipped. Communicate that to the compiler by expressing both assertions as invariants before the call to forward_weight on line 103.

[pirapira]

I first want a Viper interpreter in a theorem prover. Then I can test the Viper definition in the theorem provers against their actual behavior.

[fubuloubu]

Deprecated in favor of #711