The core issue is that RNG used in generating random inputs can differ across different runs of verify_deployment.
The failing case manifests in the following way:
The execution of cast r0 into r1 as scalar; creates an invalid scalar field element when r0 is larger than the scalar field modulus.
The resulting value is ejected before storing the result into the register r1.
Scalar::eject_value halts, if the scalar field element is invalid.
Consequently, a deployment of the above program can fail to verify depending on the random inputs that were used.
Solution
To fix this issue, this PR deterministically seeds the RNG used in deployment verification with the lower 64 bits of the deployment ID. This ensures that validators will use the same seed for a particular deployment, which ensures that they will always agree on whether the deployment is valid or not.
Testing
This PR includes a test that attempts to deploy a program that loads and stores data types with invalid scalar field elements. The test verifies that the status of the deployment is consistent: always valid or always invalid, independent of the RNG.
In addition to this PR, additional mitigations can be put in place to ensure that:
Scalar::eject_value does not halt
Loading and storing circuits to registers does not invoke eject_value. This is dependent on whether or not the invocations of eject_value are intended to serve as a value check or a less strict type check.
This PR:
Failing Case
This issue was found in a deployed program with a similar structure to:
At a high-level, deployments are verified by randomly generating inputs, executing the program, extracting the assignment, and checking that the associated certificates match the structure of the assignment. Note that the actual values do not matter. Source
The core issue is that RNG used in generating random inputs can differ across different runs of verify_deployment.
The failing case manifests in the following way:
cast r0 into r1 as scalar;
creates an invalid scalar field element whenr0
is larger than the scalar field modulus.r1
.Solution
To fix this issue, this PR deterministically seeds the RNG used in deployment verification with the lower 64 bits of the deployment ID. This ensures that validators will use the same seed for a particular deployment, which ensures that they will always agree on whether the deployment is valid or not.
Testing
This PR includes a test that attempts to deploy a program that loads and stores data types with invalid scalar field elements. The test verifies that the status of the deployment is consistent: always valid or always invalid, independent of the RNG.
CI for this branch is running here.
Considerations
In addition to this PR, additional mitigations can be put in place to ensure that:
Scalar::eject_value
does not halteject_value
. This is dependent on whether or not the invocations ofeject_value
are intended to serve as a value check or a less strict type check.Related PRs
Use this PR over #2534