Push Button Verification for BitVM Implementations | Hanzhi Liu - Nubit

[Music] all right uh good afternoon everyone uh thank you all for being here today and uh in case you don't know me I'm H I'm one of the co-founders of new bit and I'm also aeed student at ussb where I do research in blockchain security and SEC technology so today I'm going to introduce our uh recent work on uh push button verification for BVM in implications so let's get started uh first of all uh everybody is celebrating the buom market where uh Bitcoin is hitting alltime highs again and however despite the introduced in the same paper by Satoshi Bitcoin as the currency and the Bitcoin Network are like two opposite extremes so on one side uh Bitcoin dominates over 60% % of the market share and with over 20 billion daily volume and on the other hand Bitcoin as the network can only handle four transactions per second and how many can Visa handle it's 24,000 per second that's a huge gap and given the previous numbers it's not very hard to understand while there are like hundreds of uh Bitcoin ecosystem projects early last year such as layer two uh oracles Defi and none of them went very far due to this uh brutal limit of Bitcoin and with let's say ordinals and inscriptions we immediately see the consequence of the limitation via uh netal congestions and Rising fees so uh like there are also many uh Bitcoin native projects including a bunch of layer tools defies they claim to solve this problem and however if you analyze their uh data flow uh none of them goes far beyond their own Central servers it's because getting their transactions settled on the Bitcoin network is not only expensive but technically highly non-trivial so what can we do luckily we got BVM uh originally proposed by Robin lus two years ago it was born to address this limitation so the high level idea of BVM is very easy to understand so since the competition power of Bitcoin is both expensive and limited so let's move the heavy lifting competition of chain and only defer the onchain ver validation process with an onchain verifier deployed on bitcoin so you only need to trust science and like Bitcoin network instead of any third parties or centralized providers it's much like an altim way to uh verify computations on bitcoin and with bvn the future looks awesome right but why we haven't seen anything yet well because making bvn from a prototype in the paper to a product is highly non-trivial it's extremely challenging so why it's because Bitcoin script is not touring complete just like any programs you first have to implement BBM let's say uh let's say we pick a gr 16 verifier uh for ZK SN in some high level program language such as rust uh it is pretty simple uh it's easy as you can only like need to write a few hundred lines of code uh due to there are lot already like very sophisticated librar such as arwork and uh since this program need to be processed by a compiler to an IR and all the way down to the it's lowlevel Bitcoin script and now I hope you can understand like notice the the issue so why we all know that Co script is toally incomplete and you may ask what do you mean exactly so well if you think of the experess of even by cod as adults who can express her rich emotions such as happy sad angry the experess of Bitcoin script is like a oneyear old baby who can like only have has two states cry and not cry so that means translate such a small program uh CK verifier in to bitcoin could be extremely large for GR Sy verifier it will take 1 gab of data and manually construct such a complex and large program May highly possibly introduce security vulnerabilities so what can we can do so to solve this problem to ensure the correctness of suchar program we need a proper formal verification tool for Bitcoin script so our keing idea is simple so we want to automatically verify Bitcoin script BM implementations uh so it's it's very low level set relies on some complex uh stack operations so instead of manually checking this code our approach translates this lowlevel B script into a higher level clear representation and then like you can think of it as like uh converting this a Danse technical instruction Manu into some plan language instructions that are much easier to understand and verify for computer so the first St of uh the whole process is to convert Bitcoin script into what we call a domain specific language or DSL so this DSL abstracts away the Massy details of Stack operations by replacing them with register like operations so imagine you have like a complicated C track that involves reordering cards in a very precise way so our convention process takes that complex procedure and rewrites it as simple steps like add copy uh move much like clear uh instructions so this results in a cleaner simpl version of the original uh Bitcoin script that we can analyze much more easily and after we have our this High Lev DSL the next phase is to automatically verify this code so this is where we check that the converted code meets its intended Behavior so we use techniques such as Loop environment and symbol execution so the core contribution here is the loop environment so the loop environment are conditions that must hold true before and after each iteration of the grp so by summarizing the effect of repeated uh operations with the r environment we capture the essential behavior of the code without having have to like inspect every single step so this can make the whole process more scalable and imagine you put a like giant Bitcoin script with Millions lines of code since there's no counter flow and you need to unroll all the loops and this will be a disaster for the symbol execution so with Loop environment to summarize the behavior the solving time can be much less than the the vanilla way so together with this method Loop environment simpli secution and the high level DSL we simplify the verification condition significantly allow our tool to automatically confirms that uh the the specific Bitcoin script is correct so essentially we are taking a very complex set of instructions and reduce it to a clear logical statements that it's it's much easier to for for the solvers to to verify and now let's look some uh let's look at some concrete examples uh the first example is is the bigin multiplication so bigin multiplication is a crypto crypto op uh operation that used in many blockchain protocols it is used to handle very large numbers uh numbers are so big that they can be processed with standard types so it is used in BVM in CK proof in ecdsa basically every single crypto protocol needs this operation and in the original uh Bitcoin script uh to implement this big multiplication is extremely hard I think uh on the left hand side the script must manually handle each length of the large numbers essentially it's the chunks of the L big integer and it it use a series of Stack manipulations like duplication rotation shifts and I also need to track all these operations by hand which make it super hard to verify and using our tool we first convert this low-level script into our high level the cell so in this representation the sequence of Stack operations is abstract into to clear higher level uh instructions on the right hand side so for example instead of rapidly moving pieces around our DSL expresses the entire multiplication uh using a loop uh sets like upat two key variable so one represents the current result and the other represents the Dem multiplicate and which doubled at each step and a loop environment is then uh established to capture the relationship between these variables after each iteration so this invar like States in in simple term uh the multiply like the result so far equals to the uh the original mcant multiplied by the process bits of the multiplier so with this concept summary so our Ren tool can quickly check that the entire multiplication is performed correctly without getting lost in the low level Bitcoin script details and uh our to is is bling fast so we can talk about our experimental results so we EV evaluate our V tool on 78 different uh benchmarks from BVM and the results is is kind of promising so our two successfully verified 80% 8 83% of of all the cases and the average Ving time per Benchmark was just 12 seconds and this Tool uh we compare this two with with in vanilla Solutions which uh simply convert the Bitcoin script into to verification conditions without any like looping environment and uh inference uh that it it shows faster time and can solve much better uh benchmarks and importantly our tool also identified the previously unknown vulnerability so for example here on the left hand side there is a buggy implementation of uh is positive which will count zero as a positive number which is wrong so and on the right hand side it is the fix version uh and this bug is discussed using our tool to summarize uh our work push button verification for Bitcoin script uh basically simplifies and automates the verification of Bitcoin scripts and which shows practical impact on uh improving the security of real world applic applications such as BVM so if you are interested in our work feel free to scan the QR code above and uh have a nice day uh thanks for listening so