[Music]
good morning everyone so today I'll talk
about fuzzing for zero knowledge
infrastructure and this is Joint work
with my collaborators from the Technical
University of
Vienna so just to kind of make sure we
are all on the same page um let's have a
short definition of what I understand by
zero knowledge infrastructure so uh for
this talk I'll um Define zero knowledge
infrastructure as software components
that are used for compiling executing
proving and verifying ZK circuits so
examples would be the processing
pipelines that are commonly used by uh
dsls for describing ZK uh circuits or
maybe in the future we'll also look at
entire ZK
EVMS so um with this out of the way um
let's um look at why this is an
important topic and why um more people
should be doing this well first zero
knowledge infrastructure is highly
complex and highly critical for instance
it's used in several L2 chains so kind
of bugs there uh could have uh
catastrophic financial and reputational
uh impact and we should really make sure
these components are as bulletproof as
they can
get um while we haven't seen a really
catastrophic incident uh in this field
may maybe perhaps uh comparable to the
Dow hack in
2016 uh it's really important that um we
have uh rigorous testing for these
components and we use um you know the
best ering uh discipline that we can um
have right uh because these components
are really complex and getting them
right is is not
easy so what is fuzzing I don't think I
have to like explain this after the last
uh talk but fuzzing is widely used in
industry um for instance at Microsoft
Google meta uh they're fuzzing a lot of
their infrastructure uh to catch Buck
before um hackers can actually exploit
them in
practice so in this talk I'll give you
an overview of our fuzzer for um finding
critical bugs in processing pipelines
for zero knowledge circuits um the
fuzzer is called Circus and it already
supports four of these pipelines namely
uh circum cor uh gar and Noir and
there's you know like a a gazillion of
different
dsls popping up it seems like you walk
around here and you see another one in
the corner um and we've already found uh
16 bugs in total for the four uh
pipelines we looked at um 15 have
already been fixed so that kind of shows
that these bugs are really uh taken
seriously and um developers sometimes
respond within hours to actually get
them
fixed um you can also see a kind of uh
breakdown of the different
bugs and where we found them and as you
can see they're kind of very evenly
spread across the different uh pipelines
so it's not like there's one pipeline
that's you know responsible for all the
bugs uh that we
found um now kind of to make sure that
everybody understands I mean like I yeah
I assume not all people are aware of
what these uh processing pipelines look
like look like uh here's a short kind of
summary um you can see in the sort of
yellow box um there is a circuit that
the user writes um that goes into the
compiler and then the compiler um hands
some output to the witness generator and
the witness generator can then take the
input so the you the user input uh to
the circuit and generate a witness uh
that can be then used by the prover and
then theover generates a proof that can
then be very verified to essentially
check that the circuit was actually
executed so um now that we have a bit of
an understanding of how these pipelines
look like let's uh dive a bit uh deeper
to understand how we find these
bugs so first I want to be very clear um
we are not cryptographers this is not
our uh this is not my background my
background is in you know uh software
security uh program
analysis um and for this reason I can't
really you know try to understand the
the logic that's in the integrate log
logic in many of these
components um which is uh why we treat
these essentially as a blackbox so much
like what a typical user would do uh we
just view them as a
blackbox so how can we still find all
these bugs right well first we have a
lot of experience
uh in testing uh complex or software for
complex domains and building fuzzers for
them so we've done quite a bit of work
on uh fuzzing for smart contracts it's
probably the work that's most closely to
the audience that's here um and for
instance we created the Harvey fuzzer um
many years ago and we're still kind of
maintaining it um we also did some work
on ML models um and on on testing ml
models and testing program analysis
tools um yeah if you want to know more
check out the papers that are um online
um and the second reason why we were
able to find these bugs is that we have
a not so secret weapon which is called
metamorphic
testing so before um explaining in a bit
more detail what metamorphic testing is
let me just give you kind of a uh short
summary of how we got here how we got
into this uh interested in this topic um
so we as I said we were um working on
fuzzing for smart contracts mainly uh
for many years and then at some point um
I guess maybe like a year ago roughly um
consensus they released the linear
blockchain um that is one of the first
ZK
EVMS and we were like well this is
really complex uh we started looking
into it a bit um and we saw that there
are these components like the Gnar
library and and the corset language for
um processing zero knowledge circuits so
we were like oh what can we do to you
know um test these what can we do to
make sure that there no bugs in these
components um and that's when we started
building um kind of a predecessor to
this fuzzer uh I'm presenting today uh
which is called
Rio um so the Rio is a fer for the Gnar
Library specifically and then
essentially this uh C ccus fuzzer I'm
presenting today is essentially an
evolution of this uh fuzzer that is a
bit more General and can Target multiple
um
dsls all right now uh back to
metamorphic testing so what is
metamorphic testing um I think the
shortest way to summarize it it's kind
of a way to define test oracles uh in a
pretty elegant and concise way so to
illustrate I've um I've uh collected a
few examples that um yeah explain this
uh and try to um explain what
metamorphic testing is so the first
example is how to actually test that the
Sorting function uh sort for an input
let's say an array of integers X
actually does the right thing well
there's many ways to to check this but
here's uh a way to check it um using
metamorphic testing so you take you sort
um the input X and then you also sort
for uh X but you Shuffle it randomly
right and these two um the output of
both of these invocations of the
function they should have the same
output right so pretty nice and concise
uh specification so let's look at
another example uh here um we want to
test um essentially some procedure for
computing the shortest path in uh graph
G between the nodes n and M so how can
we do this this with metamorphic testing
well one way to do it is to say you know
the shortest path um between n and M in
the graph G is less than uh the shortest
path between n and n and n and M um in
the graph where we take G but we remove
uh some random Edge right because that
edge might have been on the the shortest
path and then the shortest path could
become longer
right so
we can also do apply the same kind of
principle to more complex uh components
like a entire compiler right so here's
an example of how to do this with
metamorphic testing um when you take a
program p and you compile it and then
run it you should essentially see the
same behavior as when you take um the
program P but you add some dead code
somewhere randomly right and you compile
it and you run it shouldn't matter right
should give you the same output
essentially
so with this um let's look at how we can
apply kind of the same reasoning
principle to uh zero knowledge uh
circuits so the fuzzer what it does is
uh it first generates a random circuit
uh C1 and then it applies a random
transformation to C1 to get a new
circuit C2 so now we have two circuits
that are essentially
syntactically perhaps completely
different uh but semantically they
should have uh the same
behavior and now we the fuzzer generates
an input I and um invokes the processing
pipelines for both of these
circuits um and if there's any
difference in you know the output or the
behavior then that's a bug somewhere in
this processing
pipeline so for instance um the for one
circuit we might not be able to generate
a witness but for the other one we would
then there's probably a bar somewhere in
the compiler or in the witness
generator so um let's look at a few of
these uh Transformations uh to kind of
understand how the fuzzer does this um
so here's a very simple transformation
uh if you have somewhere in your circuit
an expression e uh you can always apply
um you can always multiply the
expression by one right that should not
change anything um or you can also
divide by one again shouldn't have any
effect on the
circuits um another transformation is to
basically negate the expression e
twice or you can also apply other
Transformations like um swapping um the
two oper of a
multiplication and then we also have um
um some Transformations that use
essentially new randomly generated
Expressions so here for instance we
replace an expression e with e minus
some random expression plus some random
expression right that should again not
have any effect
um and we have a small DSL for
describing these circuits so there's
many more of these transform
formations um So currently we support
roughly 90 uh such rules but you can
easily add more of them and think of new
ones if you want like
to so uh we also found a number of bugs
in um the different uh pipelines and
let's look at a few of them um just to
kind of give you the the idea and show
give you a concrete example um that you
can look at so here on the left uh we
see uh a small uh example circuit in in
the circuit circum um language uh you
can also look up the GitHub issue uh if
you if you'd like to
um but this essentially a minimized uh
cleaned up um version of the
circuit um and as you can see there's a
variable P um in practice this is
essentially just a constant uh just
didn't fit on the on the slide so I um
yeah put it at the bottom um but think
of P just as a normal constant in your
program and now what the fuzzer does is
it generates a transformation of this
this circuit which is the one uh that's
shown on the right and here it applies a
number of um metamorphic Transformations
so for instance it seems like the fuzer
first
um multiplied the expression P by one
then subtracted Zero from one and then
divided um that expression uh by one and
when we execute this um when we execute
these two circuit
we can see that
um that the output out one and out two
actually are not the
same so this is bad and this is was a
bug that we found um seemed like there
was a bug in the witness generation
part um and here's another bug um that
we found in gnark um so at the top you
can again see the the original circuit
that the fuzer generated and then we can
also see the transform circuit um where
the fuzzer essentially changed the
expression zero to just zero or zero
which should be um equivalent right and
here um we observed that for C1 uh there
was no witness that was generated uh
whereas for C2 there was so this again
is um a bar somewhere in this uh
pipeline
and yeah now that You' kind of hopefully
got an overview of the of the tool and
saw a bit how these bugs look like in
practice um I hope more people will you
know uh uh start looking into this
problem uh because I think it's a it's a
very important problem uh we need to
really make sure that these components
are uh bulletproof uh because otherwise
you know pretty bad things can happen
and it's better to do this before the
some you know attacker does it right um
and you don't need to be a cryptographer
to actually find these bugs so you know
that makes um gives us a lot more um
people that can actually uh look into
this um because I think so far we only
really scratch the surface so there's
more more things that need to be done to
to test these components also there's
components like this popping up um uh
every now and then so we really need to
uh make sure they're safe and we also
should do um continuous fuzzing of all
these components so for the gnark team
we actually implemented a continuous
fuzzing setup where you know they when
they whenever they commit the latest
version to master uh we we start a new
fuzzing campaign uh we run for 24 hours
we tell them if something is wrong and
then the next day same thing happens um
we're also planning to do the same for
cors and if you're interested in um you
know us uh taking a look at your uh ZK
infrastructure uh please reach
out and if you want to know more about
uh what's going on in the fuzzer then
please just check out our paper uh you
can scan the QR code there um and if you
you know want to let take a
look um
yeah fantastic thank you Val Valentine
for this presentation um let's get to
the question shall we yeah all right so
I've sorted the questions again you have
a QR code here you can ask your
questions and I'll ask the ones that are
the most voted so let's get to the first
one when you identify a bug can you just
say hey there's a bug or do you provide
a path to fix it like do you identify
where the bug exist within the circuit
uh we don't directly identify where the
bug is but when we generate the the test
inputs like the circuits uh we try to
minimize them so we try to keep them as
small as possible so the developers can
really hopefully quite easily identify
where things go wrong um and yeah so far
I think the complaint the the the
developers very very happy with the bugs
reported um and I think there was no
issues finding the the bug once they had
the the input makes sense thank you
second question do you fuzz logical
Expressions they're encoding in
circuits uh yeah we do I think yeah so
for instance we apply some you know some
common uh Transformations like applying
the Morgan's Rule and so on um so
there's a bunch of um these
Transformations that we that we use in
the fuzer
wonderful
third where is the bug Nest where do
bugs usually reside in your historical
fuzing like from what you've seen um I
think it's it's hard to like can you
read derive U enough data from you found
17 yeah yeah I think it's yeah it's
probably too early to say but we did
observe that um the fer found bugs
basically in um different components so
we found bugs in the compilers we found
bugs in the witness generator we found
bugs in the approver as well I don't
think we found bugs in the verifier
seems like yeah that's kind of towards
the end of the pipeline uh and I think
many people are are you know very
concerned about the you know getting the
verifier right so maybe that's also
paying off uh here um but we'll we'll
keep trying um we'll yeah we'll see nice
um okay when Kyo
fuzzing um yeah we're I guess you insert
it in your slide if we're interested
people talk to
you somebody from starware wants to you
know uh us to look at more at CYO then
yeah please please reach out um we're
interested um it's definitely a a good
idea to to do that yeah wonderful well
I'll reach out um what do you think of
concolic testing of Z
circuits um I had to ask chat GPT what
concolic testing is okay and I still
don't understand it okay um yeah so
concolic testing um essentially I mean
for the audience maybe it's essentially
a way to you know generate um new inputs
by doing some kind of symbolic execution
uh but basically for some Expressions
that might be really complex like you
have non nonlinear expressions in these
circuits so there you might want to uh
concretize some inputs um and that's a
con concolic part so it's like concrete
and symbolic um but yeah so the I think
that's that's an interesting area it's
not sort of what we focused on uh
because we we're not so much interested
in actually ating inputs for these uh
circuits um that's something you would
probably want to do if you want to have
a specific circuit that you want to you
know get right and you want to make sure
it h satisfies some properties then you
probably should think about you know
concolic testing for that circuit um
yeah perfect thank you how does it feel
to find a bug it like literally when you
find one is it is it scary is it
exciting I mean you're looking for those
so it's probably a bit exciting but it's
also SEC there's probably money on the
line how does it feel no it's definitely
I mean it's definitely exciting um and I
work a lot with students um and you know
it it really you know they you can see
they're they're excited when they find a
bark uh they're happy they're making you
know an impact um and also the reactions
from the developers are a great
motivation to find more bugs because
usually they're very um yeah they have
been very positive I don't believe you
there there's no way you go to people
and say Yeah I broke your and
they're like oh yeah
amazing yeah I mean if if if you're sort
of yeah if
you're um yeah L2 and one bug like this
can you know wreck your system then yeah
in some sense your your job is also on
the line so you should you want to find
those bugs I'm not saying you don't want
to it's just scary when I think about
bugs I think like yes I want to fix them
the first thing that comes to mind is
like oh yes no
but you're right it's better to be aware
of FR than not okay we can actually take
the last oh one seconds left let's wrap
it up or do you want to are you using
property based testing for choosing the
input um we're I mean you can call it
property based testing but we're
generating the inputs right now uh
completely randomly so it's kind of
blackbox fuzzing that we're doing and
we're also considering to do more you
know feedback directed fuzzing like you
saw in the last talk um yeah fantastic
thank you thank you Valentine thank you