chriseth · November 6, 2022 19:55 · Jul 8, 2016 · Jul 8, 2016 · Jul 8, 2016 · Jul 8, 2016
diff --git a/0 README.md b/0 README.md
@@ -38,7 +38,7 @@ corresponds to
     throw;
   shares -= amount;
 ```
-i.e. a contract that contains the recursive call exploit. The why3
+i.e. a contract that is exploitable by recursive calls. The why3
 tool should tell you that it was not able to verify the condition
 in that case.
 

diff --git a/0 README.md b/0 README.md
@@ -18,8 +18,8 @@ More specifically, the difference between the total balance and the shares
 is constant across the lifetime of the contract. Thus, this difference is
 a so-called invariant.
 
-All you need to do on the Solidity side is add this invariant as a
-why3-annotation to the contract, as seen in the first line.
+All you need to do on the Solidity side is add this invariant as an
+annotation to the contract, as seen in the first line.
 
 The Solidity compiler will then translate the contract into a language
 called why3 and use the why3 tools to verify that this invariant is

diff --git a/0 README.md b/0 README.md
@@ -55,5 +55,5 @@ What still needs to be done:
 
 Note that these features still do not protect you from bugs in the compiler or
 the EVM. In order to get protection at this level, the formal model of the
-source code needs to be mathed to the one of the generated bytecode. This
+source code needs to be matched to the one of the generated bytecode. This
 is part of our ongoing research into formal verification.
diff --git a/0 README.md b/0 README.md
@@ -1,7 +1,7 @@
 This gist shows how formal conditions of Solidity smart contracts can be automatically verified
 even in the presence of potential re-entrant calls from other contracts.
 
-Solidity already supports formal verification of contracts that do not make calls
+Solidity already supports formal verification of some contracts that do not make calls
 to other contracts. This of course excludes any contract that transfers Ether
 or tokens.
 

diff --git a/2 Fund.mlw b/2 Fund.mlw
@@ -38,8 +38,6 @@ module Contract_Fund
 	(* This is the translation of the actual Solidity function *)
 	let _withdraw (this: account) (arg_amount: uint256):
 			(account)
-			(* TODO: Check that this is satisfied by the constructor *)
-			requires { invariantFun this > 0 }
 			(* This will be auto-inserted by solidity *)
 			ensures { invariantFun (old this) = invariantFun result }
 		=

diff --git a/1 Fund.sol b/1 Fund.sol
@@ -3,8 +3,8 @@ contract Fund {
     uint shares;
     function withdraw(uint amount) {
         if (amount < shares) {
-            shares -= amount;
-            if (!msg.sender.call.value(amount)())
+            shares -= amount; // subtract the amount from the shares
+            if (!msg.sender.call.value(amount)()) // send the actual money / ether
                 throw;
         }
     }

diff --git a/2 Fund.mlw b/2 Fund.mlw
@@ -27,12 +27,10 @@ module Contract_Fund
 	(* 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 }
-	let call_external (this: account): call_result
+	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) }
-		=
-		{success = true; new_state = this}
 
 	(* TODO: the code has to reject incoming ether and this functionality has
 	 * to be part of the model *)

diff --git a/0 README.md b/0 README.md
@@ -5,11 +5,14 @@ Solidity already supports formal verification of contracts that do not make call
 to other contracts. This of course excludes any contract that transfers Ether
 or tokens.
 
-The Solidity contract below models a crude crowdfunding contract, that can hold
-Ether and some person can withdraw ether according to their shares.
+The Solidity contract below models a crude crowdfunding contract that can hold
+Ether and some person can withdraw Ether according to their shares.
 It is missing the actual access control, but the point that wants to be made
-here is the following: You cannot withdraw more than your shares by a recursive
-call exploit.
+here is the following:
+
+You cannot withdraw more than your shares, not by a recursive call exploit
+or any other means. Recursive calls are allowed, but the contract can
+still handle them fine.
 
 More specifically, the difference between the total balance and the shares
 is constant across the lifetime of the contract. Thus, this difference is

diff --git a/0 README.md b/0 README.md
@@ -0,0 +1,56 @@
+This gist shows how formal conditions of Solidity smart contracts can be automatically verified
+even in the presence of potential re-entrant calls from other contracts.
+
+Solidity already supports formal verification of contracts that do not make calls
+to other contracts. This of course excludes any contract that transfers Ether
+or tokens.
+
+The Solidity contract below models a crude crowdfunding contract, that can hold
+Ether and some person can withdraw ether according to their shares.
+It is missing the actual access control, but the point that wants to be made
+here is the following: You cannot withdraw more than your shares by a recursive
+call exploit.
+
+More specifically, the difference between the total balance and the shares
+is constant across the lifetime of the contract. Thus, this difference is
+a so-called invariant.
+
+All you need to do on the Solidity side is add this invariant as a
+why3-annotation to the contract, as seen in the first line.
+
+The Solidity compiler will then translate the contract into a language
+called why3 and use the why3 tools to verify that this invariant is
+indeed an invariant.
+
+If you want to do that youself, go to http://why3.lri.fr/try/ copy
+the .mlw file into the text pane there and click on the gear symbol.
+Then, after some time, green ticks should appear on the right pane.
+
+Oh and if you are in the mood, you can try moving the line that says
+`storage_shares := !(storage_shares) - !(_amount);` to after
+`raise Revert;` and click the gear sybmol again. This change
+corresponds to
+```
+  if (!msg.sender.call.value(amount)())
+    throw;
+  shares -= amount;
+```
+i.e. a contract that contains the recursive call exploit. The why3
+tool should tell you that it was not able to verify the condition
+in that case.
+
+
+This is a proof of concept that still needs to be verified by experts,
+but I think we are already quite far here.
+
+What still needs to be done:
+
+ - model the actual "message", i.e. incoming ether, which needs to be rejected
+ - add a matching condition to the constructor
+ - add these features to the existing Solidity -> why3 translator
+ - add why3 to browser-solidity for ease of access
+
+Note that these features still do not protect you from bugs in the compiler or
+the EVM. In order to get protection at this level, the formal model of the
+source code needs to be mathed to the one of the generated bytecode. This
+is part of our ongoing research into formal verification.
diff --git a/2 Fund.mlw b/2 Fund.mlw
@@ -41,7 +41,7 @@ module Contract_Fund
 	let _withdraw (this: account) (arg_amount: uint256):
 			(account)
 			(* TODO: Check that this is satisfied by the constructor *)
-			requires { to_int this.balance >= to_int this.storage._shares }
+			requires { invariantFun this > 0 }
 			(* This will be auto-inserted by solidity *)
 			ensures { invariantFun (old this) = invariantFun result }
 		=

diff --git a/Fund.sol → 1 Fund.sol b/Fund.sol → 1 Fund.sol
diff --git a/Fund.mlw → 2 Fund.mlw b/Fund.mlw → 2 Fund.mlw
diff --git a/Fund.mlw b/Fund.mlw
@@ -0,0 +1,78 @@
+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 }
+	let call_external (this: account): call_result
+			ensures { result.success = false -> this = result.new_state }
+			ensures { result.success = true ->
+					(invariantFun this) = (invariantFun result.new_state) }
+		=
+		{success = true; new_state = this}
+
+	(* 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)
+			(* TODO: Check that this is satisfied by the constructor *)
+			requires { to_int this.balance >= to_int this.storage._shares }
+			(* 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
diff --git a/Fund.sol b/Fund.sol
@@ -0,0 +1,11 @@
+/// @why3 invariant { to_int this.storage._shares - to_int this.balance }
+contract Fund {
+    uint shares;
+    function withdraw(uint amount) {
+        if (amount < shares) {
+            shares -= amount;
+            if (!msg.sender.call.value(amount)())
+                throw;
+        }
+    }
+}