feat: constrain (r, s, v) signature values (a16z#259)

examples/simple/src/BadElections.sol

@@ -0,0 +1,38 @@
+// SPDX-License-Identifier: AGPL-3.0
+pragma solidity >=0.8.0 <0.9.0;
+
+import {ECDSA} from "openzeppelin/utils/cryptography/ECDSA.sol";
+
+/// DO NOT USE, this demonstrates signature malleability problems
+contract BadElections {
+    event Voted(uint256 proposalId, bool support, address voter);
+
+    mapping (bytes32 => bool) hasVoted;
+
+    // maps proposalId to vote count
+    mapping (uint256 => uint256) public votesFor;
+    mapping (uint256 => uint256) public votesAgainst;
+
+    // vote on a proposal by signature, anyone can cast a vote on behalf of someone else
+    function vote(uint256 proposalId, bool support, address voter, bytes calldata signature) public {
+        bytes32 sigHash = keccak256(signature);
+        require(!hasVoted[sigHash], "already voted");
+
+        bytes32 badSigDigest = keccak256(abi.encode(proposalId, support, voter));
+        address recovered = ECDSA.recover(badSigDigest, signature);
+        require(recovered == voter, "invalid signature");
+        require(recovered != address(0), "invalid signature");
+
+        // prevent replay
+        hasVoted[sigHash] = true;
+
+        // record vote
+        if (support) {
+            votesFor[proposalId]++;
+        } else {
+            votesAgainst[proposalId]++;
+        }
+
+        emit Voted(proposalId, support, voter);
+    }
+}

examples/simple/test/BadElections.t.sol

@@ -0,0 +1,60 @@
+// SPDX-License-Identifier: AGPL-3.0
+pragma solidity >=0.8.0 <0.9.0;
+
+import "forge-std/Test.sol";
+
+import {SymTest} from "halmos-cheatcodes/SymTest.sol";
+
+import {BadElections} from "src/BadElections.sol";
+
+contract BadElectionsTest is SymTest, Test {
+    BadElections elections;
+
+    function setUp() public {
+        elections = new BadElections();
+    }
+
+    /// The output will look something like this:
+    ///
+    ///     Running 1 tests for test/BadElections.t.sol:BadElectionsTest
+    ///     Counterexample:
+    ///         halmos_fakeSig_bytes_01 = 0x00000000000000000000000000000000000000000000000000000000000000003fffffffffffffffffffffffffffffff5d576e7357a4501ddfe92f46681b20a100 (65 bytes)
+    ///         p_proposalId_uint256 = 0x0000000000000000000000000000000000000000000000000000000000000000 (0)
+    ///     [FAIL] check_canNotVoteTwice(uint256) (paths: 7, time: 0.63s, bounds: [])
+    ///
+    /// the counterexample values are not meaningful, but examining the trace shows
+    /// that halmos found a signature s.t. the voter can vote twice on the same proposal,
+    /// and the final vote count is 2
+    function check_canNotVoteTwice(uint256 proposalId) public {
+        // setup
+        bool support = true;
+        (address voter, uint256 privateKey) = makeAddrAndKey("voter");
+
+        bytes32 sigDigest = keccak256(abi.encode(proposalId, support, voter));
+        (uint8 v, bytes32 r, bytes32 s) = vm.sign(privateKey, sigDigest);
+        bytes memory signature = abi.encodePacked(r, s, v);
+
+        // we start with no vote
+        assertEq(elections.votesFor(proposalId), 0);
+
+        // when we cast the vote
+        elections.vote(proposalId, support, voter, signature);
+
+        // then the vote count increases
+        assertEq(elections.votesFor(proposalId), 1);
+
+        // when we vote again with the same signature, it reverts
+        try elections.vote(proposalId, support, voter, signature) {
+            assert(false);
+        } catch {
+            // expected
+        }
+
+        // when the same voter votes with a different signature
+        elections.vote(proposalId, support, voter, svm.createBytes(65, "fakeSig"));
+
+        // then the vote count remains unchanged
+        // @note spoiler alert: it does not
+        assertEq(elections.votesFor(proposalId), 1);
+    }
+}

src/halmos/cheatcodes.py

@@ -521,6 +521,16 @@ def handle(sevm, ex, arg: BitVec) -> BitVec:
                 # associate the new signature with the private key and digest
                 known_sigs[(key, digest)] = (v, r, s)
 
+                # constrain values to their expected ranges
+                in_range = And(
+                    Or(v == 27, v == 28),
+                    ULT(0, r),
+                    ULT(r, secp256k1n),
+                    ULT(0, s),
+                    ULT(s, secp256k1n),
+                )
+                ex.path.append(in_range)
+
                 # explicitly model malleability
                 recover = f_ecrecover(digest, v, r, s)
                 recover_malleable = f_ecrecover(digest, v ^ 1, r, secp256k1n - s)

src/halmos/utils.py

@@ -182,8 +182,13 @@ def extract_string_argument(calldata: BitVecRef, arg_idx: int):
     return string_bytes.decode("utf-8") if is_concrete(string_bytes) else string_bytes
 
 
-def extract_bytes(data: BitVecRef, byte_offset: int, size_bytes: int) -> BitVecRef:
+def extract_bytes(
+    data: Optional[BitVecRef], byte_offset: int, size_bytes: int
+) -> BitVecRef:
     """Extract bytes from calldata. Zero-pad if out of bounds."""
+    if data is None:
+        return BitVecVal(0, size_bytes * 8)
+
     n = data.size()
     if n % 8 != 0:
         raise ValueError(n)

tests/expected/all.json

@@ -1486,6 +1486,15 @@
                 "time": null,
                 "num_bounded_loops": null
             },
+            {
+                "name": "check_ecrecover_eip2098CompactSignatures(uint256,bytes32)",
+                "exitcode": 0,
+                "num_models": 0,
+                "models": null,
+                "num_paths": null,
+                "time": null,
+                "num_bounded_loops": null
+            },
             {
                 "name": "check_ecrecover_explicitMalleability(uint256,bytes32)",
                 "exitcode": 0,
@@ -1710,6 +1719,24 @@
                 "num_paths": null,
                 "time": null,
                 "num_bounded_loops": null
+            },
+            {
+                "name": "check_vmsign_tryRecover(uint256,bytes32)",
+                "exitcode": 0,
+                "num_models": 0,
+                "models": null,
+                "num_paths": null,
+                "time": null,
+                "num_bounded_loops": null
+            },
+            {
+                "name": "check_vmsign_valuesInExpectedRange(uint256,bytes32)",
+                "exitcode": 0,
+                "num_models": 0,
+                "models": null,
+                "num_paths": null,
+                "time": null,
+                "num_bounded_loops": null
             }
         ],
         "test/SmolWETH.t.sol:SmolWETHTest": [

tests/regression/test/Signature.t.sol

@@ -127,6 +127,19 @@ contract SignatureTest is SymTest, Test {
         assertNotEq(addr, address(0x42));
     }
 
+    function check_vmsign_valuesInExpectedRange(
+        uint256 privateKey,
+        bytes32 digest
+    ) public {
+        (uint8 v, bytes32 r, bytes32 s) = vm.sign(privateKey, digest);
+
+        assert(v == 27 || v == 28);
+        assertGt(uint256(r), 0);
+        assertLt(uint256(r), secp256k1n);
+        assertGt(uint256(s), 0);
+        assertLt(uint256(s), secp256k1n);
+    }
+
     function check_vmsign_consistent(
         uint256 privateKey,
         bytes32 digest
@@ -180,6 +193,17 @@ contract SignatureTest is SymTest, Test {
         assertNotEq(r1, r2);
     }
 
+    /// FIXME: this should pass, but it doesn't because we always return 32 bytes
+    // function check_ecrecover_invalidCallReturnsNothing() public {
+    //     uint256 returnDataSize;
+    //     assembly {
+    //         let succ := call(gas(), ECRECOVER_PRECOMPILE, 0, 0, 0, 0, 0)
+    //         returnDataSize := returndatasize()
+    //     }
+
+    //     assertEq(returnDataSize, 0);
+    // }
+
     function check_vmsign_ecrecover_e2e_recoveredMatches(
         uint256 privateKey,
         bytes32 digest
@@ -220,6 +244,27 @@ contract SignatureTest is SymTest, Test {
         assertNotEq(ecrecover(digest, v, r, s), ecrecover(digest, otherV, otherR, otherS));
     }
 
+    function check_vmsign_tryRecover(
+        uint256 privateKey,
+        bytes32 digest
+    ) public {
+        (uint8 v, bytes32 r, bytes32 s) = vm.sign(privateKey, digest);
+        bytes memory sig = abi.encodePacked(r, s, v);
+        address originalAddr = vm.addr(privateKey);
+
+        // we don't want ecrecover to return address(0), it would indicate an error
+        vm.assume(originalAddr != address(0));
+
+        (address recovered, ECDSA.RecoverError error, ) = ECDSA.tryRecover(digest, sig);
+        if (error == ECDSA.RecoverError.InvalidSignatureS) {
+            // tryRecover rejects s values in the high half order
+            assertGt(uint256(s), secp256k1n / 2);
+        } else {
+            assertEq(uint256(error), uint256(ECDSA.RecoverError.NoError));
+            assertEq(recovered, originalAddr);
+        }
+    }
+
     function check_ecrecover_explicitMalleability(
         uint256 privateKey,
         bytes32 digest
@@ -294,6 +339,25 @@ contract SignatureTest is SymTest, Test {
         assertEq(ecrecover(digest, v2, r2, s2), vm.addr(privateKey2));
     }
 
+    function check_ecrecover_eip2098CompactSignatures(
+        uint256 privateKey,
+        bytes32 digest
+    ) public {
+        address addr = vm.addr(privateKey);
+        (uint8 v, bytes32 r, bytes32 s) = vm.sign(privateKey, digest);
+
+        // assume s is in the lower half order
+        vm.assume(uint256(s) < secp256k1n / 2);
+
+        // convert to compact format
+        uint8 yParity = v - 27;
+        bytes32 vs = bytes32(((uint256(yParity) << 255) | uint256(s)));
+
+        // check that the compact signature can be verified
+        address recovered = ECDSA.recover(digest, r, vs);
+        assertEq(recovered, addr);
+    }
+
     function check_makeAddrAndKey_consistent_symbolic() public {
         string memory keyName = svm.createString(32, "keyName");
         (address addr, uint256 key) = makeAddrAndKey(keyName);