Theory Reentrancy
section‹Reentrancy›
text ‹
In the following we use our calculus to verify a contract implementing a simple token.
The contract is defined by definition *bank* and consist of one state variable and two methods:
▪ The state variable "balance" is a mapping which assigns a balance to each address.
▪ Method "deposit" allows to send money to the contract which is then added to the sender's balance.
▪ Method "withdraw" allows to withdraw the callers balance.
›
text ‹
We then verify that the following invariant (defined by *BANK*) is preserved by both methods:
The difference between
▪ the contracts own account-balance and
▪ the sum of all the balances kept in the contracts state variable
is larger than a certain threshold.
›
text ‹
There are two things to note here:
First, Solidity implicitly triggers the call of a so-called fallback method whenever we transfer money to a contract.
In particular if another contract calls "withdraw", this triggers an implicit call to the callee's fallback method.
This functionality was exploited in the infamous DAO attack which we demonstrate it in terms of an example later on.
Since we do not know all potential contracts which call "withdraw", we need to verify our invariant for all possible Solidity programs.
›
text ‹
The second thing to note is that we were not able to verify that the difference is indeed constant.
During verification it turned out that this is not the case since in the fallback method a contract could just send us additional money without calling "deposit".
In such a case the difference would change. In particular it would grow. However, we were able to verify that the difference does never shrink which is what we actually want to ensure.
›
theory Reentrancy
imports Weakest_Precondition Solidity_Evaluator
"HOL-Eisbach.Eisbach_Tools"
begin
subsection‹Example of Re-entrancy›
definition[solidity_symbex]:"example_env ≡
loadProc (STR ''Attacker'')
([],
([], SKIP),
ITE (LESS (BALANCE THIS) (UINT 256 125))
(EXTERNAL (ADDRESS (STR ''BankAddress'')) (STR ''withdraw'') [] (UINT 256 0))
SKIP)
(loadProc (STR ''Bank'')
([(STR ''balance'', Var (STMap TAddr (STValue (TUInt 256)))),
(STR ''deposit'', Method ([], True,
ASSIGN
(Ref (STR ''balance'') [SENDER])
(PLUS (LVAL (Ref (STR ''balance'') [SENDER])) VALUE))),
(STR ''withdraw'', Method ([], True,
ITE (LESS (UINT 256 0) (LVAL (Ref (STR ''balance'') [SENDER])))
(COMP
(TRANSFER SENDER (LVAL (Ref (STR ''balance'') [SENDER])))
(ASSIGN (Ref (STR ''balance'') [SENDER]) (UINT 256 0)))
SKIP))],
([], SKIP),
SKIP)
fmempty)"