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

43 阅读 0 评论 29 点赞

我是靠谱客的博主任性唇膏，最近开发中收集的这篇文章主要介绍用形式化验证缓解智能合约漏洞，觉得挺不错的，现在分享给大家，希望可以做个参考。

概述

Solidity已经支持对未调用其他合同的某些智能合约进行正式验证。当然，这不包括任何转让代币的合约。

下面的Solidity合同模拟了一个原始的众筹合约，该合约可以持有Token，某些人可以根据其股份提取Token。它缺少实际的访问控制，但此处要说明的要点如下：

您不能通过递归调用漏洞或任何其他方式提取最多的代币。允许递归调用，但是合约仍然可以处理它们。

更具体地说，在合约的整个生命周期中，总余额和代币之间的差额是恒定的。因此，这种差异是所谓的不变性。

在Solidity端您需要做的就是将此不变式添加为合同的注释，如第一行所示。

然后，Solidity编译器会将合同转换为一种名为why3的语言，并使用工具来验证该不变量确实是一个不变量。

如果您想自己做，请转到http://why3.lri.fr/try/将.mlw文件复制到此处的文本窗格中，然后单击齿轮符号。然后，一段时间后，绿色刻度线应出现在右窗格中。

尝试移动storage_shares := !(storage_shares) - !(_amount); 到 raise Revert; 之后；在改动后恢复；然后再次触发。此更改对应于

if (!msg.sender.call.value(amount)())
    throw;
  shares -= amount;

即可被递归调用利用的合同。 why3工具应该告诉您在那种情况下它无法验证条件。

这是一个概念证明，仍然需要专家进行验证，但是我认为我们已经走了很远。

仍然需要做的是：

模拟实际的“消息”，即需要拒绝的toekn
向构造函数添加匹配条件
将这些功能添加到现有的Solidity-> why3转换器中

请注意，这些功能仍不能保护您免受编译器或EVM中的错误的侵害。为了在此级别获得保护，源代码的形式模型需要与生成的字节码之一匹配。这是我们正在进行的对形式验证的研究的一部分。

以下是示例代码 :

solidity

/// @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;
        }
    }
}

编译后

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