Theory Reentrancy
section‹Reentrancy›
text ‹
In the following we use our semantics to verify a contract implementing a simple token.
The contract is defined by definition ∗‹victim› 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 ∗‹INV›) 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 implict 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.
Thus, the core result here is a lemma which shows that the invariant is preserved by every Solidity program which is not executed in the context of our own contract.
For our own methods we show that the invariant holds after executing it.
Since our own program as well as the unknown program may depend on each other both properties are encoded in a single lemma (∗‹secure›) which is then proved by induction over all statements.
The final result is then given in terms of two corollaries for the corresponding methods of our contract.
›
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 withouth 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 Solidity_Evaluator
begin
subsection‹Example of Re-entrancy›
value "eval 1000
stmt
(COMP
(EXTERNAL (ADDRESS (STR ''Victim'')) (STR ''deposit'') [] (UINT 256 10))
(EXTERNAL (ADDRESS (STR ''Victim'')) (STR ''withdraw'') [] (UINT 256 0)))
(STR ''Attacker'')
(STR '''')
(STR ''0'')
[(STR ''Victim'', STR ''100''), (STR ''Attacker'', STR ''100'')]
[
(STR ''Attacker'',
[],
ITE
(LESS (BALANCE THIS) (UINT 256 125))
(EXTERNAL (ADDRESS (STR ''Victim'')) (STR ''withdraw'') [] (UINT 256 0))
SKIP),
(STR ''Victim'',
[
(STR ''balance'', Var (STMap TAddr (STValue (TUInt 256)))),
(STR ''deposit'', Method ([], ASSIGN (Ref (STR ''balance'') [SENDER]) VALUE, None)),
(STR ''withdraw'', Method ([],
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
, None))],
SKIP)
]
[]"
subsection‹Definition of Contract›
abbreviation myrexp::L
where "myrexp ≡ Ref (STR ''balance'') [SENDER]"
abbreviation mylval::E
where "mylval ≡ LVAL myrexp"
abbreviation assign::S
where "assign ≡ ASSIGN (Ref (STR ''balance'') [SENDER]) (UINT 256 0)"
abbreviation transfer::S
where "transfer ≡ TRANSFER SENDER (LVAL (Id (STR ''bal'')))"
abbreviation comp::S
where "comp ≡ COMP assign transfer"
abbreviation keep::S
where "keep ≡ BLOCK ((STR ''bal'', Value (TUInt 256)), Some mylval) comp"
abbreviation deposit::S
where "deposit ≡ ASSIGN (Ref (STR ''balance'') [SENDER]) (PLUS (LVAL (Ref (STR ''balance'') [SENDER])) VALUE)"
definition victim::"(Identifier, Member) fmap"
where "victim ≡ fmap_of_list [
(STR ''balance'', Var (STMap TAddr (STValue (TUInt 256)))),
(STR ''deposit'', Method ([], deposit, None)),
(STR ''withdraw'', Method ([], keep, None))]"
subsection‹Definition of Invariant›
abbreviation "SUMM s ≡ ∑(ad,x)|fmlookup s (ad + (STR ''.'' + STR ''balance'')) = Some x. ReadL⇩i⇩n⇩t x"
abbreviation "POS s ≡ ∀ad x. fmlookup s (ad + (STR ''.'' + STR ''balance'')) = Some x ⟶ ReadL⇩i⇩n⇩t x ≥ 0"
abbreviation "INV st s val bal ≡
fmlookup (storage st) (STR ''Victim'') = Some s ∧ ReadL⇩i⇩n⇩t (accessBalance (accounts st) (STR ''Victim'')) - val ≥ bal ∧ bal ≥ 0"
definition frame_def: "frame bal st ≡ (∃s. INV st s (SUMM s) bal ∧ POS s)"
subsection‹Verification›
lemma conj3: "P ⟹ Q ⟹ R ⟹ P ∧ (Q ∧ R)" by simp
lemma fmfinite: "finite ({(ad, x). fmlookup y ad = Some x})"
proof -
have "{(ad, x). fmlookup y ad = Some x} ⊆ dom (fmlookup y) × ran (fmlookup y)"
proof
fix x assume "x ∈ {(ad, x). fmlookup y ad = Some x}"
then have "fmlookup y (fst x) = Some (snd x)" by auto
then have "fst x ∈ dom (fmlookup y)" and "snd x ∈ ran (fmlookup y)" using Map.ranI by (blast,metis)
then show "x ∈ dom (fmlookup y) × ran (fmlookup y)" by (simp add: mem_Times_iff)
qed
thus ?thesis by (simp add: finite_ran finite_subset)
qed
lemma fmlookup_finite:
fixes f :: "'a ⇒ 'a"
and y :: "('a, 'b) fmap"
assumes "inj_on (λ(ad, x). (f ad, x)) {(ad, x). (fmlookup y ∘ f) ad = Some x}"
shows "finite {(ad, x). (fmlookup y ∘ f) ad = Some x}"
proof (cases rule: inj_on_finite[OF assms(1), of "{(ad, x)|ad x. (fmlookup y) ad = Some x}"])
case 1
then show ?case by auto
next
case 2
then have *: "finite {(ad, x) |ad x. fmlookup y ad = Some x}" using fmfinite[of y] by simp
show ?case using finite_image_set[OF *, of "λ(ad, x). (ad, x)"] by simp
qed
lemma balance_inj: "inj_on (λ(ad, x). (ad + (STR ''.'' + STR ''balance''),x)) {(ad, x). (fmlookup y ∘ f) ad = Some x}"
proof
fix v v' assume asm1: "v ∈ {(ad, x). (fmlookup y ∘ f) ad = Some x}" and asm2: "v' ∈ {(ad, x). (fmlookup y ∘ f) ad = Some x}"
and *:"(case v of (ad, x) ⇒ (ad + (STR ''.'' + STR ''balance''),x)) = (case v' of (ad, x) ⇒ (ad + (STR ''.'' + STR ''balance''),x))"
then obtain ad ad' x x' where **: "v = (ad,x)" and ***: "v'=(ad',x')" by auto
moreover from * ** *** have "ad + (STR ''.'' + STR ''balance'') = ad' + (STR ''.'' + STR ''balance'')" by simp
with * ** have "ad = ad'" using String_Cancel[of ad "STR ''.'' + STR ''balance''" ad' ] by simp
moreover from asm1 asm2 ** *** have "(fmlookup y ∘ f) ad = Some x" and "(fmlookup y ∘ f) ad' = Some x'" by auto
with calculation(3) have "x=x'" by simp
ultimately show "v=v'" by simp
qed
lemma transfer_frame:
assumes "Accounts.transfer ad adv v (accounts st) = Some acc"
and "frame bal st"
and "ad ≠ STR ''Victim''"
shows "frame bal (st⦇accounts := acc⦈)"
proof (cases "adv = STR ''Victim''")
case True
define st' where "st' = st⦇accounts := acc, stack := emptyStore, memory := emptyStore⦈"
from True assms(2) transfer_mono[OF assms(1)] have "(∃s. fmlookup (storage st) (STR ''Victim'') = Some s ∧ ReadL⇩i⇩n⇩t (accessBalance acc (STR ''Victim'')) - (SUMM s) ≥ bal ∧ bal ≥ 0)" by (auto simp add:frame_def)
then have "(∃s. fmlookup (storage st') (STR ''Victim'') = Some s ∧ ReadL⇩i⇩n⇩t (accessBalance (accounts st') (STR ''Victim'')) - (SUMM s) ≥ bal ∧ bal ≥ 0)" by (auto simp add: st'_def)
then show ?thesis using assms(2) by (auto simp add:st'_def frame_def)
next
case False
define st' where "st' = st⦇accounts := acc, stack := emptyStore, memory := emptyStore⦈"
from False assms(2) assms(3) transfer_eq[OF assms(1)] have "(∃s. fmlookup (storage st) (STR ''Victim'') = Some s ∧ ReadL⇩i⇩n⇩t (accessBalance acc (STR ''Victim'')) - (SUMM s) ≥ bal ∧ bal ≥ 0)" by (auto simp add:frame_def)
then have "(∃s. fmlookup (storage st') (STR ''Victim'') = Some s ∧ ReadL⇩i⇩n⇩t (accessBalance (accounts st') (STR ''Victim'')) - (SUMM s) ≥ bal ∧ bal ≥ 0)" by (auto simp add: st'_def)
then show ?thesis using assms(2) by (auto simp add:st'_def frame_def)
qed
lemma decl_frame:
assumes "frame bal st"
and "decl a1 a2 a3 cp cd mem c env st = Normal (rv, st')"
shows "frame bal st'"
proof (cases a2)
case (Value t)
then show ?thesis
proof (cases a3)
case None
with Value show ?thesis using assms by (auto simp add:frame_def)
next
case (Some a)
show ?thesis
proof (cases a)
case (Pair a b)
then show ?thesis
proof (cases a)
case (KValue v)
then show ?thesis
proof (cases b)
case v2: (Value t')
show ?thesis
proof (cases "Valuetypes.convert t' t v")
case None
with Some Pair KValue Value v2 show ?thesis using assms by simp
next
case s2: (Some a)
show ?thesis
proof (cases a)
case p2: (Pair a b)
with Some Pair KValue Value v2 s2 show ?thesis using assms by (auto simp add:frame_def)
qed
qed
next
case (Calldata x2)
with Some Pair KValue Value show ?thesis using assms by simp
next
case (Memory x3)
with Some Pair KValue Value show ?thesis using assms by simp
next
case (Storage x4)
with Some Pair KValue Value show ?thesis using assms by simp
qed
next
case (KCDptr x2)
with Some Pair Value show ?thesis using assms by simp
next
case (KMemptr x3)
with Some Pair Value show ?thesis using assms by simp
next
case (KStoptr x4)
with Some Pair Value show ?thesis using assms by simp
qed
qed
qed
next
case (Calldata x2)
then show ?thesis
proof (cases cp)
case True
then show ?thesis
proof (cases x2)
case (MTArray x t)
then show ?thesis
proof (cases a3)
case None
with Calldata show ?thesis using assms by simp
next
case (Some a)
show ?thesis
proof (cases a)
case (Pair a b)
then show ?thesis
proof (cases a)
case (KValue x1)
with Calldata Some Pair show ?thesis using assms by simp
next
case (KCDptr p)
define l where "l = ShowL⇩n⇩a⇩t (toploc c)"
obtain c' where c_def: "∃x. (x, c') = allocate c" by simp
show ?thesis
proof (cases "cpm2m p l x t cd c'")
case None
with Calldata MTArray Some Pair KCDptr l_def c_def True show ?thesis using assms by simp
next
case s2: (Some a)
with Calldata MTArray Some Pair KCDptr l_def c_def True show ?thesis using assms by (auto simp add:frame_def)
qed
next
case (KMemptr p)
define l where "l = ShowL⇩n⇩a⇩t (toploc c)"
obtain c' where c_def: "∃x. (x, c') = allocate c" by simp
show ?thesis
proof (cases "cpm2m p l x t mem c'")
case None
with Calldata MTArray Some Pair KMemptr l_def c_def True show ?thesis using assms by simp
next
case s2: (Some a)
with Calldata MTArray Some Pair KMemptr l_def c_def True show ?thesis using assms by (auto simp add:frame_def)
qed
next
case (KStoptr x4)
with Calldata Some Pair show ?thesis using assms by simp
qed
qed
qed
next
case (MTValue x2)
with Calldata show ?thesis using assms by simp
qed
next
case False
with Calldata show ?thesis using assms by simp
qed
next
case (Memory x3)
then show ?thesis
proof (cases x3)
case (MTArray x t)
then show ?thesis
proof (cases a3)
case None
with Memory MTArray None show ?thesis using assms by (auto simp add:frame_def simp add:Let_def)
next
case (Some a)
then show ?thesis
proof (cases a)
case (Pair a b)
then show ?thesis
proof (cases a)
case (KValue x1)
with Memory MTArray Some Pair show ?thesis using assms by simp
next
case (KCDptr p)
define m l where "m = memory st" and "l = ShowL⇩n⇩a⇩t (toploc m)"
obtain m' where m'_def: "∃x. (x, m') = allocate m" by simp
then show ?thesis
proof (cases "cpm2m p l x t cd m'")
case None
with Memory MTArray Some Pair KCDptr m_def l_def m'_def show ?thesis using assms by simp
next
case s2: (Some a)
with Memory MTArray Some Pair KCDptr m_def l_def m'_def show ?thesis using assms by (auto simp add:frame_def)
qed
next
case (KMemptr p)
then show ?thesis
proof (cases cp)
case True
define m l where "m = memory st" and "l = ShowL⇩n⇩a⇩t (toploc m)"
obtain m' where m'_def: "∃x. (x, m') = allocate m" by simp
then show ?thesis
proof (cases "cpm2m p l x t mem m'")
case None
with Memory MTArray Some Pair KMemptr True m_def l_def m'_def show ?thesis using assms by simp
next
case s2: (Some a)
with Memory MTArray Some Pair KMemptr True m_def l_def m'_def show ?thesis using assms by (auto simp add:frame_def)
qed
next
case False
with Memory MTArray Some Pair KMemptr show ?thesis using assms by (auto simp add:frame_def)
qed
next
case (KStoptr p)
then show ?thesis
proof (cases b)
case (Value x1)
with Memory MTArray Some Pair KStoptr show ?thesis using assms by simp
next
case (Calldata x2)
with Memory MTArray Some Pair KStoptr show ?thesis using assms by simp
next
case m2: (Memory x3)
with Memory MTArray Some Pair KStoptr show ?thesis using assms by simp
next
case (Storage x4)
then show ?thesis
proof (cases x4)
case (STArray x' t')
define m l where "m = memory st" and "l = ShowL⇩n⇩a⇩t (toploc m)"
obtain m' where m'_def: "∃x. (x, m') = allocate m" by simp
from assms(2) Memory MTArray Some Pair KStoptr Storage STArray m_def l_def m'_def
obtain s where *: "fmlookup (storage st) (address env) = Some s" using Let_def by (auto simp add: Let_def split:option.split_asm)
then show ?thesis
proof (cases "cps2m p l x' t' s m'")
case None
with Memory MTArray Some Pair KStoptr Storage STArray m_def l_def m'_def * show ?thesis using assms by simp
next
case s2: (Some a)
with Memory MTArray Some Pair KStoptr Storage STArray m_def l_def m'_def * show ?thesis using assms by (auto simp add:frame_def)
qed
next
case (STMap x21 x22)
with Memory MTArray Some Pair KStoptr Storage show ?thesis using assms by simp
next
case (STValue x3)
with Memory MTArray Some Pair KStoptr Storage show ?thesis using assms by simp
qed
qed
qed
qed
qed
next
case (MTValue x2)
with Memory show ?thesis using assms by simp
qed
next
case (Storage x4)
then show ?thesis
proof (cases x4)
case (STArray x t)
then show ?thesis
proof (cases a3)
case None
with Storage STArray show ?thesis using assms by simp
next
case (Some a)
then show ?thesis
proof (cases a)
case (Pair a b)
then show ?thesis
proof (cases a)
case (KValue x1)
with Storage STArray Some Pair show ?thesis using assms by simp
next
case (KCDptr x2)
with Storage STArray Some Pair show ?thesis using assms by simp
next
case (KMemptr x3)
with Storage STArray Some Pair show ?thesis using assms by simp
next
case (KStoptr x4)
with Storage STArray Some Pair show ?thesis using assms by (auto simp add:frame_def)
qed
qed
qed
next
case (STMap t t')
then show ?thesis
proof (cases a3)
case None
with Storage STMap show ?thesis using assms by simp
next
case (Some a)
then show ?thesis
proof (cases a)
case (Pair a b)
then show ?thesis
proof (cases a)
case (KValue x1)
with Storage STMap Some Pair show ?thesis using assms by simp
next
case (KCDptr x2)
with Storage STMap Some Pair show ?thesis using assms by simp
next
case (KMemptr x3)
with Storage STMap Some Pair show ?thesis using assms by simp
next
case (KStoptr x4)
with Storage STMap Some Pair show ?thesis using assms by (auto simp add:frame_def)
qed
qed
qed
next
case (STValue x3)
with Storage show ?thesis using assms by simp
qed
qed
context statement_with_gas
begin
lemma secureassign:
assumes "stmt assign ep env cd st = Normal((), st')"
and "fmlookup (storage st) (STR ''Victim'') = Some s"
and "address env = (STR ''Victim'')"
and "fmlookup (denvalue env) (STR ''balance'') = Some (Storage (STMap TAddr (STValue (TUInt 256))), Storeloc STR ''balance'')"
and "accessStore x (stack st) = Some (KValue (accessStorage (TUInt 256) (sender env + (STR ''.'' + STR ''balance'')) s))"
and "ReadL⇩i⇩n⇩t (accessBalance (accounts st) (STR ''Victim'')) - (SUMM s) ≥ bal"
and "POS s"
obtains s'
where "fmlookup (storage st') (STR ''Victim'') = Some s'"
and "ReadL⇩i⇩n⇩t (accessBalance (accounts st') (STR ''Victim'')) - (SUMM s' + ReadL⇩i⇩n⇩t (accessStorage (TUInt 256) (sender env + (STR ''.'' + STR ''balance'')) s)) ≥ bal"
and "accessStore x (stack st') = Some (KValue (accessStorage (TUInt 256) (sender env + (STR ''.'' + STR ''balance'')) s))"
and "POS s'"
proof -
define st'' where "st'' = st⦇gas := gas st - costs assign ep env cd st⦈"
define st''' where "st''' = st''⦇gas := gas st'' - costs⇩e (UINT 256 0) ep env cd st''⦈"
define st'''' where "st'''' = st'''⦇gas := gas st''' - costs⇩e SENDER ep env cd st'''⦈"
from assms(1) have c1: "gas st > costs assign ep env cd st" by (auto split:if_split_asm)
have c2: "gas st'' > costs⇩e (UINT 256 0) ep env cd st''"
proof (rule ccontr)
assume "¬ costs⇩e (UINT 256 0) ep env cd st'' < gas st''"
with c1 show False using assms(1) st''_def st'''_def by auto
qed
hence *:"expr (UINT 256 0) ep env cd st'' = Normal ((KValue (createUInt 256 0),Value (TUInt 256)), st''')" using expr.simps(2)[of 256 0 ep env cd "st⦇gas := gas st - costs assign ep env cd st⦈"] st''_def st'''_def by simp
moreover have "gas st''' > costs⇩e SENDER ep env cd st'''"
proof (rule ccontr)
assume "¬ costs⇩e SENDER ep env cd st''' < gas st'''"
with c1 c2 show False using assms(1,4) st''_def st'''_def by auto
qed
with assms(4) have **:"lexp (Ref (STR ''balance'') [SENDER]) ep env cd st''' = Normal ((LStoreloc ((sender env) + (STR ''.'' + STR ''balance'')), Storage (STValue (TUInt 256))), st'''')" using st''''_def by simp
moreover have "Valuetypes.convert (TUInt 256) (TUInt 256) (ShowL⇩i⇩n⇩t 0) = Some (ShowL⇩i⇩n⇩t 0, TUInt 256)" by simp
moreover from * ** st''_def assms(1) obtain s'' where ***: "fmlookup (storage st'''') (address env) = Some s''" by (auto split:if_split_asm option.split_asm)
ultimately have ****:"st' = st''''⦇storage := fmupd (STR ''Victim'') (fmupd ((sender env) + (STR ''.'' + STR ''balance'')) (ShowL⇩i⇩n⇩t 0) s'') (storage st)⦈" using c1 st''_def st'''_def st''''_def assms(1,3) by auto
moreover define s' where s'_def: "s' = (fmupd ((sender env) + (STR ''.'' + STR ''balance'')) (ShowL⇩i⇩n⇩t 0) s'')"
ultimately have "fmlookup (storage st') (STR ''Victim'') = Some s'"
and *****:"fmlookup s' ((sender env) + (STR ''.'' + STR ''balance'')) = Some (ShowL⇩i⇩n⇩t 0)" by simp_all
moreover have "SUMM s' + ReadL⇩i⇩n⇩t (accessStorage (TUInt 256) (sender env + (STR ''.'' + STR ''balance'')) s) = SUMM s"
proof -
have s1: "SUMM s = (∑(ad,x)|fmlookup s (ad + (STR ''.'' + STR ''balance'')) = Some x ∧ ad ≠ sender env. ReadL⇩i⇩n⇩t x) + ReadL⇩i⇩n⇩t (accessStorage (TUInt 256) (sender env + (STR ''.'' + STR ''balance'')) s)"
proof (cases "fmlookup s (sender env + (STR ''.'' + STR ''balance'')) = None")
case True
then have "accessStorage (TUInt 256) (sender env + (STR ''.'' + STR ''balance'')) s = ShowL⇩i⇩n⇩t 0" by simp
moreover have "{(ad,x). fmlookup s (ad + (STR ''.'' + STR ''balance'')) = Some x} = {(ad,x). fmlookup s (ad + (STR ''.'' + STR ''balance'')) = Some x ∧ ad ≠ sender env}"
proof
show "{(ad, x). fmlookup s (ad + (STR ''.'' + STR ''balance'')) = Some x} ⊆ {(ad, x). fmlookup s (ad + (STR ''.'' + STR ''balance'')) = Some x ∧ ad ≠ sender env}"
proof
fix x
assume "x ∈ {(ad, x). fmlookup s (ad + (STR ''.'' + STR ''balance'')) = Some x}"
then show "x ∈ {(ad, x). fmlookup s (ad + (STR ''.'' + STR ''balance'')) = Some x ∧ ad ≠ sender env}" using True by auto
qed
next
show "{(ad, x). fmlookup s (ad + (STR ''.'' + STR ''balance'')) = Some x ∧ ad ≠ sender env} ⊆ {(ad, x). fmlookup s (ad + (STR ''.'' + STR ''balance'')) = Some x }"
proof
fix x
assume "x ∈ {(ad, x). fmlookup s (ad + (STR ''.'' + STR ''balance'')) = Some x ∧ ad ≠ sender env}"
then show "x ∈ {(ad, x). fmlookup s (ad + (STR ''.'' + STR ''balance'')) = Some x}" using True by auto
qed
qed
then have "SUMM s = (∑(ad,x)|fmlookup s (ad + (STR ''.'' + STR ''balance'')) = Some x ∧ ad ≠ sender env. ReadL⇩i⇩n⇩t x)" by simp
ultimately show ?thesis using Read_ShowL_id by simp
next
case False
then obtain val where val_def: "fmlookup s (sender env + (STR ''.'' + STR ''balance'')) = Some val" by auto
have "inj_on (λ(ad, x). (ad + (STR ''.'' + STR ''balance''), x)) {(ad, x). (fmlookup s ∘ (λad. ad + (STR ''.'' + STR ''balance''))) ad = Some x}" using balance_inj by simp
then have "finite {(ad, x). (fmlookup s ∘ (λad. ad + (STR ''.'' + STR ''balance''))) ad = Some x}" using fmlookup_finite[of "λad. (ad + (STR ''.'' + STR ''balance''))" s] by simp
then have sum1: "finite ({(ad,x). fmlookup s (ad + (STR ''.'' + STR ''balance'')) = Some x ∧ ad ≠ sender env})" using finite_subset[of "{(ad, x). fmlookup s (ad + (STR ''.'' + STR ''balance'')) = Some x ∧ ad ≠ sender env}" "{(ad, x). fmlookup s (ad + (STR ''.'' + STR ''balance'')) = Some x}"] by auto
moreover have sum2: "(sender env,val) ∉ {(ad,x). fmlookup s (ad + (STR ''.'' + STR ''balance'')) = Some x ∧ ad ≠ sender env}" by simp
moreover from sum1 x1 val_def have "insert (sender env,val) {(ad, x). fmlookup s (ad + (STR ''.'' + STR ''balance'')) = Some x ∧ ad ≠ sender env} = {(ad, x). fmlookup s (ad + (STR ''.'' + STR ''balance'')) = Some x}" by auto
ultimately show ?thesis using sum.insert[OF sum1 sum2, of "λ(ad,x). ReadL⇩i⇩n⇩t x"] val_def by simp
qed
moreover have s2: "SUMM s' = (∑(ad,x)|fmlookup s' (ad + (STR ''.'' + STR ''balance'')) = Some x ∧ ad ≠ sender env. ReadL⇩i⇩n⇩t x)"
proof -
have "inj_on (λ(ad, x). (ad + (STR ''.'' + STR ''balance''), x)) {(ad, x). (fmlookup s' ∘ (λad. ad + (STR ''.'' + STR ''balance''))) ad = Some x}" using balance_inj by simp
then have "finite {(ad, x). (fmlookup s' ∘ (λad. ad + (STR ''.'' + STR ''balance''))) ad = Some x}" using fmlookup_finite[of "λad. (ad + (STR ''.'' + STR ''balance''))" s'] by simp
then have sum1: "finite ({(ad,x). fmlookup s' (ad + (STR ''.'' + STR ''balance'')) = Some x ∧ ad ≠ sender env})" using finite_subset[of "{(ad, x). fmlookup s' (ad + (STR ''.'' + STR ''balance'')) = Some x ∧ ad ≠ sender env}" "{(ad, x). fmlookup s' (ad + (STR ''.'' + STR ''balance'')) = Some x}"] by auto
moreover have sum2: "(sender env,ShowL⇩i⇩n⇩t 0) ∉ {(ad,x). fmlookup s' (ad + (STR ''.'' + STR ''balance'')) = Some x ∧ ad ≠ sender env}" by simp
moreover from ***** have "insert (sender env,ShowL⇩i⇩n⇩t 0) {(ad, x). fmlookup s' (ad + (STR ''.'' + STR ''balance'')) = Some x ∧ ad ≠ sender env} = {(ad, x). fmlookup s' (ad + (STR ''.'' + STR ''balance'')) = Some x}" by auto
ultimately show ?thesis using sum.insert[OF sum1 sum2, of "λ(ad,x). ReadL⇩i⇩n⇩t x"] Read_ShowL_id by simp
qed
moreover have s3: "(∑(ad,x)|fmlookup s' (ad + (STR ''.'' + STR ''balance'')) = Some x ∧ ad ≠ sender env. ReadL⇩i⇩n⇩t x)
=(∑(ad,x)|fmlookup s (ad + (STR ''.'' + STR ''balance'')) = Some x ∧ ad ≠ sender env. ReadL⇩i⇩n⇩t x)"
proof -
have "{(ad,x). fmlookup s' (ad + (STR ''.'' + STR ''balance'')) = Some x ∧ ad ≠ sender env} = {(ad,x). fmlookup s (ad + (STR ''.'' + STR ''balance'')) = Some x ∧ ad ≠ sender env}"
proof
show "{(ad, x). fmlookup s' (ad + (STR ''.'' + STR ''balance'')) = Some x ∧ ad ≠ sender env}
⊆ {(ad, x). fmlookup s (ad + (STR ''.'' + STR ''balance'')) = Some x ∧ ad ≠ sender env}"
proof
fix xx
assume "xx ∈ {(ad, x). fmlookup s' (ad + (STR ''.'' + STR ''balance'')) = Some x ∧ ad ≠ sender env}"
then obtain ad x where "xx = (ad,x)" and "fmlookup s' (ad + (STR ''.'' + STR ''balance'')) = Some x" and "ad ≠ sender env" by auto
moreover have "s''=s" using assms(2,3) s'_def *** st''''_def st'''_def st''_def by simp
moreover from `ad ≠ sender env` have "ad + (STR ''.'' + STR ''balance'') ≠ (sender env) + (STR ''.'' + STR ''balance'')" using String_Cancel[where c="(STR ''.'' + STR ''balance'')"] by auto
ultimately show "xx ∈ {(ad, x). fmlookup s (ad + (STR ''.'' + STR ''balance'')) = Some x ∧ ad ≠ sender env}" using s'_def by simp
qed
next
show "{(ad, x). fmlookup s (ad + (STR ''.'' + STR ''balance'')) = Some x ∧ ad ≠ sender env}
⊆ {(ad, x). fmlookup s' (ad + (STR ''.'' + STR ''balance'')) = Some x ∧ ad ≠ sender env}"
proof
fix xx
assume "xx ∈ {(ad, x). fmlookup s (ad + (STR ''.'' + STR ''balance'')) = Some x ∧ ad ≠ sender env}"
then obtain ad x where "xx = (ad,x)" and "fmlookup s (ad + (STR ''.'' + STR ''balance'')) = Some x" and "ad ≠ sender env" by auto
moreover have "s''=s" using assms(2,3) s'_def *** st''''_def st'''_def st''_def by simp
moreover from `ad ≠ sender env` have "ad + (STR ''.'' + STR ''balance'') ≠ (sender env) + (STR ''.'' + STR ''balance'')" using String_Cancel[where c="(STR ''.'' + STR ''balance'')"] by auto
ultimately show "xx ∈ {(ad, x). fmlookup s' (ad + (STR ''.'' + STR ''balance'')) = Some x ∧ ad ≠ sender env}" using s'_def by simp
qed
qed
thus ?thesis by simp
qed
ultimately have "SUMM s' = SUMM s - ReadL⇩i⇩n⇩t (accessStorage (TUInt 256) (sender env + (STR ''.'' + STR ''balance'')) s) "
proof -
from s2 have "SUMM s' = (∑(ad,x)|fmlookup s' (ad + (STR ''.'' + STR ''balance'')) = Some x ∧ ad ≠ sender env. ReadL⇩i⇩n⇩t x)" by simp
also from s3 have "… = (∑(ad,x)|fmlookup s (ad + (STR ''.'' + STR ''balance'')) = Some x ∧ ad ≠ sender env. ReadL⇩i⇩n⇩t x)" by simp
also from s1 have "… = SUMM s - ReadL⇩i⇩n⇩t (accessStorage (TUInt 256) (sender env + (STR ''.'' + STR ''balance'')) s) " by simp
finally show ?thesis .
qed
then show ?thesis by simp
qed
moreover have "POS s'"
proof (rule allI[OF allI])
fix x xa
show "fmlookup s' (x + (STR ''.'' + STR ''balance'')) = Some xa ⟶ 0 ≤ (⌈xa⌉::int)"
proof
assume a1: "fmlookup s' (x + (STR ''.'' + STR ''balance'')) = Some xa"
show "0 ≤ (⌈xa⌉::int)"
proof (cases "x = sender env")
case True
then show ?thesis using s'_def a1 using Read_ShowL_id by auto
next
case False
moreover have "s''=s" using assms(2,3) s'_def *** st''''_def st'''_def st''_def by simp
ultimately have "fmlookup s (x + (STR ''.'' + STR ''balance'')) = Some xa" using s'_def a1 String_Cancel by (auto split:if_split_asm)
then show ?thesis using assms(7) by simp
qed
qed
qed
moreover have "ReadL⇩i⇩n⇩t (accessBalance (accounts st') (STR ''Victim'')) = ReadL⇩i⇩n⇩t (accessBalance (accounts st) (STR ''Victim''))" using **** st''_def st'''_def st''''_def by simp
moreover from assms(5) have "accessStore x (stack st') = Some (KValue (accessStorage (TUInt 256) (sender env + (STR ''.'' + STR ''balance'')) s) )"using **** st''_def st'''_def st''''_def by simp
ultimately show ?thesis using assms(6) that by simp
qed
lemma securesender:
assumes "expr SENDER ep env cd st = Normal((KValue v,t), st')"
and "fmlookup (storage st) (STR ''Victim'') = Some s"
and "ReadL⇩i⇩n⇩t (accessBalance (accounts st) (STR ''Victim'')) - SUMM s ≥ bal ∧ POS s"
obtains s' where
"v = sender env"
and "t = Value TAddr"
and "fmlookup (storage st') (STR ''Victim'') = Some s'"
and "ReadL⇩i⇩n⇩t (accessBalance (accounts st') (STR ''Victim'')) - SUMM s' ≥ bal ∧ POS s'"
using assms by (auto split:if_split_asm)
lemma securessel:
assumes "ssel type loc [] ep env cd st = Normal (x, st')"
and "fmlookup (storage st) (STR ''Victim'') = Some s"
and "ReadL⇩i⇩n⇩t (accessBalance (accounts st) (STR ''Victim'')) - SUMM s ≥ bal ∧ POS s"
obtains s' where
"x = (loc, type)"
and "fmlookup (storage st') (STR ''Victim'') = Some s'"
and "ReadL⇩i⇩n⇩t (accessBalance (accounts st') (STR ''Victim'')) - SUMM s' ≥ bal ∧ POS s'"
using assms by auto
lemma securessel2:
assumes "ssel (STMap TAddr (STValue (TUInt 256))) (STR ''balance'') [SENDER] ep env cd st = Normal ((loc, type), st')"
and "fmlookup (storage st) (STR ''Victim'') = Some s"
and "ReadL⇩i⇩n⇩t (accessBalance (accounts st) (STR ''Victim'')) - SUMM s ≥ bal ∧ POS s"
obtains s' where
"loc = sender env + (STR ''.'' + STR ''balance'')"
and "type = STValue (TUInt 256)"
and "fmlookup (storage st') (STR ''Victim'') = Some s'"
and "ReadL⇩i⇩n⇩t (accessBalance (accounts st') (STR ''Victim'')) - SUMM s' ≥ bal ∧ POS s'"
proof -
from assms(1) obtain v t st'' st''' x
where *: "expr SENDER ep env cd st = Normal ((KValue v, t), st'')"
and **: "ssel (STValue (TUInt 256)) (hash (STR ''balance'') v) [] ep env cd st'' = Normal (x,st''')"
and "st' = st'''"
by (auto split:if_split_asm)
moreover obtain s'' where "v =sender env"
and "t = Value TAddr"
and ***:"fmlookup (storage st'') (STR ''Victim'') = Some s''"
and ****: "ReadL⇩i⇩n⇩t (accessBalance (accounts st'') (STR ''Victim'')) - SUMM s'' ≥ bal ∧ POS s''"
using securesender[OF * assms(2,3)] by auto
moreover obtain s''' where "x = (hash (STR ''balance'') v, STValue (TUInt 256))"
and "fmlookup (storage st''') (STR ''Victim'') = Some s'''"
and "ReadL⇩i⇩n⇩t (accessBalance (accounts st''') (STR ''Victim'')) - SUMM s''' ≥ bal ∧ POS s'''"
using securessel[OF ** *** ****] by auto
ultimately show ?thesis using assms(1) that by simp
qed
lemma securerexp:
assumes "rexp myrexp e⇩p env cd st = Normal ((v, t), st')"
and "fmlookup (denvalue env) (STR ''balance'') = Some (Storage (STMap TAddr (STValue (TUInt 256))), Storeloc STR ''balance'')"
and "fmlookup (storage st) (STR ''Victim'') = Some s"
and "ReadL⇩i⇩n⇩t (accessBalance (accounts st) (STR ''Victim'')) - SUMM s ≥ bal ∧ POS s"
and "address env = STR ''Victim''"
obtains s' where
"fmlookup (storage st') (address env) = Some s'"
and "v = KValue (accessStorage (TUInt 256) (sender env + (STR ''.'' + STR ''balance'')) s')"
and "t = Value (TUInt 256)"
and "ReadL⇩i⇩n⇩t (accessBalance (accounts st') (STR ''Victim'')) - SUMM s' ≥ bal ∧ POS s'"
proof -
from assms(1,2) obtain l' t'' st'' s
where *: "ssel (STMap TAddr (STValue (TUInt 256))) (STR ''balance'') [SENDER] e⇩p env cd st = Normal ((l', STValue t''), st'')"
and "fmlookup (storage st'') (address env) = Some s"
and "v = KValue (accessStorage t'' l' s)"
and "t = Value t''" and "st'=st''"
by (simp split:if_split_asm option.split_asm)
moreover obtain s'' where
"fmlookup (storage st'') (STR ''Victim'') = Some s''"
and "ReadL⇩i⇩n⇩t (accessBalance (accounts st'') (STR ''Victim'')) - SUMM s'' ≥ bal ∧ POS s''"
and "l'=sender env + (STR ''.'' + STR ''balance'')" and "t'' = TUInt 256" using securessel2[OF * assms(3,4)] by blast
ultimately show ?thesis using assms(1,5) that by auto
qed
lemma securelval:
assumes "expr mylval ep env cd st = Normal((v,t), st')"
and "fmlookup (denvalue env) (STR ''balance'') = Some (Storage (STMap TAddr (STValue (TUInt 256))), Storeloc STR ''balance'')"
and "fmlookup (storage st) (STR ''Victim'') = Some s"
and "ReadL⇩i⇩n⇩t (accessBalance (accounts st) (STR ''Victim'')) - SUMM s ≥ bal ∧ bal ≥ 0 ∧ POS s"
and "address env = STR ''Victim''"
obtains s' where "fmlookup (storage st') (STR ''Victim'') = Some s'"
and "v = KValue (accessStorage (TUInt 256) (sender env + (STR ''.'' + STR ''balance'')) s')"
and "t = Value (TUInt 256)"
and "ReadL⇩i⇩n⇩t (accessBalance (accounts st') (STR ''Victim'')) - SUMM s' ≥ bal ∧ bal ≥ 0 ∧ POS s'"
proof -
define st'' where "st'' = st⦇gas := gas st - costs⇩e mylval ep env cd st⦈"
with assms(3,4) have *: "fmlookup (storage st'') (STR ''Victim'') = Some s"
and **: "ReadL⇩i⇩n⇩t (accessBalance (accounts st'') (STR ''Victim'')) - SUMM s ≥ bal ∧ POS s" by simp+
from assms(1) st''_def obtain v' t' st''' where ***: "rexp myrexp ep env cd st'' = Normal ((v, t), st''')"
and "v' = v"
and "t' = t"
and "st''' = st'"
by (simp split:if_split_asm)
with securerexp[OF *** assms(2) * **] show ?thesis using assms(1,4,5) that by auto
qed
lemma plus_frame:
assumes "expr (PLUS (LVAL (Ref (STR ''balance'') [SENDER])) VALUE) ep env cd st = Normal (kv, st')"
and "ReadL⇩i⇩n⇩t (accessStorage (TUInt 256) (sender env + (STR ''.'' + STR ''balance'')) s) + ReadL⇩i⇩n⇩t (svalue env) < 2^256"
and "ReadL⇩i⇩n⇩t (accessStorage (TUInt 256) (sender env + (STR ''.'' + STR ''balance'')) s) + ReadL⇩i⇩n⇩t (svalue env) ≥ 0"
and "fmlookup (storage st) (STR ''Victim'') = Some s"
and "ReadL⇩i⇩n⇩t (accessBalance (accounts st) (STR ''Victim'')) - SUMM s ≥ bal"
and "fmlookup (denvalue env) (STR ''balance'') = Some (Storage (STMap TAddr (STValue (TUInt 256))), Storeloc STR ''balance'')"
and "address env = (STR ''Victim'')"
shows "kv = (KValue (ShowL⇩i⇩n⇩t (ReadL⇩i⇩n⇩t (accessStorage (TUInt 256) (sender env + (STR ''.'' + STR ''balance'')) s) + ReadL⇩i⇩n⇩t (svalue env))), Value (TUInt 256))"
and "fmlookup (storage st') (STR ''Victim'') = Some s"
and "ReadL⇩i⇩n⇩t (accessBalance (accounts st') (STR ''Victim'')) = ReadL⇩i⇩n⇩t (accessBalance (accounts st) (STR ''Victim''))"
proof -
define st0 where "st0 = st⦇gas := gas st - costs⇩e (PLUS (LVAL (Ref (STR ''balance'') [SENDER])) VALUE) ep env cd st⦈"
define st1 where "st1 = st0⦇gas := gas st0 - costs⇩e (LVAL (Ref (STR ''balance'') [SENDER])) ep env cd st0⦈"
define st2 where "st2 = st1⦇gas := gas st1 - costs⇩e SENDER ep env cd st1⦈"
define st3 where "st3 = st2⦇gas := gas st2 - costs⇩e VALUE ep env cd st2⦈"
from assms(1) obtain v1 t1 v2 t2 st'' st''' st'''' v t where
*: "expr (LVAL (Ref (STR ''balance'') [SENDER])) ep env cd st0 = Normal ((KValue v1, Value t1), st'')"
and **: "expr VALUE ep env cd st'' = Normal ((KValue v2, Value t2), st''')"
and ***: "add t1 t2 v1 v2 = Some (v,t)"
and ****: "expr (PLUS (LVAL (Ref (STR ''balance'') [SENDER])) VALUE) ep env cd st = Normal ((KValue v, Value t), st'''')"
using st0_def by (auto simp del: expr.simps simp add:expr.simps(11) split:if_split_asm result.split_asm Stackvalue.split_asm Type.split_asm option.split_asm)
moreover have "expr (LVAL (Ref (STR ''balance'') [SENDER])) ep env cd st0 = Normal ((KValue (accessStorage (TUInt 256) (sender env + (STR ''.'' + STR ''balance'')) s), Value (TUInt 256)), st'')"
and "st'' = st2"
proof -
from * obtain l' t' s'' where *****: "ssel (STMap TAddr (STValue (TUInt 256))) (STR ''balance'') [SENDER] ep env cd st1 = Normal ((l', STValue t'), st'')"
and ******: "fmlookup (storage st'') (address env) = Some s''" and "v1 = (accessStorage t' l' s'')" and "t' = t1"
using st0_def st1_def assms(4,6) by (auto simp del: accessStorage.simps ssel.simps split:if_split_asm option.split_asm STypes.split_asm result.split_asm)
moreover from ***** have "expr SENDER ep env cd st1 = Normal ((KValue (sender env), Value TAddr), st2)" using st2_def by (simp split:if_split_asm)
with ***** have "st'' = st2" and "l' = sender env + (STR ''.'' + STR ''balance'')" and "t' = TUInt 256" by auto
moreover from ****** `st'' = st2` have "s''=s" using st0_def st1_def st2_def assms(4,7) by auto
ultimately show "expr (LVAL (Ref (STR ''balance'') [SENDER])) ep env cd st0 = Normal ((KValue (accessStorage (TUInt 256) (sender env + (STR ''.'' + STR ''balance'')) s), Value (TUInt 256)), st'')"
and "st'' = st2" using * by (auto split:if_split_asm)
qed
moreover from ** `st'' = st2` have "expr VALUE ep env cd st2 = Normal ((KValue (svalue env), Value (TUInt 256)), st3)" and "st''' = st3" using st1_def st3_def by (auto split:if_split_asm)
moreover have "add (TUInt 256) (TUInt 256) (accessStorage (TUInt 256) (sender env + (STR ''.'' + STR ''balance'')) s) (svalue env) = Some (ShowL⇩i⇩n⇩t (ReadL⇩i⇩n⇩t (accessStorage (TUInt 256) (sender env + (STR ''.'' + STR ''balance'')) s) + ReadL⇩i⇩n⇩t (svalue env)), TUInt 256)" (is "?LHS = ?RHS")
proof -
have "?LHS = Some (createUInt 256 (⌈(accessStorage (TUInt 256) (sender env + (STR ''.'' + STR ''balance'')) s)⌉+ ⌈(svalue env)⌉), TUInt 256)" using add_def olift.simps(2)[of "(+)" 256 256] by simp
with assms(2,3) show "?LHS = ?RHS" by simp
qed
ultimately have "v= (ShowL⇩i⇩n⇩t (ReadL⇩i⇩n⇩t (accessStorage (TUInt 256) (sender env + (STR ''.'' + STR ''balance'')) s) + ReadL⇩i⇩n⇩t (svalue env)))" and "t = TUInt 256" and "st' = st3" using st0_def assms(1) by (auto split:if_split_asm)
with assms(1) **** have "kv = (KValue (ShowL⇩i⇩n⇩t (ReadL⇩i⇩n⇩t (accessStorage (TUInt 256) (sender env + (STR ''.'' + STR ''balance'')) s) + ReadL⇩i⇩n⇩t (svalue env))), Value (TUInt 256))" using st0_def by simp
moreover from assms(4) st0_def st1_def st2_def st3_def `st' = st3` have "fmlookup (storage st') (STR ''Victim'') = Some s" by simp
moreover from assms(5) st0_def st1_def st2_def st3_def `st' = st3` have "ReadL⇩i⇩n⇩t (accessBalance (accounts st') (STR ''Victim'')) - SUMM s ≥ bal" by simp
moreover have "ReadL⇩i⇩n⇩t (accessBalance (accounts st') (STR ''Victim'')) = ReadL⇩i⇩n⇩t (accessBalance (accounts st) (STR ''Victim''))" using st0_def st1_def st2_def st3_def `st' = st3` by simp
ultimately show "kv = (KValue (ShowL⇩i⇩n⇩t (ReadL⇩i⇩n⇩t (accessStorage (TUInt 256) (sender env + (STR ''.'' + STR ''balance'')) s) + ReadL⇩i⇩n⇩t (svalue env))), Value (TUInt 256))"
and "fmlookup (storage st') (STR ''Victim'') = Some s"
and "ReadL⇩i⇩n⇩t (accessBalance (accounts st') (STR ''Victim'')) = ReadL⇩i⇩n⇩t (accessBalance (accounts st) (STR ''Victim''))" by auto
qed
lemma deposit_frame:
assumes "stmt deposit ep env cd st = Normal ((), st')"
and "fmlookup (storage st) (STR ''Victim'') = Some s"
and "address env = (STR ''Victim'')"
and "fmlookup (denvalue env) (STR ''balance'') = Some (Storage (STMap TAddr (STValue (TUInt 256))), Storeloc STR ''balance'')"
and "ReadL⇩i⇩n⇩t (accessBalance (accounts st) (STR ''Victim'')) - SUMM s ≥ bal + ReadL⇩i⇩n⇩t (svalue env)"
and "ReadL⇩i⇩n⇩t (accessStorage (TUInt 256) (sender env + (STR ''.'' + STR ''balance'')) s) + ReadL⇩i⇩n⇩t (svalue env) < 2^256"
and "ReadL⇩i⇩n⇩t (accessStorage (TUInt 256) (sender env + (STR ''.'' + STR ''balance'')) s) + ReadL⇩i⇩n⇩t (svalue env) ≥ 0"
and "POS s"
obtains s'
where "fmlookup (storage st') (STR ''Victim'') = Some s'"
and "ReadL⇩i⇩n⇩t (accessBalance (accounts st') (STR ''Victim'')) - SUMM s' ≥ bal"
and "POS s'"
proof -
define st0 where "st0 = st⦇gas := gas st - costs deposit ep env cd st⦈"
from assms(1) st0_def obtain kv st'' where *: "expr (PLUS (LVAL (Ref (STR ''balance'') [SENDER])) VALUE) ep env cd st0 = Normal (kv, st'')" by (auto simp del: expr.simps split:if_split_asm result.split_asm)
moreover have "fmlookup (storage st0) (STR ''Victim'') = Some s" using st0_def assms(2) by simp
moreover from assms(5) have "ReadL⇩i⇩n⇩t (accessBalance (accounts st0) (STR ''Victim'')) - SUMM s ≥ bal + ReadL⇩i⇩n⇩t (svalue env)" using st0_def by simp
ultimately have **: "kv = (KValue ⌊(⌈accessStorage (TUInt 256) (sender env + (STR ''.'' + STR ''balance'')) s⌉::int) + ⌈svalue env⌉⌋, Value (TUInt 256))"
and st''_s:"fmlookup (storage st'') STR ''Victim'' = Some s"
and ac: "ReadL⇩i⇩n⇩t (accessBalance (accounts st'') (STR ''Victim'')) = ReadL⇩i⇩n⇩t (accessBalance (accounts st0) (STR ''Victim''))"
using plus_frame[OF _ assms(6,7) _ _ assms(4,3), of ep cd st0 kv st''] by auto
define v where "v= (⌈accessStorage (TUInt 256) (sender env + (STR ''.'' + STR ''balance'')) s⌉::int) + ⌈svalue env⌉"
moreover from * ** assms(1) st0_def obtain rl st''' where ***: "lexp (Ref (STR ''balance'') [SENDER]) ep env cd st'' = Normal (rl, st''')" by (auto simp del:expr.simps lexp.simps accessStorage.simps split:if_split_asm result.split_asm)
moreover from *** assms have "rl = (LStoreloc ((sender env) + (STR ''.'' + STR ''balance'')), Storage (STValue (TUInt 256)))" and st'''_def: "st''' = st''⦇gas := gas st'' - costs⇩e SENDER ep env cd st''⦈"
proof -
from *** assms(4) obtain l' t' where
"fmlookup (denvalue env) (STR ''balance'') = Some (Storage (STMap TAddr (STValue (TUInt 256))), Storeloc (STR ''balance''))"
and *:"ssel (STMap TAddr (STValue (TUInt 256))) (STR ''balance'') [SENDER] ep env cd st'' = Normal ((l',t'), st''')"
and "rl = (LStoreloc l', Storage t')"
by (auto simp del: ssel.simps split:if_split_asm option.split_asm result.split_asm)
moreover from * have "ssel (STMap TAddr (STValue (TUInt 256))) (STR ''balance'') [SENDER] ep env cd st'' = Normal ((((sender env) + (STR ''.'' + STR ''balance'')), STValue (TUInt 256)), st''⦇gas := gas st'' - costs⇩e SENDER ep env cd st''⦈)" by (simp split:if_split_asm)
ultimately show "rl = (LStoreloc ((sender env) + (STR ''.'' + STR ''balance'')), Storage (STValue (TUInt 256)))" and st'''_def: "st''' = st''⦇gas := gas st'' - costs⇩e SENDER ep env cd st''⦈" by auto
qed
moreover have "Valuetypes.convert (TUInt 256) (TUInt 256) (ShowL⇩i⇩n⇩t v) = Some (ShowL⇩i⇩n⇩t v, TUInt 256)" by simp
moreover from st''_s st'''_def have s'''_s: "fmlookup (storage st''') (STR ''Victim'') = Some s" by simp
ultimately have ****:"st' = st'''⦇storage := fmupd (STR ''Victim'') (fmupd ((sender env) + (STR ''.'' + STR ''balance'')) (ShowL⇩i⇩n⇩t v) s) (storage st''')⦈"
using assms(1) * ** st0_def assms(3) by (auto simp del:expr.simps lexp.simps accessStorage.simps split:if_split_asm)
moreover define s' where "s' = (fmupd ((sender env) + (STR ''.'' + STR ''balance'')) (ShowL⇩i⇩n⇩t v) s)"
ultimately have "fmlookup (storage st') (STR ''Victim'') = Some s'"
and *****:"fmlookup s' ((sender env) + (STR ''.'' + STR ''balance'')) = Some (ShowL⇩i⇩n⇩t v)" by simp_all
moreover have "SUMM s' = SUMM s + ⌈svalue env⌉"
proof -
have s1: "SUMM s = (∑(ad,x)|fmlookup s (ad + (STR ''.'' + STR ''balance'')) = Some x ∧ ad ≠ sender env. ReadL⇩i⇩n⇩t x) + ReadL⇩i⇩n⇩t (accessStorage (TUInt 256) (sender env + (STR ''.'' + STR ''balance'')) s)"
proof (cases "fmlookup s (sender env + (STR ''.'' + STR ''balance'')) = None")
case True
then have "accessStorage (TUInt 256) (sender env + (STR ''.'' + STR ''balance'')) s = ShowL⇩i⇩n⇩t 0" by simp
moreover have "{(ad,x). fmlookup s (ad + (STR ''.'' + STR ''balance'')) = Some x} = {(ad,x). fmlookup s (ad + (STR ''.'' + STR ''balance'')) = Some x ∧ ad ≠ sender env}"
proof
show "{(ad, x). fmlookup s (ad + (STR ''.'' + STR ''balance'')) = Some x} ⊆ {(ad, x). fmlookup s (ad + (STR ''.'' + STR ''balance'')) = Some x ∧ ad ≠ sender env}"
proof
fix x
assume "x ∈ {(ad, x). fmlookup s (ad + (STR ''.'' + STR ''balance'')) = Some x}"
then show "x ∈ {(ad, x). fmlookup s (ad + (STR ''.'' + STR ''balance'')) = Some x ∧ ad ≠ sender env}" using True by auto
qed
next
show "{(ad, x). fmlookup s (ad + (STR ''.'' + STR ''balance'')) = Some x ∧ ad ≠ sender env} ⊆ {(ad, x). fmlookup s (ad + (STR ''.'' + STR ''balance'')) = Some x }"
proof
fix x
assume "x ∈ {(ad, x). fmlookup s (ad + (STR ''.'' + STR ''balance'')) = Some x ∧ ad ≠ sender env}"
then show "x ∈ {(ad, x). fmlookup s (ad + (STR ''.'' + STR ''balance'')) = Some x}" using True by auto
qed
qed
then have "SUMM s = (∑(ad,x)|fmlookup s (ad + (STR ''.'' + STR ''balance'')) = Some x ∧ ad ≠ sender env. ReadL⇩i⇩n⇩t x)" by simp
ultimately show ?thesis using Read_ShowL_id by simp
next
case False
then obtain val where val_def: "fmlookup s (sender env + (STR ''.'' + STR ''balance'')) = Some val" by auto
have "inj_on (λ(ad, x). (ad + (STR ''.'' + STR ''balance''), x)) {(ad, x). (fmlookup s ∘ (λad. ad + (STR ''.'' + STR ''balance''))) ad = Some x}" using balance_inj by simp
then have "finite {(ad, x). (fmlookup s ∘ (λad. ad + (STR ''.'' + STR ''balance''))) ad = Some x}" using fmlookup_finite[of "λad. (ad + (STR ''.'' + STR ''balance''))" s] by simp
then have sum1: "finite ({(ad,x). fmlookup s (ad + (STR ''.'' + STR ''balance'')) = Some x ∧ ad ≠ sender env})" using finite_subset[of "{(ad, x). fmlookup s (ad + (STR ''.'' + STR ''balance'')) = Some x ∧ ad ≠ sender env}" "{(ad, x). fmlookup s (ad + (STR ''.'' + STR ''balance'')) = Some x}"] by auto
moreover have sum2: "(sender env,val) ∉ {(ad,x). fmlookup s (ad + (STR ''.'' + STR ''balance'')) = Some x ∧ ad ≠ sender env}" by simp
moreover from sum1 x1 val_def have "insert (sender env,val) {(ad, x). fmlookup s (ad + (STR ''.'' + STR ''balance'')) = Some x ∧ ad ≠ sender env} = {(ad, x). fmlookup s (ad + (STR ''.'' + STR ''balance'')) = Some x}" by auto
ultimately show ?thesis using sum.insert[OF sum1 sum2, of "λ(ad,x). ReadL⇩i⇩n⇩t x"] val_def by simp
qed
moreover have s2: "SUMM s' = (∑(ad,x)|fmlookup s' (ad + (STR ''.'' + STR ''balance'')) = Some x ∧ ad ≠ sender env. ReadL⇩i⇩n⇩t x) + v"
proof -
have "inj_on (λ(ad, x). (ad + (STR ''.'' + STR ''balance''), x)) {(ad, x). (fmlookup s' ∘ (λad. ad + (STR ''.'' + STR ''balance''))) ad = Some x}" using balance_inj by simp
then have "finite {(ad, x). (fmlookup s' ∘ (λad. ad + (STR ''.'' + STR ''balance''))) ad = Some x}" using fmlookup_finite[of "λad. (ad + (STR ''.'' + STR ''balance''))" s'] by simp
then have sum1: "finite ({(ad,x). fmlookup s' (ad + (STR ''.'' + STR ''balance'')) = Some x ∧ ad ≠ sender env})" using finite_subset[of "{(ad, x). fmlookup s' (ad + (STR ''.'' + STR ''balance'')) = Some x ∧ ad ≠ sender env}" "{(ad, x). fmlookup s' (ad + (STR ''.'' + STR ''balance'')) = Some x}"] by auto
moreover have sum2: "(sender env,ShowL⇩i⇩n⇩t v) ∉ {(ad,x). fmlookup s' (ad + (STR ''.'' + STR ''balance'')) = Some x ∧ ad ≠ sender env}" by simp
moreover from ***** have "insert (sender env,ShowL⇩i⇩n⇩t v) {(ad, x). fmlookup s' (ad + (STR ''.'' + STR ''balance'')) = Some x ∧ ad ≠ sender env} = {(ad, x). fmlookup s' (ad + (STR ''.'' + STR ''balance'')) = Some x}" by auto
ultimately show ?thesis using sum.insert[OF sum1 sum2, of "λ(ad,x). ReadL⇩i⇩n⇩t x"] Read_ShowL_id by simp
qed
moreover have s3: "(∑(ad,x)|fmlookup s' (ad + (STR ''.'' + STR ''balance'')) = Some x ∧ ad ≠ sender env. ReadL⇩i⇩n⇩t x)
=(∑(ad,x)|fmlookup s (ad + (STR ''.'' + STR ''balance'')) = Some x ∧ ad ≠ sender env. ReadL⇩i⇩n⇩t x)"
proof -
have "{(ad,x). fmlookup s' (ad + (STR ''.'' + STR ''balance'')) = Some x ∧ ad ≠ sender env} = {(ad,x). fmlookup s (ad + (STR ''.'' + STR ''balance'')) = Some x ∧ ad ≠ sender env}"
proof
show "{(ad, x). fmlookup s' (ad + (STR ''.'' + STR ''balance'')) = Some x ∧ ad ≠ sender env}
⊆ {(ad, x). fmlookup s (ad + (STR ''.'' + STR ''balance'')) = Some x ∧ ad ≠ sender env}"
proof
fix xx
assume "xx ∈ {(ad, x). fmlookup s' (ad + (STR ''.'' + STR ''balance'')) = Some x ∧ ad ≠ sender env}"
then obtain ad x where "xx = (ad,x)" and "fmlookup s' (ad + (STR ''.'' + STR ''balance'')) = Some x" and "ad ≠ sender env" by auto
then have "fmlookup s (ad + (STR ''.'' + STR ''balance'')) = Some x" using s'_def String_Cancel[of ad "(STR ''.'' + STR ''balance'')" "sender env"] by (simp split:if_split_asm)
with `ad ≠ sender env` `xx = (ad,x)` show "xx ∈ {(ad, x). fmlookup s (ad + (STR ''.'' + STR ''balance'')) = Some x ∧ ad ≠ sender env}" by simp
qed
next
show "{(ad, x). fmlookup s (ad + (STR ''.'' + STR ''balance'')) = Some x ∧ ad ≠ sender env}
⊆ {(ad, x). fmlookup s' (ad + (STR ''.'' + STR ''balance'')) = Some x ∧ ad ≠ sender env}"
proof
fix xx
assume "xx ∈ {(ad, x). fmlookup s (ad + (STR ''.'' + STR ''balance'')) = Some x ∧ ad ≠ sender env}"
then obtain ad x where "xx = (ad,x)" and "fmlookup s (ad + (STR ''.'' + STR ''balance'')) = Some x" and "ad ≠ sender env" by auto
then have "fmlookup s' (ad + (STR ''.'' + STR ''balance'')) = Some x" using s'_def String_Cancel[of ad "(STR ''.'' + STR ''balance'')" "sender env"] by (auto split:if_split_asm)
with `ad ≠ sender env` `xx = (ad,x)` show "xx ∈ {(ad, x). fmlookup s' (ad + (STR ''.'' + STR ''balance'')) = Some x ∧ ad ≠ sender env}" by simp
qed
qed
thus ?thesis by simp
qed
moreover from s'_def v_def have "ReadL⇩i⇩n⇩t (accessStorage (TUInt 256) (sender env + (STR ''.'' + STR ''balance'')) s') = ReadL⇩i⇩n⇩t (accessStorage (TUInt 256) (sender env + (STR ''.'' + STR ''balance'')) s) + ⌈svalue env⌉" using Read_ShowL_id by (simp split:option.split_asm)
ultimately have "SUMM s' = SUMM s + ⌈svalue env⌉"
proof -
from s2 have "SUMM s' = (∑(ad,x)|fmlookup s' (ad + (STR ''.'' + STR ''balance'')) = Some x ∧ ad ≠ sender env. ReadL⇩i⇩n⇩t x) + v" by simp
also from s3 have "… = (∑(ad,x)|fmlookup s (ad + (STR ''.'' + STR ''balance'')) = Some x ∧ ad ≠ sender env. ReadL⇩i⇩n⇩t x) + v" by simp
also from s1 have "… = SUMM s - ReadL⇩i⇩n⇩t (accessStorage (TUInt 256) (sender env + (STR ''.'' + STR ''balance'')) s) + v" by simp
finally show ?thesis using v_def by simp
qed
then show ?thesis by simp
qed
moreover have "POS s'"
proof (rule allI[OF allI])
fix ad xa
show "fmlookup s' (ad + (STR ''.'' + STR ''balance'')) = Some xa ⟶ 0 ≤ (⌈xa⌉::int)"
proof
assume a1: "fmlookup s' (ad + (STR ''.'' + STR ''balance'')) = Some xa"
show "0 ≤ (⌈xa⌉::int)"
proof (cases "ad = sender env")
case True
then show ?thesis using s'_def assms(7) Read_ShowL_id a1 v_def by auto
next
case False
then show ?thesis using s'_def assms(7,8) using Read_ShowL_id a1 v_def by (auto split:if_split_asm)
qed
qed
qed
moreover have "ReadL⇩i⇩n⇩t (accessBalance (accounts st') (STR ''Victim'')) = ReadL⇩i⇩n⇩t (accessBalance (accounts st) (STR ''Victim''))" using **** ac st0_def st'''_def by simp
ultimately show ?thesis using that assms(5) by simp
qed
lemma secure:
"address ev1 ≠ (STR ''Victim'') ∧ fmlookup ep1 (STR ''Victim'') = Some (victim, SKIP) ⟶ (∀rv1 st1' bal. frame bal st1 ∧ msel c1 t1 l1 xe1 ep1 ev1 cd1 st1 = Normal (rv1, st1') ⟶ frame bal st1')"
"address ev2 ≠ (STR ''Victim'') ∧ fmlookup ep2 (STR ''Victim'') = Some (victim, SKIP) ⟶ (∀rv2 st2' bal. frame bal st2 ∧ ssel t2 l2 xe2 ep2 ev2 cd2 st2 = Normal (rv2, st2') ⟶ frame bal st2')"
"address ev5 ≠ (STR ''Victim'') ∧ fmlookup ep5 (STR ''Victim'') = Some (victim, SKIP) ⟶ (∀rv3 st5' bal. frame bal st5 ∧ lexp l5 ep5 ev5 cd5 st5 = Normal (rv3, st5') ⟶ frame bal st5')"
"address ev4 ≠ (STR ''Victim'') ∧ fmlookup ep4 (STR ''Victim'') = Some (victim, SKIP) ⟶ (∀rv4 st4' bal. frame bal st4 ∧ expr e4 ep4 ev4 cd4 st4 = Normal (rv4, st4') ⟶ frame bal st4')"
"address lev ≠ (STR ''Victim'') ∧ fmlookup lep (STR ''Victim'') = Some (victim, SKIP) ⟶ (∀ev cd st st' bal. load lcp lis lxs lep lev0 lcd0 lst0 lev lcd lst = Normal ((ev, cd, st), st') ⟶ (frame bal lst0 ⟶ frame bal st) ∧ (frame bal lst ⟶ frame bal st') ∧ address lev0 = address ev ∧ sender lev0 = sender ev ∧ svalue lev0 = svalue ev)"
"address ev3 ≠ (STR ''Victim'') ∧ fmlookup ep3 (STR ''Victim'') = Some (victim, SKIP) ⟶ (∀rv3 st3' bal. frame bal st3 ∧ rexp l3 ep3 ev3 cd3 st3 = Normal (rv3, st3') ⟶ frame bal st3')"
"(fmlookup ep6 (STR ''Victim'') = Some (victim, SKIP) ⟶
(∀st6'. stmt s6 ep6 ev6 cd6 st6 = Normal((), st6') ⟶
((address ev6 ≠ (STR ''Victim'') ⟶ (∀bal. frame bal st6 ⟶ frame bal st6'))
∧ (address ev6 = (STR ''Victim'') ⟶
(∀s val bal x. s6 = transfer
∧ INV st6 s (SUMM s + ReadL⇩i⇩n⇩t val) bal ∧ POS s
∧ fmlookup (denvalue ev6) (STR ''bal'') = Some (Value (TUInt 256), Stackloc x)
∧ accessStore x (stack st6) = Some (KValue val)
∧ sender ev6 ≠ address ev6
⟶ (∃s'. fmlookup (storage st6') (STR ''Victim'') = Some s'
∧ ReadL⇩i⇩n⇩t (accessBalance (accounts st6') (STR ''Victim'')) - (SUMM s') ≥ bal ∧ bal ≥ 0 ∧ POS s')) ∧
(∀s bal x. s6 = comp
∧ INV st6 s (SUMM s) bal ∧ POS s
∧ fmlookup (denvalue ev6) (STR ''bal'') = Some (Value (TUInt 256), Stackloc x)
∧ fmlookup (denvalue ev6) (STR ''balance'') = Some (Storage (STMap TAddr (STValue (TUInt 256))), Storeloc STR ''balance'')
∧ accessStore x (stack st6) = Some (KValue (accessStorage (TUInt 256) (sender ev6 + (STR ''.'' + STR ''balance'')) s))
∧ sender ev6 ≠ address ev6
⟶ (∃s'. fmlookup (storage st6') (STR ''Victim'') = Some s'
∧ ReadL⇩i⇩n⇩t (accessBalance (accounts st6') (STR ''Victim'')) - (SUMM s') ≥ bal ∧ bal ≥ 0 ∧ POS s')) ∧
(∀s bal. s6 = keep
∧ INV st6 s (SUMM s) bal ∧ POS s
∧ fmlookup (denvalue ev6) (STR ''balance'') = Some (Storage (STMap TAddr (STValue (TUInt 256))), Storeloc STR ''balance'')
∧ sender ev6 ≠ address ev6
⟶ (∃s'. fmlookup (storage st6') (STR ''Victim'') = Some s'
∧ ReadL⇩i⇩n⇩t (accessBalance (accounts st6') (STR ''Victim'')) - (SUMM s') ≥ bal ∧ bal ≥ 0 ∧ POS s'))
))))"
proof (induct rule: msel_ssel_lexp_expr_load_rexp_stmt.induct
[where ?P1.0="λc1 t1 l1 xe1 ep1 ev1 cd1 st1. address ev1 ≠ (STR ''Victim'') ∧ fmlookup ep1 (STR ''Victim'') = Some (victim, SKIP) ⟶ (∀rv1 st1' bal. frame bal st1 ∧ msel c1 t1 l1 xe1 ep1 ev1 cd1 st1 = Normal (rv1, st1') ⟶ frame bal st1')"
and ?P2.0="λt2 l2 xe2 ep2 ev2 cd2 st2. address ev2 ≠ (STR ''Victim'') ∧ fmlookup ep2 (STR ''Victim'') = Some (victim, SKIP) ⟶ (∀rv2 st2' bal. frame bal st2 ∧ ssel t2 l2 xe2 ep2 ev2 cd2 st2 = Normal (rv2, st2') ⟶ frame bal st2')"
and ?P3.0="λl5 ep5 ev5 cd5 st5. address ev5