Verifying Reentrant Computation

[DavePearce]

To verify reentrant computation relies on a two state predicate which summarises the effect making one (or more) reentrant calls into a method could have on local state. For example, consider this:

int state = 0

public method inc()
modifies state
ensures old(state) +1 == state:
   state = state + 1

The necessary two-state predicate is actually old(state) < state for inc() since we can call inc() arbitrarily many times from external code. What we need is a way to either infer such a specification or (perhaps easier) to check such a specification is already transitive.

Syntax

There are various ways we could try to encode the logic we need. One approach might be to impose constraints on how global data could be modified. For example:

type uiint256 is (uint256 v)
varies old(v) < v

Actually the varies clauses is perhaps similar or identical to Liskov and Wing's constraint clause.

References

• Rich Specifications for Ethereum Smart Contract Verification (link)
• See 2Vyper Github Repo here
• Behavoural Notion of Subtyping, Liskov and Wing, 1994 (link]

[DavePearce]

variant unchanged(&int p)
where old(*p) == *p

map<address,uint256> balances = ...
bool lock = false

public method get_balance(address sender) -> uint256
 unchanged(&balances):
   ...

public method deposit(address sender):
   sender.transfer(123) <- 

public method main()
always lock ==> unchanged(&balances)
eventually ended

The keywords are from temporal logic. These are the transitive and reflexive closures of ensures.

[DavePearce]

The rough idea is to use a keyword always which reasons over the history. The intention is that this is a transitive constraint and, hence, we can use it to reason about multiple invocations of a method. Some notes:

• One of the challenges with transitive constraints is that we cannot easily infer them from a postcondition. Rather, having the programmer write them means we can, instead, just check them. This is a little bit like loop invariants.
• However, what I'm not sure is how to interpret always clauses. For the example above, its quite easy as we can just imagine it holds after multiple calls to main(). But, what about a method which accepts one or more parameters? Or is a function rather than a method ?
• Its almost like the constraints apply to data locations rather than methods per se. Its much easier to reason about data locations, since its really just about when they are assigned.

[DavePearce]

Another aspect of this idea is that we can use it for authorisation as well. For example, we can say something like this:

"unless msg::sender equals a particular account, this variable cannot be changed".