Add EIP: Theorem-Carrying-Transaction - TCT

EIPS/eip-7534.md

@@ -0,0 +1,255 @@
+---
+eip: 7534
+title: Theorem-Carrying-Transaction - TCT
+description: TCT ensure that every transaction must carry a theorem that guarantees its adherence to the properties in the invoked contracts.
+author: Shuo Chen (@cs0317), Nikolaj Bjørner (@NikolajBjorner), Tzu-Han Hsu (@tzuhancs), Ashley Chen (@ash-jyc), Nanqing Luo (@Billy1900)
+discussions-to: https://ethereum-magicians.org/t/eip-7534-transactioncarrying-theorem-tct-proposal/17125
+status: Draft
+type: Standards Track
+category: Core
+created: 2023-10-12
+---
+
+
+## Abstract
+
+Smart contracts are crucial elements of decentralized technologies, but they face significant obstacles to trustworthiness due to security bugs and trapdoors. To address the core issue, we propose a technology that enables programmers to focus on design-level properties rather than specific low-level attack patterns. Our proposed technology, called Theorem-Carrying-Transaction (TCT), combines the benefits of runtime checking and symbolic proof. Under the TCT protocol, every transaction must carry a theorem that proves its adherence to the safety properties in the invoked contracts, and the EL clients checks the proof before executing the transaction. The unique design of TCT ensures that the theorems are provable and checkable in an efficient manner. We believe that TCT holds a great promise for enabling provably secure smart contracts in the future.
+
+## Motivation
+
+This proposal is necessary since the Ethereum protocol does not ensure the safety features on the design level. It stems from the recognition of the significant obstacles faced by smart contracts in terms of trustworthiness due to security bugs and trapdoors. While smart contracts are crucial elements of decentralized technologies, their vulnerabilities pose a challenge to their widespread adoption. Conventional smart contract verification and auditing helps a lot, but it only tries to find as many vulnerabilities as possible in the development and testing phases. However, in real cases, we suffer from the unintentional vulnerabilities and logical trapdoors which lead to lack of transparency and trustworthiness of smart contract.
+
+## Specification
+
+First, we give several terminology:
+
+- $\tau$: it denotes the theorem. Every transaction must carry a theorem that proves its adherence to the specified safety properties in the invoked contracts.
+
+- $\mathrm{f}$: it denotes the entry function of transaction.
+
+- $\varphi(\mathrm{V}, \mathrm{s})$: $\varphi$ denotes hypothesis which defined over input parameter $\mathrm{V}$ and blockchain state $\mathrm{s}$.
+
+- $\mathrm{h}$: code path hash which is used for execution path match.
+
+- Invariant: contract invariants like the ones are ensured before and after every transaction. They contain quantifiers, sum of map, etc., which are difficult to check concretely.
+
+- behavioral subtyping: Unlike the conventional notion of OOP subtyping, which underpins today’s smart contracts and many other real-world systems, behavioral subtyping ensures that a derived class cannot violate properties defined in a base class.
+
+For each transaction which is executed, it SHOULD satisfies the following theorem:
+
+$$
+\tau::=(\mathrm{f}, \varphi(\mathrm{V}, \mathrm{s}), \mathrm{h})
+$$
+
+The above theorem means​ for any transaction started by invoking $\mathrm{f}$ when $\varphi$ is satisfied, if it is completed (i.e., not reverted by EVM) and the hash of the code path equals $\mathrm{h}$, then all the assertions along the code path are guaranteed to hold. ​
+
+Technically, code path hash $\mathrm{h}$ will be added into `Transaction` struct so each transaction will carry its own hypothesis hash $\mathrm{h}$.
+
+```go
+// Transaction is an Ethereum transaction.
+type Transaction struct {
+	inner TxData    // Consensus contents of a transaction
+	time  time.Time // Time first seen locally (spam avoidance)
+
+	// TCT hypoHash
+	HypoHash common.Hash
+
+	// caches
+	hash atomic.Value
+	size atomic.Value
+	from atomic.Value
+}
+```
+
+Given `HypoHash`, it could retrieve the hypothesis through function `retrieveHypoHash`. And then execute the given transaction in a new EVM environment. The executed evm bytecode will be checked by TCT along with the hypothesis to ensure whether it violates the theorem.
+
+```go
+func applyTransaction(msg *Message, config *params.ChainConfig, gp *GasPool, statedb *state.StateDB, blockNumber *big.Int, blockHash common.Hash, tx *types.Transaction, usedGas *uint64, evm *vm.EVM) (*types.Receipt, error) {
+    ...
+    // TCT: get hypothesis given hypoHash
+    hypothesis, err := retrieveHypoHash(hypoHash)
+    ...
+    // Create a new context to be used in the EVM environment.
+    txContext := NewEVMTxContext(msg)
+    evm.Reset(txContext, statedb)
+
+    // Apply the transaction to the current state (included in the env).
+    result, err := ApplyMessage(evm, msg, gp)
+    ...
+}
+```
+
+## Rationale
+
+Conventional approaches predominantly resort to specialized tools and the expertise of domain professionals to detect and address known vulnerabilities or bugs, targeting the prevention of unintended contract behaviors. While these methods have their merits, empirical evidence suggests a palpable shortfall in ensuring comprehensive safety features. In contrast, our application of TCT brings forth a robust security guarantee via runtime verification, markedly elevating the safety standards compared to the traditional strategies.  
+
+While numerous projects delve into runtime verification, our approach is distinctly tailored to focus solely on transactions which has several merits:
+
+- **Minimal runtime overhead**: By so doing, we anticipate a tangible reduction in the overhead typically associated with blanket verification mechanisms.
+
+- **Concolic testing**: Further, by synthesizing the merits of runtime verification with symbolic proof, our methodology stands out in ensuring both the provability and verifiability of theorems, setting a benchmark in efficacy and reliability. 
+
+
+## Backwards Compatibility
+
+The primary concern lies in the potential for incompatibility, particularly with regards to the occurrence of a fork. The Theorem-Carrying-Transaction (TCT) system may reject certain transactions that violate the theorem, while the original Ethereum network may accept these transactions. This discrepancy in transaction acceptance could lead to a network fork, resulting in divergent block states. To address this issue, we propose conducting a comprehensive evaluation of TCT's effectiveness and stability by initially deploying it on a testnet such as `Goeril`.
+
+## Test Cases
+
+We extract a token contract as shown below:
+
+```solidity
+// SPDX-License-Identifier: MIT
+
+/* Vulnerability examples:
+
+   reentrancy:
+   https://blog.chain.link/reentrancy-attacks-and-the-dao-hack/
+
+   integer overflow:
+   https://peckshield.medium.com/integer-overflow-i-e-proxyoverflow-bug-found-in-multiple-erc20-smart-contracts-14fecfba2759
+*/
+pragma solidity >=0.8.0;
+
+abstract contract Token {
+    address public owner;
+    uint256 public totalSupply;
+    function balanceOf(address _owner) public view virtual returns (uint256 balance);
+}
+
+/// @custom:tct invariant: forall x:address :: 0 <= balances[x] && balances[x] <= totalSupply
+/// @custom:tct invariant: sum(balances) == totalSupply 
+abstract contract StandardToken is Token {
+
+    function balanceOf(address _owner) public view override returns (uint256 balance) {
+        return balances[_owner];
+    }
+
+    mapping (address => uint256) balances;
+}
+
+contract MultiVulnToken is StandardToken {
+    string public name = "Demo token with reentrancy issue, integer overflow and access control issue";
+    constructor (uint256 initialSupply) {
+        totalSupply = initialSupply;
+        balances[msg.sender] = totalSupply;
+    }
+    function transferProxy(address _from, address _to, uint256 _value, uint256 _fee
+        ) public returns (bool){
+		unchecked{
+			require(balances[_from] >= _fee + _value);
+			require(balances[_to] + _value >= balances[_to]);
+			require(balances[msg.sender] + _fee >= balances[msg.sender]); 
+
+			balances[_to] += _value;
+			balances[msg.sender] += _fee;
+			balances[_from] -= _value + _fee;
+			return true;
+		}
+    }
+
+    //This function moves all tokens of msg.sender to the account of "_to"
+    function clear(address _to) public {
+        uint256 bal = balances[msg.sender];
+        require (msg.sender!=_to);
+        balances[_to]+=bal;
+        bool success;
+        (success, ) = msg.sender.call(
+            abi.encodeWithSignature("receiveNotification(uint256)", bal)
+        );
+        require(success, "Failed to notify msg.sender");
+        balances[msg.sender] = 0;
+    }
+}
+
+
+contract reentrancy_attack {
+    MultiVulnToken public multiVulnToken; 
+    address _to;
+    uint count=0;
+    constructor (MultiVulnToken _multiVulnToken, address __to) 
+    {
+        multiVulnToken=_multiVulnToken;
+        _to = __to;
+    }
+    function receiveNotification(uint256) public { 
+        if (count < 9) {
+            count ++;
+            multiVulnToken.clear(_to); 
+        }
+    } 
+    function attack() public {
+        multiVulnToken.clear(_to);
+    }
+}
+
+contract Demo {
+    MultiVulnToken MultiVulnTokenContractAddress;
+
+    address attacker1Address = address(0x92349Ef835BA7Ea6590C3947Db6A11EeE1a90cFd); //just an arbitrary address
+    reentrancy_attack attacker2Address1;
+    address attacker2Address2 = address(0x0Ce8dAf9acbA5111C12B38420f848396eD71Cb3E); //just an arbitrary address
+
+    constructor () {
+        MultiVulnTokenContractAddress = new MultiVulnToken(1000);
+        attacker2Address1 = new reentrancy_attack(MultiVulnTokenContractAddress,attacker2Address2);
+
+        //suppose attacker3Address1 has 5 tokens initially
+        MultiVulnTokenContractAddress.transferProxy(address(this), address(attacker2Address1),5,0
+                                      );
+    }
+
+    function getBalanceOfAttacker1() view public returns (uint256){
+        return MultiVulnTokenContractAddress.balanceOf(attacker1Address);
+    }
+    function attack1_int_overflow() public {
+        MultiVulnTokenContractAddress.transferProxy(address(this), 
+                                      attacker1Address,
+                                      uint256(2**255+1),
+                                      uint256(2**255)
+                                      );
+    }
+
+    function getBalanceOfAttacker2() view public returns (uint256){
+        return MultiVulnTokenContractAddress.balanceOf(address(attacker2Address1))
+            +  MultiVulnTokenContractAddress.balanceOf(attacker2Address2);
+    }
+    function attack2_reentrancy() public {
+        attacker2Address1.attack();
+    }
+}
+```
+
+Note that we have provided the invariant for the entry functions above `abstract contract StandardToken`. Since TCT enables behavioral subtyping for smart contract, it still delivers its children contract such as `MultiVulnToken`.
+
+For the contract `MultiVun`, we have provided a theorem for the entry function of transaction as below
+
+```json
+{
+	"entry-for-test":"MultiVulnToken::clear(address)",
+	"entry-for-real":"0x88c436e4a975ef5e5788f97e86d80fde29ddd13d::0x3d0a4061",
+	"def-vars": {
+		"totalSupply": ["", "this.totalSupply", "uint256"]
+	},
+	"hypothesis": [
+		"totalSupply < TwoE256 && tx_origin != _to"
+	],
+	"path-hash-for-test": "*",
+	"path-hash-for-real": "the real hash (not implemented yet)",
+	"numerical-type": "int"
+}
+```
+
+If attacker’s obligation to prove the theorem, the attempt would be doomed to fail.​
+
+## Reference Implementation
+
+We have implemented the first demo of TCT in our repository.
+
+## Security Considerations
+
+In the current construct of our theorem repository, potential security vulnerabilities may exist. Given our intention to migrate the theorems to the InterPlanetary File System (IPFS), a compromised repository could precipitate a significant security breach.
+
+## Copyright
+
+Copyright and related rights waived via [CC0](../LICENSE.md).