ZK12: Zero-Knowledge Location Privacy via Accurate Floating-Point SNARKs - Jens Ernstberger

Transcript

[Music] cool great um yeah thank you so much uh today I'm going to present a recent work um which is called zero knowledge location privacy via accurate floating Point snarks um this is Joint work with changu Luca Philip who's also in the audience um and Sebastian um and this work uh was actually accepted next year as at S&P so uh very happy to present it already here at CK Summit great um so to kick off a little bit with motivation um what we have these days is a lot of location based

services so for example probably everybody that is in this room has something similar to tile or Aerotech enabled or uses uh their smartphone in some kind of like uh geolocation enhanced um uh way um which means that the the location data that you uh kind of um uh present of yourself every single day is used either in open source data sets uh such as for example on the right you can see open cell ID which is uh essentially mapping uh the wireless data coverage uh on a map based on uh voluntarily submitted um uh GPS data as well as kind of like measurement data or an open street map which some of you

might also be familiar with Sim similarly it's also used for spatial data processing uh for example Uber uses it to plan their rides uh Airbnb uses it uh to recommend prices uh and there's also um marketplaces to sell geospatial data so as you can see there's a lot of demand for geospatial data uh on the other hand this is also problematic um because frequently there is uh data preaches and uh privacy enhancement or obfuscation of data set is not not always enough right so in4 14 there was for example this uh uh very interesting data leak um where a supposedly anonymized data set for taxi data so rides historical rides uh with kind of

like destinations and Origins as well as ride fars uh were revealed um uh essentially they used an md5 hash of uh the identification number of the uh of the taxi um uh which was easily uh reversed in uh around 3 minutes per record um and which then revealed uh by mapping it or the the data of the the the identification number of the taxi with paparazzi photos uh to reveal which celebrity visited which script club or gave no tip at all right so this is a serious concern so the um uh the actual question that this raises is can we

actually develop an mechanism that provides location obfuscation um very strong obfuscation Loc location ofation without without ever disclosing the the actual location in the first place right so ideally we would like like to have a non interactive proof that proves that I'm in a certain location uh where the input is the latitude and longitude and the output is something else that kind of like off skates this location um so what would be good here um so our idea was uh there's uh a lot of algorithms already that do geometric mapping uh onto the sphere of the Earth for example um The Uber H3 algorithm uh which is a hexagonal geospatial index um

hexagons have established themselves to be very useful in this use case um as they have a very good uh Symmetry and equidistance centers uh which allows for uh uh an ease of uh performing certain calculations um such as for example R fars uh in the Uber case and Uber has this interesting software Library um where you have an index that is assigned uh to each of the hexagons and you have a varying resolution right so uh you essentially have a mapping of the hexagons of the of the round sphere of the earth um and the hexagons can be scaled from like one square meter to around 4 million square kilm right um

which makes this very interesting as it uh allows for variable privacy in the protocol that we're trying to design here as well good um now the next question is if we have this point um uh as a latitude and longitude latitude and longitude uh are usually uh numbers that are separated by coma so they can either be represented as fixed point or floating Point uh numbers the question is what happens if we get to the boundary of a specific hexagon especially with very very high resolution or very kind of like which which is equivalent to a very small hexagon um the problem here becomes that if you're very close to a boundary and

you don't have sufficient accuracy you end up basically proving that you're in the boundary NE in the in the hexagon next to it which which is equivalent to soundness error right um so this is basically the the motivation why we also want to uh do floating Point computation so we want to uh have represent latitude and longitude in circuits um as floating Point numbers um and do computations on them to prove that you're basically in a certain hexagon so this is uh essentially the the problem setting um here on the bottom you can also see uh this is the experiment that you will see later in the evaluation uh so red is for example the number is is the uh point that we

want to prove uh in our experiment we logarithmically approach the boundary uh of the actual hexagon uh and then on top we design an application which we call peer-to-peer proximity tracing um where you have another member which is PU in this case and pu can calculate the minimal distance to the boundary the closest point on the boundary of the hexagon in plane and the total number um uh the total the total run time that you have for you in this case is the verification of the proof and the computation um on the boundary in plane um yeah great uh so quick show of hands how many people here uh know about floating point and know about the actual

representation of floating Point great roughly a little bit more than half it was more than the last time when I asked 513 great um good so let me give you a brief overview of this um a floating Point number is usually represented as a c as a sequence of bits um where you have always one sign bit which indicates if you have a positive or A negative number um you have an exponent e e is for um single Precision floating Point 8 for double Precision floating Point 11 and you have a mantisa m which is 23 for single Precision floating point and 52

for double Precision floting Point um and what you see on the bottom here the alpha is the actual real uh the representation of the real number once you take all those bits and assign them basically uh to the values that you have so you can can see the exponents determines the range of the number um and the mantisa essentially the the Precision Precision after after the comma um and the sign bit should be self-explanatory right good um so why is in this case fix Point uh uh less than floating point or floating Point better than fix Point um I can make like a very rough comparison here so if you have a fixo number with 16 bits on the

whole um uh number and 16 bets on the fractional side as you can see see here in the example which encodes 45.16% that are a lot smaller and a lot larger at the same time which is fairly beneficial right and this encodes in this case the same number but you only have uh half the number uh of bits assigned uh as you would need for the uh

fix Point case um and some of these things can also lead to very uh detrimental effects uh if you use numbers of uh uh Precision there is that is not high enough this can lead to arithmetic errors such as in this case with the Ariana Rockets uh in I think it was the' 70s um where casting an integer um uh no casting a floating point value of 64 bits to an integer unsigned integer of 16 bits uh led to an exception and led to the rocket explode which was very expensive um yeah so we ideally want to avoid that um so let me tell you uh how floating Point arithmetic actually works and then

successively tell you how we actually encode this in circuit okay so here you can see essentially uh addition subtraction multiplication and division so for addition what you do is you have Alpha and beta are two two real numbers right um so you take for addition you take the maximum um of uh the exponent uh and then you have the mantisa for the mantissa you add or subtract the mantisa if you do want to want to do uh addition or subtraction similarly for for uh multiplication what you do is you add the exponents multiply the Manas um similarly for division you subtract the exponents and then divide the Manas um after that um if you you need

to normalize right so this is the normal step that you need to do if the mantisa is too small so you have an underflow you shift left and you decrement e so the exponent if the mantisa is too large you shift right and increment e because you always want to have a leading uh one bit um for normalization purposes the next thing that you need need to do if you do for example multiplication or something you need to do rounding um so uh if you multiply for example to mantisa you end up with a number that is uh with with a sequence of bits that is longer than what you actually can represent so you need to map that back to the to the initial length uh of the of the floating Point number that you can represent so you need to apply some kind of rounding um

in I e754 which is the floating Point standard this works with something called uh the parity bids the guard bids the round bits as well as the sticky bits so if you're in single Precision floating Point um everything until the up until the parity bit uh would be 32 bits actually 23 because this is only the mantisa um then everything after your the first bit after is the guard bit the second bit is the round bit and the rest of them are the sticky bit uh this uh is are the sticky bits the sticky bit itself is a logical or of all the bits that come after the round bits and then what you see on the bottom is the actual kind of like round that you need to do right so this uh uh Boolean formula determines in which direction

you round and the rounding rule that is the most common in 99.9% of the cases is round to nearest ties to even which means you round to the nearest number and if you have a tie so if you have for example 2.5 you round to the nearest even number which in this case would be two um right and then the last case that you need to do is you need to handle the edge cases um so if you you have to multiplication uh uh or you have Division and you want to divide by zero that also needs to be handled uh in your floating Point representation so we also need to handle that uh in circuit so to give you a quick overview of how this actually looks like and to make it a little bit more intuitive uh

of the actual representation of numbers that you can do you can represent zeros which is basically the all zeros Vector of exponent as well as mantisa um you can represent subnormal numbers which is when the exponent is zero and uh the mantisa is something that is not zero you can represent normal numbers uh which are in the range 1 to 2 to the^ of e minus 2 where the exponent uh is everything but zero all zeros or all ones uh and the mantisa is anything from uh from one to all ones uh and then you can also represent infinites uh and not a numbers infinites and other numbers are reserved um where the exponent is all ones uh the mantisa is zero or the Mena is something that is

not zero for not a number okay so now that you know what you have to do in arithmetic if you want to do a multiplication um which is essentially the operations on exponent mantisa normalization rounding uh as well as handling the edge cases and you know the representation of the numbers uh let's talk about how to actually encode this uh in circuit and is there a knowledge proof good uh so there's essentially two potential ways you can do this um uh I assume that most of you are familiar with the with the kind of design Spectrum here um uh you either can do it with tailor circuits so you really design the arithmetic circuit um and then take it from there or you use

universal circuit and Universal circuits uh in a zero knowledge uh virtual machine and support basically the instruction sets uh that you need for to support floating Point numbers which in for risk 5 would be something that is called the F extension right in this work we work over tailored circuits um so on the bottom left you can see the general way of how you encode an uh encoder circuit uh so you compile to the constraint system you have the backend backend handle setup uh Pro and verifier and then you do the witness generation what we're going to talk about in this talk mainly is just like how to set up uh the the circuit that then compiles through constraint system to minimize the number number of constraints

right good um so given that we're operating in the um uh circuit optimization framework there's certain tools of optimization for optimization that are known and that we can use what we use in this work mainly are one non non-deterministic advice uh or something that is also called a hint um as well as lookup arguments so just briefly uh for you to know what is non-deterministic advice um non-deterministic advice this is very simply U exemplified at the case of the square root example if you want to compute a square root in circuits what you would naively do is you take an algorithm that already exists to compare

compare the square root right um in uh literature this is Newton's algorithm um which is basically an iterative algorithm that approaches the square root of a certain number now if you want to do this in an arithmetic circuit such as shown on the right uh this blows up the arithmetic circuit and the number of constraints because you basically need to flatten the whole Loop that you're trying to do in approaching the actual number of the square root so what can a what can a hint do uh in a hint what you can do is you can you can provide the results right the square root itself um and the actual input so X in this case and then you just do one multiplication you multiply the square root with with itself and check that it's equivalent to the other input that you give um which

basically ensures that you that that that you have the square roots um of that number that you're trying to give the square root of um good that is one optimization the other optimization is lookup arguments um for lookup arguments you essentially have a table uh and a set of querries uh and what you want to do is you want to ensure that the CES are in the table how get how can that help uh for example if you want to do a constant size uh range check range check such as 0 to 2 to the power V you could either do in circuit uh decomposition of bits or you provide the bits in this case v0 to whatever uh however many bits long uh the actual value is you provide

that as a hint and then you enforce that uh the bits appended to each other are equivalent to the actual number and uh all the bits are in the lookup table good so these are the optimizations that we use um uh that are in general applicable to any kind of uh circuit that you have um now additionally we adapt the representation of floating Point numbers uh such that we can handle them in circuit more efficiently so as you heard before you need to treat uh subnormal and normal numbers differently uh what we do is we let the exponent essentially underflow um by shifting uh the mantisa dbits to the left until we have a leading implicit

one um and subtracting that from the exponent um uh we expand normal numbers uh to simplify computations by taking the implicit one bit and making it explicit and oper op ating over an unbiased exponent so we also don't have to handle the bias so for every number that goes into the circuit uh we uh represent it in unbiased form um and for nans uh we do do not uh treat them separately but we actually unify them um by making the um uh mantisa all zeros in our computations um right so let me show you how this actually looks if you actually so this

is the circuit for multiplication um uh that you actually do in in uh in the zero knowledge floating Point implementation what you simply do is you add the exponents um you multiply them and tia in this case because we have subnormal and normal numbers uh unified we need to account for that right because because we did that in the previous step in a different representation we also need to ensure that the result is in the correct number range so uh What uh so we have the mantisa is always in the range 2 to the^ 2 m uh to 2 to^ 2 m + 2 as uh the matisa of Alpha and matisa of beta is in the range 2^ of M 2^ of m

+ 1 um if we now want to normalize uh what we can do is we can uh only check basically whether the most significant bit so the 2 M plus one bit of M um uh is zero or one so um M always either has 2 m or 2 M plus one bits so you do not shift left so you do not normalize because it's already normalized if the most sign most significant bit is zero and you left shift by one if the most signant most significant bit is one um yeah so we use for example the hint here uh as well as range checks um uh and we need to enforce of course that the bit that we provide is actually

binary um uh and also enforce the correct range um yeah and then additionally we need to do rounding uh for for the mantisa to cut it into the right range in this case either single single Precision or double Precision floating Point um and handle the edge cases accordingly yeah cool uh so this was a very brief overview of how this actually looks in circuits um uh talking about everything would be a huge blowup of everything um and uh uh yeah so there's a lot more things to do um uh you need to do the adapted rounding to also account for subnormal is normal by treating them in a unified fashion in the circuits um you

need to uh do um the implementation of optimized integer operations so you need absolute values maximum and minimum values as well as left shift and right shift which are very important because you uh shift basically all the time the mantisa um and you also need to do the rest of the floating Point operations right now what you saw was only the multiplication um uh so you also need to do addition subtraction multiplication division square roots and the edge cases good so now we can handle the actual applications um so projecting onto a sphere uh here you can see the algorithm that we extracted from the Uber software implementation essentially what you do uh you see uh this is the Baseline algorithm um you have a Latitude a

longitude and a resolution and what comes out is the JK coordinates uh I'm not going to go into what is the actual transformation um but you'll see what the problem here is in a second so in each of these steps you have trigonometric Transformations right so you need to apply sign cosine uh extensively in a number of these steps uh which again is very very expensive because these are iterative appro approximations right um so ideally we want to get rid of them um so we want to optimize the circuits what you can see here is the optimized circuit that does not have a single trigonometric relation so we do not need s cosine or tan at all uh what do we do is basically we use hints in kind of

like a fashion that makes it uh that enables us to compute the right numbers only by applying a square roots um and then successively we uh use standard trigonometric relations that probably everyone here has learned in uh their high school education to essentially um uh represent uh every calculation in a non-t trigonometric way um yeah so as you can see here on the left is the unoptimized uh uh uh implementation uh and on the right is the optimized implementation uh that has basically been um uh yeah optimized with trigonometric identities to get rid of all of the uh trigonometric relations

what you can see on the right uh wherever there's a trigonometric relation still that is basically a constant um yeah okay so how can we ensure that everything is correct uh in the beginning I talked about the resolution and approaching approaching the the boundary of the hexagon in a log in a logarithmic fashion which you can see here every uh resolution 11 12 13 14 and 15 um uh has um basically uh around like 10 test cases and each uh resol each each hexagon 11 12 13 14 and 15 is always kind of like decreasing in size you can see for for P6 which is a fix point

implementation you have a lot of errors and for single Precision uh as well as double Precision uh you're basically uh fine besides like 415 for the floating Point implementation uh we ensure that everything is correct by testing it with the Berkeley test float implementation um uh so in this case we achieve equivalence with the i e standard how costly is all of this actually um so we have two parts native constraints and lookup constraints on the bottom left you see the equation that you need to check for the lookup look lookup con constraints um the good thing here is uh on the right hand side so you need to do three three things calculate the left hand side check the

equality and calculate the right hand side um the second and third are actually constant um so this amortizes the more multiplications floating Point mul multiplications you actually have in your circuit right so um to briefly give you a gist of the rights um what we have for example for fp32 which is single Precision floating Point implementation uh you get down to 64 um uh constraints uh per single multiplication as soon as you have around 2 to the^ of n um uh multiplications in your circuit right um for the evaluation of our application zero knowledge location

privacy I mentioned in the beginning um uh you want to calculate distance for uh um uh for peer-to-peer proximity testing as well for that we can Tex test the proximity proximity with a single proof uh up up to so yeah you receive like as a verifier 400 proofs and you can check all of them in like uh less than uh a second um and on the prover side uh we have a approver time of also less than a second and roughly 20,000 constraints for single Precision floating Point implementation um uh and roughly around 50 to 80,000 constraints for uh double Precision floating Point implementation yeah and yeah so

remaining challenge is still uh location authenticity as you might uh know uh or might have realized um there is no Assurance of the actual uh authenticity of the input latitude and longitude uh which is still problematic we think this is a very nice uh future research Direction where you can either figure out how to do it with satellites uh with TLS notary um or with some kind of like Hardware processing devices so tees um and we also think that this would be fun to do with IVC so you can do something like uh write share calculation across uh uh yeah a similar kind of like uber algorithm where you could apply incrementally verifiable computation um yeah and privacy

preserving validated Shield location is also very great cool um yeah uh now you can use floating Point arithmetic in your custom circuit um yeah happy to take any questions thank you all right we got one question we have time for one question um what do you estimate the amount of work that needs to be done to extend this floating Point Unit into any of the ZK VMS exist um I've actually worked a bit on this in the summer um uh and this is kind of like still upcoming work uh so

what you need to do is um uh you would need to figure out uh how to model basically um uh model the there's there's the um there's the uh F extension already right for for uh risk 5 um which is already implemented in plane so now you have to figure out uh I worked on this for jolt so we Tred to figure out how to represent this as multilinear extensions to use it with the lasso lookup argument right uh to make it amenal amenable to proving with Jolt similar to the base uh instruction set um uh which was basically the initial contribution of

jolt base instruction set uh plus M extension um uh yeah and the F extension would basically follow a similar Paradigm uh but if you want to have uh I e754 compliance uh you need to implement a lot of branching right and I think there's a lot of optimization here the question is do you need I e754 compliance for every single application I guess not so um yeah I think a lot of these applications could also benefit from cutting out cutting out a lot of constraints that are only relevant for edge cases right which are still used in in our implementation uh because we wanted to achieve that yeah thank you very much Jens thank you you