Sitvanit/add curve

.gitignore

@@ -7,3 +7,5 @@
 **/package-lock.json
 **/.idea/
 **/cache/
+**/emv-*
+

CVLByExample/Curve/README.md

@@ -0,0 +1,33 @@
+
+#Curve 
+
+This directory contains the contract Curve which has the read only reentrancy weakness. 
+
+##Contracts
+The original contract is Curve whose weakness is found by the builtin rule viewReentrancy. In addition we have the
+contract MungedCurve that allows finding the weakness also with a regular rule.
+
+##Specs
+certora/specs contains two spec files for exposing this weakness.
+
+1. BuiltinViewReentrancy.spec uses the builtin rule viewReentrancy that checks that for every solidity function and every
+   view function the read only reentrancy weakness is not present. This spec is used for finding the weakness in Curve.
+2. ViewReentrancy.spec uses regular rules for checking that for every solidity function but only for the view function
+   getVirtualPrice() the read only reentrancy weakness is not present. This is done by using ghosts for tracking:
+    1. The value of getVirtualPrice() at the current state.
+    2. The value of getVirtualPrice() before the unresolved call that is in the solidity function.
+    3. The value of getVirtualPrice() after the unresolved call that is in the solidity function.
+    4. The existence of read only weakness with respect to getVirtualPrice().
+    Two hooks are defined. One for updating (1) and one for updating (4).
+    Additional munging is required in order to catch the bug. This spec works on the contract MungedCurve.
+
+Both rules check the existence of the weakness by checking 
+that the result of a view function after an
+unresolved call is equal either to the result of this view function at the beginning or at the end of the 
+solidity function.
+
+Both specs find that the weakness exists in the contract.
+
+## Failing Rules:
+no_read_only_reentrancy for function remove_liquidity. I remove liquidity the unresolved call is performed in an unstable
+state, after the call to CurveToken(lp_token).burnFrom and before the call to ERC20(coins_1).transfer.

CVLByExample/Curve/certora/conf/runViewReentrancyBuiltinRule.conf

@@ -0,0 +1,20 @@
+{
+  "files": [
+    "contracts/Curve.sol",
+    "contracts/CurveTokenExample.sol",
+    "contracts/ERC20.sol"
+  ],
+  "verify": "Curve:certora/specs/BuiltinViewReentrancy.spec",
+  "link": [
+    "Curve:lp_token=CurveTokenExample",
+    "Curve:coins_1=ERC20"
+  ],
+  "msg": "Curve builtin linking coins_1 w/ view guard",
+  "send_only": true,
+  "optimistic_loop": true,
+  "loop_iter": "6",
+  "prover_args": [
+      "-optimisticFallback true"
+  ],
+  "server": "staging"
+}

CVLByExample/Curve/certora/conf/runViewReentrancyRegularRule.conf

@@ -0,0 +1,20 @@
+{
+  "files": [
+    "contracts/MungedCurve.sol",
+    "contracts/CurveTokenExample.sol",
+    "contracts/ERC20.sol"
+  ],
+  "verify": "MungedCurve:certora/specs/ViewReentrancy.spec",
+  "link": [
+    "MungedCurve:lp_token=CurveTokenExample",
+    "MungedCurve:coins_1=ERC20"
+  ],
+  "msg": "Curve builtin linking coins_1 w/ view guard",
+  "send_only": true,
+  "optimistic_loop": true,
+  "loop_iter": "6",
+  "prover_args": [
+      "-optimisticFallback true"
+  ],
+  "server": "staging"
+}

CVLByExample/Curve/certora/specs/BuiltinViewReentrancy.spec

@@ -0,0 +1 @@
+use builtin rule viewReentrancy;

CVLByExample/Curve/certora/specs/ViewReentrancy.spec

@@ -0,0 +1,35 @@
+
+using ERC20 as Token;
+using CurveTokenExample as LPToken;
+
+
+ghost uint256 before_func1;
+ghost uint256 after_func1;
+ghost uint256 current_func1;
+ghost bool cond;
+
+// hook on the return value of the view function
+hook Sstore solghost_return_func1 uint256 newValue (uint256 oldValue) STORAGE {
+    current_func1 = newValue;
+}
+
+// hook on the read only reentrancy condition.
+// true is the current result of the view function is equal to the result before the unresolved or
+// to the result after the unresolved.
+hook Sstore solghost_trigger_check bool newValue (bool oldValue) STORAGE {
+    cond = cond && ((current_func1 == before_func1) || (current_func1 == after_func1));
+}
+
+// Using require for setting before_func1 to the value of getVirtualPrice before the unresolved call and
+// setting after_func1 to the value of getVirtualPrice after the unresolved call.
+rule no_read_only_reentrancy(method f)
+{
+    env e;
+    env e_external;
+    calldataarg data;
+    require cond;
+    require before_func1 == getVirtualPrice(e_external);
+    f(e, data);
+    require after_func1 == getVirtualPrice(e_external);
+    assert cond;
+}

CVLByExample/aave-token-v3/lib/openzeppelin-contracts/contracts/utils/Context.sol → CVLByExample/Curve/contracts/Context.sol

@@ -1,7 +1,7 @@
 // SPDX-License-Identifier: MIT
 // OpenZeppelin Contracts v4.4.1 (utils/Context.sol)
 
-pragma solidity ^0.8.0;
+pragma solidity ^0.8.13;
 
 /**
  * @dev Provides information about the current execution context, including the
@@ -21,4 +21,4 @@ abstract contract Context {
     function _msgData() internal view virtual returns (bytes calldata) {
         return msg.data;
     }
-}
+}

CVLByExample/Curve/contracts/Curve.sol

@@ -0,0 +1,236 @@
+// SPDX-License-Identifier: Unlicense
+pragma solidity ^0.8.13;
+import "./ERC20.sol";
+import "./ReentrancyGuard.sol";
+import "./CurveToken.sol";
+import "./CurveTokenExample.sol";
+
+contract MintableToken is ERC20 {
+
+    constructor (string memory name, string memory sym) ERC20(name, sym) {
+
+    }
+
+    function mint(address _user, uint _amount) public {
+        _mint(_user, _amount);
+    }
+}
+
+contract Curve is ReentrancyGuard{
+    //uint128 public constant  2 = 2;
+    uint256  constant A_PRECISION =100;
+    uint256  constant PRECISION = 10e18;
+    uint256  future_A_time;
+    uint256  future_A;
+    uint256  initial_A_time;
+    uint256  initial_A;
+    uint256[2]  admin_balances;
+    // storage var "address[2] coins" was seperated to be able to link
+    address  public coins_0;
+    address  public coins_1;
+    address  public lp_token;
+    address  owner;
+    // address  public underlying_token; // would be linked to ERC20 and equal to coins[1], but can't do directly due to CVL limitations
+    uint256  kill_deadline;
+    uint256  fee;
+    uint256  admin_fee;
+    uint256  future_fee;
+    uint256  future_owner;
+    uint256  future_admin_fee;
+    uint256  _DEMO_D;
+
+    mapping(uint256 => mapping(uint256 => mapping(uint256 => uint256))) _DEMO_D_MAPPING;
+
+
+
+
+    // constructor(uint256 _future_A_time, uint256 _future_A, uint256 _initial_A_time, uint256 _initial_A, address owner ) {
+
+    constructor(address _lp_token, address _token_addr) payable {
+        lp_token = _lp_token;
+        coins_1 = _token_addr;
+    }
+
+
+    // function get_D(uint xp_0, uint xp_1)
+
+    function get_D(uint256[2] memory xp,uint256 amp) public view returns(uint256) {
+        uint256 S = 0;
+        uint256 Dprev = 0;
+        // Demo simplificaiton - unconstrained CONST
+        // get_D currently crashes the prover's pre-SMT analysis or something
+        // uint256 x; 
+        // return _DEMO_D; 
+        // return _DEMO_D_MAPPING[xp[0]][xp[1]][amp];
+        return xp[0] + xp[1];
+        // Simplification end
+
+        for (uint256 _x=0;_x<xp.length;_x++){
+            S +=xp[_x];
+        }
+        if(S == 0){
+            return 0;
+        }
+
+        uint256 D=S;
+        uint256 Ann = amp * 2;
+        for (uint _i=0;_i<255;++_i){
+            uint256 D_P = D;
+            for (uint256 _x=0;_x<xp.length;_x++){
+                D_P = D_P * D / (xp[_x] * 2 +1);
+            }
+            Dprev = D;
+            D = (Ann * S / A_PRECISION + D_P * 2) * D / ((Ann - A_PRECISION) * D / A_PRECISION + (2 + 1) * D_P);
+            if (D > Dprev){
+                if (D - Dprev <= 1){
+                    return D;
+                }
+            }
+            else{
+                if (Dprev - D <= 1){
+                    return D;
+                }
+            }
+        }
+        revert();
+    }
+
+    function _A() view internal returns(uint256) {
+
+        // Demo simplificaiton - return unconstrained CONST
+        return future_A;
+        // Simplification end
+
+        uint256 t1 = future_A_time;
+        uint256 A1 = future_A;
+        if (block.timestamp < t1){
+            uint256 A0 = initial_A;
+            uint256 t0 = initial_A_time;
+            if (A1 > A0){
+                return A0 + (A1 - A0) * (block.timestamp - t0) / (t1 - t0);
+            }
+            else{
+                return A0 - (A0 - A1) * (block.timestamp - t0) / (t1 - t0);
+            }
+        }
+        else{
+            return A1;
+        }
+    }
+
+    function _balances(uint256 _value) internal view returns(uint256[2] memory) {
+        return [
+            address(this).balance - admin_balances[0] - _value,
+            ERC20(coins_1).balanceOf(address(this)) - admin_balances[1]];
+    }
+
+    // function _balances_guarded(uint256 _value) public view returns(uint256[2] memory) {
+    //     require(!_reentrancyGuardEntered(), "reading during reentrancy not allowed!");
+    //     return _balances(_value);
+    // }
+
+    // function getVirtualPrice_guarded() public view returns(uint256) {
+    //     require(!_reentrancyGuardEntered(), "reading during reentrancy not allowed!");
+    //     return getVirtualPrice();
+    // }
+
+    function getVirtualPrice() public view returns(uint256){
+        uint256 D = this.get_D(_balances(0),_A());
+        uint256 totalShares = ERC20(lp_token).totalSupply();
+        return D * PRECISION / totalShares;
+    }
+
+    function remove_liquidity(
+        uint256 _amount,
+        uint256[2] memory _min_amounts
+        )
+        nonReentrant 
+        public 
+        returns(uint256[2] memory) 
+    {
+        uint256[2] memory amounts = _balances(0);
+        uint256 total_supply = ERC20(lp_token).totalSupply();
+        CurveToken(lp_token).burnFrom(msg.sender, _amount);
+        for (uint256 i;i<2;i++){
+            uint256 value = amounts[i] * _amount / total_supply;
+            assert (value >= _min_amounts[i]);
+            amounts[i] = value;
+            if (i == 0){
+                msg.sender.call{value:value}("");
+            }
+            else{
+                assert (ERC20(coins_1).transfer(msg.sender, value));
+            }
+        }
+        return amounts;
+    }
+
+    function addScenarioEther() public payable {
+
+    }
+
+}
+
+
+contract scenario {
+
+    uint constant other_user_lp = 40e18;
+    uint constant underlying_asset_before = 80e18;
+    uint constant deposited_ether_before = 4e18;
+    uint constant attacker_lp = 40e18;
+    uint constant attacker_underlying = 80e18;
+    uint constant attacker_deposit_eth = 4e18; 
+    address constant other_user = 0xAb8483F64d9C6d1EcF9b849Ae677dD3315835cb2;
+
+    function init_scenario(/*address other_user*/) payable public returns(address) {
+        CurveTokenExample lp_token = new CurveTokenExample(); 
+        MintableToken token = new MintableToken("example", "ex");
+
+        // setup Curve contract and its ETH and shares BEFORE the attacker
+        require(msg.value >= deposited_ether_before + attacker_deposit_eth, "Not enough funds sent to init the scenario");
+        Curve _curve = new Curve{value: deposited_ether_before}(address(lp_token), address(token));
+        lp_token.mint(other_user, other_user_lp);
+        token.mint(address(_curve), underlying_asset_before);
+
+        // Log the price before the attacker
+        // console.log("before the attacker got in the price is %s", _curve.getVirtualPrice());
+
+        // attakcer contract
+        attacker _attContract = new attacker(address(_curve));
+
+        // setup state (mints)
+        _curve.addScenarioEther{value: attacker_deposit_eth}();
+        lp_token.mint(address(_attContract), attacker_lp);
+        token.mint(address(_curve), attacker_underlying);
+
+
+        // Run the exploit
+        _attContract.exec();
+
+        return address(_attContract);
+    }
+}
+
+contract attacker{
+    Curve public attacked;
+    ERC20 token;
+    CurveTokenExample lp_token;
+
+    constructor(address attackedAddr){
+        attacked = Curve(attackedAddr);
+        token = ERC20(attacked.coins_1());
+        lp_token = CurveTokenExample(attacked.lp_token());
+    }
+    function exec() public {
+    // prepare token
+        // console.log("After Attacker deposit price is %s",attacked.getVirtualPrice());
+        uint256 my_lp_balance = lp_token.balanceOf(address(this));
+        uint[2] memory zeros = [uint(0), 0];
+        // console.log("trying to remove liq....");
+        attacked.remove_liquidity(my_lp_balance, zeros);    // virtual price dropped
+        // console.log("after the attack price is %s",attacked.getVirtualPrice());
+    }
+    fallback() external payable {
+        // console.log("during the attack price is %s",attacked.getVirtualPrice());
+    }
+}

CVLByExample/Curve/contracts/CurveToken.sol

@@ -0,0 +1,6 @@
+pragma solidity ^0.8.13;
+
+interface CurveToken{
+    function mint(address to, uint256 value) external returns(bool);
+    function burnFrom(address to, uint256 value) external returns(bool);
+}