Picus is an implementation of the
If you are looking for the documentation for the artifact evaluation of
Picus currently supports three targets: Circom, R1CS, and gnark.
Target | File extension | Notes |
---|---|---|
Circom (>= 2.0.6) | .circom |
circom installation required. |
R1CS | .r1cs |
|
gnark | .sr1cs |
gnark library required. See https://github.com/Veridise/picus_gnark for details |
This section provides basic instructions on how to test out the tool for the kick-the-tires phase. We provide pre-built docker image, which is recommended.
docker build -t picus:v0 .
docker run -it --memory=10g picus:v0 bash
Note: you should adjust the total memory limit (10g) to a suitable value according to your machine configuration. Adding the memory restriction would prevent some benchmarks from jamming docker due to large consumption of the memory. Usually 8g memory is recommended since some benchmarks could be large.
You can skip this section if you build the tool from Docker.
Building from source is not recommended if you just want to quickly run and check the results. Some dependencies require manual building and configuration, which is system specific. One only needs to make sure the following dependencies are satisfied before the tool / basic testing instructions can be executed.
- Racket (8.0+): https://racket-lang.org/
- Either cvc5 with finite field theory suport or Z3 (>= 4.10.2). The former is recommended. See cvc5 vs Z3 for further details.
- Circuit compiler backend, as indicated in the support table above.
Run raco pkg install
under the project directory to install Picus.
First change the directory to the repo's root path:
cd Picus/
Then test some benchmarks, e.g., the Decoder
benchmark, run:
./run-picus ./benchmarks/circomlib-cff5ab6/[email protected]
A successful run will output logging info similar to the following (note that actual counter-example could be different due to potential stochastic search strategy in dependant libraries):
The circuit is underconstrained
Counterexample:
inputs:
main.inp: 0
first possible outputs:
main.out[0]: 1
main.out[1]: 0
main.success: 1
second possible outputs:
main.out[0]: 0
main.out[1]: 0
main.success: 0
first internal variables:
no first internal variables
second internal variables:
no second internal variables
Exiting Picus with the code 9
If you see this, it means the environment that you are operating on is configured successfully.
The following lists out all available options for running the tool.
usage: run-picus [ <option> ... ] <source>
<source> must be a file with .circom, .r1cs, or .sr1cs extension
<option> is one of
--json <json-target>
either:
- json logging output path; or
- '-', which suppresses the text logging mode and
outputs json logging to standard output
(default: no json output)
--noclean
do not clean up temporary files (default: false)
--timeout <timeout>
timeout for SMT query (default: 5000ms)
--solver <solver>
solver to use: cvc4 | cvc5 | z3 (default: cvc5)
--selector <selector>
selector to use: counter | first (default: counter)
--precondition <precondition>
path to precondition json (default: none)
--noprop
disable propagation (default: false / propagation on)
--nosolve
disable solver phase (default: false / solver on)
--strong
check for strong safety (default: false)
--truncate <truncate>
truncate overly long logged message: on | off (default: on)
--log-level <log-level>
The log-level for text logging (default: INFO)
Possible levels (in the ascending order): DEBUG, ACCOUNTING, PROGRESS, INFO, WARNING, ERROR, CRITICAL
circom options (only applicable for circom source)
--opt-level <opt-level>
optimization level for circom compilation (default: 0)
circom and r1cs options (only applicable for circom and r1cs source)
--wtns <wtns>
wtns files output directory (default: don't output)
other options
--help, -h
Show this help
--
Do not treat any remaining argument as a switch (at this level)
Multiple single-letter switches can be combined after
one `-`. For example, `-h-` is the same as `-h --`.
If <source>
is a R1CS file from a Circom source, we highly recommend that the Circom compilation should use the --O0
flag and with the --sym
option.
Otherwise, Picus may not be as effective as it can.
Picus will not output false positive. Potential outputs are:
safe
: Picus cannot find underconstrained bugsunsafe
: Picus can find an underconstrained bug and it usually will also output the attack vectorunknown
: Picus cannot get a result within the given time limit. Manual review or an increase in time limit for the solver is necessary.
Picus can be used with either cvc5 or Z3 SMT solver.
Different shapes of finite field constraints may have different difficulties for solvers with different theories. z3
currently does not have a finite field theory, so it will not work well in majority of the cases for ZK circuits, while cvc5
has basic finite field support so it will work better.
Regarding the results reported, supposing that there are no other bugs in the system and solver, if z3
reports safe
, it means z3
can solve the constraints and get the result. When cvc5
returns unknown
, it means it got stuck in solving. In this case, the result would be safe
since z3
terminates with concrete results while cvc5
cannot, supposing everything else is correct.
Conflicting results (safe
for one and unsafe
for the other) indicate a bug in Picus, and we would appreciate a bug report. In this case, the only way to know which one is correct is to manually verify the counter example outputted by the solver that reports unsafe
.
- In case of
Killed
error: it might be a resources problem. Try to increase the memory allocated to docker. - In case no response / solving for a long time: this usually means the finite field solver in
cvc5
chokes. There is currently no direct solution to quickly improve the solver's performance.
A common way to mitigate the above issues is to split a big circuit into smaller pieces and feed them to the tool one by one.
If a big target is too difficult to verify all at once fully automatically (which is the case for many real-world circuits), it is possible to do a semi-automatic way by manually tearing the circuits into pieces and perform automatic verification for each piece of them. If each piece can be verified successfully, this means the whole circuit is properly constrained. If all queries to the tool return safe
, the overall result is also safe. If any query returns unsafe
or unknown
then the overall result is unknown
since local unsafe cases could (but not always) lead to global vulnerability (since other parts of the circuit could have fixed the issues).
In some difficult cases where a template is very complicated -- e.g., a crypto hashing function -- and it is already difficult to verify the hash function itself, but supposing it is correct, it is possible to manually rewrite this difficult template into a relatively simple one with the same output domain to keep the computation easy for verification.
For example, suppose there is a circuit that is composed by f(g(h(x)))
and h(x)
is difficult to verify and blocking the remaining steps. But it is known that h(x)
is definitely safe and the output domain of h(x)
is known (let's say it is h(x)
with a variable h(x)
needs to be done carefully if there are more constraints applied on it, e.g., a(b(h(x)))
-- basically the rewriting should not be breaking the semantics of the remaining part of circuit, or at least not under-approximating their relations -- that being said, if the circuit is rewritten to cover a larger variable space and can still verify it, it is ok.
Note that these two options can be used to prove the correctness of the circuit. If there is indeed a bug there, then other approaches are needed to excavate the counter-example (something like an attack vector). When these two options say a circuit is safe
then it is definitely safe
(given that the rewrite is correct), but when they say a circuit is unsafe
, it may not necessarily be unsafe
since the variable space is over-approximated-- another semi-automatic way is needed to construct the counter-example.
Yes, it is possible to output more counterexamples, but there is no user interface for now. The idea is that once a first counterexample is outputted, to get a different one, the solver can be invoked again with the first counterexample banned — it will then search for a counterexample different than the first one.
If you find our work and this tool useful in your research, please consider citing:
@ARTICLE{pldi23-picus,
title = "Automated Detection of {Under-Constrained} Circuits in
{Zero-Knowledge} Proofs",
author = "Pailoor, Shankara and Chen, Yanju and Wang, Franklyn and
Rodr{\'\i}guez, Clara and Van Geffen, Jacob and Morton, Jason
and Chu, Michael and Gu, Brian and Feng, Yu and Dillig, I{\c
s}{\i}l",
journal = "Proc. ACM Program. Lang.",
publisher = "Association for Computing Machinery",
volume = 7,
number = "PLDI",
month = jun,
year = 2023,
address = "New York, NY, USA",
keywords = "SNARKs, program verification, zero-knowledge proofs"
}