NEAR Whiteboard Series with NEAR | Technical Deep Dive Sessions, 31 Jul 2020

Previous Meeting Next Meeting

⏯

youtube image

►

From YouTube: Whiteboard Series with NEAR | Ep: 39 Rikard Hjort from Runtime Verification

Description

Runtime Verification (@rv_inc), Formal Verification Engineer Rikard Hjort (https://twitter.com/@rikardhjort) and NEAR Developers Dr Maksym Zavershynskyi and Nikolay Igotti (https://twitter.com/@NEARProtocol) discuss Runtime Verifcation.

------- About Whiteboard Series ---------

The Whiteboard Series with NEAR is a set of video interviews with Founders who are building scalable solutions for Blockchain. We deep dive into their story, what they're developing and how it is helping the ecosystem.

Follow the latest from NEAR Protocol on,

Website: https://near.org/
Discord: https://near.chat
Twitter: https://twitter.com/NEARProtocol
GitHub: https://near.ai/github

#WhiteboardSeries #Blockchain #FutureIsNEAR

A

All right, uh rickard thanks for joining us, and uh do you want to introduce yourself.

B

um Yeah, I'm ricardo. I am a former verification engineer with runtime verification and blockchain nerd.

B

And day-to-day I work on on k, awesome, which is our implementation of webassembly. So that's.

C

So when you say when you say your implementation of assembly, you who.

B

uh So runtime verification or the the k framework.

A

B

Implementation of webassembly, so basically it's a formal, formal and executable specification of web.

A

B

uh Written in what would look like a high functional language to many programmers, I think I see, but it has some nice special properties, I'm sure we'll get around to talking more about it.

A

Cool and nikolai, what do you do.

D

Yes, uh I work near uh helping with uh with what we call the contract runtime, which is, which is essentially the way how we execute uh contracts, smart contracts, which which are technically web assembly programs inside of our blockchain, and how we integrate it with what you call transactional, which is essentially uh the part responsible for the functioning of uh of the blockchain as a distributed database. This consequences.

C

So I'm working also with nikolai. My name is max on the runtime which, as he said, includes the execution of the contracts, also trying to figure out all possible safety aspects of our runtime, because safety is incredibly important for the blockchain you kind of can live without liveness. If you, if your node stalls or crashes, it's okay, you can just restart it have some social consensus about things.

C

You know when to restart the notes or whatever get a new binary version, but if your safety is broken, it can be fatal for the blockchain. Therefore, it's mine and nikolai's huge focus in our contract, runtime and transaction runtime on how do we make sure the contracts execute deterministically and execute correctly?

C

That's what we're going to be discussing today, so I'm going to let you guys kick it off.

D

Actually, oh, I think it would be very nice before we start discussing, like particular technologies such as webassembly or formal verification of runtime verification, the company uh to discuss a little bit uh background ideas like mathematics, behind that uh the reasoning behind behind the formal verification so regard. What would you like to share.

B

Well, in essence, I think um a good way to describe it is that formal verification is a process which takes right a bit. It takes a program, you take a program p and a specification s.

A

Are you writing.

C

B

Yeah, can you see it in the whiteboard? Oh.

A

Now I can wait, wait a second.

B

B

You put it through this.

B

Typical program, refreshing, magic box and out comes either a proof that the specification holds or a counter example, and in in in theory, that that's that's what you want, but in practice there's also this uh slight possibility that we often don't talk about that. You can report, uh I don't know like the.

B

We could neither find a counter example or a proof, but but in principle you, you formulate something you want to hold of your program. For example, you know the if it's a token contract it could be. uh The number of tokens are, is constant or no one can have negative balance, uh and then you give the the program the contract as input, and you ask a system to uh prove that this is true or come up with a counter example, and you often end up in this kind of don't don't know face so this.

B

This box here often requires some manual manual intervention uh and that's what formal verification engineers spend a lot of a lot of their time on.

D

And what is the language for expressing, b and deaths respectively, so how I think, for b, it's mostly like predefined and depends on the on the area where you essentially perform the phone verification. But how do you formulate s.

B

Well, I mean there are many ways to formulate p as well. I mean you can't say: well, it's just a program, but the thing the thing that is say, I'm going to say it's implicit in all of this- is that there is this semantics that are goes into the box and that's one way to express what a program is.

B

So essentially it's like you define you define the world of all programs in a language that could be rust or webassembly, or what have you and then your program is just a specific, a specific element in this world of languages, but to do formal verification, you need to express this language, l in a mathematical fashion and that's, for example, the the web assembly implementation, I'm working on, is basically a way of turning the webassembly written, admittedly mathematical um specification into uh another mathematical specification that we can run uh with our system.

B

So the way you express s depends on how you have expressed the language l or rather like how you express this world around here. um So you usually don't just give the program as source text into this system or you you can. But the first thing that is bound to happen is that the program is turned into this mathematical object and, for example, we use something called matching logic.

B

So you write your specifications in matching logic. uh If it's a if you're, using a tool like isabel hall, you will have a.

B

You'll have an isabelle hall model of of the language, and you can express things in regular higher order logic, or it could be first order logic. It's it's. It depends on the tool and the best way to come up with or finding a good balance between powerful specification languages where you can express a lot of things and.

B

But you don't want to be able to express too much, because if you have a too powerful specification language, then you uh verification can become harder. So there's a balance to be found there and there's also. Obviously a user experience aspect to it. uh Where you know you want to find a way to express specification that makes sense to developers.

B

A very easy way could be to have assertions in your code and then just have the tool, transform those or transform the specification into or write a specification for you. That basically says we're never going to revert because of an assertion, but you might want to express temporal properties as well like say like well, if, if you ever touched this variable during the run of the program, you are not allowed to touch this later and that.

D

B

D

But doesn't it actually mean that in a good case or for for modification p and s better, be the same uh because uh it like programmer uh shall express his her desire in a program and a part of the those like desires and tensions uh logic? You also express the invariance.

D

So, for example, a search, as I mentioned is, is a very simple form of the formal runtime verification. So why do we want to go beyond asserts.

B

um Well, first of all, like I personally agree with you like, and a big part of uh making formal verification more widespread, is to make sure that it's has good ergonomics for developers, and you know systems where you can use asserts or do um or do uh like write annotations for like pre and post conditions, for example.

B

That usually makes more sense for the developer.

B

The problem is that if you want to do source level, verification or like you know, if, if you just want to have the developer as the writing code also, you know write specifications.

B

That's often a good thing, but there's not necessarily a big chance that the automatic, formal verification engine is going to be able to prove that and if you're, a former verification engineer, you usually know your tool, the the engine you're working well with pretty well and some ways. The formulating specifications are more amenable to verification, and you might want to like take this high level specification and break it up into many different, smaller uh smaller sub goals that you want to prove, for example, and then, then you need to have a language to express it.

B

In I mean it's the same thing if you write, if the first thing that happens to the program is that you, it will be expressed in this um mathematical specification of the language. If the specification is also part of the source code, then the same thing happens with the specification the specifications derived from the source code, but the first thing that gets put into the actual formal verification tool is going to be this.

B

It's going to be written in you know some specification language that is usually more powerful um and you want. I mean, if you're doing formal verification you probably want to be able to. You know, write your own specifications that you don't have to go through the source code to implement.

D

But actually, if we talk about languages, uh I think uh usually, there are like formal languages in like in in the form of formal grammar standing behind the language and that's kind of one layer of languages, but actually uh with languages. There is associated around time, semantics and certain behavior behavioral characteristics, and the question is which part of the language is actually to be addressed by the formal verification. Is it is it on time behavior? Is it like a certain uh syntactical properties of the language.

B

Well, I can't really think of anything that would be all that interesting to uh verify. uh Just using syntax, I mean usually most languages try to have a very like straightforward uh and not too complex and undecidable um grammar like if you want to write a parser you'll write an lr1 parser, like you know,.

B

That's parsing techniques, um but then to give meaning to your language, uh that's sort of where the magic happens so so to speak, uh and that's also, you know where languages become more equivalent. Any touring complete language is essentially, you know, are essentially the same to some extent and the way you define what each construct in the language does.

B

I'd say: that's the that's the more interesting part I mean I'm thinking whether there's something that could be very interesting to verify as like what a programmer usually thinks of the pure syntax, but I mean, if it's rejected by the parser, then you're probably going to have a parse error and resolve that, and that's I mean the parser is a verifier. It verifies that your what you're giving it is something that is expressible in the language syntactically and the type the type checker is a verifier. It verifies that uh you are not doing anything.

B

That's considered illegal by the languages type system, yeah.

D

B

D

Like on a different level, layers or levels of of the language, uh there are different rules like on the lowest level. uh There are like pretty much syntactic rules of of the of the formal language on the on the level of the type system.

D

There are different uh different computation, essentially expressed in a type system, and I think a significant part of of the language research like during last 50 years was put into into essentially making a type system such that uh most of the semantics are are actually caught on on the level of of the type system and- and so my question about, like like the formal verification as a technique is, is essentially how it augments uh the research because, like every everybody, knows how to write parsers, many people know how to do like a type system and how to how to perform uh like, uh like that type checkers on on lattices and so on.

D

But uh I think uh not so many people at least not myself, are aware how to go on on the next semantic layer which, which is which is higher than a type system. So how to express uh formal statements in that area, which builds like a complete exchange system which which could be actually used for uh as as input for any like reasoning, machine which which any formal verifier is, and so that's that's pretty much. My question.

B

Just so, I understand you correctly, you're you're, trying to like figure out what what's what's? What's the gap between you know the the type level kind of verification that a programmer is expected to do and what the things that we usually call formal verification where you know you hire a formal verification engineer to prove properties of your program.

B

I mean really yes, pretty.

D

Much it's like it looks more like uh the, for example. Type. Verification is absolutely like mathematical procedure. It's an algorithm you once you have a described system uh for the language and it's usually in some form. It's formalized as a part of the language. uh You can verify that the types type attribution is correct in a particular program and that's mechanical process, and you don't need any additional uh operation and it's not important in the program uh like on the same language.

D

If, if it's like a word processor or web server, the type syst the type system manipulation will be exactly the same and because because it's compiler and which does the verification- and so my question is um imagine uh if you have a form of verification or what is the formal system against which verification happens so like how how uh how it could be built, how it is built in in your tool or not in other tools,.

B

um Well, so in in our tool, um it's built through something called matching logic, which looks fairly similar to most logics that people may have encountered, but it's slightly more slightly more expressive um but say, for example, in isabella hall, you are using a slightly more familiar, probably higher order uh logic to express the.

B

The meaning of of of programs- and I mean it's not really- the type system and like these kind of formal verification uh things we generally do- are not really in uh competition, because the idea with the type system is usually that it's supposed to be uh fully decidable. Like I mean it, should be pretty straightforward for your type checker to just say this well typed or it's not well typed uh and might be unification.

B

Like oh you're, doing addition- and you know it's going to see that you know one uh actually, this is a good whiteboard moment like if you have, if you're doing one plus one somewhere in your program, or rather, if you're doing like p plus q and the type checker can infer that this is an int, and this is an int.

B

Then you know this expression is it's well typed, but that for that, the um the type checker must be able to infer the type of every every expression, the program uh which puts a limit on the type system's expressiveness. If you want to have a type system that can express any anything, then you move into undecidable territory, now type checking becomes undecidable, and I mean this this limitation here that you will sometimes end up in don't know. That's just like a sort of mathematical threshold you cross at some point.

B

Things are no longer decidable. Decidability means there is an algorithm that can decide this and will always be successful. Regular type checking is something like haskell or rust, or java is decidable, because the type checker will always succeed to tell you whether your program is well typed or not, but if you want to have a slightly more expressive logic system, uh things become undecidable.

C

So a question you're saying it's undecidable when it's theoretically undecidable, not something that your tool cannot uh infer because of there's some computational limitations.

B

Well, I mean I mean. Obviously there can be computational limitations. Like I mean there is, there is definitely a uh I mean in practice. For example, I think in isabel there's a tactic that I think is called blast, which is technically. uh You know it can take certain. I think, linear formulas, let's call and do and check if they are uh true and it's like a com. uh Sorry, I lost the word. It's not is it.

B

You don't say that it's complete. Well, you.

A

B

It's it should always succeed in theory, but in practice there's obviously a timeout limit, some some somewhere, the children give up. But there is also um I mean the.

D

Halting problem and so forth.

B

Exactly the halting problem is like the example that you know like. If, if I give you the simplest, if I make the simplest turing complete language or if I give you lambda calculus and say well, you know: will this program ever terminate for a great deal of programs? That's pretty straightforward, uh but there are. There are going to be some programs where it's not straightforward. So, for example, I mean people often confuse this and think that, oh you know, the halting problem is undecidable. Therefore they can't be. You know it's meaningless to try.

B

But honestly, in many cases I mean, if you, if you're writing a smart contract and your contract just looks like this. It's just like straight line code, then I can tell you well, you know if- and this contains no calls and no jumps, then I can tell you you know this is going to terminate.

B

But if you have a jump in here or you have a little while loop all of a sudden, uh then it becomes more complex. Maybe I won't be able to decide whether this terminates or not, but for and the way many tools work is that they make sure that you, uh when you write like certain functions, for example in isabel, you also have to provide a termination proof. But if you, if you just define your functions and start using certain simple structures, then the program can automatically tell you sure this is going to terminate.

B

And if you want to do something more complex, then it's your job to also provide a proof.

C

So the loops also include like loops in let's say, standard arithmetic operations, mathematical operations like let's say, hash, computation, right or or like signature computation, I mean like if, if we use it somewhere in our code, then we might end up in this done, don't know, state.

B

um What was your example well.

C

I mean let's say we have like a very simple example: that our our program verifies certain uh hash or, like certain signature right and like we want to prove that the assertion that says the hash doesn't match never never fires in the program, and so we cannot really prove it for for the input, because you need to literally pre-image the hash which right and but but like hash. But this is like an example of like a very simple program where you just have a hash computation.

A

C

You just cannot prove that the program will not panic, because the hash has been like one way. Function has been is being used somewhere in the code, but those one way functions are like incredibly popular in in smart contracts, even like basic, like asset manipulation like defy contracts, so wondering whether if someone drops in this kind of like crypto function, will it automatically you know, uh make it unusable that they formulification usable.

B

Oh, oh, no and I mean, for example, you I think you can scroll down a bit maxim. I'm just yep.

C

Let me scroll down below.

B

uh There you go. That's my terrible like what you do in general. Let's see where you are okay, uh what we tend to do is like we. If, if we have, um I mean often you're doing something called symbolic, symbolic execution, which means that instead of like put inputting specific values into your program, you are inputting.

B

um Let's see there, we go uh you're inputting like a variable x, right and so say your your input to a program is x and then at some points you get to a place where you do hash x, oops.

B

Since x is unknown, we probably won't be able to call this function. So what we'll do is we'll just leave the symbolic variable hash x here and now we know certain things about this value x. For example, it's between 0 and 2 to the power 256.

B

Minus 1 or something right, and we also know that if you do, if you also have y and you do hash oops, I mean the because you you're just defining it as a function and if you say well, let's do hash y, then we have the same situation, but now I, if you ask me to prove, can you prove that uh hash oops?

B

Sorry, it's a bit of a lag on my end, so this becomes pretty ugly. uh If you ask me to prove, given that x equals y, that hash of x and hash of y are the same, I can do that because that's a work, that's I I just have that as some assumption of my specific hash function. I I write like a lemma saying that you know this hash is correct and that's usually what you do you you're. I think it's tony.

B

That said, something like uh the job of formal methods is to elucidate the assumptions upon which formal correctness depends. That's a fancy way of saying well, the way you're doing formal verification is you're, trying to figure out that something is correct, given certain assumptions.

B

So, for example, if you, if I'm verifying a smart contract, I will often assume things about cryptography, because I'm not really proving things about cryptography and proving things about the program, and I will say this program is correct, given that the cryptographic primitives are correct, like you know, if I do encrypts x with a key, that's a key, and then I do decrypt with the same key.

B

I have a lemma saying or, like I have an assumption essentially saying. Well, you know that's going to be the same thing as x. If I encrypt it and then decrypt it and I use the same key, that's going to work, I will also have- or I might have a lemma saying the opposite, but you know I mean I guess, there's usually a chance that there is some probability that the problem with crypto with cryptography is that it's very probabilistic.

B

So, for example, if I'm computing, if I'm storing two values, let's say x and y, are not equal and you ask me- is hx equals to hy the answer is maybe unfortunately we could just add as a an assumption saying that, oh you know if x and y aren't equal, their hashes are not going to be the same. Basically, there are no pre-images, that's not true, but you can say that you know given that you're not getting a house collision. Your program is correct and then you can decide.

C

A

You can employ.

B

Your reasoning about that to say, if that's good enough for you.

D

If, if your data is longer than uh 256 bits, then for 256 bit hashtags, you are guaranteed to have at least one collision. That's uh like uh that's.

B

D

B

Yes, I mean so the the point is and- and that's why I come back to this- this horror quote: is that what you're doing is you're, usually not saying you know this program will always work in every circumstance, because you know there are physical, there's a physical world out there and things can go wrong and you know no, it's just going to work correctly, given that every node fails in the same way.

B

At the same time, maybe not, but you can, if you just have encode that as an assumption that you know your virtual machine is deterministic or you encode as an assumption that you will never have a hash collision, then you can prove certain things, but that also means your proof doesn't work unless you state that as an assumption and that's valuable right um and you can remove that assumption and say: oh no, our contract works, even if there are hash collisions uh but either either way.

B

You can, I mean you're, not you, wouldn't you probably wouldn't state that you know there are no such thing as hash collisions, because that's I mean that's patently wrong. You could use, like you said the pigeonhole principle to prove that wrong and now your whole system is unsound, but you could add an assumption saying well for these particular values x and y.

B

They do not collide, and then you can prove that you know you're you're, no one. No one is able to steal your tokens, given that they can't produce a pre-image, for example,.

D

And actually like, I really like our discussion. However, it gets very, uh very theoretical and probably uh close to like mathematical problems or even like foundation of computations, let's say so so if we I have, I hate to be kind of a moderating person here, but but I guess to make it more like closer to the theme which we, which we aim to discuss, uh we probably can discuss more like a practical aspect, so so imagine that, in our case, p is like a rust, smart contract.

D

uh Could you give an example? What would be an s in your uh verification example, and how? uh How does it bring the value to uh to the like a normal developer who's, not mathematician, not a formal logician but like like a smart person. Writing smart contracts.

B

um Sure I mean if so, if you're writing a program in rust- and um I mean the my standard example- is it's a token contract, and I mean history has proven that history, like the last 10 years, have proven that even something as on the surface, simple as a token contract, can have all kinds of really bad bugs in them a program that looks super simple.

B

Can you know accidentally mint tokens, um and so I mean that that's that's an s that I usually take as an example that uh the in a token transfer the the outgoing sum of every um of every address touched or the outgoing balance of every program touch is equal to the sum of all the in-going balances. So if uh a on the inputs plus b on the input plus, you know forever is equal to. If if these are all the the addresses that are sent as input to the transfer function,.

B

uh And you know these can be very complex. You know it can be like. Oh it's delegating to someone somewhere and it's you know giving something to the um to the contract owner address and whatever, but I can say that you know the in-going, um the in-going transfer or the balances has to be the same as the outgoing balances, and I mean this fails for all kinds of reason. I mean you could say you might, or you know the transfer might fail.

B

An excellent example, of course, is overflow. I mean if one of these, if one of the addresses overflow during the transfer, then this doesn't hold, um and so you might say that okay, this is going to hold, assuming that all the uh none of the addresses there's no overflow in here, and you have to express that as a property like assuming that you know the changes in balances, don't cause overflow.

B

uh This works. This is once one property you want to hold, but another property you want to hold, for example, is that all the all the balances? uh Oh sorry, all the out balances should be. uh Oh, wait! Sorry!

B

Actually, let me do this by text, that's easier, so a I a I uh b, I etc. uh The outgoing balances are larger than zero, or so that the ingoing balance are a lot larger than zero. That's going to imply that all the outgoing balances are larger, equals zero, for example, and that's another property you might want to prove, um and from from this, you might want to prove that you know the um the the total amount of tokens in the contract is always the same. This might not be something you want.

B

Maybe this contract is supposed to do minting, um but I mean from this perf you might be able to extract quite easily the property like okay, if you do a transfer, the transfer doesn't affect the number of tokens in the contract, um and I think one way this can help a developer, and we often have this conversation. It's like. How can we make formal verification easier? One way to make format.

B

Verification easier is to make sure you're always very explicit about your assumptions and you try to like at least give enough information in your comments or your specification documents, or by the way you name things or whatever, that or by assertions uh that uh it make it look very clear that these kind of things can never be be violated, but I mean, if you just write a straightforward transfer function.

B

There are many ways that can go wrong, but if you write this down this kind of specification and then try to just look at your code, you're going to there's probably going to be places in there where, where this is violated, and then you need to start thinking. Okay, am I sure that this is going to go back to uh a proper state like there might be, there's going to be somewhere where the value of ace balance has been decremented without the value of these balance have been having been incremented and so on.

B

So I think like until we get, I mean our tools are improving rapidly we're in like a formal methods renaissance, but for the programmer on the ground. Right now. I think, starting to familiars become a bit familiar with formal verification and maybe with like property-based testing is an excellent way to make use of this right now, because if you just start writing down your assumptions and your invariance.

B

Then you're probably going to catch yourself, making certain mistakes or or end up I mean if you, if you write down an invariant, that's saying like for example, say you never want your contract balance to you. Want it to be constant, and you just look over your contract and you're trying to like make sure that that holds. If there's one function, where you're kind of scratching your head and saying: oh, I'm not sure, but yes, I think I put it.

B

I think I thought it through once and it should work, then maybe you can rewrite that function to make it clearer and convince yourself and others that um that it's correct.

A

B

I I think the formal methods, thinking and approach is valuable to everyone, and I mean especially in the.

A

B

D

Yeah, I just I just wanted to say that it's like it's what you described sounds like a very good hinging, which most good programmers. I I'm aware of pretty much follow, even without without much of the for training in you know, formal verification so, like I know that good programmers writing complex systems always write a source so like, like checking your invariants frequently as possible, is is very common and very good habit. That's uh that's. I'm fully agree, but this kind of uh gets back to the previous question, which I had so don't.

D

You really believe that uh the best practical form of verification is where at least languages for p and s coincide all mover even where uh the pia and that's itself inside, so where uh the formal verification must be a part of the program.

C

Yeah, I would even add to that, because I was going to ask in the same kind of lines the question that you know when engineers design a program and have invariance in mind. They they enforce them through asserts for the assertions right and the the way they. Basically, the assertions that express the invariance is the is the s for the engineers like that's what I think nikola is going with. Is that you have a program right.

C

You wrote a program and then you go over and you try to make sure that the invariants hold and your ass is actually a set of assertions that you put in the in the strategic spots in your program and since they have to do it like anyway, like good engineers right they have to. They need to be aware of the invariants and have to add the asserts everywhere.

C

um Where does the value of the formalification comes in since we enforce the invariance through the asserts like? Why do we need? Why do we need to prove them? Additionally, on top of that.

B

um I mean that depends. I mean I guess there are two kinds of asserts. One one kind of assert is like you know, sanity checking that everything works and if it doesn't abort like you know, checking well is someone trying to transfer money to themselves. Then you know we, you can abort, for example, or that kind of thing, but another way we could use a search that isn't that isn't really meant to be functional. Is writing down these research that should never be violated, and you believe that there is no way they can be violated.

B

uh Those are the kind of research you probably want to remove at compile time. It depends, but I mean those could cause your contract to to um dost like you know.

B

Well, if, if you have an assert that you think can never be violated and all of a sudden, you know- and you know that's say- in the transfer function um and somehow you're wrong and that ends up being violated uh and there's no and the only way to modify it is by you know, calling transfer, then you know you're never going to be able to transfer anything. With your token contract again and now, your token is like worthless, probably yeah.

B

um So I I say there are two kinds of research like people will often like you know, write a cert like sanity. Checking your input like you call this thing correctly and you're not going to break anything if that's wrong. We're just going to.

B

If this is his theory, we're going to eat your gas or you know it's it's your problem um and but that's that's input, validation and that's that's saying and that's exactly like you're saying every like or most good engineers when they're, not under the very like some certain very tight deadline or something they should have those in place, um but they're also the the system invariants- and I think I mean my I I haven't been over- all all the all the contracts, all the different platforms, but I think those are usually less not present as much and those are really the kind of things you want like you want to be able to say that your system will always be in this consistent state.

B

Your your deposit contract is never going to lock up you're, never going to lose these funds or so on, and those aren't really like input checking a search. Those are a search of your system and like and if those are violated, if it's your system is probably designed around those always holding and if those are suddenly violated. Are you sure that you know you have the correct fallbacks for that um and.

A

I mean, and I mean if.

B

That's all you take with you like: oh I'm, gonna, I'm gonna. If you want to say, I'm gonna show those those uh former verification engineers that I don't need them and I'm gonna write a search and I'm gonna say well. If this invariant is ever violated, we're gonna call the fallback function and all our things are going to be liquidated and everyone's going to be reimbursed. Then great, like you've added some great some great um panic handling.

B

Basically, but you did that by trying to like think what are the variants I expect to always hold? Where can they be violated?

B

Am I sure that I can handle them correctly, because that's the kind of thing a verification engineer would find like you know you assume that this would always hold well, it won't hold in this case you say, okay, but if, in that case, I'm going to deal with it like this and that's great now we have better software.

D

Yeah and and actually in this regard, I have like related questions, because uh one of the like uh I'm a practical engineer in the sense that I uh I did look for various like complex systems and uh it showed that there are like two very powerful practical techniques for verification. One is the sword which I mentioned and and other is some form of a virtual machine, because because you can put some invariant checking actually into into your execution uh engine, for example, things like a for jvm.

D

There is a form of formal verification of of stack, manipulat manipulation, correctness for example, so so that, like it's a stack machine. So when you, when you put values on on stack and from stack, you essentially ensure that stack is balanced and properly typed and uh similar thing exists in in many other virtual machines. So um so some some invariants could be checked and insured by uh by the virtual machine. So uh so what uh what do you think of formal verification could bring to the virtual machine?

D

For example, if we have like wasn't virtual machine, do you think there could be something uh which we could add to this virtual machine to execute smart contracts in a safer way.

B

um I mean what you're talking about. I mean, if I understand it correctly. This sounds like runtime monitoring, like checking that you know uh certain things like checking at runtime, that things always work and maybe like executing this exercising the system and running a lot of things and making sure that things always work is. Is that correct.

D

It's not exactly continuous, no! No! For example, if you look at the john virtual machine, uh it has a bytecode verification, but verification is essentially uh before executing the the code.

D

The bytecode you check that the the manipulations with stack uh are correct, correctly, like balanced and so on, and uh uh and- and so uh there are other chats like uh memory manager in this, in a sense is, is something which helps perform modification because it ensures that objects for which the reference being held are not actually disposed, which could happen in language like a c or c plus plot uh and.

B

I mean so this web assembly has four more.

A

B

Yeah and I.

A

B

And I mean those are kind. Those are properties that are super good to verify and are actually also kind of relatively easy to verify. Again. They're decidable, you can say that these uh you can just look at a a sequence of um jvm, um uh jvm, bytes and say: okay, these are not going to violate.

B

You know: yeah cause stack underflow, for example, and that's because it's a decilable property- and it's also you know it's well known that that's something you can do if you just design your language correctly, uh but some things are not decidable and especially like if you're, if you're an engineer, writing writing contracts, it's very hard to design a general process that is going to check some meaningful property of every proper possible program you can, you can construct, I mean essentially like formal verification, is you know, applying applying all these formal methods to things that are not easy, or rather I mean the thing you're describing is also sort of formal verification, but it's the kind we take for granted.

B

It's the same way, we take um type checking for granted. It's something we know how to do. There's nothing. We can do well, it's something most people will be familiar with and therefore we do it. Obviously, um there is no real such process for uh checking these kind of specifications of a token contract.

B

If there were, we would just apply them and every every uh program on the evm or the near virtual machine would, you know, be guaranteed to satisfy these properties, but since we don't have that we need to do whatever we can and that's usually takes some human ingenuity and in 30 years in 30 years, we're going to have a lot of cool new decision procedures to automatically verify a bunch of things that we think are important for smart contracts. But, right now you know no one's thought of them.

B

Yet so what you're describing are a bunch of properties that are very important to verify.

B

But there are other properties that are important to verify that are not as easy. It's not like the the in in algorithms, like I mean there's a bunch of algorithms there's, there's p and mp like there's a bunch of things that are easy to do, uh and there's a bunch of things that are not easy to do. But the things that are not easy to do might still be important.

B

Therefore, we're applying our ingenuity to try to solve the best as we can, even though we know that there are some or okay, we don't know, but even though we assume, we think that there are some basic limitations to how how well we can do it. We still want to do it. So, even though we don't, we know that there is no decision procedure for whether a program halts.

B

We want to be as good as possible in detecting halting, and we want to be as good as an automatic as possible in detecting important properties of smart contracts and when they're violated and when they're satisfied and that's sort of where the research is happening.

D

Yeah yeah, that's that's absolutely correct. I just uh just wanted to like uh understand the practical uh consequences of uh formal verification for uh for engineers. So what would be uh the best practices? I guess we we can understand. One of the best processes which which is uh asserting uh other probably would be uh adding more checks uh into into vm, but uh um that's as as you said, it's it's on the lower level. So it's it's less on the semantic layer and more on like.

D

On just execution engine layer and- and so if we talk about uh like semantic related or formal gratification. So what would you recommend people to do here essentially how to other than think about the before the program, which is probably very valuable suggestion, but still.

B

um It's hard to do in general, it's sort of like saying you know what are the principles you should adhere to to make good software, I mean it depends on what software you're building, if you're, building a website or you're building a a nuclear missile launch system. You have different practices um and there are some things that are. You know, obviously always good like you know, document your stuff and think through things, um and I think it comes down to.

B

Being clever, like I mean that's, you know, keep it simple, stupid principle. Like I mean if you want to do something really really clever uh something that optimizes something in a really smart way, but it's that is not obvious.

B

You need to convince yourself and ideally convince someone else that this holds so I mean code review is a great example. I mean if you, if you make sure you do good code and honest code review like people. Actually don't just you know, let your stuff go through. Like people actually say, I'm not sure this works. Can you show me and convince me 100 that it works?

B

If you can convince them, and you just like write that down in a comment or in a document somewhere, uh then you know you're, I mean you're, essentially doing formal verification on paper. If you, if you can write, I mean mathematics, is essentially writing convincing enough stuff, um but also you know try to convince. I I think we often stop in this place where okay, it's probably true, and I can't I can't think of any way.

B

This would not work um whereas of course, verification deals with the problem of like am I 100 sure this can never be violated um so, but I mean, and then I mean I also think one shouldn't be too hung up on formal verification as, like you know the holy grail either I mean there are all kinds of things that are in between I mean in essence. You have like. uh Let me let me grab the whiteboard again. uh You're gonna have this: uh let's do an arrow.

B

Oh, it's very laggy. Sorry, let's see.

B

That's a bad arrow like more and more better verification, uh and I mean if you do testing if you write unit tests and integration tests and everything great you've, you've taken a step in the right direction right um and if you do um like runtime monitoring or like you know, you know, you're always checking at runtime that things are working properly, uh that's a step in the right direction and there there's all these things that happen on this scale and I'd say where the more formal verification stuff starts. Is things like.

B

Bounded symbolic model checking.

B

And say um symbolic execution like.

B

uh You you find a symbolic execution engine and run your program on different inputs and try to verify things or use. You know state-of-the-art tools.

B

There's every step to the right is probably an improvement, but I think we tend to get stuck in testing and then this fluffy thing, which is you know just oh hang on this- is not going well uh here. We go this fluffy thing which is hard to place on the scale which is auditing right. That's someone looking at things and saying: oh, this probably works, and this falls best practice um I mean one thing: we're working on is trying to make a tool called firefly, which focuses very much on um using the existing test.

B

Suite like your your existing program, test suite and our formal methods to find make sure that you know you've exercised every branch in your on the bytecode level and we can also use those that testing to do symbolic, execution and check for properties getting violated, and you can write like invariants of your system like saying your. My system should never violate this property, and then we can have that invariant and we're going to keep it with us, as we are running your test suite and we're going to make sure that that always holds so.

B

Essentially your tests, we did not is not only testing the things. That is that it's supposed to test. In a sense, it's also uh making sure at all times that all your systems variants are not violated, and I think it's important to not not get stuck in, like full, formal verification, because full form modification is valuable, but it's also harder than these other techniques.

B

And it's therefore right now it's sort of reserved for the most important things, the things that can absolutely never go wrong, uh like you know the beacon chain contract on ethereum like making sure that you know that is going to work and making sure that whole certain properties hold of it. uh That's a good place to employ for more verification. If you have the the tools and the means, but it's not going to work.

A

D

Everyone at all times yeah. Could it give like an example? How, um because this sounds uh like a super cool idea to uh to what you just described, to uh to actually take tests and like uh essentially uh do like factorize it in a sense, so, instead, instead of of actual uh values used in tests, just use equivalence classes of of the text which, which leads to like the same or different uh program behavior. uh Could you please explain how how it uh how it works in in the file.

B

So I I'm not sure I understand the question you're saying how the how you can automatically generate tests or how.

D

Now, how how could you like translate test from the actual execution to symbolic execution? I think, if I understand what you described here, you you essentially use use a test as an input to symbolic execution uh engine so that you kind of understand. What's.

B

What's going on.

D

B

Okay, yeah, so I I don't. I don't work on firefly, so I don't pretend to be an expert on this, but the way I understand it is that what you do is you have. uh We just have a specific contract uh and if you are calling that within firefly we're going to catch that and give you a symbolic value back or initially we're going to give you a random value back just so you can do some random testing, but then we might also give you a symbolic value back.

B

But if you run the same test in say ganache, then uh it's just going to give you a specific number at all times, or maybe a random number. So the way the way. The way I think firefly does is is like you ask for a random value from a specific point and if firefly sees you doing that that it's gonna uh turn that into symbolic value.

B

If I understand correctly um so essentially like you're, you have to write your tests and or, like you, write your tests as a property-based test like a randomized test, uh and then I don't think this f uh feature is fully implemented.

B

But in the future uh we're gonna turn that into a symbolic or we can turn in a symbolic value, for example, but I mean so I mean it's it's it's all just standard like you know, programming tricks using hooks and you know checking work which environment you're in and um so I mean formal verification is just it's very similar to programming I've. I I identify myself as like a software engineer day-to-day because, like it doesn't feel that different, it's just working on a slightly different domain.

B

It's like I'm building the tools to help specific development work um and it's and I'm just doing it in a specific special language that has some neat features. um So I mean I I don't I I think it's important. I know that formal verification doesn't get stuck in an ivory tower of. Like you know I I know I talk in very abstract terms, sometimes because I want to make sure I don't I I stay correct and don't say things that are like probably wrong, but uh I think I mean a problem with formal verification.

B

Sometimes is that it can be a bit too abstract and I think what we're doing what I like to do is just you know, show the tools, I'm working on and say: like hey here's, what this can do and it it looks like you're doing functional programming, which is probably not that scary and it's something you probably should do like just kind of putting it in the hands of people and making sure like I said that people start thinking about.

B

uh Oh, I wanna, I wanna prove something, and then you start by saying: oh, what is you wanna prove right, because people often come and say: oh, can you prove I just to prove that my contract is correct and then you asked have to ask well what does that mean? What does it mean for your contract to be correct and like well half the time people don't really have like? Oh, but you know, I know what it's supposed to do. Well, you know, then it's doing what it's supposed to right.

B

I mean unless you have something written down, that you can check it against. um You can't really do verification, and unless you have that it's quite possible that you haven't fully thought through what your system is doing, and it's also even more possible that it's going to be hard for you to explain it to someone else.

C

So I have like- um and this is a question here- yes, sorry, nicole and.

C

That's also about the practical aspect, so we talked about the financial contracts here right and uh you might have heard that many financial contracts were broken or abused.

C

Not because um you know there was some bug in the code, but because people were able to find a way to combine them somehow together or to do some manipulations on them in such a way that they at the end they come out profitable.

B

Like or oracle manipulation and like with like flat.

C

Phones, for example, yeah like flash flash loans like yeah whatever just like you know, like some temporal manipulation like you can you can like you know like jack up the price, then then you know the dump it and all those kind of things right and.

B

Call out some other contract and yeah manipulate the price. Ask you.

C

Yeah and your thing like, even without going, you know like in those areas where we talk about the cross-contract, you know interaction, everything. How would you go on with trying to prove that your contract cannot be financially manipulated in like in temporal way in such way that someone can somehow come out profitable at the end? By just doing some, a bunch of like atomic operations on your contract.

B

um Well, I mean always start with the simplest way of doing things, and I mean the simplest way of doing things would probably not be. You know to do full, formal verification on all the code and all the contracts. It would probably be probably be something like uh set up a model like just a little graph of the different contracts, how they interact and um like and and again like you have to come up with well, like you said, how do you make sure someone doesn't walk away profitable?

B

Well, how would you you have to come up with a way to specify that, and it kind of depends on exactly what you're trying to uh what you're trying to specify? One thing you could say like, for example, I don't know these all these facts in like in the specifics, but you say, like you want to prove that someone will not be able to manipulate the price of a uni-swap uh swap as their you know. In the body of the code, for example, yeah.

C

I mean like yeah, sorry I mean like before we go into the details, like the reason why I like express this concern because it sounded like to me at least it should be intuitively, really easy to formalize something. You know like like something like a property of like some energy preservation thing where you say like something that we're trying to talk about uh which is like you cannot mint or or like your total supply stays the same.

C

Something in in the lines of you know, whoever interacts with the contract loses, took the gas or, like always, you know it. It's it's more like you know, like some some law of thermodynamics, he interact with the contract. You always come out. You know at least losing the assets for the gas.

B

C

And it's and like in the direction you're going with is, is trying to say like well uh trying to formalize is too abstract, so you need to express more specifically what are the properties in there and then try to for like to prove formally that they they hold well. Well, I'm saying: can we can we come up with some set of like almost like a laws of thermodynamics, but for the financial contracts that we can formulate overall for all financial contracts and then just run verification independently? What is the body of the contract is.

B

uh That's a really cool idea.

B

um Yeah, I mean definitely get a committee on that, just like trying to figure out what are like figure out the thermodynamics of financial contracts, and you know make sure that I mean again since, like you know, I can publish a financial contract and it's term complete and you can do anything. Not all contracts are going to adhere to it, but we can at least put down you know some best practices saying like all these things should always be respected by any good um financial contract. That would be really cool.

B

I don't know what that would look like. uh That would be really cool and it would, I think, definitely be amenable to um the formal verification. One problem with smart contracts is that they like to call out to other contracts, which is a good thing.

B

That's you know composability, but it also means that you have to extend your assumptions to other contracts, so you have to say like if you are doing, if you're entering a specific function and that calls out to another contract- and you want to make sure you don't violate the laws of thermodynamics.

B

You also have to assume that the other contract doesn't violate the laws of thermodynamics, but what if your contract call can be pretty complex? Maybe like there's, you know, you're calling out a different contract and, depending on you know the world state. There are four different paths you can take and each one of those paths call out to a different contract.

B

All of a sudden like now, you have like a pretty complex, you might come up with a pretty complex system of interacting contracts um and and and of course you know, users can define checks to say. Oh, please call this contract in in the in the course of all this, and I think it in practice. It can be hard to do that, like at code level, co-level verification, um unless, like we have all the code which we usually don't, because you know often you can call arbitrary contracts.

B

It's usually not a white list that you can only call these um and that's why it's often good to model it in a more abstract sense like make an abstract model of the system as interacting interacting objects and so on, and try to work. It out from there and that's.

A

B

Mean you know definitely, if you're, if you come from physics or something then for complex adaptive systems, then that's, I think, that's a great exercise, but then you know it's. It's also interesting. How do you bridge that gap because oftentimes you do verification at like a protocol level or a systems level uh and well?

B

What I do is usually I do verification at like the code level and there's definitely room for error in in the gap between those uh where, like you know, you have some implicit assumptions in your in your big model and those are slightly different in the code. Verification and you know that can be violated.

B

But basically you know if you, if you're expressing your system in mathematical terms, mathematical terms and doing some reasoning and proving things about your system, you're doing formal verification- and that's I mean that's just the description of the the action and whether it's usually useful or not depends entirely what you're doing just like in math. There are absolutely you can do things that are not very meaningful. You can do things that are really really important like you can calculate.

B

You know the triangular theorems in graphs that don't really have a strong application or you can calculate you know the stability of bridges and uh you know, security of financial systems and so on. So.

D

Actually, I have very similar question to what marx had asked just just from another standpoint, but exactly about exactly the same problem, I mean uh if, when you started talk about formal verification, as essentially mathematical modeling, I think humanity has very long experience of mathematical modelling and especially in area physics and in physics. We quickly realized.

D

Well, uh in any physics like one of examples, um I was thinking about like like, uh like gas dynamic, for example or thermodynamics, as as max said, it's it's the same, so you can, in theory, uh solve like a dynamic equations uh for every molecular in air to to to essentially make make a statement about uh uh like absolutely perfectly valid statements about uh about the air around you, but that will be first uh absolutely understandable by a human uh who think about that.

D

And secondly, it will be absolutely useless or you can say that it's like 25 degrees, tells you in in this room, and it will be like very simple statistic: property which first makes sense and um and relatively easy, like measured and and computed. So so my point is that was exactly the same, so from human point of view. So if, if you make a validation of very complex uh software models, they became useless, it's very easy to make to make a mistake. It's not important how how smart is a particular person.

D

It just means that uh the like the complexity have to be like a little bit, bigger and uh and and the brain will will break. Our brain is not that powerful technology, and so we have we simplify and and like um the trick here is that are there a way to not to not model or not even precisely model, but quite the opposite, uh uh to model in in a way which uh uh which avoids uh like the then they need to understand every behavioral aspect of the program right.

B

Still be useful for yeah. Absolutely absolutely, and I mean that's that's I mean, if you're doing like protocol verification.

B

That's often what you're doing you just have actors that uh that way, that's more more discrete deterministic thing, uh but again, like I'm not coming from the realm of physics and like if you get a committee together and decide to work out like a theory of thermodynamics for these kinds of systems and a way to model, you know your smart or the smart contract platform um where you can like look look for pro these kinds of properties. That would be really cool.

B

um I'm not like again, I'm not it's, not my area of expertise, so I'm not 100 sure what the use cases would be. I can. I can imagine something like okay. That would be. That would be great. Like you know money you know, value isn't destroyed anywhere, for example, or even if it moves around in interesting and complex ways, it doesn't like go up in smoke or so on.

B

But uh all I can say that it's that it sounds really cool, but uh and no I not, but it sounds really cool and I hope you do it and get back to me when you do. um But I also want to counter your point on saying. Like you know, oh, if you're trying to verify a system, that's super, it's super complex, uh then you know the brain is going to explode, because it's so big and it's so hard. I mean that that can be true, but I mean verification.

B

One of the powers of verification is that you can ex you can have very complex systems that do a lot of tricky stuff and it's very hard to prove that they're right. But the statement of correctness can still be quite simple. Like a famous example, is the four color theorem? um So basically, the idea that any any world map or any possible word world map can be colored in using only four colors uh without having.

A

B

Countries um having the same color, I mean that's, that's the layman's statement. The proof is immensely complex, like super complex and it's been verified with, like you know, proof, assistance, and but the thing is the thing is the statement is pretty straightforward and I, I absolutely 100 believe the four caller theorem, not because I can understand the proof, but because I can understand at least somewhat the um the proof checker and someone says like I have a long string of you know. That represents a proof. We pass that through a very simple kernel.

B

That is a proof checker. That only does like some very simple logic and won't allow you to do anything uh anything like obviously bad and it's going to say in the end, oh yeah, I've seen you've actually derived this simple thing. You you here.

B

This is something that you have a simple statement and I can attest to that this complex body, that is the proof, actually proves this theorem, and now we're done so I mean it and and your head doesn't have to explode around the theorem, even though, like the proof of course, took like a huge amount of people and a lot of years to work out, uh and I think that's one of the powers of verification, because we often talk about how, like the number of bugs in code scale with the number of lines of code.

B

And I'd say that you know the more complex your theorem statements are the easier it is to make a mistake.

B

If you have a lot of complex assumptions and complex encodings of states, then it's going to be easy for you to make a mistake, but oftentimes your your theorem statement can be quite small, and the process of verification is often taking these more complex statements like, for example, we did here with the uh the transfer function. I mean the statement. The transfer function you know, doesn't violate the loss of thermodynamics, like the the amount of tokens stays constant or shrinks, or whichever one we choose.

B

uh That's a simpler statement than saying every variable that is used somewhere in the body of the program. Has these properties at the input output? That's a I'd say that's this. The second statement of the problem leaves more room for error, but you can use that to then prove the bigger theorem, and I mean that's pretty common in mathematics. You have like you have to if you're doing group theory like lagrange's theorem, is really really easy to state and prove you can do it in a tweet.

B

But you have to create this more complex body of other things. First, but then the actual statement and the proof are pretty simple and I think that's one of the really cool things about verification is that you can kind of get this very high assurance, because you have a very, very small statement and you have I'd, say absolute assurance that your statement is true.

B

B

Yeah I mean, but in practice, especially with smart contracts, you often end up saying, like you know well, this is through given these and these assumptions, because, obviously it's a software system- and this can be hard to encode these assumptions in an intuitive way.

D

Yeah, this sounds natural yeah, so I guess we actually already like to 20 minutes before our like land deadline. However, uh I guess uh we have very interesting discussion. I I personally truly truly enjoyed it and and like the ideas which we discussed here, and so I want to say say thanks thanks a lot to eureka to to max for for, like for for joining this, this talk, and- and so maybe uh we can- we can continue discussing uh this.

D

uh This manners in matters in in some in some other format, uh because because it seems to be very, very deep and very uh they say uh uh strangely, it's very practical in a sense, because, because what we do, we we we all write a complex system and we and we regularly and routinely verify them so so probably discussing it with uh from more, like a distant point of view, maybe very uh very enlightening for any software engineer. So thank you. A lot.

A

Thank you so much. It was uh fun.

C

All right see ya thanks around for.

C