Since the tables are defined over a finite field, if the initial program counter is too large, the next program counter in the final row may wrap around to zero before the halt syscall is reached.
|
if i == proof.0.len() - 1 && public_values.next_pc != BabyBear::zero() { |
As a result, a malicious prover can generate a proof that appears to show successful program termination, even though the halt syscall was never actually executed.
This issue is disclosed with the permission of @johnchandlerburnham.
Since the tables are defined over a finite field, if the initial program counter is too large, the next program counter in the final row may wrap around to zero before the halt syscall is reached.
sphinx/prover/src/verify.rs
Line 93 in 8a39b95
As a result, a malicious prover can generate a proof that appears to show successful program termination, even though the halt syscall was never actually executed.