Scribble in a Nutshell

DeFi Security Summit 2022 · 27 Aug 2022 · 5:09

Joran Honig of ConsenSys Diligence introduces Scribble, a specification language that makes property-based testing of Solidity contracts easier. Annotations above contracts and functions describe properties, which the tool translates into runtime checks that can be used with unit tests, fuzzing, symbolic execution and formal verification. Presented at DeFi Security Summit 2022.

Speakers

Topics

From DeFi Security Summit 2022, hosted by DeFi Security Summit.

Transcript

so a diligence we have built so many tools that we could like fill the whole day talking about all of them but uh so I'm just gonna talk about the one of them um and I'm gonna explain you like the basic function of what it's uh like intention is and then after all uh the lightning talks are done you can come by and then try out this super cool tool called scribble um so uh if you're a solidity developer or a developer at all you're probably familiar with unit testing and this is this practice where you take isolated situations like

um I have a contract I have a function add and if I put these two values in there one and two then there should be a result and you should get three out of it um I don't know about you but I think writing unit tests is kind of boring uh and it takes a lot of time you need to go through tons of edge cases and uh it's also really easy to miss something and this is why these tools like fuzzing and formal verification are so cool but there's an underlying principle to starting this process of fuzzling property based testing and this is the use of properties so a property as

opposed to a unit test is something that describes all possible situations rather than just a single one of them where you put one and two into an ad function and you expect something to come out so um instead of that you describe the behavior so in case of AD it's kind of simple you say well this function add is supposed to take two numbers and give you the sum of them um but you can do much more interesting things so for example if you have a short function you can say that the result should be well a sorted list and that that list is actually a fermentation of the original list because otherwise like sort could just always return an empty list and this is

also not what you want um and um let's see oh so to apply this idea of property-based testing you don't actually need a special tool you don't need formal verification you don't need a fuzzer you can already apply it just kind of like in a testing a base approach and this is kind of I know it's Python and not solidity but this was kind of shorter you can do this with just like the language that you're using so this is an example in Python of the exact property that I just described for Simplicity I've made like two simple functions for sorted and permutation and

all that you need to do now after you've written this function is call it a few times with different lists and then you've tested a whole bunch of cases without having to come up with a lot of edge cases it's like and there's a few ways to make this more easy so what I just described where you come up with that like this the cases yourself that would be parametric unit testing uh with fuzzing you ask a a tool uh to come up with the edge cases for you and then with fuzz with verification uh there's some more like medical type reasoning about it so scribble

um is a tool to make this property-based testing or writing properties a lot easier than what they would be if you would just have to write them in pure solidity uh so it's a specification language which means this is kind of parched so you have a picture here of a token and you see two lines or a few lines of comments above a function and above the contract and these are kind of like programmatic descriptions of the properties that you would want to have hold over this contract what we do with the tool is we take

these properties that are super simple and high level and more expressive than normal solidity and we translate them into runtime checks and the nice thing about runtime's checks is that almost everything can reason about them so you can use them with unit tests which we sometimes do you can use them with fuzzing which is another tool we've built diligence buzzing you should check it out but you can also do symbolic execution on it you can do verification on it and it's kind of framework agnostic so I think you can use it with almost all the other tools that are going to be demoed here which is really cool and that's it [Applause]