# Formal Verification of Smart Contracts and Protocols: What, Why, How (Devcon5)

- Channel: [Devcon](https://streameth.org/devcon)
- Date: 2020-10-09
- Duration: 1:32:07
- Topics: blockchain, smart contracts, distributed ledger, ethereum
- Watch: https://streameth.org/watch/yt-xggtkB7w3es
- YouTube: https://www.youtube.com/watch?v=xggtkB7w3es

## Description

By Grigore Rosu, Everett Hildenbrandt, Daejun Park, Shuvendu Lahiri

Testing shows the presence, not the absence of bugs” (Dijkstra, 1969).  Although remarkable progress has been made in testing during the last 50 years, exhaustive testing is still infeasible in most cases and we have learned, sometimes the hard way, that the remaining bugs can have catastrophic consequences.  

The nature of the blockchain, where code that accesses a shared state is public and can be invoked by anybody from anywhere, amplifies both the speed at which bugs are found by hackers and the consequences of their exploits.  Testing is therefore simply insufficient here.  Formal verification is the only known viable alternative.

This talk will explain what formal verification is in the context of blockchain smart contracts, tokens and protocols, why it is becoming increasingly critical, how it is done, and what tools are available.  Several approaches are covered, from automated and light-weight that find bugs to interactive and comprehensive that analyze all the behaviors, from high-level source-code that developers write and understand to low-level bytecode that is executed by node clients.  

This talk also aims to raise awareness that, contrary to common misunderstanding where formal verification is confused with code auditing, it takes significantly more effort to formally verify a program than to write the program first place.  Think 9x more!  Indeed, a rule of thumb at NASA is that 20% of a project’s budget goes into code writing and 80% goes into verification and validation; and NASA code is not public and nobody but NASA can invoke it once deployed.

## Transcript

So, I guess we can start. Thank you everybody for being here so early and have coffee. Um so, this talk with the with the seminar will be given by formal verification and Microsoft. Sugar is from Microsoft. And we try to give you a broad overview of what we can do with formal verification and then we'll dive a bit into our own techniques and approaches. But to set the mood for the for the seminar, let me start with a famous quote by famous person, Dijkstra, who said that program testing can be used to show the presence of bugs, but never to show their absence. Okay, so what that is telling us is that while testing is very useful, we cannot rely entirely on just testing if what we really want is to prove correctness of our of our program. To prove correctness, we need formal methods, which are mathematically grounded techniques to model and reason about about systems. And before we dive deeper into formal methods, I'd like to also share another quote by another famous person, Tony Hoare. Both Tony Hoare and Dijkstra are the same word which is the first word in the dictionary, but you understand. And he said that the job of formal method is to elucidate the assumptions under which formal correctness depends. Right? So, if somebody tells you that, "Hey, I formally verified or I formally modeled my system." What that really means or what it should mean is that they clarified all the assumptions under which the property they claim to be formal. So, this is overview of our presentation today. We are going to give an overview of formal verification and then we'll dive deeper into our approach based on the K framework. Then we'll show you some examples of how we formally verify for smart contracts and uh we'll use three different approaches that we want to put together under one umbrella. And then we'll conclude. So, what is formal verification? At a very high level, formal verification can be seen as taking as input a program or a system or a protocol, something that computes, something that evolves from one state to another and does something. Let's call that the program P. And a property or some properties or specifications, uh which are properties of this program P. And let's call that S. And what we'd like to know as output is whether the program P indeed satisfies the specification S. Uh, meaning that no matter how the program is executed under no under whatever input and under whatever environment and under whatever non-determinism that you might have in that program, the program will satisfy S no matter what. Or if you cannot prove that, then you'd like to have a so-called counterexample. You'd like to have some run or input, some environment in which P violates S. And that's very useful because then you can use to improve a program or the specification. The typical advantages that that we as a community know that formal verification has has are the following. So, the the Obviously, what you really want when you do formal verification is to be able to prove that your program is correct. But that depends a a on many factors, on what properties, what do you mean by correctness? Um and um in general what you really can claim is that your program doesn't have certain vulnerabilities post deployment. And those vulnerabilities are whatever you specify in your specification, right? If you forgot to say to specify a certain vulnerability, then uh the program will still have that problem. Right? In the extreme case, you can prove that your program satisfies a specification through for the empty specification and then you satisfy it, but it doesn't mean much. Also, formal verification helps you find very subtle bugs, um bugs that you haven't thought about when you wrote your program initially. Because formal verification will enforce to go through all the all the execution all the behaviors of the program and because of that, you will know when um um it will tell you when a certain corner case or um a certain case that you forgot about uh still lurks in your code. Also, it helps you It helps you focus testing and auditing efforts, right? Because if you have many functions in your code and you verify many of them formally verify 19, but you couldn't verify one of them, you know that you should look at that. You should investigate that more deeply. And also, if you use it routinely, if you use formal verification routinely, if you have tools and there are tools that you can use on a regular basis, then that can help you in your everyday development of your of your code. You start thinking actually differently about your code. You think of the code through the abstract lens of the properties that the code should satisfy and because of that, um you write better code in the end. So, that's uh that's probably one of the least known benefits of formal verification. What I'd like to do next is to go through the entire spectrum of formal verification or formal analysis or not even formal analysis tools and and technologies techniques and you can methods for your for your program. And I would like to use a metaphor, a dial metaphor, to present them. And I warn you up front that it's going to be very rough approximation of the reality. There is a an entire universe of research and work. I cannot cannot minimize all that in just a couple of slides. But I think it will give you an idea that you can go as deep as you want with formal analysis and formal verification. But at the same time, you can stay very light. And you have to find your right balance, where you think you should you should stay. So the minimum So if you turn the dial to the left, you get very cheap methods, but at the same time, very little assurance. As you go to the right, you get more expensive methods, but but also you get more and more assurance. So the minimum you can do and you should do is testing. And you should have lots of tests for your for your program. Ideally, giving you full smart contract even with coverage. In reality, in real life, in real software, full coverage is is is very rarely achievable, but in smart contract, that's not too hard because they are smaller. But keep in mind what Dijkstra said, that no matter how heavy you test, you are still not going to get any formal guarantees, any assurance of correctness. You have more and more confidence that your code is correct, but you don't know if it is correct indeed. So that's why we say that testing is the minimum. Once you have lots of tests, then you can move further and do what I call here runtime monitoring, that comes under lots of names. Some people call it runtime verification, others call it runtime assurance. Um there's lots of different names. So what runtime monitoring really, what I mean by runtime monitoring on this slide, is that you can run the program, but now observe its execution. Don't look just at the simple go/no-go relationship, if it passed the test or not. Look at the sequence of the behavior of the program. And you can monitor actually the program as it runs. And if you see any violations, then then you can report errors. An example could be division by zero, right? So, on EVM division by zero is fine, but you may not want to. So, then you can monitor for division by zero. Or other properties could be that you want to revert before the end of a function if you have an overflow during the function. Look at the sequence of statements and you can monitor that. And I'm putting it right after testing because it's um it's pretty easy to achieve once once you have a running system. Of course, you have to instrument your program somehow to observe what's going on, but that's that's much lighter than uh um the other methods later on. However, like testing, runtime monitoring does not ensure correctness unless you combine it with more complicated techniques like that. So, we're not going to go into that here. So, we're not going to go Further, you can do static analysis. Static analysis, there is a large variety of static analysis techniques out there, and I strongly encourage you to use any static analysis tool that you can put your hands on because they give you immediate feedback about your code that you can use right away to improve the quality of your of your code. So, static analyzers typically they scan your code and they look for known patterns. Um bad code, code that you shouldn't code, bad coding practices, or code that you should not write. Um and the advantage of static analysis tools is that they are typically very fast, you get immediate feedback, they show you where, they color your code to tell you exactly where the problems lie in your code. Uh the problem with static analysis could be that they miss certain errors that they are not trained for or they don't implement, or they may give you false alarms because they have to make trade-offs. You can never prove a program correct statically completely automatically. You have to make some trade-offs, and one of the trade-offs that static analysis tools make is to give you potential errors in your program. And then when you investigate them deeper, you realize that it's actually not a problem because I know what the program condition is at this point in time. So static analysis tools typically analyze the code, scan the code, but they don't go deep into the semantics of the programming language necessarily. If you want to go deeper into actually the semantics of a programming language, you do what we call symbolic execution. And what symbolic execution is, you're still running the program, but you run the program with inputs which are not known. If your function has two inputs A and B, you run the program with input A and B without knowing exactly what the inputs are. What is the symbolic value of B? And as you execute the program, you keep track of all the logical constraints and what's going on in the in the in the running program. And the advantage of symbolic execution is that you cover a larger state space or space of behaviors of the program. Essentially in theory, all possible behaviors. The problem now starts being that it doesn't scale. At some moment it will be very slow, or at some moment you will have to make compromises because you don't know when the certain condition holds or not. So if you want to make it automatic, then you have to again accept some trade-offs. And one of the trade-offs that have been combination with symbolic execution is what we call bounded model checking, where you explore all the program behaviors up to a certain bound. Let's say up to two iterations of each loop, or up to two recursive calls for each function at most. And once you put such limits, then you can explore exhaustively state space, but the problem is that you enforce yourself a finite smaller state space, which means that you may you may lose errors. If you want to be absolutely sure that you don't lose any behavior, then you have to go into uh into formal verification. And here I'm calling it state-of-the-art verification because this is what most of the people who do formal verification understand by verification, and probably most of the people also in this room, which is um the fact that you have a programming language, and that programming language provides some specification language, another language on top of your existing language, that allows you to specify properties of interest, and then your tool, your formal verification tool, analyzes all the behaviors of the program against those uh specified properties, and with some help, eventually you may be able to to prove maybe some additional things, additional lemmas, you may be able to prove the properties correct. Uh so, this is the conventional program verification, and I say conventional because um what you're going to see next goes beyond beyond beyond that. Um so, the limitation actually of of the traditional verification approach of of programs is that um you tend to be stuck with one particular language or version of your programming language, and one and more more importantly, one particular version of your specification language. Like you think that some language constructs are really important to specify, or some specification constructs like always eventually are really important, so you add them into your language for properties, but then later on, if you need something else, you're out of luck. You cannot the tool doesn't support that. Um Yes, you want to have to start going into into into deeper reasoning, a deeper analysis of your of your system, then you go to formal modeling and validation of your model, meaning that you take your program and you model it in some other system, a theorem prover or or or interactive verification environment, where you can now reason completely mathematically about your program, forgetting any programming language. You don't care about the programming language anymore. I can define the transition system in your more abstract environment, and then you can reason about it there and prove what the property is there without taking the code at all into consideration. And that's really useful because it helps you find high-level errors potentially in your in your in your code that may have been hidden in the actual code. So, when you are more abstract, you can see more abstract problems. For example, you can see design issues of your business logic, of your entire contract that that that So, many many people many customers we work with we take them through the various steps, and at some point they get to this point and they say, "Oh, actually we really wanted that." So, once you understand the value of of modeling, then you really like to go to go that path. But now you have a gap between that model and the actual code that needs to be filled. And this is what takes us to the to the final stage, which is um verification or proving your code correct using frameworks. All right, so you take a programming language a program in a programming language, and you have a formal mathematical model of what you meant to be implementing in your code. Now you have to prove that these two are that the program indeed implements the the formal model. And to do that you need another language, a language which can which can express both of these and do all the proofs. And you may have heard of systems like Coq or Isabelle, and the system that we use, K, falls into the same category. Right. So, as we go from left to right, cheaper, less assurance, expensive but more assurance. And ideally we would like to do all this automatically, but unfortunately it is not possible. There is only that much that we can automate. And traditionally we can automate almost all everything up to symbolic execution and even some part of symbolic execution, but when you try to go beyond that, a human expert tends to be needed unless you restrict yourself to very simple properties. But uh Yeah, so that's the general um uh picture that we have for program analysis. You cannot have anything um free or automatic. But nevertheless, you should use everything that is automatable in your contracts. If you are planning to do anything with high assurance, you should be, then you should use all these all these tools. So, what we intend to do today is to show you how we approach this spectrum of formal analysis tools uh from our angle. And our angle is the K framework. Um The K framework is great in what regards expressiveness, so with putting the right hands, you can do almost everything you want with it. But um on the other hand, many people find it heavy to use because of the heavy notation and uh and uh lack of automation. So, our challenge here is how can we automate as much as possible in what you can do with our with our language like K 1 like like K. And here we look at two types of automation, automation that we know about, things that we have done with K and we know that those can be done better and faster. Um and that's what we try to do with the Firefly tool, that's the average tool we talk about. So, basically Firefly tries to automate everything we know we can automate in K for smart contracts and verification of smart contracts. And then there is a lot of automation going on in the program verification community developed by decades of research by amazing researchers like Shuvendu here and and Microsoft research actually is a leader in in that field. And And what we'd like to do is to take advantage of all this automation, incorporate it into the K framework. And we want to do that by connecting the K framework with VeriSol, a program verification tool for Solidity contracts developed by Microsoft. Now, I'm going to go into more detail about how to how to do that. Before we dive into our own approach, I'd like to tell you that there is a suite of tools with a high degree of automation for formal analysis of smart contracts that you should definitely look at and try, which are not developed by us. Uh and many of them have talks actually uh uh uh in this Devcon. Like MythX and Mythril, I think they're not here. We talked at 10:30 half an hour. Um Slither by Trail of Bits, Securify and VeriX by Chain Security. All these are amazing amazing tools that you should definitely try try to use them, especially when when when they were uh out of the box. And now I'm going to go deeper into into our approach. Based on the K framework. So, why do we like the K framework? It's mainly because it it's it supports all languages. It's designed to work with all programming languages. And in particular, it works with all versions of a given particular language. Take Solidity, it does all versions the same the same way. You don't have to touch anything in the K framework to switch from one version of a language to another or from one language to another completely. And this is the philosophy or the vision underlying the K framework, that you should define a programming language once and for all. Have a formal language definition that includes syntax, semantics, everything. And everything else, all the tools that you need for that language, should be derived automatically or semi-automatically from that one definition of your language. That includes not only parsers and interpreters, but also symbolic execution engines, checking, deductive program verifiers, and everything. And all of these black boxes, blue boxes, are separate tools, but they are all completely language agnostic. Or put it differently, when you implement a tool, a formal analysis tool, or analysis tool for a language, you typically pick two things. You pick the language and you pick the tool. But then you develop a system, your tool, um which is hardwired now to that language and to that particular platform analysis. So, you have languages and then you have tools, and many tools pick one language and one tool, like Java or etc., for example. Right? So, what the K framework proposes is actually to not do that. It proposes to encapsulate all the tools and to make them all parametric in a programming language. And the programming language then can be formalized and passed as input to the tool. The tool takes the programming language as an And when we say programming language, we don't mean a translation of the programming language to some other intermediate language. No, just exactly the programming language it is. Uh so, that approach, we started working on the K framework like more than 20 years ago. And only 2 years ago we switched to a blockchain, and it was really easy to do because all we had to do was to plug and play blockchain language. Everything else stayed exactly exactly the same. And for Ethereum blockchain, we immediately looked at the Ethereum Virtual Machine. We didn't want to verify programs at the Solidity level at the beginning. We just wanted to start directly with the bytecode to eliminate potential errors in compiler in the compilers uh from the from the the trust base. And um and uh we had given actually Everette and other students, I know if they should go to the university, taking classes and and they said, "Oh, actually we need to develop formal semantics for EVM. And then we use the K framework for EVM." And that past project then turned into a research project, and then it turned into an actual product now. So, there's a complete formal semantics of the EVM in K. It's open source, everything we do is is open source. Um, and um, and um, it is complete uh, in the sense that we can run any EVM program with it. It's like a like a client. And actually we generate from the semantics number one of the blue boxes with the interpreter. With that interpreter we generate an actual client uh, EVM client. Um, um, and uh, and uh, it is pretty efficient or efficient enough you can use it for uh, for uh, actual real real work. In particular, it is uh, a bit faster than Ethereum JS, which is a JavaScript emulator of EVM in JavaScript. And it is only a few times slower than the C++ implementation of Ethereum. So that really makes it usable as an implementation, but remember it's just a mathematical model. The exact same mathematical model we use for verification without any gap uh, between the implementation and the verification. Also several people in the community use it use the EVM the K EVM semantics as as the canonical specification of the EVM. Um, and we have a website yellowpaper.org where uh, which website was completely automatically generated from the EVM semantics. And we generate it we update it each time we modify the semantics. And that's human readable. Uh, you can go and read it. It's uh, it's the canonical specification of the EVM. All right, and the Firefly tool that everyone will talk about is and as I mentioned it tries to automate what we're already doing in K, but in a way that other people can also use this automation, not only uh, experts uh, in K or formal methods. So it is an instance of the K framework with the EVM semantics and with lots of automation in various boxes and all under the hood so that for new users of Firefly it's just a push button technique. You just push button and you don't even need to see what this does. So, that's So, Firefly attempts to automate whatever is there in the K framework already, while the combination of VeriSol the invention here is to to build upon the legacy of successful tools developed by Microsoft Research. And many of you may have heard of C3, Boogie, Coral. So, all these amazing technologies are already incorporated in VeriSol. The problem is that there is a gap between what VeriSol does, analysis of Solidity level, and what we do with KEV which analyzes at the bytecode level using an actual formal semantics. So, what we'd like to do now is to connect the two and to regard VeriSol as a as a as a user-friendly lightweight front end that that generate all the verification artifacts that you need down there and to reconstruct the proof at the bytecode level. And this way you achieve everything you want to achieve, automation, a very small part of the formal semantics of Solidity and at the same time we have the formal semantics of the EVM. And at the same time And with that I'm going to to to let the actual people who implement the tools talk. And we'll start with Vishvendu give us an overview of VeriSol. So, thanks for coming. So, thanks for inviting me as part of the session. I was quite honored. So, um I work at Microsoft and I see some familiar faces. Um uh thanks to all the shout-outs to the research from Microsoft Research. I don't claim uh credit for any of them, but I've been on the engine room while these technologies like Z3, Boogie, and Corral Can you hear me? have been developed. So, I've been fortunate enough to sort of be part of some of these technologies or be in the engine room while these have been developed. So, um So, the goal was uh So, we had uh a team in Microsoft called Azure Blockchain and they started uh taking dependence on smart contracts. So, it was naturally quite interesting to us to see if we can help them. So, that's how the journey got started. And uh uh then we've been talking with uh Grigore about how to combine these two techniques and what's the landscape of tools and so on. So, So, what is VeriSol? So, the way I think of it is a formal specification and verification tool for Solidity smart contracts and it's a research project in my mind. So, um um There's the GitHub page. There are lots of collaborators from Microsoft, from Austin, and the coin set of collaborators from other places in Argentina and so on. So, what was the motivation for VeriSol? So, to me the motivation was that we need to empower the developers who are writing smart contracts for a living because there are as Gregori said it's a it's a very crucial important set of applications that you build with lots of security holes and you would like to reason about them not just for audit but also while you're developing so you have some idea. Uh and this initially started with the focus on the actual blockchain smart contracts that they were building for the infrastructure and also samples so we had some uh that was the starting point. And also as Gregori said one of the goal is to expose a lot of research that is sort of mature in the research community bring it up to developers with fairly well defined expectations. So it's not all of them are the most automated tools in the market but they have sort of an expectation that uh exactly what is expected of them. So um So these three many of the many of the tools uh use Z3 for symbolic reasoning. Boogie is a state-of-the-art intermediate verification language so instead of as as K it's uh it's it's a different flavor like it's a verification language that you can map different languages. And Corral is a push button interprocedural checker so it's completely push button scalable driven by the assertion that you want to prove not by the number of paths in the program. And there's a lightweight but very predictable uh inference of annotations when you don't have all the annotations. And also I I try to focus a lot on the research community look at more And as I said this is these are not the most optimized for the purpose but they have a sort of well defined expectations. Um I've been fortunate to use some of these tools in production in Windows and uh I have found lots of bugs. Um People have used it in the static driver verifier which is shipped with uh the driver verifier so these tools have a history of being tested in production. And people are taking dependencies on these tools. Um so, I will go ahead and give a few examples as I go along. And then we recently released uh uh dot net global tool. So, you can try to install it at some point. That would be fun. And I have a set of examples that I going to walk through today just to give a flavor of what the tool looks like. We'll start with the Dow example. It's most famous and notorious. So, uh So, this is the Dow example. So, this is the notorious Dow example. And we all know about the reentrancy bug. But let's say you're just rewriting the Dow example and you knew nothing about reentrancy. So, what is it that you were looking for? Let's say a language that doesn't have reentrancy. What is it that you should be thinking about? So, here's one example that says that uh well, there's a withdraw method that is responsible for withdrawing funds from the balances of the account. But I guess one of the invariants that you want to preserve is that no matter what the contract is, what you want to say is that if I call withdraw, then the sender should not withdraw more than they have in their account. That's That seems like a natural specification. It should be equal, ideally, but I'll show you examples where it actually can uh equal equality is too strong. Because uh an attacker can actually go and donate something to the user. What this says that roughly that anybody should not get more than the money that they want. So, you write the specification. So, it uses some code contracts libraries that it supports. So, it uses mostly Solidity syntax and shows that all of the new things are there. And then So, I have the bug in there in line 27. And then So, it's a command line tool right now. And it tries a couple of things. It tries to get a proof first. And if it doesn't find a proof then it tries to look for counter examples. So, in this case, it sort of gives you a counter example that says you have to call the constructor with some arguments. Then you donate because without donating you cannot withdraw. So, you donate. And then you withdraw all the withdraw methods, right? And then the assertion that we wrote down fails. And uh uh for uh Unfortunately, only for Windows at this point, we have viewer that can help you debug through the tape trace. I'm not going to show it. But you can actually step through the trace and see values as they uh So, you can see values printed along the trace just to get you a better sense of what's going on. Uh So, that's the experience. And uh uh So, I'll go ahead and do the fix, which is uh you update So, basically if many people know we basically update the credit of the sender before we uh So, before we do that So, in this case it actually found a proof. Meaning that uh this doubt will be able to satisfy the property that we wrote down. And the interesting thing is uh the detail is how do you model the adversary? So, we have a notion called callback where the adversary can call into any of your functions. So, with that with that model we have a proof. So, this is sort of the experience. Um So, I'll show you the ERC20 something that So, this is sort of I guess many people are familiar with ERC20 token. This is the one from Open Zeppelin with sort of modified a bit. And uh the thing that we're trying to reason about here Right, again the question is what do you what do you do with the token? Once you design the token, what do you look for? So, one nice specification uh is that uh the total supply that's in the token should be the same with sum of all the balances in the in the of all the addresses. And that will sort of get a good mental model of what what an internal invariant is. And if you show this to a customer, they might say, "Okay, this looks reasonable. I If you can show this, maybe I'll trust you for that." And so, the thing I'm going to show is uh So, up here That's the dummy. I'm sorry. So, this is the method called transfer. And interestingly, OpenZeppelin doesn't check for uh when you send an amount, the the sender has to have that much amount. And the reason it doesn't because it relies on the underflow semantics of the safe math. So, the safe math is safe. Because if you don't have enough money, the safe math would fail and then you'll abort the execution. So, how do you find that without knowing the internals of safe math? So, the invariant that I wrote down if you change the safe math to a regular subtraction, then So, again, it refuses to find a proof. And it calls you uh it shows a counter example where you try to drain an amount one from somebody who did not have any any any credits in there. And uh And this is interesting because it requires you to reason about sort of underlying semantics of arithmetic. If you don't If you're not careful and don't use modular arithmetic, you might see a proof where it does not exist. So, this shows basically various levels of abstraction you can reason at the kind of guarantees you can get. The modular arithmetic is not a very scalable solution. So, if you try to use it for other line programs with lots of deep invariants, it will not scale. So, you have to choose, but you sort of set up an expectation of where you want to invest. Okay. Um I just want to show one more example um which is an example from uh uh this tool called Azure Blockchain systems that Microsoft was one of the products that Microsoft shipped about a year back, something like that. And it had a very nice way to decompose a workflow policy. Many They realized many uh smart contracts implementing some kind of workflows. They're getting very very popular in uh in the enterprise scenario. So, they provided a nice language, uh a JSON-based language for clear semantics of what a workflow looks like. And then the question is does the Solidity program implement a workflow? Can you make it full screen? So, people can see. Yes, thank you. Right. So, here is think of this uh specification language with a bunch of state machines and actions and then some access control and there's the Solidity smart contract. And the question is whether uh the smart contract defines the state machine. Um So, in this case it turned out there was a discrepancy in It turns out it was in the specification, but nevertheless there was something that was uh different in the two two versions. And so, this requires sort of a very deep analysis because you have to take uh up to seven steps to reach to this state, right? So, shallow execution will not be able to get to this point. So, this is I'm going to show this example. Um So, in this case it did not find a proof, but it takes a little while to actually find a counterexample. But still, it's reasonable, it's a few seconds, but it just shows you the complexity of the search space. So, since this is assertion guided, it can scale a little better, but of course it has its limits. You can see you have to issue one, two, three, four, five, six, seven transactions to reach this. So, people in testing have might have missed this. So, Um okay. So, So, getting back um What's the time now? 7 minutes. Okay. So, it shows you the flavor of verification. So, for this one, for example, if you just want to do a push button verification, you have access to this for all. If you want to do proofs, you can write ingredients and uh interact with the tool. Um But, the nice thing we've observed is that the way the smart contract is kind of nice in that the open environment of adversary makes it easier for the verification to go through in many cases. Um so, that is actually a nice thing. So, the infrastructure for Verisol looks like this. So, we have a Solidity program with specifications. Uh for specifications, it includes this uh code contract library uh that is available. And uh I call it code contract because it's sort of the Solidity syntax. You get the resolution from Solidity. You can get syntax errors in the specification directly from the compiler. And then we're working on uh translating the subset of Solidity to Boogie that is very reasonably high level. So, we're not going to try to do deep verification about how data is laid out by the bytecode compiler. That's something that KeY does very well. And that's something that we try to model high very hard to automate at the bytecode level. And it also sort of tries to do what the compiler is doing. So, here the reasoning is much more abstract level. Which I think is good for business logics that we see in enterprises. Um and there's a host of tools that we rely on um which are being extended by us, by the community as they feel the need. And so, the outcome has three uh outcome. It has a proof or you can have a trace or in the middle you have something like well I've not been able to verify it fully or find a trace. But I have this uh guarantee that any transaction of depth K any set of transactions if you issue up to K transactions then I'm going to give you some assurance. So this gives you a a reasonable uh a guarantee to give me stop testing and formal verification at this point. Okay, so the way it works is it takes a contract of think of this small contract with constructor and bunch of arguments and then creates this uh driver of the harness that sort of in a in a infinite loop calls any of the natural numbers uh in in a with arbitrary arguments. So you can imagine if you can verify something of this program you've verified it for all executions. Uh Right. So the capability at this point is the core contract library. And we've consciously taken the decision decision to start with a known language so developers can uh understand them without uh under- needing a whole bunch of uh sophisticated semantics of languages um Our initial customer with the folks in Azure blockchain who are uh uh systems developers but they sort of understood the specifications at least to some level. And uh so we have a scalable push button button validation violations and highly automated two season Boogie. And by highly automated I don't mean completely automated. You can need might have to support some extra facts on the side. Um so that's sort of the research problem is how do you lower the boundary? And so we uh uh uh did start with some of the study on how we workflow policies, the example that I showed. And also check some critical infrastructure that were being used in smart contract in some of the products they have services they are sharing. And this is sort of the governance protocols that underlie these uh things like Ethereum and Azure or Azure blockchain service. So, basically they have implemented some of the governance and smart contracts in Solidity. And so, it's very crucial because any bugs there might just compromise the entire infrastructure. And so, you have to ask questions like can I get into a deadlock? Like can I remove the last administrator so that now no one can fix the issue? And usually the work happened as like it happens in K, you consult with the designer and you come up with specifications, do boundary checking, and then come up with invariants, and you repeat them while the code is being developed. So, we were very fortunate that we could actually do this while the program was being developed and tested and found bugs and all that. So, that was a very nice experience and I think that's uh would be nice to scale up such kind of experience. So, that's sort of the goal of the VeriSol tool is to take it from research prototype where we have a few customers to what help more people try to get a sense of the technology and uh enable the community either directly or like collaboration with folks at RV and uh So, I'll mostly gloss over the specifications that we've been adding to the whole contract library is evolving. So, we need to keep checking back in a few months maybe to evolve. But essentially, these are sort of well-known uh well-known facts that you that are necessary for doing any program verification. These may not be sufficient. So, pre-post pre-post conditions, smart contract invariants, loop invariants. And the contract invariants can mean various things to various people, so you have to there's a spectrum of what it can mean. And uh so it's it's a library and then you have uh stubs for uh people's conditions. So for example, you can call the metadata of contract invariant requires and ensures invariant and and I know there's a work in the Solidity compiler on supporting some of these specification primitives, so we are sort of we we've been watching to see once they come up we can sort of leverage some of that and uh so it's not tied to this language in any way. This is just a way to expose the the facilities to developers. And then again, once you have a social network you need to reason about the old value and uh mappings uh so the example I showed in ERC practically really need to say that. Total choice total supply is equal to the sum of all the balances and that's very hard to do uh in in the code because you cannot even write such a specification uh because mappings don't allow uh iterating over all the indices and so on. So so there are some things that is uh really going to a lot of value to specifying it uh and even doing bounded checking. And then we're working on other extensions uh uh part of the talk that we had in the are these what kind of stuff. So they have a lot of experience in the contracts and the low-level specifications. So what are the good uh high-level reasoning that we can apply to the question. So next 3 to 6 months we have a bunch of bug fixes covering the Solidity. So the reason I said high-level reasoning, I don't think we are going to go have uh the parts of Solidity that require uh like low-level reasoning. That is not to scale very well. And uh at the higher at the at the SMT level. So if you want automation, then you have to sort of carve out sort of high-level language. What I've seen in the enterprise, people don't really care about Well, I shouldn't generalize. Um they're happy to live with a fragment that they can be more sure of. Probably they don't care about optimized gas. So, so there is a hope that a lot of the reasons can be reasoned to high level. Um there's a VS Code extension to make it easier. And then going forward uh this the discussion we're having is what kind of applications can we add beyond like assertions, temporal logics, and there are a lot of researchers in our community also are doing how to improve the main difference, how to give users more control of how to eliminate difference, and and through the grand challenge, how do we push these tools all the way down to bytecode? I think that's a very very interesting problem that will require research. So, yeah. So, with that I'll conclude and There are no questions from anybody. Yeah. Questions? Yes. So, I'm I'm sorry to interrupt you. Did you describe Do you use K as the back end? No, that's the future plan. It's Once you have a proof at the very small level, we'd like to convince K that it can actually uh holds at the bytecode level, right? So, that is the That is the long-term goal. I'll talk about that as well. Are you considering to have a Linux version for the There is both a Linux and a Mac version of the tools. Yeah, you can download it now. It's not the visual answer to the same. The visual answer Somebody has to go to the visualizer. The left of the tool Yeah, there's a new strategy to use the tool. Yes. I am going to work on formal verification of consensus algorithms. For instance, of what? Consensus algorithms. Consensus algorithms. Yes, we are going to go and talk a little bit about that at the end. All right. Um, let's get started. So, I My name is Daejun. Um, going to talk about verification of the EVM bytecode. Um, with more focus on the case study of ETH 2.0 deposit contract we recently verified. Uh The title is contains verification, but I'm not going to talk about the verification that too much because already uh we talked about verification. I'm talk about more about the bytecode. So, those of you don't know about bytecode will learn something about bytecode. If you know a little bit about bytecode, you will find this interesting. So, before uh going to that, uh let me give a quick overview of our bytecode verification tool. So, we have the EVM bytecode verification tool that builds on top of the K framework and K EVM that we call And this tool has two inputs, um program bytecode and a specification, uh and it checks that the program satisfies the uh the specification or not. Um, this is very similar to VeriSol at the high level. The main difference is that it works at the bytecode level. Um, why the Why the bytecode level uh better? I will talk about it a little bit later, but let me give you a quick example how this tool works. So, this is the program, very simple program that similar like ERC-20 transfer types of program. We have the receiver address from sender Sorry, from and to and value. And update balances of the from and to using this same pattern. So, it If any underflow or overflow exists in the contract. So, given this program, you first compile down into the bytecode. You put in the bytecode into our tool. And then that you have to write down a specification. Which which specify what the behavior that this program should have. So, here we are describing here the behavior of the program in the success case, which means that if the balance is enough, I mean, sender's balance is enough, and there's no overflow happens, then the balances will be updated as like proper way. I'm not going to too details about how this specification uh mean details, but the thing is you have to write down the specification at the bytecode level in this way. And some people say that wow, specification is longer than program. So, yeah, and and this is why what Gregor mentioned, it requires more network to write down the specification and also working at this level. Our future goal is to let you just write down the specification as annotation language like ensures and requires for pre- this transfer function, if the two pre-conditions satisfied like balances is enough and no overflow happens, then the post condition means that whenever this transfer returns safely, I mean it comes through whatever it was not but if balance is should be updated as expected. So, if you write down this specification at the high level in the source code level, our goal is automatically generate this I mean bytecode level specification, so you don't need to work on this level. Um but that's the future work. We are still working on that, but we are hoping that uh provide this feature. So, using our this tool, we verified some high profile smart contract. So, very recently we verified 2.0 deposit contract that I guess you will learn more about this in the later this E 2.0 uh talk. Uh but the main thing is that this contract is really important contract when you want to be a validator of E 2.0 because you want you need to deposit your some ether to be validator. Sending your deposit into this contract at the E 1.X and then this contract is one-way function, so you can deposit something but you cannot you cannot withdraw. But the deposit whatever made here will be claimed in the E 2.0 uh network. So, it's really important first to make sure that you cannot even withdraw. The second, whatever you deposit here will be available in the E 2.0 network. So, it's really important contract that needs to be correct, so we recently verified this. And this is our case study. I will I will show you what we found while verifying this contract. And we have other contract like Gnosis Safe. Um I think is it Oh, yeah. Uh yeah, it's than signature wallet. And uh we also I mean the maker dial is still recording or still by using our K verification tool, but not by us, by them guy. So, we are very happy that our tool is used by another to verify their own system. So, we are hoping to more people using our verifier to verify their system. And then that's why we are working really hard push ourselves to more much more easier to use our tool. And that's the more or less the Firefly opening final talk. And then we have some other bunch of the smart contract. And now I'm going to explain why we are really obsessed in this bytecode level verification. The first reason is the bytecode is what really runs on the blockchain, not the source code, right? And then compilers, believe it or not, have bugs. I'm not talking about the Solidity compiler, just uh uh I mean usually compiler, even the C compiler like GCC or LLVM, which is really mature and developed long period of time, has bugs. New bugs reported even now today. And some bugs actually hidden in for 20 years. Simply some guys unlucky to hit trigger the bugs hidden for 20 years and they didn't notice. So, compiler has bugs, actually more than you expected. So, the thing is even if you verify your source code is correct, if compiler has has a problems, then that doesn't mean that the quotient verifier, the using verifier verify thing, it just assume that compiler is correct. If that's not the case, then your verification is does not actually guarantee what you really want. So, this is really important. That's why we are actually working at the bytecode level, and indeed we found some issues that if you input the bytes contract while we verify the bytecode level, that's I'm going to talk about. So, before explaining what bugs we found, let me give a very quick uh background of the how to read the bytecode. I mean, how to arrays. So, okay. Suppose you have a bytes arrays like length two words, 32 33. How that represented at the EVM level? The single byte is not represented as a single byte. It represented as two words, essentially 64 bytes. So, essentially uh is each line uh 32 bytes line. The very first 32 bytes denotes what the size of this byte, which is one, that's 0001. And then you have a actual byte data, one byte, and then followed by zero bytes. So, 31 zeros. If you have a a byte of two, then again, size two there, and then two bytes here, and then zero bytes, and so on and so forth. Um if you have a 32 bytes, you know, it's already aligned, so so you you don't need to have any zero bytes there. That's the how bytes arrays are represented in the EVM level, and if you have a tuple of bytes arrays like arguments, uh or if you return something, then they stored as a tuple of the bytes. And then if you have a for example, two uh tuple of two bytes array, then you simply put this these guys, put these two, and then you put on top of these simply offset. But this offset are points where the each element starts. So, since the offset is simply fixed, so if you want to find some first or element offset, that's element, you find that you go to the offset, find that byte where it start, and you read the size, and then read from here to the size. That's how you decode or encode this byte array. That's all you need to know to understand how it works. Okay, so first what we found is the balance contract. So, this is uh one of the function in the balance contract called get the balance count function, which simply just return some Oh, by the way, this is a Viper. Uh those of you not familiar with this Viper, it's similar to Solidity, but simply Python each syntax. So, you can I guess read. Uh so, it return this deposit count, this storage value, but in the little Indian form. So, simply uh uh reversed bytes. So, whatever Okay, so assume that this little Indian is simply correct. Then those of you think that I mean any problem in this simply too large for you. How could it be wrong, right? I mean, assume that this is correct, right? Assume that this is little Indian is correct. Can you think about something's wrong with this code? Yes? So, when you shuffle it around, then you cut off to get the bytes eight, you might cut off the wrong data. Uh that's that's very good um guess, um but that's somehow handled by very well this little Indian. But yeah, very good. Yes, that's right. It's Yeah, I'm sorry. Actually, I tortured you because I you cannot get this because because it probably happens in the compiler. By the compiler. So, this is the return the uh value when you call this function if this contract compiled by Viper version 1.0 beta 11 which is the latest version at the time we started this project. Can you see any problem with this? Uh if you follow me the previous preliminarily Yeah. Uh Yeah, it uh the the when you add it Right. This needs to be always zero, but here we see something is non-zero there. What happened? What? So, what really happened is that so, compiler Oh, first of all, don't worry about it. It's already fixed. What compiler does is that they when they compile this period, they need to prepare this data in the local memory and then they return. They first write down offset, this is correct, and write down this size and then they copy this the body count body count and then they need to be put all the zero like this is eight bytes, so 24 bytes of zero there. But, somehow compiler thought they only need to put the zero only eight bytes. They leave whatever this 16 bytes there and the problem is this 16 bytes of the local memory garbage came from this function. Um side effect. So, there is just garbage there which is non-zero. So, um So, this is the the example of the compiler bug. And then you cannot find this unless you work on the bytecode level. And And then, I mean, if you develop I mean, if you develop foundation by down this code, there's good job and no problem. But, just deploy this without this verification, right? And then, you have this non-incorrect zero bytes. And then, somehow the another contract that assume that it's expected that it's over zero may be exploited by some attacker. But, this is a real thing. That's why we really think that that the bytecode verification is important. Um I have a another um which is more interesting. But, I will not But, I will not Okay, let me put very quick. So, this is a main function, the party, as you see. The dispatch function takes now three arguments. All the bytes array. And then, they check that the length is whatever is passed in. Now, this is the uh tuple of three elements, like offsets and and the uh three arguments. Now, what if this call data input is not valid? For example, like by mistake or maliciously uh uh corrupted. For example, like there's no actual bytes, only these six words. So, this is a record one, 12 words. What if you provide only six words? You might think that oh, there's no bytes, right? You have no data. So, data length is zero. So, but now we have a length check. So, it may debug, right? Right? But, what will happen is this is a counter example, simply 6 bytes. Offset 96, 128, 160, and the three size like 48, 32, 96 taken from this uh size. And then no bytes. This is all. And then given this, the default function simply go through. Doesn't it work? Let Let me explain why. First, you try to read off key, so the first argument. The first offset it goes the this this is a start of data. Then you read the size. Oh, size is size is 48. So, you you read 48 bytes. Simply starting from here to here. And they simply decode. Consider this garbage as a off key. Move on. Next, you go to second offset, it goes this, and its size is 36 and 32, and it simply read this guys, which is actually another size, another garbage Even more, now starting third one, you go to third offset. It points this, you read the size, which is 96, and try to read beyond the code data, this 96, and what really happen is the yellow paper of uh Ethereum Virtual Machine says that if you want to read something beyond code data, you read that as if infinite zeros are there already. Means that it simply when you read this, simply out of bounds access simply return all zeros. This is what happened. Given this invalid code data, the decoding process simply read three arguments, all of the garbage, which which I am missing is all zero. You cannot claim later in in 2.0 chain whenever you are depositing. So, if you if you make any mistake or somehow manages to use your somehow uh flip the bits in your call data, then you have this. But, this shouldn't happen. But, previously, simply they go through and deposit this wrong information, and then you simply lost your So, again, the story is it's really important to work at the bytecode level if you want to full assurance of of your smart contract when you develop. And then, so far, we are using our K tool, which requires some effort and then some really effort. So, so far, actually, the large group like Ethereum Foundation or some who can afford this large effort can use our tool to verify that. But, we are really hoping that even small startup can use our tool to fully guarantee the of their smart contract, and that's why we are working on this uh next step of Five out. Any Any questions about the future slides? Quotation? So, concerning the first issue, Yep. so, the the non-zero bytes and they affect the correctness of that that um then uh of that call specifically because it sounds like uh did they affect the correctness of that call? Yeah, first of all, this is not ABI uh standard return value. The ABI standard specifically says that if you have a picture um non-aligned return value, you need to have a full zero bytes. And then, that ABI is simply like protocol, right? So, whoever who called this that contract would assume that there is a there are going to be a zero bytes. If somehow they exploit that fact, like they just just copy those into another local memory, assuming that all is zero, may have different behavior. But this is a promise, right? I mean, you need to return something, you need to follow some rules. So, yeah. That's all. Thanks, Dejun. Dejun had some more interesting slides after that, which I'm bummed we didn't get to, but you should ask him about it afterwards on some of the formal verification stuff that he would get. Um okay, so I'm here to talk about Firefly, and this is our attempt to take uh EVM, which is kind of hard to use, uh and wrap it up into an easy-to-use tool that kind of just works in the background and does everything in automated fashion, um as opposed to now, where you basically need a tool to even use the the K tool at all. Um so, this is an overview of my talk. First, I'm just going to talk briefly about the motivation of why we'd want something like this. Uh I'll show you our road map. It's stretched out over about 2 years. Uh and then I'm going to talk about the individual tools that are on our road map, which we have prototypes for all of the tools except this last one, but the road map is still spread out over some time so we can do testing and internal stuff like that. Um As a motivation, we have tools like Verisol that are easy to use. They're high-level. They're at the Solidity source code level. Um and developers can just basically use them out of the box. Uh Um but the problem is is Dejun pointed out, you don't get the guarantees that you would want at the EVM bytecode level. Um but then we have KVM, which is a low-level EVM bytecode verification tool, which really takes an expert to use. Um and somehow there's not something bridging the gap between these two. So, that's what we're trying to try to do. Um so, ideally the ideal scenario for Firefly is that it's going to be a drop-in testing client replacement for whatever you use as your testing framework. Right now, we're kind of targeting Truffle. So basically just replace Ganache with Firefly and then you're off to races. Um, and just a couple more bullet points, but yeah, one goal no user intervention required. It should be that you just run the tool instead of your normal testing tool and it does the extra analysis and reports the results back to you. Uh, another goal is easy for us to roll out more features and reporting over time. Uh, and then another goal is easy to dispatch large jobs in parallel to a server somewhere. Uh, so these are kind of some long-term goals of the project, uh, not specifically tied to any of the actual tools we're developing, but we'll we'll develop the tools with this in mind. Here's the long-term road map. Um, you can see it goes out to December 2020. Uh, I'll talk about these ones which are part of the Firefly suite a little bit more, but then they're on the right-hand side. Uh, beyond Firefly are where we get back into where you need a formal methods expert present again. Um, and we are doing some kind of prototyping of these tools out here. Um, so specification generation instead of having to write down a specification and verify your contract, we'll generate it for you. Uh, and proof obligation generation is basically the highest level of assurance that you can get with, uh, with anything formal methods. Um, usually usually not done except in like the most, uh, safety critical sorts of systems, but we're, you know, we're toying with the idea of moving that direction. Uh, this is our more specific Firefly road map. Uh, we have K set up so that we have like a front end which basically takes the K specification and translates it into multiple back ends. The LLVM back end is our fast interpreter. So whenever we talk about the performance of K compared to other things, we're talking about the LLVM generated interpreter um, for the for the K specification. And then whenever we talk about symbolic execution and proving, we're talking about the Haskell back end which is the one that actually does the proof steps needed to do symbolic execution. Um, I'm going to talk about each of these tools in a little more detail, but we're starting off with just a test runner. You just basically replace, you know, Ethereum JS VM with KVM, and then everything looks the same as normal from the perspective of, you know, running truffle tests. Test case coverage reporting is next. That's what we're working on right now is kind of integrating that coverage report data back into the truffle. Runtime monitoring, which is like bounded model checking V1, um, and then assertion violation checker, which is where we're going to actually integrate with the Verisol tool to get kind of an assist from them. Bounded model checker V2, which is where we're going to do it symbolically and exhaustively, and as opposed to here, which is going to be concrete and only on the test cases that your your actual tests exercise. And then finally at the end is test case generation. That's the one tool we don't have a prototype for yet, but we will will get there. I'll explain why that's important or why it's nice. Maybe it's not important. I don't know. It's probably important. Yeah. Um, Okay, so the test runner. Basically, what we're doing is we're taking KVM and we're making it into a full client kind of full client functionality so that you can just use it anywhere where you would use a full client for doing testing. So, we're just going to support the web3 JSON RPC, and we already have it to where you can basically just run truffle tests, but where you're running the KVM server in the background instead of running the Firefly server in the background instead of running an Ush, and it just works. Um, benefit of that is you get kind of more confidence in the test results because KVM is kind of regarded as a canonical spec of the EVM, and it's one of the canonical specs. So, I mean, some people like that. Take it or leave it. And then performance is comparable to Ethereum JS VM, but we actually have several performance enhancements coming out that are going to make us faster than Ethereum JS VM. And then we have just kind of special purpose Firefly under guard web3 JSON RPC commands for getting back reporting data from GVM about you know coverage or analysis like the runtime monitoring stuff like that. So, um Yeah, so then uh So, this is this is just like the bare functionality. You need this exists right now. Um but the but then everything is going to build on the fact that okay, now this is just a drop-in replacement. You can switch over to using it and not really notice any change and then we'll start rolling out features. Um So, the first feature we roll out is just a test coverage. Um we're specifically going to have our opcode coverage. Um so, here's an example of a report that the prototype spit out. Um and you can see there's kind of this this place after this jump by that's not tested by anything. Everything else is tested by 73 different tests, but these are tested by zero tests. That's a hole in the coverage uh data. Um and so, as a developer, if you were to see this report, what you'd want to do is you'd want to say, "Okay, where is this code coming from?" So, you use a source map back to Solidity and uh write a test in your whatever testing harness you're using, Solidity tests or or uh Fire I don't know Fire Monster. Blanking on Truffle tests. Um I swear I know the word Truffle. Yeah, so write a write a test that targets these lines and then uh you would add that to your test set and then the coverage report would come back green saying, "Okay, every every opcode at least is covered." Which like you know, there's a lot of literature about whether you know, opcode coverage or branch coverage or path coverage or something is the correct thing to do, but at least this is something. Um by the way, there are tools that will do coverage already. So, if you look at Brownie, that's a that's an existing tool that will uh do coverage already. So, common pitfalls in tests are you know, you might not test something like the default or fallback function, right? You might only write tests for the positive cases of your contract where things are going smoothly. Um So, you don't write tests for the revert cases. You might not write tests that actually exercise the underflow, overflow. Um And then uh you might not even test the ABI decoding because at a solidity level the ABI decoding is not apparent or obvious at all because the compiler takes care of that for you. But as Dejun pointed out, if you assume that the compiler is doing it correctly, you could um you know, lose all the ETH 1 funds when you're trying to move over to ETH 2. Um I guess so. Okay, so then the next uh tool on the road map is a runtime monitor. Um So basically what the runtime monitor is is we instrument the semantics with uh specific events, which basically can fire on any particular data from any particular point of execution during uh during running. Uh the events that I have here as examples are overflow and revert in this example. So overflow we just detect, you know, are we doing an addition and the addition overflows or are we doing a subtraction and the subtraction underflows? Um and revert is just that the revert opcode uh fires and then I'm making like a little state machine-ish thing here saying, you know, if we're doing execution and neither of these events are firing, we're just in this normal mode. If execution ends, we we go to this no violation found mode. But if an overflow event fires, then we know that we have to revert and if we end without reverting, then it's a violation. Uh but if we end uh with revert right here, then there's no violation because the overflow was followed by a revert. Um so these properties are are temporal in nature. So it's not enough to just say there are no overflows because it's pretty common that you will have an overflow during execution, but you have to instead say temporally, every overflow is eventually followed by a revert before the end of the contract. Um So we're just going to build these events directly into the semantics. Um and you know, users can supply more if they like, but then the semantics has to be recompiled. But the uh the properties themselves to check like this formula right here can be specified on the command line at run time. So, we can We'll provide a preset bag of properties. Users can write their own properties. Um And then basically, we're just going to run the the user's normal test sets. You still just run Truffle test, um but it runs it with this instrumented mode where it will check, you know, are these properties violated on these test runs? And then if it finds a violation of one of these properties on this test run, uh the user can inspect that violation and write an actual Truffle test that would have caught that violation anyway, uh so that you don't have to rerun this tool to get the same guarantee. So, you kind of add tests that uh target these properties to your own test set. Um so, that's bounded model checking V1. Assertion violation checker from our road map is the uh is where we would get into looking at the pre- and post-conditions that Ishan was talking about or that Verisol will look at. Um and so, Verisol checks this property at the Solidity level, but it And there's lots of tools that do this, right? There's like the the Solidity SMT checker, there's uh Verax, they have like an incomplete list somewhere. So, for uh circular Let's go back to circular. All right. There There's lots of tools that will do this, but we, you know, we're going to do it at the EVM bytecode level instead of at Solidity level for the higher guarantees you get there. Um And basically, because of the way EVM is start or way that Solidity compiles EVM, all we have to ask is is it possible to ever reach the invalid opcode because the assertions and the post-conditions at the end of the functions are translated to the invalid opcode in EVM. Um And if you don't find it that it's possible, then likely the user stated pre- and post-conditions hold. Uh if you do, then we can provide a counterexample, and once again, that counterexample can turn into an actual Truffle test so that it's quicker to catch next time uh without having to rerun this tool. Um So then, we are planning on getting an assist from Verisol. So, Verisol will first check it at the Solidity level. Uh and it's and it's much quicker to run Verisol at the Solidity So it'll check it at the Solidity level. If it finds a violation, then you can just work with that directly. But then Verisol gives you the green check mark. Then we run KVM and double-check it at the bytecode level. And that'll guard against bugs in the compiler and um and bugs in Verisol. Um Yeah, so that's kind of the the plan for this assertion violation checker. Okay, fine. Uh next is the bounded model checker, which is basically the symbolic version of this uh runtime monitor. So, this runtime monitor only exercises checks for violations in the runs of your tests, which are run on specific concrete inputs. Um but you might want to know is it possible there's violations in any runs of of the program. And so to do that, we basically will just run the same test, but now on symbolic inputs instead, and then run the bounded model checker out to some specific depth, and see if we can find a violation there. So it could be this example I have here is uh you know, it could be that the test only exercises cases where X is less than three, in which case you go directly from this exact state to the no violation state cuz no overflow ever happens. But when X is greater than or equal to three, you get this overflow, and then you get this end without a revert, uh which is a violation of this property. And so the this wouldn't be caught by the runtime monitor because it only exercises the cases that are in your test set, but then we here we would catch it and provide a counter example saying, "Oh, try X is seven." or something like that. And then you would add that back to your test set, and then you wouldn't have to rerun this tool to find that violation the next time. You would just be part of your test set now. Okay. Sorry I'm going so fast through this. I don't have any time. Um Finally, the the last tool that we're thinking of is for each of these I've said, you know, so once you find the violation, add a test back to your test set that uh would catch it without having to rerun the tool and that's to kind of speed up your later development process and and to guard against um other issues. Uh but the very last tool we're planning on putting in Firefly is where we'll just generate that test for you. Um so in the case of here, you know, we'll add for opcodes 12, 14, and 15, we'll do some analysis and find a test that will actually exercise that uh particular those particular opcodes basically. Um or here, you know, in the case where X greater than or equal to three, we can ask the Microsoft tools, "Hey, give us an example of an X that's greater than or equal to three." I know that's really easy to do like seven or something. But sometimes it's harder, you know. And so then uh and then the tools can say, "Okay, here's here's an assignment variables that will exercise that particular uh execution path." So that's the overall road map for Firefly at the moment. Um I'm going to put up this road map again. You can see it kind of extends out a ways. Um we are in this phase right now. Like I said, we have prototypes of all the tools going up here, not of test case generation, but we've given ourselves some time to really make sure that the everything's ironed out and works well. You know, we we just want it to be basically drop-in. We want you That's one of the goals is users don't have to know that they're um that they're using the tool until it tells them, "Hey, here's a problem." Okay, we're just going to wrap up. Um Any questions for the break? Anyone? Um yeah, you mentioned for the test uh for the test you mentioned the case of the ABI encoding. And then you could go back uh in general if there's missing uh test coverage, you can go back with the source mapping. Yeah, it may not be possible in all Like that, you might have to actually grab some specific transaction or call data to exercise like incorrect ABI encoding or something. Yeah, no, but I'm also saying like um so how are you experiencing this like often source nothing for this kind of generated code doesn't give you any meaningful Yeah, so the source nothing would be more just to assist the developer. It wouldn't be used probably in the automated test generation because there we do just generate exactly the call data we need to feed in to exercise that case. And for overflows in our experiences lots of overflows because the compiler likes to use them in our kind of testing that you have any filtering for that already or Well, so that's why you would you need the temporal property which says like overflows are okay as long as they're followed by a revert in some case. Obviously, that's like a little too broad scope of a property but you have I mean because like sometimes the subtraction is optimized into like an addition with overflow and stuff like that. Okay. So But yeah, we can add that. So you're going to have two back ends right? One with LLVM and one with Those already exist actually. That's just part of the cake right now. I was just showing that's how the tool is made right now. I have a diagram so Uh Go ahead. Which So I wanted to ask you about the two back ends after December 2020 why would you use the LLVM back end rather than the other one because of its speed or Yeah, yeah actually so we the LLVM back end is basically take the semantics and generate LLVM bit code that directly implements an interpreter for that language but it can't do any symbolic execution. But there's a lot of overhead in doing symbolic execution that slows it down too much for actually making a reference interpreter or something like that. So One minute left. Oh, we have like we have until 35. Oh, five? Five? Yeah. Okay, my bad. Okay. So I was just going to say I think it's important to note that the technology is It's available. It works. We use it internally. It's simply actually modifying extending it out to make it further so Please note, please note this is not vaporware by any means, right? Internally, internally we already use the K-framework for all these different variants of using the formal methods, formal verification for analysis. Each of the tools require experts, require us or others who have expertise in formal methods. What we want to do literally is to leverage the capabilities of the tool through automation and make them available to everybody. And and automation comes from what we already do in our our audits when we analyze them. When we analyze people's code, we know that certain things can be automated. We already do that and that's what Firefly does as much as we can. And others come from the entire community and especially from from all these amazing tools that Microsoft has and are under the hood in a very small So, key the keyword in this is automation. And once the tools work, then we make them available to you as push-button analysis tools for your company. I also wanted to add we are looking for, you know, people who are interested in conversing with us and being kind of alpha users in like a closed alpha sort of thing. So, grab me at the conference if you want to be a part of that. Come to our booth downstairs. All right. So, again, I want to remind you that the K-framework is language parametric or language agnostic. None of the tools in the K-framework care about what programming language you plug and play in these tools. And that gives us opportunities to do the same with many other languages. And we're already defining some of these for several other languages which will all take advantage of the tools that we support and we improve right now as as part of Firefly and and this integration with Red Hat. Among other besides Wasm, we're also working on several other languages. Maybe only C blow based on earlier times and the social system like like move. And then you have out of the box from our nice tools for the language. Once you define them for the language, to incentivize people formalize their languages in K. And thanks to the LLVM interpretation, which is pretty fast, you can think of it as you implement your language in K. And if you are happy with the speed, then you might not need other interpretation. We have some customers who say that here, I think that's good enough actually for us. We don't even need to implement have an aspect implementation of the language. Um, also somebody asked about protocols. If you want to to formalize and analyze the protocols, yes, this is another advantage of the K framework that it doesn't even care whether what you are defining is a programming language or not or is going to be you have a notion of transition from one state to another. And once you formalize that, and that can be in particular a protocol or a token specification, once you do that, then you can use again all the tools of the K framework to analyze your your your protocols or tokens. And we are already doing it commercially. We have formalized and analyzed several protocols. Actually, right now we are working with one company, Casper CBC. Yes, and also the beacon chain. And all of these become You can think of K at that moment as a programming language. You can have implementing my protocol in K. Um, and then you can execute and run things the same as you would implement them and run them with Python or Go. But at the same time, you can also formally analyze them exactly as they are without any gaps between what you run and what you verify. And with this, we'd like to conclude. And if you liked that we'll what you saw, we strongly encourage you to attend the three other events that I'm aware of that mentioned K in the or after related to K in Devcon 5. Um, Come to our booth downstairs, get a t-shirt, stickers. Go to the K website, K 21 4 can be free framework. There are lots of languages defined, for example, K framework, JavaScript K framework. Not only EVM, several others. The Firefly tool is available for download. Download, play with it, and become an alpha tester. Very soon also free for download. And if you really like to develop a system of verification, but you do not want to do it yourself, we are here to help. Contact us at our booth, and we'll help you. Formally verify your contracts or tokens or protocols. And we have a few minutes for questions. One minute left. Now a real one minute. Yes. What about Rust? Rust is a programming language? Yeah. If If you have a formal semantics? Yeah. There is There are two formal semantics defined by other groups, not by us. And we don't know how good they are. We haven't played with them, we haven't looked at them, but there are two semantics. One of them for sure defines the entire state of Rust. Um for Rust. Um but we are working on verifying some WASM code that is generated from Rust, for instance. So that's also And you can define your language yourself. You don't have to um There are a lot of examples, and uh And I We believe that all the tools that K provides incentivize people to formalize everything. Uh so I have a question. Yes. If we don't have access to the formal uh verification space, uh you know, for me, I'm just like like a general Right. What kind of practice we can apply in our daily coding? So that's why the Firefly is supposed to be. Firefly will be a tool that will adapt under the hood all the automation of the game framework. But then you need to formally specify the properties and that's unavoidable. That's either you need to learn or work with other people helping you. That's what we call the part of part of our bodies. More than half the time in an audit we spend with a customer understanding their their properties to help them formalize the specifications of their properties. Yeah, but I I want to know what are some like low-hanging fruits we can pick up. For example, nowadays I guess a lot of programmers use testing especially like the swap property checking in testing. Yes. Can we use some of the tools Yeah, quality quality audit. I mean we don't need to spend too much time Yes. to change the way we coding but this is an example. Exactly. That's what we want to verify for exactly what we do. Uh does it mean that because you say that testing could be automated? Does it mean that uh we don't really need to write You still you still need to write tests to get execution traces for verifying faults. But the point is that now you can get more out of writing your tests. That's the idea. I think so. I mean there's some work that's unavoidable. You need to somehow tell it this is what I want my contract to do either in the form of tests or in the form of formal specification which is more exhaustive but I mean for example, if you're working with Solidity, if you're assertion Solidity in Solidity by the song. You have to tell the tool what you want. Yeah, yeah, definitely. I just want to know Mhm.