Squash All the Bugs with Omniscience & Formal Verification

Transcript

all right uh let's get started everybody thanks for joining uh I know this wasn't on the official agenda this was kind of a last minute Edition uh to the schedule today uh so my name is Magnus I'm head of product at block sense we're a programmable decentralized Oracle network uh but we also have a programming languages team uh within the company that's actually contributing to the Noir language uh and also building out some of the developer ecosystem around it some of the developer tooling full disclosure I'm playing substitute teacher today uh so you may have heard me say I'm head of product I'm not an engineer by trade and uh this was going to be our head of engineering stand

doing the presentation today uh but his flight isn't Landing till tonight luckily he's recorded some uh videos for us uh so I will be relying on those partially uh just so that you can get all of the technical information you might want um and we also have a telegram group set up uh so afterwards if you have any questions that I can't answer uh then uh you can you can join that group and uh our engineering team will be will be happy to assist uh but yeah so the title of today's Workshop is squash all the bugs with omniscience and formal verification uh so quick show of hands who here knows what an omniscient debugger is kind of okay formal ver verification

any familiarity with this more all right good so hopefully hopefully by the end of this half an hour to 40 minute Workshop you'll be a little more confident on both both Concepts uh so but just kind of as a as a primer so omniscient debuggers so the team has actually built out a a TR time traveling debugger and that's what omnicient refers to it's a class of debugger uh that records all the variable assignments in code uh and then is able to basically replicate um both forward and backwards what the what the code did uh and that's uh that's kind of like the big advantage of code Tracer which

is our debugger is you can actually go forwards and backwards in time and flawlessly uh yeah like replicate what happened but you can also share that with anyone kind of like sharing a URL and they can also see how the code was executed and anything that happened um and then formal verification I think like more people are probably familiar with this concept um it's essentially the practice of using mathematical methods to formally uh prove that a system works correctly under any kind of input that is permitted in that system uh and this is uh this is kind of uh it's been around for for quite some time and it's recently started to grow uh interaction more with a lot of adoption from the likes of

Microsoft um and we actually have extended Microsoft's open source framework called Varys for formal verification um but you can yeah you can think of formal verification as like a more sophisticated more advanced uh way of testing your code and uh this is especially useful for like Mission critical software uh things like it's it's quite widely used in the aviation industry uh and the rockets Industries uh because they're like even at 0.01% error rate is not tolerable um similarly if you think of all the billions of dollars that currently are and even more so that will be in the future secured by zero knowledge uh systems uh similarly like you cannot uh

you cannot tolerate any kind of incorrectness in the code but zero knowledge is kind of notoriously difficult a difficult field for people to grasp um and you shouldn't have to be a mathematician to be able to work with it securely and so that's kind of the the the thesis behind why we've we've gone ahead and uh and invested in formal verification of block sense um so there's actually studies that have been done recently uh that showed so Microsoft like I said uh developed various open source framework um they used it on on aour and found that it reduced uh the critical bugs by 30% more than just testing did it's actually like a lot more extensive but it didn't increase the development

time um so yeah it's it's kind of as I say like it's it's growing in traction these days and the real challeng Cheng is to make it like less uh less clunky and faster to work with and that's where sort of modular formal verification comes in where you don't try and improve an entire system but you can kind of like prove components at a time um so yeah with that uh just a quick background just to take a step back so uh as I mentioned briefly uh block sense is a Oracle Network so we uh we came out of uh a16 Z's accelerator crypto accelerator last fall and currently on 30 plus

EVMS um with the plan to be cross chain so uh we'll be on every chain uh hopefully by end of year um next coming is like svm the Mam and so on and uh what block sens does a little bit differently from other Oracle networks is uh it's actually secured off Shan so like the the consensus that runs block sense network uh is sec offchain uh using a kind of like a ZK rollup architecture um and so what happens is the block senses its own network and The Operators that run that network will vote on the result of different tasks so uh it could be price feeds for defi

lending and uh perpetuals protocols but it can also be any kind of arbitrary IO uh so inference AI inference or other kind of compute tasks essentially those get run through the network uh of operators and we reward the or the network rewards The Operators that vote with the majority and it slashes those that do not vote with majority and this way we're able to reach what's called a shelling point so like a natural kind of uh point of um agreement between players in a system that cannot communicate and the cannot communicate part is very important here right because uh you don't want your operators to be able to collude uh when they're when they're

voting on a result right so you could imagine a scenario where um all of us are operators and uh there's a a malicious actor who wants to bribe us into changing our our answer or we kind of like work together and uh if if that happens then obviously the network becomes very susceptible to an attack so this is where the ZK comes in we actually um we actually perform all of that computation off chain and then uh verify it on chain uh with ZK snarks and this way we're able to like uh keep the identities of The Operators and their votes completely Anonymous which then makes it much harder to to bribe uh the network so that's uh that's kind of like why we are

using ZK at block sense and in our journey we um actually been working with the Aztec team on Noir for over a year we started with uh building the front end and uh more recently contributed the plun key to um backend for Noir so Noir Noir ships with the backend proving system called barenburg plunet 2 of gained in prominence as a like a faster approving system more performant and uh so that's that's available in our Fork of Noir which we keep synced with uh with Upstream Noir and uh kind of from there uh we we noticed like you know some some room for improvement in different areas and this is where um the formal verification and

uh code tracer uh IDE F Noir came came to be uh so I'm going to stop uh yabbering about uh about things that I'm familiar with and I'm going to let the uh uh the video that my colleague uh our head of engineering stand put together uh do the talking now and uh give you some more um some more insight into uh formal verification how we do it uh with Noir block sense hello and welcome to this video about the nor compiling contributions that the block sense team have done over the past year so what you see on my screen is the noblock sense. Network website which summarizes all these contributions but I will actually be

showing you my local Bild because there's an extra section there that should be live by the time you watch this video we have three main contributions one is the Noir formal verification effort the Noir py2 back end and the Noir Tracer I'll start actually with the second one the nor pl2 backend because it also has instructions about how to build the software so if you open this page the No plony 2 back end there is some information about what is plony 2 and what is Noir and specifically what we built here is a compiler back end that translates nor programs into the plony 2 proving system so that people can benefit from that proving system rather than using the standard barenberg proving engine that comes with nor this is just an alternative we're not planning that it's

better or worse but we wanted to see how it would perform so this is why we built this in the started section you can see that Step Zero is to install some dependencies specifically you need the mix package manager and dur so the nextx package manager you can install with the official installation guide either a multiuser or single user installation should work on your machine and that should work for anything that is POS compliant including Mac OS once you have the package manager you need to also install durf or de f and that again has a standard way of installation and there are instructions for Mac OS a bunch of Linux

distributions and even windows but we have not really tested that don't forget that once you install their F you also need to hook it into your shell so follow these instructions but it should be as simply as adding it to your BH RC adding this line at the end and opening a new terminal once you're set up you can start following the instructions in our documentation so clone our for cu the more proing language and once it's done you can build it and test that it works so we have cloned the repo if I enter this directory I get the message that dur m is not enabled so if I say durf l from now on every time I enter this directory durf and the next package

manager will make sure that all the dependencies I need are installed for building the nor compiler once that's done you can skip these steps if you don't have further issues but now I should be able to just say cargo test ZK tension and in a few minutes that should compile the whole compiler and test our back end with an our program language the ZK dungeon program is something we've written that is very complex and tests various features of the language so now we see that the tests have passed and they include a few variations on this test that test not only the pl to back end but a few other

things as well but you don't need to worry about this as well the important thing is that now we know that the compiler is working so we can write our program ourselves let's use the nargo three which again is installed thanks to the and the nextx package manager and if you just say nargo new and the program name it's going to create a new project for you now we need to enter this directory and let's copy this in the text of the program so now this is just a program that asserts that we know a private divider of a public number if we run Nar check that should also generate our approver Tomo file

again these are features that came from Upstream Noir so nothing new here but we just show you that we use the same process as normal Noir when writing programs let's now see what the Prov T contains it contains empty inputs so let's replace those with the following inputs a big public number X and a smaller private number y that divides X so at this stage if we issue Naro proof that is going to trigger the blony to back end in Upstream Noir the Nar proof command was removed so there are extra steps needed to generate the proof and then verify it but we've brought it

back because we feel that this is more convenient we don't see any error messages this note here is something we've valed just as a reminder in development but because there are no error messages that means the Nar proof succeeded the last step is to run Naro verify so Naro verify is going to perform a verification the zero knowledge program that we just generated a proof for and again if there are no extra messages that means that the verification succeeded and the proof is actually stored in proofs by program proof and it contains a very big number if we remove this proof we can see that the proving of the program can also fail so let's

paste the same inputs but change the second number to something that does not divide the first number now I press control d by the way to stop cat now if I say now proove we can see an error mess which which says that we failed to assert this constraint so no proof was generated and if we try to Nar verify now there's actually nothing to verify so we're going to get another error message so this is how the plunky 2 back end for Mar can be used and you can head over to no if you don't know Noir learn more about it and see what progress you can prove with this and now I'm going to show you another project that we've been working

on and we call it formal verification this is a system that allows you to perform formal verification on an Noir program without actually generating appr Pro or running the program but by adding some annotations and analyzing those with our system so that you can prove certain properties of the program itself if you go to the section there is a introduction followed by a getting started page again so this page is standing to clone the repository and switch to the formal verification Branch but since we have already cloned the repository which is is going to be check out for more verification as you can see de M makes sure that the environment is configured so that you can build the system and if we go ahead and say Caro build that is

going to build the Noir compiler with formal verification capabilities added now that the system has built you can skip all these steps now for you depending on your system you might do some different things but as you saw we managed to build the system so now we can go ahead and run it so let's create a new project in the standard way and enter this directory if we now in addition to the main function write some attributes on top we can use normal Noir formal verification so what is this function it's a function that takes a number and divides it by five and return Returns the result so if we add an attribute that requires that the argument is greater than or equal to 100 the system

can prove that the result is going to be greater than or equal to 20 so let's try this I copy this text and and I paste it as the program text note that Pro Tomo does not exist because we're not going to use Narco proof but we're going to use Naro FV which is just going to use the annotations that we wrote to perform formal verification of the program and if we change the program so that we try to prove something that is wrong like as you just saw me right we now try to ensure that the result is greater than or equal to 21 trying to prove this is going to fail because we cannot actually Ensure this and similarly if we try to prove something that is more relaxed than the most tight condition we can prove this

is actually going to work because if the result is greater than or equal to 20 it's also going to be greater than or equal to 19 so this is just getting started with the project let's see what the other pages in the documentation tell us so there is a section of the specifications of the formal verification system and it talks about preconditions po post conditions and assertions so precondition the requires annotations that we saw so if we have this function for example without any annotations let's use this as the source of our program and see what happens if we try to verify this function so verifying it might sound strange at this moment because there is nothing that we actually try to ensure for this program

but still AR FV can be useful because in this case it finds out that there is a possible arithmetic overflow and this is because the type of our variables is i8 which means that if we add two of these variables this might lead to an overflow so that's what the system is warning us about so let's add precondition let's write this we require that X is actually between - 64 and plus 64 so that we can add it to itself and still get a number that is an I8 let's save this close the file Nal FB is still going to fail but on the second line because even though the first addition is fine X2 is now between -28 and plus 128 so if we add it

to itself that could lead to an overflow so we actually need to restrict X1 be between Min - 32 and plus 32 and now running this is going to succeed so we can verify this program and verify that there's no overflows in this case so let's rename this file and call it quadruple and let's have actually a separate main function which call scruple with a number like 40 because 40 is not in the boundaries minus 32 and 32 if we try to verify the program now the verification is going to fail on the call site so this precondition is actually not met so we cannot call this function with 40 let's

call it with 25 and see that now actually verification succeeds so this is how we use preconditions let's add some post conditions so that we can make the verification even more useful if we now write our program and try try to assume sorry try to assert that 10 is 100 if we multiply 25 by 4 we should get 100 so this assert should actually work but if we try to prove this program we get a message that we couldn't actually verify this assertion this is because we have not told the system what this function does it inspects the body of the function to make sure that the requirements are met and there's no overflows but then we actually need to manually say that this now ensures that the result is actually 4 * X1 as you can see

here with this additional annotation running Naro FV succeeds and we can prove that this program is formally valid the documentation talks further about modular verification which I encourage you to read and finally says that assert in our programs is translated to the assert in the smt Z3 solware that is used underneath to power all of this so that's why we could write an assert in our program and that takes part of the form proof that is performed if we continue with documentation it talks further about quantifiers this is a very interesting feature that we have implemented and it allows us to call Universal and existential quantifiers so we could

write the program like this what this program does is it says that if we require that each of the elements can array is a power of two then we can ensure that the result is a power of two if the result is the middle element we can write this in a different way actually let me show you that this works first of all verification succeeds so instead of writing this one by one it can be continuious if we have 10 or 100 elements we can actually use a universal quantifier and say that we require that for o i within some bounds that is power of two for R of I holds so this is another way to write the same program and we can see that it

still works and this would work even if we have 300 elements and 149th Elements which is the middle one kind of is returned by the function verification works for this as well and we then have to write 300 lines that requires here and finally there is a section about the existential quantifier which is saying that if we write our annotations in such a way that we require the first element and the last element are power of two but the middle one is not then we can ensures Clause that says there exists an index for which the result is a power of two so let's real quick try this example we can see that verification

succeeds here as well and we can also prove that there exists an for which it's not a power of two so the documentation continues with discussion about cost functions and the fact that we don't need them for Naro head because the language is simpler than other languages recursion and Loops again there's no recursion in Noir and Loops are bounded which makes our life easier so an example like this where we want to prove some property about a function that contains Loop Works without problem and we have some additional features here discussed in the documentation but I wanted to point out the specification syntax which describes completely about everything you can

write in these annotations and how you can use it and finally let's move to the Noir Tracer project Noir Tracer is a useful tool that we've built at the Block sence Network that allows you to record the execution of Noir program so that this execution can later be replayed in a specialized program and you can get insights about how the program behaved during the execution so the installation of this tool is the same as the installation of the Noir PL to back end it's on the same branch of our Fork of Noir so for that I'm going to just switch back to the block sense branch of our clone of the Noir compiler so now that's done I'm going to again create a

new program using the nargo new command so this is going to create a simple Loop program and if I navigate into it we can paste the following code for our program source code so what this program does is it takes a public input X and a private input Y and creates a new temporary variable Z that equals y and then multiplies Z by y three times at the end it asserts that this result divides X evenly we're going to run Naro check so that Pro Tomo is generated that can contain the inputs if we print the pro Tomo it is empty as expected so

let's populated with the following values we know that 4 the^ 4 is 256 and 256 divides 372 so if we run nargo proof that we succeed also Naro verify will succeed Etc we can do Naro execute Naro debug step through the program Etc however this page is about n Trace which is the new command we built if we run Nar Trace that is actually going to perform an execution of the program and record the effects of this execution so for that we need to have a directory

where we want to store the traces and then if you run n Trace with this directory we're going to have the traces saved in this directory this directory now traces will contain three files but it would not be very easy to read them now because they are minimized for size so there is no white space for this reason we created another command called nargo formats trace and if we pick the main Trace file which is trace. Json and we specify that we want the formatted Trace to be in formatt trace. Json now we can output this format its trace and it looks like this if we open it in an text editor we can have some highlighting and

we can see that the value of set actually here is the first first one it's four and then during the steps it is increased to 16 then later to 64 and then later to 256 and this is basically what narot Trace does again we use a specific format which is specified in this runtime tracing library and this format allows us to interface with another tool and actually a graphical user interface it's built by a partner company of ours and the tool is called cold Tracer it's a time traveling debugger and there's a lot to tell you about this as well but I'll stop this video all right so that was uh our planky 2 implementation and formal

verification um and we'll take some questions at the end but I know we're a little bit short on time so I want to jump to the next video this one's a lot shorter I promise you um and so at the end of the last video Stan teased uh about this Cod Tracer tool um and so the output from Trace is actually uh what Cod Tracer expects to be able to then do the time traveling uh time traveling debugging so uh let's look at how that looks here this is cod Tracer a powerful time Char in the bger for Noir unlike traditional debuggers code Tracer works by recording the execution of a program into a self-contained Trace file you can think of the trace file like a video

recording of a program's execution once the execution has been recorded anyone can use this Trace file to replay the execution of the program in precise it the same way each time now let's see code Tracer in action we can step through code normally or we can step backwards just as easily and on the right we can find the code Trace view it shows the full history of the executed functions and it lets us jump instantly to any one of them we are at the start of this function but we can already see what's about to happen all local variables display their values in line the taken if branches are highlighted and the unexecuted code is D out let's step into another function we can use this slider to navigate through the iterations of the loop and we can see how the variables change as we go in the

bottom right we can see that the event lock also reacts to those jumps it's essentially a list of all the programs interactions with the outside world the goal of the example program is to create a zero knowledge proof that our ship Will Survive The Passage through an asteroid field without disclosing how much energy you have in our shields in the end that way the space pirates won't know if they can attack us or not now let's have a closer look at the main function according to the comments the Pirates can predict the collisions but our Shield Technologies a well guarded secret this is why the properties of our Shields are passed as private variables to the main function whereas the masses of the asteroids are public we can see the exact values in the pr file which is accessible through the file system panel right off the bed we see something

suspicious in the event loog in the first event we see Zero damage being done but every Collision should result in at least some damage and in the next event The Shield regenerates Beyond its limits let's click on the first event and let's see what exactly is going on now we are in status support function and although the reporting happens here this is most likely not where we will find our bug okay let's step out of this function this brought us to the function that iterates through the asteroids on the first iteration of this Loop we see that the calculate damage function returns zero luckily Cod trer is a time travel buger and it's easy to navigate back and step into the calculate damage function according to the comments our Shields are supposed to get exponentially less efficient as they get weaker and we see that the current

implementation does not take into account The Edge case where our Shields are at maximum capacity in this case we multiply the damage by zero instead of one okay let's step out of this function and see what the second event that damage is a negative number we can use the slider to step into the next iteration of the loop and here we see that indeed the damage is a negative number now we can step into the damage function again and we can see that the problem comes from the fact that the shield has exceeded its maximum capacity and this is why in the end we multiply the damage by minus 10 okay now that we know what's wrong let me fix this really quick by adding an statement to handle the edge case where

we are at full shields in the calculate damage function and I'll add another statement to the calculate Shield regeneration function so that it cannot regenerate past the maximum Shield capacity anymore after we done editing the code we can record the program again and see if everything is working as we expect great success this time the damage is not zero and the shield does not exceed 100% but for some reason the assion does not pass and I've been told that the example in the Pro File is correct so if you take a look at the event lock again it's not immediately obvious where the problem is and I know for sure that by the last event the shields should have been drained completely luckily we don't have to rely solely on the events from the console output uh let's step into the function where we iterate through the second

asterid cluster first we can check if we see something suspicious in the variable history uh the damage seems to be okay let's take a look at the history of the remaining Shields oh and indeed we see a negative value appear in here as well so to illustrate this better we can create our own events using that Trace lock after we open the trace we can type in a command just like that and press control plus enter if we click on the event where the remaining Shields are negative Cod Tracer will jump to that event now we can see that in all the events after iteration for the shields should have been drained but we don't stop regenerating the shields even after that moment to fix this issue I will add another if statement to the calculate

damage function which will limit the damage to not be greater than the remaining shield and since we need to have at least one unit of Shield energy to survive the cosmic radiation I will add another if statement to apply the Regeneration only if there is at least one unit of energy left let's see if everything works as we expect this time all assertions pass which is a good sign and I don't see anything suspicious in the event walk and even if you take a deeper look into the variable history we don't see anything suspicious again so I guess that's it for today feel free to join our discod server and if you if you want to support C so you can leave a star in the GI repo links are in the description below all right uh so that's it uh with

the links for uh joining the re relevant uh telegram group that was mentioned earlier are here so uh if you want to uh ask any questions to our Engineers just take the very first QR code at the top left there uh the next one is our block sense docs uh for Noir formal verification Docs that Stan took you through in the first video check the second QR code down second row down uh and then finally uh for code Tracer uh this QR code will take you to the Discord Channel and uh code Tracer will be going live for a public release this Friday uh so be sure to join the Discord and stay up to date

on the latest there thank you any questions just yeah please go ahead what led you to just going from Oracle development to go to start developing structure yeah great question so what's uh the question for the uh for the audience who's not with us live is what drove us to go from developing a decentralized Oracle Network to actually um contributing to Noir and building these different developer ecosystem tools uh so the main contribution from block sense is the plunky 2 uh back end for Noir as well as

Noir Noir Trace I should say um and the formal verification part so here like uh with block sense we take uh the ZK part of the Oracle Network very seriously uh and we want to make sure that the Oracle is as performant as possible um and so that's why we we kind of like took it on our own hands to um to develop that out because we we wanted to have planky to be the uh the proving system uh and we happen to have a top class team of programming languages Engineers so our founder and CEO uh zahari was one of the core uh contributors to the Nim programming language um and been a compiler engineer for a long time and uh

Stan who you heard is a a PhD and a lecturer in in compilers uh in in Bulgaria so it was kind of a natural fit within the team and uh we saw that it would help with the with the performance of the Oracle Network work um on the code Tracer side uh and the debugging side uh that's actually a sister team from block sense so it doesn't the development is not actually taking place within the block sense team um but it's a very closely related company and uh we kind of like share a lot of ideas and resources between the teams uh but it was again just kind of leveraging the uh the experience and expertise of uh of mainly zahari who's our our founder sure any other

questions all right well thanks so much for uh for joining I know it's kind of a last minute addition to the agenda so I appreciate your attention and uh yeah be sure to um to write on the telegram group if you have any other questions that come up thank you