Step transition for end_tx not constrained
Description
The EVM circuit, which constrains the actual execution of instruction in the EVM, is organized around steps. For each step, a StepState is stored, containing the following data:
pub(crate) struct StepState<F> {
/// The execution state selector for the step
pub(crate) execution_state: DynamicSelectorHalf<F>,
/// The Read/Write counter
pub(crate) rw_counter: Cell<F>,
/// The unique identifier of call in the whole proof, using the
/// `rw_counter` at the call step.
pub(crate) call_id: Cell<F>,
/// The transaction id of this transaction within the block.
pub(crate) tx_id: Cell<F>,
/// Whether the call is root call
pub(crate) is_root: Cell<F>,
/// Whether the call is a create call
pub(crate) is_create: Cell<F>,
/// The block number the state currently is in. This is particularly
/// important as multiple blocks can be assigned and proven in a single
/// circuit instance.
pub(crate) block_number: Cell<F>,
/// Denotes the hash of the bytecode for the current call.
/// In the case of a contract creation root call, this denotes the hash of
/// the tx calldata.
/// In the case of a contract creation internal call, this denotes the hash
/// of the chunk of bytes from caller's memory that represent the
/// contract init code.
pub(crate) code_hash: Cell<F>,
/// The program counter
pub(crate) program_counter: Cell<F>,
/// The stack pointer
pub(crate) stack_pointer: Cell<F>,
/// The amount of gas left
pub(crate) gas_left: Cell<F>,
/// Memory size in words (32 bytes)
pub(crate) memory_word_size: Cell<F>,
/// The counter for reversible writes
pub(crate) reversible_write_counter: Cell<F>,
/// The counter for log index
pub(crate) log_id: Cell<F>,
/// Whether this is end_tx. Boolean.
pub(crate) end_tx: Cell<F>,
}To constrain these values from one step to the next, the individual gadgets for EVM instructions (as well as, e.g., block end) create a StepStateTransition, which stores the transition for most of the StepState fields. A transition could be a change to an absolute value or a delta to be added to the previous value.
pub(crate) struct StepStateTransition<F: Field> {
pub(crate) rw_counter: Transition<Expression<F>>,
pub(crate) call_id: Transition<Expression<F>>,
pub(crate) is_root: Transition<Expression<F>>,
pub(crate) is_create: Transition<Expression<F>>,
pub(crate) code_hash: Transition<Expression<F>>,
pub(crate) program_counter: Transition<Expression<F>>,
pub(crate) stack_pointer: Transition<Expression<F>>,
pub(crate) gas_left: Transition<Expression<F>>,
pub(crate) memory_word_size: Transition<Expression<F>>,
pub(crate) reversible_write_counter: Transition<Expression<F>>,
pub(crate) log_id: Transition<Expression<F>>,
pub(crate) end_tx: Transition<Expression<F>>,
}
pub(crate) enum Transition<T> {
Same,
Delta(T),
To(T),
Any,
}They then call the require_step_state_transition function of the EVMConstraintBuilder, defined in zkevm-circuits/src/evm_circuit/util/constraint_builder.rs, which constrains the StepState to transition to the next step as given by the StepStateTransition:
pub(crate) fn require_step_state_transition(
&mut self,
step_state_transition: StepStateTransition<F>,
) {
macro_rules! constrain {
($name:tt) => {
match step_state_transition.$name {
Transition::Same => self.require_equal(
concat!("State transition (same) constraint of ", stringify!($name)),
self.next.state.$name.expr(),
self.curr.state.$name.expr(),
),
Transition::Delta(delta) => self.require_equal(
concat!("State transition (delta) constraint of ", stringify!($name)),
self.next.state.$name.expr(),
self.curr.state.$name.expr() + delta,
),
Transition::To(to) => self.require_equal(
concat!("State transition (to) constraint of ", stringify!($name)),
self.next.state.$name.expr(),
to,
),
_ => {}
}
};
}
constrain!(rw_counter);
constrain!(call_id);
constrain!(is_root);
constrain!(is_create);
constrain!(code_hash);
constrain!(program_counter);
constrain!(stack_pointer);
constrain!(gas_left);
constrain!(memory_word_size);
constrain!(reversible_write_counter);
constrain!(log_id);
}However, constrain!(end_tx) is missing here. There are thus no constraints added that constrain the next steps's end_tx value based on the transition and the current steps end_tx.
Impact
As this part of the code was not in scope for our assessment, we did not fully explore the impact of this finding.
Unless otherwise prevented, it appears likely that the missing constraints allow ending transactions at any step by setting the end_tx field to true and the execution_state dynamic selector to EndTx. In practice, this could be used for example by taking a flash loan and then ending the transaction without paying it back. In the other direction, it may be possible to continue execution past instructions such as STOP that should end the transaction.
Recommendations
Add the constraints for end_tx:
constrain!(rw_counter);
constrain!(call_id);
constrain!(is_root);
constrain!(is_create);
constrain!(code_hash);
constrain!(program_counter);
constrain!(stack_pointer);
constrain!(gas_left);
constrain!(memory_word_size);
constrain!(reversible_write_counter);
constrain!(log_id);
+ constrain!(end_tx);
}Remediation
This issue has been acknowledged by Scroll, and a fix was implemented in commit 0c7a5602ā.