Skip to content

fix(symbolic): require ecrecover scalars in [1, n) #18347

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
figtracer wants to merge 3 commits into
base: mablr/evm2-migration
Choose a base branch
from
Open

fix(symbolic): require ecrecover scalars in [1, n) #18347

Show file tree
Hide file tree
Changes from 2 commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
0b35b4a
fix(symbolic): require ecrecover scalars in [1, n)
figtracer Nov 10, 2026
38e9e50
fix(symbolic): fork ecrecover on signature well-formedness
figtracer Nov 10, 2026
182861f
fix(symbolic): execute redirected ecrecover target
figtracer Nov 10, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
127 changes: 112 additions & 15 deletions crates/evm/symbolic/src/executor/calls.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1060,21 +1060,39 @@ impl SymbolicExecutor {
if is_precompile_for_spec(code_address, spec_id) {
let input_len = in_size.size_word(&mut self.cx);
let input = in_size.read_from_memory(&mut self.cx, &state.memory, in_offset);
if precompile_number_for_spec(code_address, spec_id) == Some(10) {
let input_bytes = input.materialize(&mut self.cx);
return self.execute_kzg_precompile_call(
executor,
state,
worklist,
kind,
to,
call_caller,
value,
out_offset,
&out_size,
input_bytes,
input_len,
);
match precompile_number_for_spec(code_address, spec_id) {
Some(1) => {
return self.execute_ecrecover_precompile_call(
executor,
state,
worklist,
kind,
to,
call_caller,
value,
out_offset,
&out_size,
input,
input_len,
);
}
Some(10) => {
let input_bytes = input.materialize(&mut self.cx);
return self.execute_kzg_precompile_call(
executor,
state,
worklist,
kind,
to,
call_caller,
value,
out_offset,
&out_size,
input_bytes,
input_len,
);
}
_ => {}
}
let outcome =
execute_symbolic_precompile(&mut self.cx, code_address, input, input_len, spec_id)?;
Expand Down Expand Up @@ -1372,6 +1390,85 @@ impl SymbolicExecutor {
}
}

/// Forks a symbolic ECRECOVER call on whether the signature is well-formed.
///
/// A malformed signature returns no data, which concrete replay reproduces exactly, so that
/// path continues first and its counterexamples replay. The well-formed path keeps the opaque
/// recovery model, whose failures depend on curve facts the solver does not know.
#[expect(clippy::too_many_arguments)]
fn execute_ecrecover_precompile_call(
&mut self,
executor: &ExecutorView<'_>,
state: &mut PathState,
worklist: &mut VecDeque<PathState>,
kind: CallKind,
to: Address,
call_caller: Address,
value: SymExpr,
out_offset: SymExpr,
out_size: &BoundedCopySize,
input: SymBytes,
input_len: SymExpr,
) -> Result<StepOutcome, SymbolicError> {
let spec_id = executor.spec_id;
let sized = SymBytes::sized(&mut self.cx, input.clone(), input_len.clone(), 128);
let well_formed = ecrecover_signature_well_formed(&mut self.cx, &sized);
let malformed = well_formed.clone().not(&mut self.cx);
let (malformed_constraints, malformed_sat) =
self.constraints_with_condition(state, malformed)?;
let (well_formed_constraints, well_formed_sat) =
self.constraints_with_condition(state, well_formed)?;
if malformed_sat && well_formed_sat {
let mut recovering = state.clone();
recovering.constraints = well_formed_constraints;
let outcome = execute_symbolic_precompile(&mut self.cx, to, input, input_len, spec_id)?;
match self.apply_precompile_outcome(
executor,
&mut recovering,
kind,
to,
call_caller,
value.clone(),
out_offset.clone(),
out_size,
outcome,
)? {
StepOutcome::Continue => worklist.push_back(recovering),
outcome => {
*state = recovering;
return Ok(outcome);
}
}
state.constraints = malformed_constraints;
let outcome = Some(SymReturnData::empty(&mut self.cx));
return self.apply_precompile_outcome(
executor,
state,
kind,
to,
call_caller,
value,
out_offset,
out_size,
outcome,
);
}
state.constraints =
if malformed_sat { malformed_constraints } else { well_formed_constraints };
let outcome = execute_symbolic_precompile(&mut self.cx, to, input, input_len, spec_id)?;

@mattsse mattsse Nov 10, 2026

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Use the resolved code_address for precompile execution here and in the both-feasible branch. The caller dispatches this helper using code_address, but passes the original to; these differ after vm.mockFunction. For example, mock address(4) to address(1) for abi.encode(bytes32(0), uint256(27), bytes32(0), bytes32(0)), then staticcall address(4): concrete execution and the previous symbolic implementation return empty ecrecover output, whereas this call executes identity and returns all 128 input bytes. Redirecting an ordinary contract instead produces unsupported precompile. Keep the original recipient for call effects, but execute the resolved ecrecover precompile.

self.apply_precompile_outcome(
executor,
state,
kind,
to,
call_caller,
value,
out_offset,
out_size,
outcome,
)
}

#[expect(clippy::too_many_arguments)]
/// Applies a precompile call result to the current symbolic state.
fn apply_precompile_outcome(
Expand Down
24 changes: 20 additions & 4 deletions crates/evm/symbolic/src/runtime/precompiles.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,9 @@
use super::*;

/// Order of the secp256k1 curve, the exclusive bound of a valid signature scalar.
const SECP256K1_ORDER: U256 =
U256::from_be_bytes(hex!("fffffffffffffffffffffffffffffffebaaedce6af48a03bbfd25e8cd0364141"));

pub(crate) fn precompile_number(address: Address) -> Option<u8> {
let bytes = address.as_slice();
if bytes[..PRECOMPILE_ADDRESS_LEADING_ZEROS].iter().any(|byte| *byte != 0) {
Expand Down Expand Up @@ -100,10 +104,7 @@ pub(crate) fn execute_symbolic_precompile(
if let Ok(input) = input.concrete_bytes(cx, "symbolic ecrecover input") {
return execute_precompile(cx, address, &input, spec_id);
}
let v = input.word_at(cx, 32);
let v27 = SymBoolExpr::eq_word_const(cx, &v, U256::from(27));
let v28 = SymBoolExpr::eq_word_const(cx, &v, U256::from(28));
let valid_v = SymBoolExpr::or(cx, vec![v27, v28]);
let valid_v = ecrecover_signature_well_formed(cx, &input);
if valid_v.as_const() == Some(false) {
return Ok(Some(SymReturnData::empty(cx)));
}
Expand Down Expand Up @@ -217,6 +218,21 @@ pub(crate) fn execute_symbolic_precompile(
}
}

/// Returns whether a 128-byte ECRECOVER input is a well-formed signature: `v` is 27 or 28 and `r`
/// and `s` are in `[1, n)`. The precompile returns no data otherwise.
pub(crate) fn ecrecover_signature_well_formed(cx: &mut SymCx, input: &SymBytes) -> SymBoolExpr {
let v = input.word_at(cx, 32);
let v27 = SymBoolExpr::eq_word_const(cx, &v, U256::from(27));
let v28 = SymBoolExpr::eq_word_const(cx, &v, U256::from(28));
let mut valid = vec![SymBoolExpr::or(cx, vec![v27, v28])];
for offset in [64, 96] {
let scalar = input.word_at(cx, offset);
valid.push(SymBoolExpr::cmp_word_const(cx, SymCmpOp::Ult, &scalar, SECP256K1_ORDER));
valid.push(scalar.nonzero_bool(cx));
}
SymBoolExpr::and(cx, valid)
}

pub(crate) fn symbolic_modexp_precompile(
cx: &mut SymCx,
input: &SymBytes,
Expand Down
8 changes: 8 additions & 0 deletions crates/forge/tests/cli/test_cmd/symbolic_precompiles.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -225,9 +225,16 @@ contract EcrecoverReturnData {
}
}

// A signature with `r = 0` or `s = 0` never recovers.
function checkZeroScalarRecoversNothing(bytes32 digest, bytes32 r, bytes32 s) public pure {
assert(ecrecover(digest, 27, bytes32(0), s) == address(0));
assert(ecrecover(digest, 28, r, bytes32(0)) == address(0));
}

function testFuzzConformance(bytes32 digest, uint8 v, bytes32 r, bytes32 s) public view {
checkInvalidRecoveryId(digest, r, s);
checkRecoveryOutput(digest, v, r, s);
checkZeroScalarRecoversNothing(digest, r, s);
}
}
"#,
Expand All @@ -246,6 +253,7 @@ contract EcrecoverReturnData {
...
[PASS] checkInvalidRecoveryId(bytes32,bytes32,bytes32) ([METRICS])
[PASS] checkRecoveryOutput(bytes32,uint8,bytes32,bytes32) ([METRICS])
[PASS] checkZeroScalarRecoversNothing(bytes32,bytes32,bytes32) ([METRICS])
...
"#]]);
}
Expand Down
Loading