ZKPodcast: Formal Verification with Martin Lundfall

Transcript

[Music] welcome to zero knowledge a podcast where we explore the latest in blockchain technology and the decentralized web the show is hosted by me Anna and me Fredrik [Music] in this episode we sit down with Martin lund felt to discuss formal verification what it is and what frameworks are normally used as well as where it fits in the blockchain world thank you to this week's sponsor of the web 3

foundation the web 3 foundation has announced a series of grants to fund development on substrate and polka-dot if you are a group or individual contributor looking to build bridges to other change substrate runtime modules or an exciting new pair of chain this could be an interesting funding option you can find out more about the areas of interests on grants web 3.1 the criteria is it must be open source and approximately a three month work time frame for more about this program check out the blog post we have linked in the show notes thank you again web 3 foundation and now here's our interview with Martin Lynne fell so today we're gonna be talking about formal verification with Martin

Moone file hi Martin welcome to the show hey I'm glad to be on the show and I'm currently on a call not with one Swede but with two Frederick is here to block train industries of being overrun by sweet we are all parts of the Swedes so formal verification as a topic was requested by our audience actually when we put out a call earlier this year for topics we had it came up more than once we ourselves had talked about covering this and we're really happy to have you on Martin to help us navigate this what would we call it the sort of future of security the I've been describing it as the road to complete verification but

that's also a bit sensationalists so that's either a very long and winding road or a very narrow sense of complete security I think we should start off with some form of primer on formal verification because it's this topic that's kind of mystical undefined and a lot of people's eyes seems magical and a lot of people's eyes but it's also this thing that people tend to quite a lot around if you have security problems just do formal verification and you're done men like you you'll never have a security issue in your life again but obviously that's not true and there this is like a huge field that's been around for many many years long before

blockchains existed and I'm curious as well to hear how you got into formal verification yourself so maybe we can start just there and then dig into a bit more on what it is sure so I started getting into all of this by studying mathematics the school at which I was studying at Stockholm University there's a fairly strong logic department and the logic is very computer science e1 might say there's a lot of type theory I I studied with some great professors that really got me into proof assistants and writing mathematical proofs in computer languages where the proof assistant or the interactive environment with which

you interact is checking the validity of your proofs as you write them which on the one hand is like an extremely way to detailed process because computers are very bad at understanding math so you really have to spell everything out to them so a lot of the time you end up proving trivial statements with a lot of effort but it gave me a nice understanding of how we can really understand mathematics from a computer science perspective or sort of the interaction between the two and so I actually wanted to have an original project this was supposed to be my bachelor thesis I wanted to write like a proof market so if you would define the

rules of mathematics in a computer language so really like the foundations of logic you would be able to do this sort of proof checking and if you were to implement it on chain then you would be able to have statements that you want people to write the proof of and you could also attach a bounty to that proof so you could take your favorite unproved conjecture and you could attach a bounty to it and see if anybody would come up with the proof I ended up not doing that because implementing their rules of mathematics in the EVM it's kind of cumbersome and I

decided to sort of pursue different things that's that's how I got interested in really doing formal mathematics in the first place and then verifying programs came naturally as I saw the demand for that as all blockchain contract started to get hacked I had you just been like into blockchain on the side like you were studying something else from what I understood and then you just sort of ended up there but was it like a hobby that became a focus or did you learn about it at school no I learned about it through different means just hearing about it from friends and getting more and more involved but actually as I was

studying it was a fair degree of separation between the mathematics I was studying and the bar chain stuff that I was learning at the side and I was trying to unify them and I think I eventually have like right now with the work that I'm doing but as I was studying they were more separated the first time I came across formal verification myself was I think it was a good way interest learning Haskell and once you start learning Haskell you kind of go off on this tangent of formal verification and learning talk and Isabel and Idris and everything else and dependent types and these are all sort of interlinked things and I I think the first proof that I saw was that like this array was a fixed length throughout

the entire program and it's like yeah okay sure but not super impressive yeah but then like I think the second proof I probably saw was like that a red black tree was correctly constructed and that was a bit more mind-blowing that was actually like yeah that that's actually powerful what was the first time first proof that you saw or wrote yourself and and which one was the made that the one that sorta made it click for you hmm that's a good question that's really nice I think the first proof that I wrote was about real numbers defined in a sort of finest way though defining real numbers as a sequence of converging rational

numbers I was proving that you can acquit these real numbers with an equality that actually is an equivalence relation so I was proving the symmetric and transitive and reflexive part of that relation so it wasn't very computer science or program oriented it was it was more of a pure math thing Frederic you just mentioned that like Haskell kind of led you to formal verification when and I might be off here but like rust has a lot of sort of checking is that in any way related yeah I mean it depends on how you view things I would say like just from an engineering point of view like something like Python

doesn't have a type system you have no guarantees that anything does anything at all then you move in something like C and you have types like an int and your guarantee that this is an int that you know this thing will always be an int and then and there further up to type system stack you go the closer you get to something that is formal verification in my in like in my naive understanding of it because it's sort of you get to a point where eventually you have this whole system in the type system in the sort of compiler and the verifier of the program that these properties hold but something like Haskell so has an

extremely like you can't actually prove almost anything compared to something like a framework which we'll talk about later where Kay framework is this whole framework and like the you make these huge specifications of what it is your program is supposed to be doing and you know you can view it in some way at least in like I said in my naive view of it as a type system and so once you like go down that path of wanting to learn more and better type systems it kind of leads you into formal verification or at least it did for me yeah that really illustrates the two different approaches to formal verification or to getting assurances about your programs where the one is as

you said where you have strong type systems that give you guarantees when you if your program just compiles then you know that it's going to behave in a certain way and it's not going to violate certain invariants and the other one is where you have another language or another framework in which you plug in your program that you have written and you can state properties about that but you're not necessarily stating the properties and the typing language of the system you're rather putting it inside a framework where you can make claims about the nature of this program and this is sort of following along a tradition with core logic and and pre and post conditions and stuff like that

and that has been a little bit separated is also model checking is also in this category I would say that that is a different flavor or or at least a difference heuristic to to getting assurances than the strong type systems but just while we're talking about type systems there's one thing that I think should be mentioned which is the what you were getting at Frederick before and also if we're talking about rust which is the curry Howard correspondence or this paradigm of types as propositions and this is a correspondence that is really strong in in the cases where the type system is very developed and if your type system is rich enough such as

dependent types then it really becomes the case that there's a direct correspondence between the types of your programs and the program's themselves as the correspondence between the statements also like a mathematical theorem and it's proof and then if you have linear types in rust you can you can sort of understand them in different ways we haven't exactly defined formal verification yet I feel so why don't we do that I think it might make sense just like if you were to summarize what it is in a sense what is it I would define formal verification as the stating of mathematical properties about programs and their proofs so proofs of those

claims that you make about the programs and well that's the act of maybe verifying code in general and then if you want to do formal verification and that means that you are not writing these proofs down in English or in a lotof document you're actually writing them down in another formal language if there is there a specific language that formal verification usually uses or can it be all sorts of languages so generally I would say that it uses the language of mathematics and there are different flavors and different implementations of the language of mathematics and people have very strong

opinions about which ones are good implementations or which ones are true mathematics what does that mean like I'm trying I'm trying to picture what that is like for example where do you do your work like where is it so since my work is using the K framework and writing my proofs as statements in the K language and this language can be understood mathematically it's grounded in a theory of rewriting or rewriting logic it's called and and you can use like we mentioned earlier proof assistants like Coke or Isabel or Agra and they have a more direct translation of mathematics is like writing mathematics directly of

course you can also just write out proofs in plain English or in a nice PDF form or just explain it to somebody else it really just depends on the type of rigor that you're after usually I mean mathematicians don't spend their time or at least not most of their time writing down their crews in any formal system they write it down down in English or explain them to each other and that is an acceptable level of level of rigor and in most cases that is way nicer and more digestible than to see any formal proof of it but then when it comes to proving properties of programs from a mathematical perspective that claims are

not that interesting it's not like we're learning new things about some general nature of reality instead I would say that we're making very precise and involved claims about the nature of our programs that are mainly interesting to the people who will be running those programs the methodology of writing proofs is it's not very interesting either so it's something that can be done by a computer very easily it's a lot of it looks a lot like brute force you just explore a bunch of execution paths I would say that you can correct me if I'm wrong here but a simplistic view of it is I mean you sort of you write down a spec your proof of what

properties you want to prove in some fashion and this depends on what you're writing your proof in so for a simple example let's say you have an e or C 20 contract the thing that you want to prove is the total balance will not change posts deploy so you have this sort of you there will never be more or less tokens than this number and then so you how you writes that rule down like that's a simple rule to express in English but you can express that in code or you can express it in various ways depending on which framework you're using then you plug your actual contract into that in some way again depending on

what framework you're actually using and it does this like code exploration or like symbolic execution or just brute forces every possible inputs and and says ok you know your program is holding this rule like it you know this contract is now proven according to this spec yeah and I think what we're talking about that is important to highlights that formal verification is really just as powerful as the claims that you're making about your programs I mean of course you can formally verify that a program is doing nothing more than returning error for every input or that it's always returning a zero or that it

mainly exists these are all formally verified claims that you can make about the program but it might not be the interesting ones that you're after and finding the interesting claims this is the creative part writing the specs and really understanding what it is that you think this program should do and what it means for it to behave correctly is the interesting part and then the verification part is an exercise to the reader and I think yeah when it comes to real-world programs and this is where things get difficult is if you want to formally prove a networking protocol there's so many variables that are involved in correctness of a networking

protocol just like including latencies and timings and you know how routers behave in this system and how the backbone of the ISP is behaving like there's so many things that is even beyond your control that you couldn't really prove the entire system so you then it comes down to the engineer writing the proofs or the verification is like what are we trying to actually prove what's important in our particular application you very rarely get like a complete proof of an entire program maybe and I think this is why in the smart contract world it becomes a lot

more interesting because the program's become a lot smaller and it's much more likely that we can have a proof of like everything that we care about absolutely especially if we're talking about something like an A or C 20 we have like five methods maybe and all of the methods mainly do one thing there's a couple of corner cases that we need to take care of such as what happens when you transfer to yourself and stuff like this but really it's much more feasible to verify than something like a networking protocol this almost sounds then like when you start working on a project you have to get like you must have to work very closely with the people who've written the smart contract obviously it's simple you need to get inside all of their intention yeah and

this is extremely difficult especially with development methodologies if you think about scrum it's very much about just write something and figure out what it's supposed to do later and this is how a lot of programmers work so you just have a vague idea of what they need to do and then they write something and they sort of guess that's what they have written is doing or their I should say that their intention is forming as they are writing the program so it becomes kind of difficult to understand what the Platonic ideal of the program should be so yeah you definitely need to work closely with the developers and try to understand what they meant to do what they've done and how those things might

change over time this depends very much on the team and I even say like tides very closely into the language discussion of like how someone has written something what language and there are different styles and different languages there's this great talk by economic ride who's a professor I can remember where that's called is a type a lifebuoy or a lamp and he writes this program in Agda on stage and he the general like point of the talk is advocate type driven development instead of this kind of you know do something and then figure

out whether it's correct or not and he like implements something relatively simple but he writes out the types first and then in Agda you have this nice property that you can generate parts of your program from the types so he basically writes a fully defined type and then the entire program the entire implementation of that program can be auto-generated because there is only one possible way to write a program that fits this type and so you kind of get into this interesting mix of where you're stating your intention up front instead of post facts and yeah I like I really hope that we can move the

programming world especially in smart contract side towards this then I'm just gonna write something and see if it works and I'll only test never test the happy path absolutely so are you are you calling the end of scrum what's going on well a parody we called it a long time ago I don't know the names of these fancy development methodologies I can't remember who it was that said this I think it was thanks that I maybe we talked a little bit about verifying properties of programs he said that you should sit down and think hard about what you think that your program should do so I would say that this is kind of in contrast with

move fast and break things it's really all about trying to figure out what the hell you're doing before you start doing it rather than figuring that out at some point along the way it's like do you feel like there's a do come into conflict with the styles of some of the groups that you're working with because you are coming much more from this academic space and looking for that that sort of documentation first or like that clarity first I mean it's definitely a different way of looking at what programming is and how to do it as opposed to a lot of programmers like it takes me a long time or it has taken me a long time and I'm still learning to become a good programmer I mean this

isn't something that comes automatic just because you know some mathematics so when I work with people that I think of as real programmers I don't really know if I consider myself to be a real program yet it's a very nice trade-off an exchange of how to do things and how to think about things now that we've defined formal verification I'm curious why it's necessary I mean obviously it fits into the security theme that we've talked about but why is it really necessary to do formal verification and I also want to ask like if you have any examples of vulnerabilities that maybe could have been caught things that actually did go down that you think could have been saved by something like

from formal verification yeah so I think first of all there's a great value in just writing specs a lot of people keep iterating but if you're just writing a program and never write down your intention for what this program should do then as somebody coming in as a security researcher it's it's almost impossible to say whether the program is correctly written or not because in a sense you've only provided the program so if the program is also the spec then of course it's correct by by a triviality writing specs help and actually just the act of writing a spec will make you realise oftentimes a lot

of errors and things that you haven't thought about and then when it comes to what sort of bugs you can catch with this then there's really just a matter of how much effort you're willing it to put into the formal verification a lot of the common bugs that people have encountered in etherium and the history of a theremin and stuff like the dow hack to now easily be caught by automated tools that check for a certain type of vulnerability in your code or a certain pattern that is deemed to be insecure what formal verification does are really like a complete exhaustive specification of your program that you are able to verify is not only giving you this positive experience of course

maybe negative experience of finding bugs pointing out where there are bugs but also giving you assurance that there is not a bug in the program that you have been able to say everything that the program does and to show that in all cases it matches the specification I would say that yeah the difference and so what kinds of bugs you can find if we take the DAO hack as an example it happened and then there were annoying linting tools that said don't do this so it's sort of after it happened it was brought into all the tooling to say you shouldn't do this and now all future contracts are safe from this particular pattern if they run all the tools but

like these tools you know they wouldn't have caught it the first time it happened so if they had written a formal specification saying that they're 10 be no re-entrance e in the contract however you would go about writing that I'm sure that would be quite complicated but if you actually did that you would have assurance when you actually deployed it that you know it wouldn't have this going into it so it's sort of uh you know do you let this bug happen to one person first and then kind of catch it in every case after or do you write your respect up front and say like I want to like within some intention I want to be sure it against this particular thing happening if you

don't even know that this type of thing is a thing that can happen then it's really hard to write a spec about it as well so I don't know it's it's knowledge exploration versus like posts testing when you already know what can go wrong this kind of harkens back to what we are talking about earlier on about like this magic or this perceived magic that formal verification will fix everything but it sounds like if you don't know what the vulnerability could potentially be then you would possibly have a hard time using this tool to find it or to find out if you're vulnerable yeah it comes back to what I was saying before in what you're actually verifying and if you're at this scenario where you're not

trying to verify that a particular property holds you just want what people normally understand is formal verification which is that they say that the contact should be bug free so if a contract should be bug free then that means that you need to define its behavior in all possible ways that the program can be executed and that means specifying the entire nature of a program and for small programs this is easy to do and for large programs it's almost impossible well it's not very possible actually in the general case it is impossible but for most for most real applications you know things are actually finitely describable certainly most of the contracts that we interact with actually in the VM model this is a

common misconception EVM is not turing-complete because there is a gas limit yeah so as long as a block has a finite gas limit to it then you're not certain complete but a lot of people don't even deal with gas when do formal verification so when it comes to comparing different approaches to formal verification it always starts with the semantics of the language in which your programs are written so in order to verify programs that are written in the EVM we need a formal semantics of the etherium virtual machine and luckily the EVM is kind of small at least if you compare it to other possible languages in which you

can write programs that you might want to verify but it's kind of erratic and gas complicates things a lot so what a lot of people do is to not specify the gas behavior of BBM and then you actually have a turing-complete machine that's sort of weird that you can do a bunch of crazy stuff with what is really nice about the K framework is that they have a complete semantics that also deals with gas so I guess that brings us into the K framework and this is something we've mentioned here and there on the podcast before there's this ke VM thing that's being talked about quite a lot of which is this specification of

the VM in the key frame work so give us an intro to the K framework what is it the K framework is a language and the suite of tools that deal with definition of programming languages and analysis of those languages so it gives you a very nice way of formally expressing what a virtual machine or a programming language does and then it is written to be general enough that it can define any such language it has developed a bunch of tooling around the concept of a programming language in general and what you can do is you want to analyze a

language like that so once you've defined a programming language in K you get almost for free a debugger for this language and interpreter for this language and also an ability to verify programs written in this language and to be clear what's specified is not as a language is not solidity it's just the EVM opcodes is that correct yeah they're actually working on specifying solidity as well but what we're dealing with is a VM and that also saves us from the trouble of doing any verification of the compiler because we're only dealing out of like code who

is who is they so where does K framework actually come from it comes from mainly researchers at University of Illinois in urbana-champaign and then it's also being developed and worked on by runtime verification which is a company that is closely related to the University but it's an open source project that a lot of people are developing and contributing to around the world does Cardno have some stake in this are they working on this why why do I often hear Cardno and K framework used in tandem mainly because Charles Hoskinson or IO HK we should probably say has been

giving money to run time verification to do formal verification work generally but also specifically to help them develop their virtual machine for carbonyl cardona I was doing a bunch of form over application stuff in general and they're going really heavily into this direction which is they're doing some cool stuff Nathan yeah they pulled in like several big Haskell names since there are dev team which is interesting yeah they just keep throwing money at researchers this seems amazing not complaining I guess definitely not it gave us a bunch of good tooling for the K framework so I'm very happy about that so K framework the people who like it

seem to like it a lot why why do people like it so much well I like it personally because it gives a very clear conceptual picture of what a programming language is when you're defining a programming language in K you're defining it in terms of three steps I would say you specify the syntax in a way that closely resembles how you would describe it mathematically and be enough notation with some additional helpers to make it nice and accessible for everyone if you want to have some some binders or some parentheses or stuff like that they give you some helpers and then you define the configuration of your program which you can think of the States or the world

according to this program so if you have some variables defined maybe they live in some mapping somewhere or in the case of the EVM you have storage that is relevant to execution and you have the message sender which is relevant to the execution so really baking everything in the environment together under this notion of a configuration and then the last parts that defines your language is the rewrite rules which just tells you if you encounter a particular piece of syntax and your environment looks in a certain way how is the environment going to get updated and how is the whole term going to rewrites essentially and so that's one of the things that I think is quite nice about it that that as a

language it's aesthetically pleasing but perhaps more so from a practical perspective is the fact that it's written in such a general way that is very easy to experiment with writing new languages and understanding programming languages and comparing them to each other in a setting where they're all defined in the same way and then you get all of these analysis tools for them that's the main thing that I keep hearing is is the tooling around it is just so different and larger and then any other you know thing that exists like if you write some proof and for instance which is I guess the most

common one academically at least that's my impression you don't really get anything other than this proof and you know there's there's not much there other than just this program whereas with the key framework you can generate these compilers debuggers and Docs and like just generally like make Pleasant and ergonomic to use a framework so that that's like a common thing that I hear is it's all of the tooling around it it just makes the whole experience much better yeah the fact that they are pursuing generality first makes it really interesting and appealing to a large crowd of people especially if you have some sort of niche programming language like the EVM

but you want to analyze the way that people usually do a formal verification is that they write a bunch of specific tooling for the particular language that they are interested in and you get a lot of advantages by doing that mainly performance because you're tailoring the methodology of and improved heuristics for the domain that you're trying to target but having this level of generality is certainly very interesting as well do you you sort of mentioned before that you're and I don't know if I fully understood it but like can you actually analyze different languages like because you have to see them through this lens do you start to see like nuances in them do you like learn

something about them in that comparison yeah I think so you you learn a lot about what different languages can do how they deal with concurrency or non determinism you can compare them to each other in quite a nice way now this is not necessarily what you do when you're doing formal verification but if you're a programming language enthusiast then this is super nice so we just spoke a lot about the K framework but there are actually other frameworks or other products that you can use to do formal verification yeah really in order to start doing these verification efforts you need to define the operational

semantics of EVM as I mentioned before and there it's all about having completeness and one of the nice things about K is that is complete and passes all of the VM tests and general state tests that that make it as expressive as an aetherium client it's basically a client without the networking layer it is as complete as any client and then there are some efforts to defining the semantics of the evm and Isabel and hoe yuuichi was doing a lot of this work when he was still at the foundation and he isn't anymore but I think others are picking up that work and magic was also approaching completeness I don't know

where they're at right now but yeah a lot of people are doing different efforts and I think that's a good thing it's just that for now if you actually want to start verifying contracts and want to have a complete behavior complete specification of behavior and I think the key framework it is really the most comprehensive one is there anything else like that you would consider an alternative to Kay I guess people can make their own yeah for their specific program yeah and and people are I mean there's a bunch of efforts being done everywhere especially academics that are using their methods of formal verification that they've

applied to many fields throughout the decades and are now realizing that block chains are a saying and that a lot of people are craving what they have spent decades perfecting and so now they're adapting there's tools to target the EVM many of those tools aren't really out in the open or free software and open source it's kind of hard for us to work with them both practically and philosophically I think that's a lot of that's an interesting thing that I've seen similar things where a lot of quote-unquote newcomers to this space now who wants to build tools around watching they don't necessarily want to build block chains themselves but build tools around that their first instinct is to set up a company and have a

proprietary product that they sell licenses to and it's a very different kind of feel and different vibe to how things normally work in the bar chain world like I was talking to one company that was doing exactly this for formal verification I asked like what what of this is open source and you know how can we verify things and I even asked like how does this work and they wouldn't tell me because you know that's their secret sauce you know they came with a pretty big claim of like we can verify any such thing in super low time you can basically do it automatically on deployments like okay it sounds cool but how does it work I can't tell you and

it's like yeah that's that's a bit weird for the space you know I think they have some adjustment to do before that really kicks in or I don't know maybe we have to adjust more things being proprietary yeah this tended to happen to me a lot also lately when I'm speaking about for more verification at different conferences people come up to me and they're like hey we're also doing formal verification let's talk and then I try to talk to them and want to exchange some methods and ideas and really what they want to do is sell me for a mobile verification as a service and that's not that interesting to me so going back to what we were talking about before I'm just trying to really get my head around what formal verification and

specifically like this kay framework is because I think when we talked about it just before it was like as I understand it what you do is you'd write a program or dry to spec you write you do an implementation you'd use this language to map it and then you'd run tests on it and then at some point it does become sort of final and then you feel very very confident that this thing will work but the actual formal verification it's not a product and it's not it's a method well I would say that the actual verification is a proof that not less the result of it if I were to say the type signature of formal verification I would say that the inputs are the operational semantics of the language in

which you're writing your program the specification of what your program should do and then the implementation of this program and then the output is a proof that's the implementation matches the specification so it came for a framework for instance is a suite of tools and a language to you know let you write down the specification and and run the proof and you know all these other tools that also exist there languages or their specification frameworks only or their verification only like you can have symbolic execution you can do try to do an

exhaustive search type of execution and there it might not actually be a proof that comes out but like you said a confidence interval but in a proper formal verification Suites and then they're kind of different and live in the same space that's why I think this topic as a whole is so complicated to people and like they don't know what is in there or what is not in there but I think the definition you gave is it's perfect one formal verification is also being used as I understand in like other fields it's not watching specifics so where is it really big like what kind of applications do you see it in the world so it's quite big in areas where there's a lot of stake and you get one chance of

getting things right so this is the aerospace industry and airplanes and trains and some hardware components that might be super critical for you know a nuclear warhead I don't know a power plant if there is a lot at stake and if you can't just fix bugs in production then usually people are using formal methods to ensure properties of code something that I've seen that pop up quite a lot around is things like databases where like people started working out for a mobile era fication of the correctness of like PostgreSQL because basically every database in the

world now runs PostgreSQL so you know we won't have some assurance that it's not randomly deleting data for instance but it i've seen yeah like AWS Amazon Web Services they started doing a bunch of stuff back in 2014 and TL A+ so they've been at creating formal specifications of like the s3 simple storage service like high level protocol but they've also done it for like some of their databases and some like their networking stuff to guarantee that you can't talk between VP C's and they have a bunch of a6 to do networking like they're doing a lot of stuff and a lot of very cool stuff in

their formal formally verifying a lot of it as well so just lead so like yeah like a more reliable service and that's kind of what they why they're doing it they want to try to guarantee uptime and also if they actually have like a network breach between different customers that's that's like devastating to their whole idea yeah we're like I'm seeing more of it and I think we'll continue to see more and more of it I think it also develops as people understand programming generally better and this is something that is of course continually continuously worked upon by computer scientists and mathematicians to try to understand what formal

languages are and how to understand them and what properties were interested in verifying around them and develop tooling around that I think historically there's been quite a large disconnect in the theoretical side and the practical side a lot of people come up with really beautiful and elegant theories for how to state properties of your programs and they end up not being that practical and then conversely people write a lot of really practical ways of finding a lot of weird behaviors in their program but then in the worst case those methods can even be unsound because they don't have

a rigorous theoretical footing we haven't yet really talked about the projects that you're actually working on and what it means to be a researcher in this space so maybe you can share a little bit about that like what do you do every day so I've mainly been working on something called Caleb which is which can be understood as a debugger two proofs that you write in the K framework so it allows you to know where your proofs go wrong but it's also a little bit like a symbolic debugger for the EVM and it's been tailored very much to our needs so there if

smart contracts in in practice and it also has a convenience for writing specifications of smart contracts if we think of the K framework as a very general framework for analyzing programming languages in general we can think of Caleb at least so far as being as taken a key framework and optimizing and providing some nice features in order to actually apply it to the verification of smart contracts and that has all been developed in the effort of verifying the next iteration of the maker smart contracts and so we're doing two things we're developing the tooling

around that and we're also writing the actual proofs for those smart contracts what are those smart contracts written in we actually have right now two implementations we have a implementation in solidity and in solidity assembly over the course of the design phase of these contracts there was a lot of different languages that were experimented with and even writing handcrafted a VM bytecode was explored at some point or developing our own computer language that compiles down to the EVM that was called SiC that had a very interesting way of very concisely stating how storage should be updated

but now everything is being done in solidity the main implementation I'm also experimenting a little bit with Hough it's it's very nice I think if we can write smart contracts and house and formally verify them because then we should have really high assurances and really efficient gas costs Hough how do you spell that h uff it's written by the Aztek protocol guys it's like a nerdy EVM type of hobby program for some reason I thought that maker was doing some contracts and lll but can't remember who it is that's doing like a major thing you know lo which which is admittedly a very odd choice

but yeah weren't the ENS contacts didn't another well that might be maybe I had heard that the maker code again non dev here but I had heard that it was written in very like odd language I had is there something special about their code yeah a lot of people really dislike the variable names but so I think there are many various experiments that the development team has undertaking in order to really understand the core of what the contracts are and what they should do so there's been a lot of experiments in different languages and different ways to express the Platonic ideal of what makers should be and now throughout that exploration there's been

a really nice design that has come out of it a really minimal set of functions that really capture the essence of the behavior and and now the the actual implementation of those essential design components are being done in solidity plain old solidity with some interesting variable names I remember at one point a long time ago someone wrote a an EVM back-end for a dress and it was really nice to write smart contracts and because you had you know all the dependent types and you could do a bunch of cool stuff and get sort of a half way to formal verification by just writing

or program in this the problem was that the compiler output something so grossly inefficient that like even in the ERC 20 contract would fill up a whole block or something you know wasn't viable but like in your view what did what would an ideal smart contract programming language look like that's a very interesting question and first of all it would be nice if we move away from the EVM and don't have to worry about this as a compile target so already it was on things get considerably nicer and it's more realistic to do any of these nice things then I think we should have some notions that have apparently become quite important for smart contracts

as quite low-level primitive notions of a language like linearity and storage variables for example if you have a number at a location and you want this number to represent a value then you should have really careful ways in which you can actually change this number so that that the the quantity remains the same and there are some interesting projects that are working towards this I think something that I discovered recently that I think is this super interesting smart contracting language is called TX VM or there's actually now a confidential implementation called Z KVM it's by the people that developed

interstellar that seems to have at a very base level object capabilities so really rigorous tools by which you can specify who can access certain variables and and the ways in which you manage Authority and then also notions of linearity baked in at low level so language with linear types and a no cap model probably with dependent types as well and like i would add pure by default yeah that'd be nice I mean if at least we're interested in the behavior of programs all of those things make it really easy to reason about then again I recently developed

more sympathy for imperative programming because it's so much easier to reason about the resources that they use and if we're dealing with a system where resources are something that you can try to attack somebody by using up the resources then is really convenient to have languages or virtual machines where the resource usages comes out fairly directly in this I think this is an interesting like I don't see a lot of conversation around resource optimization from a compiler level so I mean obviously there are compiler optimizations but their optimizations that look like general compiler

optimizations but when we're dealing with smart contracts where we can do whole program analysis we can we can take the entire program evaluate it's a week at normal form and decide you know you know under calculus what this thing actually is the Haskell is like a terrible performance why so obviously the same thing with Idris and why you can't just put it back in like an EVM back-end on it because it's made for a generic platform he's not made for smart contracts and all program analysis it's an interesting thing it's something I think obviously as we move into was M world we will need a new like high-level language as well and both etherium and like every other projects moving to

awesome so it'll be nice if we could have one shared vision of what a good high-level language for a smart contract would be yeah definitely we just need a language for where we can analyze the resource usage the behavior of it and we want okay and we want dependent types and we want everything like this is is like utopian language that we all have been trying to figure out and husband also looks like JavaScript yeah but everybody can use in writing bug-free code for more verification as I understand it fits somewhere in the

security stack there's a number of different ways that you would check code form of verifications one of them do you think that there are times where it's being used where you think it's a little bit overkill where it's unnecessary yeah I think if there's not that much at stake then maybe formal verification is overkill when it comes to the methodology of assuring the correctness of programs you catch a lot of things with tests or these automated tools it's really just if you want the highest level of rigor and actually want this proof that your program always does as it is intended instead of just figuring out whether it might sometimes fail do sometimes people do it prematurely

because I imagine if you've designed this spec and you've mapped this out and then you're running these tests and then something changes you have to go and do it again or are you always kind of building alongside a project like did should the formal verification be there from the start or from the middle or does it come at the end I think the specification should definitely be there from the start I think you should as you are writing your program also say what you intend for it to do and then maybe you shouldn't start trying to format their verify that it that the implementation actually does that because you haven't figured out the complete architecture yet but I think writing specifications also help a lot

in the design so that's definitely something that you can do but then maybe the verification can come at a later stage once things start solidifying is it something that's continual or does it only happen like this being a process not something you do one time well you can for smart contacts if you have a mutable code and then you can definitely have some properties that you expect to always hold now there might be other properties that can change during the course of the lifetime of the contracts that you may have to continue to do it yeah I feel like in the in the blockchain space there's a lot more of one time perfecting things or trying to make things as good as possible and then

once you need to update things or if you ever do that is almost seen as a complete new variant of the whole system rather than an upgrade what's what's the future of form of verification so specifically for aetherium it's gonna be very exciting once we transitions who was them there are a couple of people I'm sort of monitoring the whole thing and not that closely involved working on implementing wasum inkay so that would be - awesome as KVM as to the EBM what i call it k wazzle and if anybody is interested in helping out and doing this

then this is a good point of entry and once you have that you'll be able to apply the same methods that we're using right now to verify EVM programs to verify EVM 2.0 or wasn't programs and this is of course nice because it's not only even aetherium specific this would be able to verify programs that are in the webassembly for any purpose and then there would need to be some tinkering to make sure that we can actually verify smart contracts written in wasum because that also look slightly different than than just pure was them so that's one thing and then in general you know we are always working on the tooling around

everything optimizing backends switching out parts and rewriting everything in Haskell who is who is we is it you at maker or is it a larger community I when I say we in this context I mean open source and free software developers what's the formal verification crew like it's um it's people it's well that's that's a good question they're very precise and are very good at arguing for their cases they share some tendencies with mathematicians and

some tendencies of mathematicians that I really enjoy is that they sometimes take a really long time to think about what they want to say before they say it one thought or curiosity I just had is when you talk about like ke V m and K was M and all these things existing your give to find the operational semantics can you use that to then formally verify the interpreter so can we get formal verifications of like the parody EVM implementation and the get EVM implementation not really that would be if we wanted to verify the clients then we would need to

instead work with the operational semantics of the language that this client is written in of course we can we can do other things like run test Suites together and make sure that we get the same result but I wouldn't call this formal verification right and the platform they're targeting is everything so it's kind of hard like it's arm and neck sixty x86 64 and everything else so yeah yeah but you can you can already say quite a few things about programs written in C++ or in Python or in JavaScript just by trying to understand the language as it is defined rather than the implementation of this language

in some lower level right machine code so it would be feasible and sometimes this is something that that we joke about when we speak about verifying a VM bytecode that we should really not be verifying a VM bytecode as according to ka VM or to the yellow paper we should be verifying a VM byte code as it is being evaluated by the clients so that means that we should have a model of rust and the parody clients and how the parody clients interprets EVM in order to really understand how parody clients will react to a certain smart contract but actually we just assume that they are reasonable in some sense yeah I

think that's an okay basic assumption but it does happen every once in a while that there are disagreements so there's actually a little bit of a movement right now in trying to make KVM into the canonical spec defining a VM so that the k vm would replace the yellow paper sometimes people refer also to the k vm as the yellow paper for some reason and then i don't really understand i think this is a great movement because really whenever i wonder something about the EBM it's it's a lot easier to look it up in the K definition of the etherium semantics then read it in the yellow paper and also the yellow paper has sort of drifted into this void were sort of

unclear who maintains it yuuichi had a huge part in maintaining the yellow paper and now it's not that frequently updated you know the difference is like the yellow paper is specified in English KVM is specified in K it will peel differently to different people I think we should have both I'm sort of torn on creating not yeah yeah maybe there should be one canonical thing that we all trust and then update the other things after that but I feel that it is important to have an English you know prose definition of it as well but but it needs to be a maintained and that's just hasn't happened in the past and I know one guy parody stepped up to try to maintain a better I don't know if he

actually has time and like yeah I know it's difficult to find someone who's actually willing to put in that kind of grunt work and you know there's been proposals as well that like every IP that modifies the EVM has to come with the updates to all the specs and all the sort of things to actually be accepted I think that's almost the way to go put it on the EIP creator to do the maintenance yeah I think a lot would be gained just from a major rewrites of the yellow paper to make it more accessible or more readable generally I mean it is good because it is very specific but it

really could have been written a lot nicer and still be specific and still be as as clear yeah I do see the value of also having an English specification or a logic specification and a bunch of formulas and it's kind of hard to say what should be the official or the canonical spec I don't know who has the authority to endorse something there necessarily needs to be one but all of them need to agree in some way yeah could you go backwards could you go from K framework interpretation to English yeah you could do this you could I mean the the case pack is actually written in literate style so it's a big

markdown document with some code blobs and so it is actually quite readable already in a lot of English already so I definitely I want to say thank you for coming on the show and helping us to explore this topic what do you recommend people do if they want to get involved so one thing that they can do is to get on the forum that I hang out with if they want to talk to me specifically which is that pub chat and if you want to read more about KVM or the K framework then I can provide some links for sure well put them in the show notes yeah cool thank you very much thank you guys and to our listeners thanks for listening thanks for listening [Music]