diff --git a/src/halmos/cheatcodes.py b/src/halmos/cheatcodes.py index 73452180..df3b3b79 100644 --- a/src/halmos/cheatcodes.py +++ b/src/halmos/cheatcodes.py @@ -1379,7 +1379,10 @@ def handle(sevm, ex, arg: ByteVec, stack) -> ByteVec | None: # explicitly model malleability recover = f_ecrecover(digest, v, r, s) - recover_malleable = f_ecrecover(digest, v ^ 1, r, secp256k1n - s) + malleable_v = 55 - v # toggle between 27 and 28 + recover_malleable = f_ecrecover( + digest, malleable_v, r, secp256k1n - s + ) addr = apply_vmaddr(ex, key) ex.path.append(recover == addr) diff --git a/tests/regression/test/Signature.t.sol b/tests/regression/test/Signature.t.sol index 67f8fd08..345a9cfe 100644 --- a/tests/regression/test/Signature.t.sol +++ b/tests/regression/test/Signature.t.sol @@ -270,10 +270,19 @@ contract SignatureTest is SymTest, Test { bytes32 digest ) public { (uint8 v, bytes32 r, bytes32 s) = vm.sign(privateKey, digest); + uint8 malleableV = v == 27 ? 28 : 27; + + assert(malleableV == 27 || malleableV == 28); + assertNotEq(v, malleableV); assertEq( ecrecover(digest, v, r, s), - ecrecover(digest, v ^ 1, r, bytes32(secp256k1n - uint256(s))) + ecrecover( + digest, + malleableV, + r, + bytes32(secp256k1n - uint256(s)) + ) ); }