# Veridise

## Formalization

1. A RefundableCrowdsale’s `claimRefund` transaction will revert if `goalReached()` or not `isFinalized`

reverted(claimRefund, goalReached() || !isFinalized)

2. After a RefundableCrowdsale `withdraw` transaction, `msg.sender`’s balance should increase by the original value (before the execution of the `withdraw` transaction) of `balanceOf(msg.sender)` and `balanceOf(msg.sender)` should be `0`.

Let `b` be `msg.sender`’s balance.

finished(withdraw, b = old(b) + old(balanceOf(msg.sender)) && balanceOf(msg.sender) = 0)

## Verification

I'm a bit confused by this question - am I to check if these two statements hold, or that if pre does entail post after `attempt`?

If it's the latter then it does entail, because every state with `started && msg.value > cost` does go through the function correctly and its effect is exactly the postcondition.

And if it's the former:

1. Precondition: `started(Game.attempt(guess), started && msg.value > cost)`

This does not always hold. `attempt(guess)` can be called with `msg.value <= cost` where `require(msg.value > cost)` will fail. And, after any time `attempt(guess)` is called with `result == target` and before any `setTarget(t)` is called, `attempt(guess)` can be called with `!started` in which case `require(started)` will fail.

2. Postcondition: `finished(Game.attempt(guess), value = fsum(Game.attempt(guess), guess))`

This always holds. Every time `Game.attempt(guess)` succeeds, `value` equals to the sum of all the `guess`s from all the time it is run.

## Detection

1. Anyone can call `setTarget`.
2. When `value` is too big, it could be that all the correct `guess`s would overflow `value`.
3. Reentrancy attack is possible where attacker guesses right and then drains the fund before `started` is set to `false`.

## Exploit

I think an exploit is possible because the contract does not check what the input `data` contains before executing it. I'm not sure what exactly can it do, but considering arbitrary code is possible, I assume there is an exploit.

## Tooling

I couldn't set up Typescript and Solidity correctly so I ran the `sol-ast-compile --tree` directly on the example program. I reasoned that, the detection script should, during the traversal of the AST, upon meeting a node of type `FunctionCall`, check if it is an "external" call where there should be a pre-determined list of such calls including `msg.sender.call`, and, if it is, mark the current `Block` and continue the traversal until its end or when an `Assignment` is met, in which case it decides that reentrancy is possible.