用形式化验证缓解智能合约漏洞

1
2
3
4
if (!msg.sender.call.value(amount)())
    throw;
  shares -= amount;

1
2
3
4
5
6
7
8
9
10
11
12
/// @why3 invariant { to_int this.storage._shares - to_int this.balance }
contract Fund {
    uint shares;
    function withdraw(uint amount) {
        if (amount < shares) {
            shares -= amount; // subtract the amount from the shares
            if (!msg.sender.call.value(amount)()) // send the actual money / ether
                throw;
        }
    }
}

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
module UInt256
	use import mach.int.Unsigned
	type uint256
	constant max_uint256: int = 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff
	clone export mach.int.Unsigned with
		type t = uint256,
		constant max = max_uint256
end

module Contract_Fund
	use import ref.Ref
	use import int.ComputerDivision
	use import UInt256
	exception Ret
	exception Revert
	type state = {
		_shares: uint256
	}
	type account = {
		balance: uint256;
		storage: state
	}

	(* This is the invariant that is specified as part of the solidity source code *)
	function invariantFun (this: account): int = to_int this.storage._shares - to_int this.balance

	(* This models a potential recursive call (or much more complicated changes
	 * to the state) because it asserts nothing apart from the invariant *)
	type call_result  = { success: bool; new_state: account }
	val call_external (this: account): call_result
			ensures { result.success = false -> this = result.new_state }
			ensures { result.success = true ->
					(invariantFun this) = (invariantFun result.new_state) }

	(* TODO: the code has to reject incoming ether and this functionality has
	 * to be part of the model *)

	(* This is the translation of the actual Solidity function *)
	let _withdraw (this: account) (arg_amount: uint256):
			(account)
			(* This will be auto-inserted by solidity *)
			ensures { invariantFun (old this) = invariantFun result }
		=
		let storage_shares = ref this.storage._shares in
		let this_snapshot = ref {balance = this.balance; storage = {_shares = this.storage._shares}} in
		let _amount = ref arg_amount in
		try
		begin
			if ((!(_amount) <= !storage_shares)) then
			begin
				storage_shares := !(storage_shares) - !(_amount);
				(* this models msg.sender.call.value(_amount)() *)
				let call_result = (
					if (!_amount) <= (!this_snapshot).balance then
						call_external {balance = (!this_snapshot).balance - !_amount; storage = {_shares = !(storage_shares)}}
					else
						{ success = false; new_state = {balance = (!this_snapshot).balance; storage = {_shares = !(storage_shares)}}}
				) in
				this_snapshot := call_result.new_state;
				if not (call_result.success) then
					raise Revert;
			end
		end;
		raise Ret
		with
			Ret -> (!this_snapshot) |
			Revert -> this
	end
end

(* The browser version of why3 requires a "main" function *)
module Test
  let main () = 0
end