[Music]
yeah we're going to talk about data
um so to kind of like situate ourselves
a little bit in I have 60 slides you
can't go through 60 slides without
knowing why you're here because
otherwise you'll just like lose
attention and collect frogs so um zerp
thesis for Data Systems is that
essentially in like one sentence
programmable cryptography so zero Notch
proof FH officiation enables what we
call the universal data adapter which is
in some way like the touring machine
moment for data what I mean by the
touring machine moment is it's we think
we basically finally have an abstraction
that's powerful enough such that it's
not like a marginal Improvement it's
like an order of magnitude improvements
the same way electrical circuits
basically got turn into like extremely
powerful beasts when we figured out how
to program them and make them General it
was not like an improvement at the
physics level it was an improvement at
the mental model level so um another way
to say that is we think cryptography is
a way to get more out of data and most
people will tell you that cryptography
is a way to make data more private or
whatever I think that that's a great
side effect but deeper than that
cryptography is a way to get more out of
data essentially make data more
interoperable be able to get data out of
their silos reap more economical
benefits out of data and it's pretty
important because we live in a world
where the value of data keeps increasing
over time um one way we we like to put
it is we take data out of their data
prison today if you want your data to be
safe and secure it's useless uh you have
to like kind of like keep it for
yourself and and it applies equally for
like individuals who want to do self
custody but also for companies like why
keep your data on your Linux server if
you can put it in the one big database
you know because the one big database
will like give you more value out of
that so there's kind of like this push
and pull between people want to keep
their data kind of like away in some
sense in in in a secure environment but
that it's equivalent to a prison you
know you can't go screw with the inmates
but inmates are not useful to society um
and and another way yet to say that is
enables more interoperability in usage
of
data um so our goal is to create more
total valuee out of this and at the same
time enable a pragmatic route towards
data ownership in a world where data
keeps increasing in value because if
data keeps increasing in value the
burden of proof for going through that
route keeps increasing okay so this is
kind of like the tldr on the data stack
we have so far far um we have pods which
are essentially specially issued packets
of cryptographic data almost like a
record in a database we have these
cryptographic machines called gpcs that
ingest pods and make claims about them
using zero knowledge proof and the
really interesting thing with this
system is it's performant enough to run
on mobile browsers uh while being
flexible and it's close to being
production ready and all of you guys are
using it uh Zupas where your tickets are
and your frogs are are is running on
pods and gpcs so as an example def
ticket is a pod a frog is a pod I use
GPC to log in into the telegram group
where you had to prove you had a ticket
when you enter the Frog Zone downstair
you also make a GPC so this stuff just
works and there's a huge like not huge
but there's there's definitely a list of
like on top of that like third party
application that is built on top of this
system mostly from the zalu ecosystem so
here's the tldr the way it works is some
authority attests to some data and signs
it via an EDSA signature on the jobjob
curve this gives you a pod you take a
bunch of PODS you put them into a GPC
and you make a claim that is verifiable
and then you can get hand that over to a
verifier that's essentially how it works
um we'll go into the details so the
issuer basically calls this like pod.
sign method on a bunch of key value data
you get out of it this thing with a
signature that is on the content ID
we'll focus on the date of birth here
for the sake of the example then you
configure a GPC config which makes a
claim about the date of birth for this
example here it's not revealed and we
prove that it's between a minimum and a
maximum and finally a verifier receives
the artifact from the proof and can
verify that claim and a really cool
thing is you don't need any new zero
knowledge circuits it's pretty flexible
and also extremely performant right so
we have this system we've been working
on it for a year um and you can go check
it out tomorrow uh at classroom B at
2:30 p.m. um but last summer we wanted
more out of our system like this is
pretty sweet but we think this is far
from being the best we can do so if we
look back at this Paradigm I just showed
you um there's a bunch of limitations
the first one is we need specially
issued data what this means is we need
to convince data testers to like change
the way they issue data which is not
very pragmatic it's limited to one round
of computation you can take pods put a
GPC on top but what you get out of is
not another pod it's like this thing
that you can't keep Computing over and
finally it's very much limited to single
player use cases what I mean is when you
create this GPC proof you actually need
to know all the input pods which means
that if you try to do it together with
multiple people one person will know all
the inputs so this is not compatible
with the world we're in today if we're
pragmatic about deploying this Beyond
you know things like zalu Defcon Etc um
first there's a lot of cryptographic
data yet it's very heterogeneous um
stuff that comes out of trusted
execution environment blockchains email
transport layer Security National ID
systems Etc all of this is cryptographic
but it follows different schemas
different signature schemes Etc um basic
use cases often require more than two
rounds of transformation like you want
to transform your data multiple time
across multiple people and we think that
there's a whole world that might open up
if it's actually possible to go more
than two rounds if you think about the
internet today we we never have like
platforms that go more than two levels
deep you know it's like we're building
on on top of mud huts and we dream of
skyscrapers we don't really know what's
going to happen if we can go deeper than
that um there is a lot of work on domain
specific system uh from the cryptography
perspective but yet there is absolutely
no interoperability over the last 18
months none of the ZK ID systems
actually work with each other you know
so it's pretty interesting like why and
from the programable cryptography
perspective the unlock of zero n proof
is trustless refactoring and import
right that's that's the right way to
think about it not as like a way to hide
data in my opinion um and you can use it
to now create a universal system for
making Claim about the world's data and
the unlock of um fully homomorphic
encryption or coar NPCs now you can
combine that data confidentially so we
want to put together a system that makes
you of these Primitives and is like
situated in a world like this without
being wishful thinking about like oh no
the whole world is going to like issue
pods with EDSA JJ signature whatever
like that's not going to happen so um
what we want is we want verifiable and
interoperable computational graph so we
want to import data as think it's about
emails API calls this is like a mobile
driver license from the state of
California we want to turn that into
pods we want to compute an arbitrary
depth with an arbitrary number of
participants on this data and find want
to export a view of this data to a
verifier that can check the Integrity of
all the computational graph and the
Integrity of all the Imports VI like a
single succinct proof right that's where
we want to get to and so that that's
putting it together again the goal for a
second version of the stack is we want
to be able to introduce anything
trustless Le and the reason trustless is
important it's not because we think that
oh like you're going to be censored when
you like import your like RuneScape
character or something like that it's
more like if it's trustless it's
scalable because any computer can do it
as opposed to having like some
bottleneck in the system somewhere we
want deep computational graphs because
actually today we've never really seen
what would happen if many parties were
to be able to operate on a piece of data
and kind of like pass it along right
most of the time you have data that gets
ingested by one big group of people and
then it gets consumed and that's it um
and we also want to do it between
multiple people while maintaining
confidentiality because we think this is
how you can tap into much bigger
economic output okay so the first
challenge we had when we faced this
which I think not many people have
thought about this is probably the most
interesting challenge is program
composability so imagine you have a list
of friends um it's probably like a list
of PODS that if you receive like each of
your friends sign something saying
they're your friend you can put in a
program here it's some Rust but anyone
can read this which counts the amount of
best friend you have best friend is just
like a a property of friend and you get
out 13 now you take this and you put
into another function that says hey do
you have a great friend groups which
counts how many best friend you have
here just can't say is it bigger or
equal than three and you get a bullan
true or false okay seems simple enough
here's how it looks like more abstractly
you have some parts that go into program
a gets a part out go into program B get
a part out okay so assuming we can do
this cryptographically what problem
remains well the main issue is if you
have a program that operates over the
output of a different program you need
program B to understand program a right
either via static analysis either via
vmer proofs but program B needs to know
what program a does so unless you write
program B after having written program a
and kind of like hardcode the link
between them it's really hard for a
program to make sense of the output of
another program if I tell you 42 and I
tell you how it was computed it's really
hard for you to know even what the
significance of that output is we don't
really think like that most of the time
like when people say oh we'll have ZK
VMS and we can solve everything the main
issue is that yeah good luck now doing
static analysis and kind of like trying
to make sense of other programs and at
the end of the day it reduces to the
holding problem so what we did is we
threw away the CPU model and we went to
logic um and we threw away the codes and
we move to logical operation so instead
of a virtual machine built on risk five
or something like that we build a logic
virtual machine we replaced memory slots
with logical statements so statements
like a is greater than b or there exists
C such that c is part of D we replace up
code with logical operation so as an
example a is smaller than b implies a is
not equal b or if you have a defined as
10 and B defined as 10 you can derive a
equals B all of these are like B basic
logical operations uh data becomes
theorems uh programs become proofs
uh not the kind of proofs that you know
about if you're a cryptographer a
different kind of proofs now we're going
to mix all the words together um it's
like a pretty interesting way to look at
the system essentially what we have is
data that gets imported our axioms
they're combined into a logic like
through logic proof they get combined
into a theorem and then more theorems
can build theorems right so the
interesting thing with that is all of
mathematics is already built on that
principle which is every time we prove
something we can prove more out of it
and we don't need to understand what has
been done so far like mathematics is
truly inter operable in a way that
programs are not um so if we get back to
this example you know after we've
counted how many best friends you have
and want to know whether you have a
great friend group what this turns into
is you have a theorem and through
another logic proof you get yet another
theorem in plain English you would have
theorem blue I have 12 best friends uh
implies theorem green I have more than
three best friends makes sense right um
so now we have two kinds of proof in the
system we have a formal proof and we
have a zero knowledge proof the Z proof
is used to show that the formal proof
was computed correctly and hide some
inputs about it right you want to be
able to say I have more than three
friends without showing who your friends
are right so um and you can you can kind
of like go arbitrarily deep here you
have theorems you make proofs out of
that you get a new theorem you combine
that with a previous theorem maybe for
someone else to make more theorem and so
forth here's how it looks like in a very
early version of our system so these are
statements these are the actual things
that are inside a pod so the most basic
statement is the value of statement
which is that the value of an entry is
this like the value of is best friend is
true in the specific pod this is how
most people think of cryptographic data
they just have the value of statement
they don't have anything else but then
we added a bunch of other stuff like the
equal statement which is this entry is
equals that entry uh or the sum of
statement which says that the sum of the
two um the entry number two and three in
the two pole equals entry number one and
this is like a very early version that
we had but you can imagine extending
this to something that is powerful
enough to essentially prove anything in
first or second order logic um and these
are our up codes as an example we have
the equality from entries up code which
says hey if you have entry one and entry
two you can apply the equality from
entries OB code only if entry 1 equals
entry two to get a statement that says
entry 1 equals entry two uh so what what
we had to do from a cryptography
perspective is essentially build a
circuit that instead of proving the
state transition of a CPR architecture
proves The Logical operations on
statement is done correctly right it's a
cryptographically verified theorem
prover if you want okay so the Second
Challenge we have is um we want to be
able to import data from The Real World
because we don't expect people changing
the way they issue data it was already
sufficiently hard to get them to export
cryptographic data in the first place
good luck coming back to them and
telling them they did it the wrong way
so what this turns into is you want to
be able to turn any verifiable piece of
data into a set of value of statement
with special metadata as an example who
signed it what was the URL if it comes
from like a web proof when was it signed
Etc right and then you can further
combine these into any other pod using
the logic um so what if I want to
compute with one of my frog right you
guys have frogs I hope you have frogs if
you don't have frogs you're a loser you
need to go get frogs um frogs are pod
ones pod ones as I was showing earlier
was the first version of our
cryptographic uh data system from the
perspective of pod two they're foreign
cryptographic objects they're on
different curves with different signing
algorithms they're merized in in a
different way yet they can be imported
via what we call an introduction Gadget
so you have this introduction Gadget
that is going to going to verify the
EDSA Sig is correct it's going to store
the signer into a value of statement
with key undor signer and it's going to
copy each of the Pod one entry into a
value of statement and then you get a
pod and the cool thing is now you can
take two frogs you can introduce them
and then you can make a proof about them
you can say uh Tod is more beautiful
that the ma mustache toad that's
something you can prove with the system
after you have introduced the data um
and the first thing we want to do is be
able to import emails um we want to be
able to import like regular API calls
and and probably deal with one of the
the the government issued ID system uh
but then over time you can imagine
importing things from ethereum importing
things from Virtual Worlds importing
bank accounts receipts or even like
actual mathematical proofs and keeping
generating statement about these Okay
the third challenge we had is making
building easy um this is what it looks
like to put together a sequence of
logical up codes and it's extremely
gnarly don't ask us why why we have
strings it should be pointers um it's a
whole story um and making sense of pods
or crafting them becomes very tedious
and easy to get wrong right the users of
the system need to craft a sequence of
logical up code to make a new pods but
on top of that they need to make sure
that the statements they get out when
they receive a pod actually match what
they're asking to be proven if you get
this you know all of these logical
statements like how do like it's hard to
know whether this actually proves that
the person matches the claim you're
trying to like verify so what we did is
we put together a a little lisp it's a
logic programming language to create
pods and verify them uh it's a list
because it's really easy to write a list
versus other kinds of programming
languages and it has an interactive
development Loop um here's what it looks
like so here I'm just making a pod
technically this is an introduction
Gadget because I'm making data out of
nowhere so I I say hey key AG is 26 zip
code is such ID is such and what I get
is a bunch of value off statements
including a magic one you know the
underscore signer one which ones to who
created it and then I can make more pods
out of it so let's go through an example
here I'm going to make a pod that says I
have both an ID card and a payub where
the user ID is the same on both and my
age is over 18 and uh I think that's
about it and I reveal my salary right so
first what I'll do is I'll query for a
pod using the Pod question mark
statement saying I want a pod that has
an age value a zip code value and an ID
value and I don't I don't care about
anything else and I bind them to these
variables then I do the same thing for
another part that has a salary a Time
stem issue in an ID and I'm going to
reveal zip code salary time stem issued
by with the same key name and I'm going
to make some assertions that ages over
18 and then I do a drawing I say ID card
ID and P tub ID are the same the cool
thing is I'm going to able to to prove
that ID cord ID and ptop ID are the same
without revealing the ID that's the
thing that's very powerful about it what
I get out is a bunch of statements and
um you kind of have to trust me on this
because it's small enough but the ID is
not revealed in the Pod itself the
fourth challenge we had is multiparty
POD creation so today if you're on the
right side like the little Smiley guy
there the red pods are private right you
only see what's in the yellow pod
but if you're the person on the left and
you're putting the proof together you
actually leak you get leaked the the
input pods so what we want to be able to
do is ENT put a box around proof
calculation I'm I'm talking about the
formal proof not the Z proof such that
the input pots are not leaked across the
party right and um we were hoping to get
a demo of this by defon but of course um
it did not happen the rest happened but
not that um so the way you solve this is
you execute logical operation into
either multiparty fhe or or something
like verifiable Garb build circuit or or
coark um in order to do this you also
need to crack verifiable fully
homomorphic encryption without
multiplicative overhead which is tricky
I won't talk too much about this but if
you're interested come to the
programmable cryptography Cs on Friday
so that spot two it's a system that can
import data um that is cryptographic
regardless where it comes from enables
deep computational graphs and then you
can you can export whatever view you
want on the data with a six proof to a
verifier um it's logic based both for
its claim its operation um and has a
bunch of cool features it's in active
development right now we hope we'll have
a production ready version by end of 25
and we'll probably go through a bunch of
pilot throughout the year if you're
interested to learn more about it uh so
first if you're interested in pod one
which you can use right now to build
stuff it's tomorrow at classroom B at
2:30 pm and if you're interested in part
two and PEX we're running a pretty long
and interesting uh workshop on Friday at
12:30 p.m. at the programmable
cryptography CLS so I'll keep the the C
codes up for a little bit
um and then I'll be done so thanks
[Applause]
guys thank you so much Justin and we
have a ton of questions so looking
through the questions and start
answering them we have 3
minutes oh so you're not going to read
the question I have to do the work okay
cool all right uh you mentioned first
order logic also second order those are
not computable Logics they're just
computable and numerable what am I
missing then your Computing for sure
this this is true so our logic so far is
a bastard logic it's a logic that is not
actually the kind of logic that
logicians use so an active area of
research is figuring out how do we
essentially like have a logical system
that is also computable in a way that is
like as sound and complete as possible
and um if you have asked that question
please come talk to me because we're
very interested in that so great
question running this is the browser
means you need to trust the server to
serve a non-compromised version of the
software uh how will this work in
practice are we going to have an open
ster for pod processing um okay so if we
go down to the level of like well you
have to trust the software you use I
have a bad news for you which is it's a
problem for all of the industry so far
so the way you'll solve this is the way
you'll solve everything else so I don't
think I want to answer this
question what's
next can you scroll or
something no they'll scroll it from
there I got there late what is this for
um it's for making data useful Beyond
this stuff that we have right now where
we just store them in databases and we
sell them to open
AI okay I think that's it thank you all
right thank you so much Justin for this
session