Universal, scalable and trustless verifiable computing - Ilja Zakharov | Pi Squared

h [Applause] Hello nice me nice to meet you all actually yeah thank you for surviving till like this last talk yeah so my name is Leah uh yeah I represent P squ I'm a engineer manager at P squ we actually big friends with runtime verification we kind of a spin-off company actually with the idea originated within runtime verification yeah but uh yeah so okay so have you heard about like uh verifiable Computing so maybe are they in your okay R yeah but maybe anybody else okay so the idea is pretty actually simple so that's uh something that people call ZK in the crypto space but originally like repairable Computing uh yeah has been invented like long ago so it's a way actually how you can prove that some execution happened without uh or with actually depending on your like problem statement revealing some uh data actually about this execution so the simplest example for instance uh if you have a program that generates some I don't know promo codes and you want to I don't know sell this promo codes for someone but at the same time actually this person shouldn't show you this promo code so just to avoid like uh some the chance of cheating so you can actually use this technology called verifiable Computing you can execute your program within some specific environment or write this program in a specific way and actually guarantee that for instance provide certificate that you generated this promo code by a specific program and you actually don't know the result of like generating so you don't know the promo code itself for instance it it was sent to your email or something but originally the state of art is actually so there are many flaws in the current state of art how people do Ral Computing especially in the crypto space so the problem is that so like doable Computing for existing computations it's really expensive because we have quite complicated programming languages we have uh evm we have rust so to actually generate zero knowledge proofs for instance using existing infrastructure you need to try TR different software quite complicated software actually millions of lines of code so you need to trust specific circuits designed for this purpose you need to trust uh interpreters or compilers so actually yeah it it's not the errorr way so even if on paper it could look like really uh like gril but uh in practice it's really difficult to achieve real like safety so because no one actually would jior like I don't know do some formal verification of your infrastructure because actually it's quite complicated and big so what P Square brings to the space is a completely different way of thinking so what we do is actually we kind of provide a way how you can uh do some Integrity checking of what ver verifiable Computing does actually so imagine like uh analogy with tcpap so for instance I don't know you want to send a message from Ellis to Bob and what you need to do is actually to have some guarantees that for instance you you use this like tcpip protocol the message will be like uh actually arriving Bob without any changes right so you have like this tag and you don't care actually about like this messaging in the internet you know that actually it will be delivered it will be delivered without changes so we don't have in the current like uh I know state of art at for verifiable computing so what pi Square actually does we bring like this level of uh like trust to to the space so we introduce additional artifact called like mathematical proofs actually into the game and using it and using like a proof checker for this mathematical proof we can guarantee is actually that uh ver Computing happening according to actually our intentions so once I attended uh Microsoft res search summer school back and there was a good actually talk about like uh um revolution in different Tech areas so and the question was like how you can even come up with something I don't know genius so and they actually told us that we back were like PhD students they told us that there actually two ways one is very difficult and it's really just happens by chance when you can come up with some brilliant idea but usually what people do they combine some cool actually ingredients already existing in the tech space and actually result of this combination brings you to something brilliant in the space so that's what we are trying to achieve in the pi squar so we have three k ingredients actually first one is also actually called k k framework we have matching logic and zero knowledge certificates so these all like three items already exist so we don't bring anything like uh crazy new but we actually came up with a super cool actually way how to compose them to achieve our final goal so let me start with the K first so the K is executable sematics framework it's been years like in when it was announced and released so there are many scientific papers it's already actually battle tested and it's applied by our entire verification different commercial engagements so it's the thing that actually allows you to generate mathematical proofs in our like uh problem statement that is pretty simple you can define Language semantics uh and actually by defining the language semantics you can get automatically different kind of tools you can do symbolic execution you can do dactic verification you can have parser interpreter compilers like other to other tools so the good thing about like language semantics is that it's pretty easy to Define and test so in traditional like uh programming languages uh way how to like Define programming languages what you need is actually to Define I don't know interpreter or develop a compiler or something so the things how the programming language is what actually does it do so they're hidden inside of like this complicated software in the semantics framework they are all explicit you just need that to write specific program called like this language semantics that just explains step by step what each I don't know statement in the program what each operator something actually does in the program for instance how the so-called like program State uh is changed by certain kind of like operation in the programming language so you can actually even test it using K using existing uh tests already developed for existing compilers or anything so another step uh another thing actually that we use in our uh product is is uh mathematical proof so mathematical proof is just an artifact generated for some specific claim so if you speak about the K so K requires this uh language uh language semantics plugged in as an input oh sorry 11 does it work okay yeah so and as input you can provide not just the program so but you also can provide some additional requirements about this program execution imagine you for instance you're sending some eth uh I don't know from Ellis to Bob and you want to ensure that balance of Bob will be definitely increased it couldn't be I don't know go below the previous like value so to ensure that you can like write some kind of specification added to the program so we call it claim but actually claim can be empty so you can have only your program so you can fit it to the K and get so-called like matching logic proof so what's the proof like by itself what's nature so the proof is specific uh actually theorem so it's just written in a specific uh formally defined language so in logics uh we have so-called like model logic so it's kind of model logic it's defined using separate like logical constraints constructs uh that has a limited set of uh simple proof rules so the matchin logic itself has been developed already by more than 15 years there are many like peer reviewed research about that but what's important about the magic logic it's kind of specific mathematical logic that allows to capture execution of almost any uh or maybe any programming language so that's important and the proof itself it's it's just like simple uh sequence of uh some axioms like initial statements that we trust in this example it's statement that for instance I don't know if it's raining then I will get wet and we can have another axom for instance it's raining we have also some claims something that we want to prove for instance this is the latest uh statement I'll get wet and we have proof rules the proof rules is specific rules in in logic that we can apply to actually deduce this uh statement so we just say for instance if we have like mod ponents logical uh proof rule so we can simply deduce this like uh the the result from these two statements so I don't go in uh like uh too complicated details so the final final part is zero knowledge proof so why do we need zero knowledge proof so zero knowledge proof just to work as a compression tool so matching logic proofs are pretty big so we can generate them as a stream but anyway so like the result of uh executing the program like and explaining uh all steps of the program in as as actually mathematical uh formulas could be quite yeah big so that's why actually we need some uh compression tool and actually to just avoid uh compressing iture what we do is actually we just run a specific program called proof Checker it's pretty simple it's just like the simplest implementation that we have right now it's just 200 lines of code what it does it just checks the consistent consistency of the generated logical proof so what we need to do is actually just to check that actually logical proof it's correct from the perspective that it applied only like soal like valid proof rules it used aoms that have been there like as our trust base that like there is not no like I don't know kind of facts uh introduced during the proof rule itself so everything like is connected in Mak sense so This Small Program actually could be executed in the some ZK environment existing environment and we can after like running this program generate ZK proof that actually shows that not just the proof was correct but actually execution was correct because we got this execution actually from actually we first like generated mathematical proof for the execution and then we got like the ZK certificate so ZK certificate actually valid for the execution so this is uh the final like the main actually idea so how we combine our tools to actually do a lot of different uh things in the space so again just to go through all like this components on the picture so we have some programs initial programs they can be written in any programming language if you have your like programming language semantics defined for instance we have like KVM we have kwm already defined and supported by the runtime verification so we can generate actually mathematical proofs using K what we can do next is that we can actually run this uh simple programs called like proof Checker inside some uh ZK environment and get uh actually zero knowledge proofs for that so it's much simpler way how things work right now because simply yeah we can plug in new programming languages really seamlessly we don't need to invent new circuits new actually zero knowledge environments for that so we can actually do many things here so for instance we can summarize proofs and generate not just I don't know mathematical proofs for for the program itself we can we can generate summaries actually for execution of some programs like compressing them using to like K we can also generate for instance check marks that some smart contur contracts have been verified by actually running uh formal reification tools and actually with with the support of our environment for instance right now if uh a company like I don't know carries out some formal verification and they got this like check mark on their side you can't actually verify right so that they actually have verified the recent version of the software that they actually provide or they support but using like this kind of uh pipeline you always can do some kind of checking you can have for formal application also some kind of guarantees some certificates that people can verify by simply wrri I don't know ZK check or something so there are many actually use cases in in the area that can can be uh implemented using our Tech so called actually proof of proof so but what we started doing recently is building a product called Universal settlement layer so Universal settlement layer is a component in the model blockchain space actually so it sits between the execution layer and both consensus da layer so what it allows actually to do is to eliminate the need for messaging platforms and actually simplify uh bridging for cross chain applications so it allows to expose actually trust because actually what we can do is reduce trust uh thrust B base for actually uh modern uh quite complicated infrastructure so we'll talk about it slightly later and what we can do is actually mitigate fragmentation between uh like four applications uh that would like to use different da layers so again just to emphasize so why actually does proof of proof uh look like a something that actually brings some more in innovation in the space so again so secret Source first is universality so as I mentioned so uh K uses uh language semantics so you don't need actually to rewrite anymore your compiler or interpreter when you need to introduce some changes in the programming language so what you need to do is actually just to change your language sematics carry out some testing and that's all actually you don't need to change the underline infrastructure you don't need to update your even ZK circuit you don't need to update your Z KVM it's really simple and easy to prototype so if you're going to build your own I don't know solution uh or uh programming language and you want to quickly build a ZK roll up you don't need actually you don't need to think about how to like build all like this complicated stuff so another thing is trustless so the core thing uh in trust is actually trust based in the space so for instance if we consider current like state in the traditional space like traditional Finance so you need to trust a lot of uh actors that you don't see for instance when you buy a cup of tea or a cup of coffee you actually pay with a cart and you to interact with different uh players so acquire card Association issuing bank so you have some actually trust base so you need to trust acquire you need to trust card Association you need to trust actually maybe issuing Bank you need to trust this point of sale Merchant as well also has its own trust base it needs to trust actually Merchant Bank and other like components so the same actually about this like uh trust B and defi so there are many data source that you need to trust actually doing your transaction you need to trust data sources you need to trust for instance oracles you need to trust uh some smart contract you are interacting with you need to trust uh I don't know wallet implementation eth node and actually compiler sitting inside the node I mean not the compiler but your virtual machine yeah but anyway so there are a lot of things that you need to trust and if actually we moving towards like this new area of modular blockchain it's getting worse right because actually there are many like this model blockchain components it's not any more like Central uh like I don't know component and you want to actually see what's happening right so if you interact with different products with different like this layers you want to actually see uh what you need to actually to thrust before you I don't know send uh your like I don't know money inside this system so what we actually want to do is actually expose this thrust show this components this actors uh actually in like exactly in like transaction metadata and what we can do actually eliminate some certain players here so we can reduce the thrust Base by using our proof of proof technology by actually reducing to two main actually players So speaking about like interpreters for instance if you have a language semantics if you have this proof Checker you don't need to trust actually virtual machine anymore you don't need to care about about like vulnerability vulnerabilities sitting in the compiler because this is actually could be easily first like spotted by the by the K actually executing your transaction uh and also while the mathematical proof is generated so now it doesn't like uh so there is no any danger is in for instance that there is some bug and K because if the proof generated incorrectly it would be easily spotted by the proof checker so you need only to trust your language semantics explicit finded actually written you can send it to your I don't know friends it can be easily audited it's human readable it's executable you can even test it with the K you can and yeah the second thing you need to dra is this uh small proof Checker it's scalable really small 200 lines of code and formally designed okay and the last component is scalability so first like before before I uh uh like talk about this point so I want to just uh show you that uh okay maybe doesn't make sense okay I want to just like emphasize that logical proofs aren't the programs itself so they are completely uh stateless so the proof itself is just a set of Lamas so-called like I don't know theories you can consider them as theories and each theory has its own proof so you can actually prove all like this theories completely independently you need to you need actually carry about like what's happening after certain Theory you just need to like do checking all like this like theorem proves in parallel and then just double check that all like claims they form a valid actually chain of claims for instance that if we start like proving a theorem or claim with certain assumption this assumption has been uh seting as a claim or theorem in the proof or it was a part of the initial like uh thrust assumptions so that's why actually scalability is uh one hour our yeah strong point oh sorry it's different strong sides yeah so we have implemented our proof Checker using different programming languages though we already have a prototype working in Risk zero that KVM L yeah K 1 K zero so there are many things we can approve actually so it's just numbers actually that we obtained at the end of the last year so we switch to a development actually our own circuit using circum mostly because we want to like uh make it more fast more scalable get more control over actually cryptographic operations because uh the thing is that uh in The Logical world we have many operation that could be actually uh carried out much more efficiently than in existing actually Z kvms so that's why we considering development our own solution and yeah so our current Vision on USL architect arure it's also temporary so because we actually just recently embarked in our journey so the idea is that uh it will be chain or that would be actually consist like that would contain different uh blocks having transaction in different programming languages uh so you can easily actually uh using our teag support uh execution for different kind of programs from for instance even generated by different execution layers like for different rollups coming to us we can sequence like sequence them and combine them uh together actually for instance if you want to B like build some I don't know breach or do some different uh actions on different chain you can even like in the same block or in the same transaction verify that for instance one uh transaction in uh evbm does something like uh step a and then there is another like transaction corresponding to the action intended for different like uh I don't know smart contract written in Rust in a different ecosystem that you actually can uh uh connect together so the thing is that we only need to settle this uh mathematical proofs we can we need only to support mathematical proofs all right so yeah join our efforts so as I mentioned we just like recently started so we have our teeken place if you have any great actually ideas how we can copyright and help each other so yeah feel free to reach us and yeah let's do rep Computing together so thank you can we get one Applause uh do any of you have any questions it's a large audience so someone has to have one thank you giving me something to do here yeah so so my question is about how easy to how it easy to like write this all these things for normal normal for for developers to to generate the proof because it looks like sometimes like developers like even lazy to write the tests and here they need like looks like they learn like new framework uh and like do you have any ideas how to make it simpler or something yeah the idea is actually we don't need people to write their own Frameworks we don't need them to support new programming language that's something that we want to actually carry carry out themselves or maybe Outsource to existing companies such as rtime verification which are actually great in development uh language sematics what we want to do is actually get like this uh language semantics ready in place uh we will support more of them so first steps like will be support evm because we already have KVM and support wasm actually and because we have some prototype for the KY was semantics so and that's all actually so for instance to generate ZK proof you don't need anything so proof Checker is developed by us so K is developed by us uh yeah you don't need anything actually you can just like take our yeah take our Tech and give us your program and we will generate uh yeah we will generate proof for you but the thing is that on the like Universal settlement layer so we likely considering like B2B uh yeah customers so maybe yeah we will talk more about during the next events about how actually we plan of like and helping people to integrate and build on top of the USL but it's not like main topic of my yeah talk today okay thank you but so for that first you need to cover everything by formal verification to generate the proofs right and yeah so but formal verification it's in place the the problem in Pro in formal verification is that it's difficult to prove something that actually kind of uh doesn't sit inside the program so if it there is like separate Claim about the program it's difficult actually to go through the pro program right and prove that but in our case what we do actually we just follow line by line through the program like generating this mathematical proof and don't thing we need to do is actually just to check it consistency so in our like practical evaluation we can generate proofs really yeah fast compare comparing like with existing solution so the last comparison was uh for G uh so G like only part like uh actually like yeah that executed like evm code it works yeah faster but maybe two three times faster for certain benchmarks not like 10 times slow like right like yeah it's really comparable to like Cutting Edge Solutions right now does that answer your question uh okay can we get one more Applause for IIA great talk thank you