V for Verification: A Unified Service for Secure Blockchains

Transcript

thank you a lot for the introduction and thank you all for uh staying for the last session so yeah I'm Costas uh I'm a principal scientist at verise a startup uh whose goal is to harden blockchain security uh by applying formal methods so today I'm going to describe briefly our technology and te some cool things that are coming uh soon but first I want to give you an Insight of why we want to uh techniques like verification to ensure blockchain security and this inside is surprise surprise money and I'm sure all of you know that uh uh bugs in this new decentralized software stock are extremely expensive and uh to make

matter worse these bugs can happen in any of these layers of this new uh developing and evolving uh stack uh for example so far we have seen uh detrimental backs in uh smart contracts consensus protocols uh zero knowledge proofs and the least goes on so uh motivated by this we started uh veridis whose goal is to develop a set of formal method tools uh in order to uh ensure uh blockchain security and to be a bit more uh clear by formal methods I refer to a set of mathematically

rigorous techniques uh who are able to both uh discover bugs in code as well as prove its correctness and the story of these techniques go way back but up until recently they mainly uh collected dust in you know academic research themselves uh but uh recently because of the security critical uh nature and monetary uh handling of uh blockchains uh we've seen an n in the need for pro uh providing correctness guarantees of deployed of deployed software um and uh to dive in a bit more uh when I refer to formal methods I

refer to a very wide range of techniques from systematic testing uh to static analysis and formal verification so for example here techniques on the um on the left side of this figure are more suited for back finding and usually require little to know uh user input whereas like techniques on the on the other end of the spectrum are more are more suited for providing correctness guarantees and usually require a bit more human effort to um make things work so uh that brings me to the main product of our company which is what we call verification as a service or vas uh where things work as follows so the user

has to provide the code artifact and optionally a set of specifications written in our own specification language called V that formally describe the desired behavior of the uh of the code so then our service will run all applicable tools uh to the input code base and will report which of the input specifications are verified and which are being violated and also uh give concrete bus for the ones that are being violated so overall uh the goals of our uh of our tool chain here are to uh be user friendly and also support as many

languages and blockchains as possible so our uh design evolves around the two following principles first uh we provide a very unified interface to all of our tools using our V specification language and second the core logic of each tool is implemented in a language and blockchain agnostic way uh this way we can later on ADD easier new blockchains and new languages uh so before I conclude I want to give a very brief introduction to these specifications using this uh very simple specification that describe the desired behavior of a wallet so in a nut cell this specification says that if a

user calls method deposit uh and this method execut successfully then at the the end we want the balance of the sender to incre to increase by the desired amount uh however this a very this is a very simplistic uh uh example NV has a lot of more uh useful and fun features where users for example can specify what happens in any possible execution for example what happens when you know a transaction reverts and also provides ways to describe system invariance and comp complex Behavioral spefic ifications uh so uh up until now we have used this uh uh this tool chain

internally to perform several uh uh Audits and we we managed to find actually quite a few issues from flash vulnerabilities in D apps to soundness bus in zero knowledge proofs so uh moving on uh we have more fun things coming uh your way uh first of all we plan to release a better better version of our vas Service uh sometime uh this year and also we are planning to release more tools targeting zero knowledge based systems like pus a common vulnerability detector for uh circuits and circum Coke which is a tool for proving functional correctness of uh of

circuits and uh finally if you want to learn more about these things and you are at Devcon in October make sure to attend our c uh talk where he will go into more details about our new ZK infrastructure thanks so much amazing thank you um is there any question for Costas before we move on to the next talk does does your ver verification language uh does it support temporal logic or is it just a first order Logic No No it's a it's a full full on like you know LTL variant that like is targeting do blockchain like applications yeah one more

question yes no or else you can find Costas after thank you