# Symbolic testing in Solidity using KEVM and Foundry - Andrei Văcaru - Runtime Verification, Inc.

- Channel: [ETH Belgrade Community](https://streameth.org/eth-belgrade-community)
- Date: 2023-10-07
- Duration: 16:59
- Watch: https://streameth.org/watch/yt-eRUFNnZmNmk
- YouTube: https://www.youtube.com/watch?v=eRUFNnZmNmk

## Transcript

okay hi everyone uh good morning my name is Andre Vaccaro I'm a former verification engineer at runtime verification and today I want to talk to you about our project KVM and how we can use it for symbolic execution in solidity using our latest integration with Foundry so as a quick overview I want to briefly go through what the founded development toolkit is what's KVM how do we set it up to work and how can we use these tools to actually do formal verification of a solidity project so uh The Foundry toolkit it gained a lot of traction and it became one of the most popular toolkits out there one big advantage that it has is that it allows solidity developers to write these parametric tests directly into solidity and this means that you can write a solidity function with some parametric with some parameters and then when the test is executed um the the arguments will be first and the execution is pretty fast you can run a test for like a thousand times in a couple of milliseconds depending on the test so that's good um another Advantage is that it provides users with some immediate feedback so if you're in the building stage or you want to have some fast answers about your uh contract then you have this advantage Also regarding feedback um when you execute a test you basically get these green check marks saying that your test is successful or you have um Red Cross and a counter example is displayed with something that some values that will actually break your cons your assertions another good part another good part is that there are no false positives so basically when a test is failing do you know that it's going to fail because you have these counter examples but on the other hand there is a trade-off you have false negatives this means that when you have a successful test this doesn't mean that the test is correct or the the contract the test is correct but only that the father was not able to identify a counter example in the limited amount of runs so that's that it can give a false sense of uh confidence but this doesn't mean that I'm here to bash on fuzzing fuzzing is good and should be used I'm here to present the the benefits of combining the accessibility of The Foundry of the solidity tests with the symbolic execution so we as random verification we developed these symbolic execution engine which is tailor-made for the ethereum virtual machine and we call it KVM basically we took the semantics from the yellow paper and we defined them in our framework called K framework and this grants us access to symbolic execution I'll be oversimplifying a lot of things so shortly it passes the same conformance test as other clients and I'm talking about the conformance test provided by the ethereum foundation and this gives us a higher confidence when it comes to the results of the verification process and of the symbolic execution it's easier than ever to install we developed a new uh package manager which you can install KVM with in a line of code or align a single line instruction and we also have Docker images released with each update so yeah we've used it in our formal engagements for a while but it's a manual process and I'll show some examples right after but we also did it some large scale proving for the maker Dao for the multicolateral die system where a domain DSL was generated to was created to generate a thousand and eleven proofs so it was used for large scale proving as well so this is how shortly a formal execution proof would look like we have this oops sorry I messed something up thank you so basically we have this claim which we call it the proof application and this is for a near C20 balancer function as an example but basically it's composed out of two components we have the configuration which shows how the state of the evm changes during the execution and we have some a constraint term which actually shows boundaries and constraints for all of our symbolic values but basically the idea is that we can Define how the initial State and how we expect the final state to be so for example on line 9 we specify that we want the execution to start and we want the execution to end so no um everything in between or every stock configuration will be rejected so if you look at line 18 for example we say that we want the call data to be the balance off function and we have a symbolic address called owner how this actually reads is that for all symbolic addresses that are in the address space when the balance of function is called to an erc20 contract we expect the execution to end and even more we expect the execution the transaction to be successful and this means that we reject all the evmc reverts or all the out of gas and stack overflows and things like that and we expect the output of the transaction to be a buffer of length 32 with a symbolic value called Bell and this Bell is the balance which is actually extracted from the erc20 contract at a specified specific hash location where the balances of owner is so I know this is hard to digest it's uh as I said the manual process and it can be very easy to make errors here so and this is also just a snapshot of how how the proof would look like the actual proof would look like this so it's a lot bigger because we have to modify we have to model the entire state of the ethereum virtual machine so the idea was that we can if we can get this to work with symbolic uh if we can get the symbolic execution to work with solidity tests then we could find a way to hide all this code under some simple solidity lines so um we go to The Horde triples which are one of the foundations of formal verification which state that for all symbolic variables if we know that some preconditions hold and we execute some code then we can do some assertions about post conditions and we can translate that into a family parametric test or a solidity parametric function which actually states that we have symbolic variables as function parameters then we can have preconditions assumed with the cheat code there's a cheat code for assume anything then we can execute the code and check the assertions check the post conditions using assertion instructions so we got we found a way to write the test but then we have to find a way to execute them symbolically too what we actually did with was Foundry to write this test and then we have a python library that actually looks at the compiled artifacts and then generates the proof that I showed you earlier so users don't actually have to touch the key code when they're writing tests um and so the same balance of test can be written in a few solidity lines uh and again I'll go through this pretty quickly so basically we have a symbolic um we have a parameter called um address and then we have a storage slot which I'll come back to you in a bit the idea is that we can compute the hash location where we can find the address in the balance is mapping and then we extract that value from the storage directly using the VM load cheat code so this actually reads the value from the storage then we can also use the balance function the balance off to extract the value from the getter and then we can assert that they're equal and this actually means that we only test that the function Returns the correct value it's supposed to from the storage so it's not quite near where the proof was and so another thing that we do if you notice I have two modifiers here one of them is the unchanged storage and the other one is the symbolic and actually what the unchanged storage is doing is that for any given bytes 32 value that could represent any storage slot of a contract I read the contents of the storage before the execution of the code and after the execution of the code and then I'm asserting that the two values are equal so it's basically saying that I run the function but nothing in the test changes the state so I know that it's only a getter um um and there's a the drawback is that you could say that after each setup function you just deploy the contract and the storage is empty if you don't do any initialization of the state so what the symbolic modifier does is that we set the symbolic storage of a coin of an address we're basically saying that let's consider that I don't know anything about this contract so instead of having an empty storage we can just say that I don't know anything about it so basically what the test is saying that for any address if I call the balance of function it Returns the correct value and it doesn't change anything in the storage and this is just an example the drawback is that if a fast test would run very fast the execution of this would be somewhere around 30 minutes so still usable on CI but not in the development process yet so yeah the benefits is that we have the symbolic execution that we know that we covered the entire input state so we don't have any more d uh we don't have any more false negatives we know that for all inputs we can catch the counter example um another Advantage is that during the execution we save snapshots of the configuration and we create this control flow graph of the execution that gives us the ability to have an interactive debugger to go through the program execution and visualize the state we can also use it as a bundled model Checker or we can Define looping variants to verify loops so again there are limited limitations that the tool has for example the execution as I said is slower this basic proof takes around 30 minutes we cannot claim formal verification of the entire project yet because in order to claim formal verification you have to prove that you have exercise all the possible cases so we can say that we have formal verification of this single test because we cover all the inputs but we cannot say that we have formal verification of the entire project because we didn't show that we covered all the possible tests that a project can have so and also the user experience can be improved because when you have a Foundry test it's either it runs and it either fails or it passes but here with symbolic execution there's another state in which the approver can get stuck and requires some manual input from the user basically it could get to a simplification that it doesn't know how to process so the tool it's easy to try but it still requires some experience to work with but it's a step forward so we are working on this regarding the execution we have an ongoing project where you write the symbolic proofer and this gives us at this point uh three times speed up so for 10 for from 30 minutes it goes to 10 minutes regarding the formal verification of a project we are working on integrating symbolish coverage symbolic coverage and this will actually tell you that hey you have these tests which are good but you haven't tried these possibilities and we're also listening to feedback from users in order to improve the user experience uh so yeah now I have I want to show another uh basic example in order to demonstrate how everything goes was the process of having um KVM run on a project and using the debugger so basically you have the solidity contract which is only for demonstration purposes it's a solidity uh contract it has a coffee break error and a public number which is a unit 56. a function that will set the number correctly but if the parameters have specific values then it's going to revert with that error so we also have a test contract which says the function correctly but then and it asserts that the number is the correct value that has been set so running this with Foundry it will be pretty hard to identify these specific values using fuzzing but we run it with the KVM boundary tool and we run it using two instructions so the first instruction which is KVM Foundry compile will run the tool and compile the solidity project and generate the specification that I told you earlier the proof and then the next command will actually run the everything and start the symbolic execution and after 15 minutes this is without the booster update we can see that the proof failed and it actually tells us the path condition on the failure so here I know it's pretty hard to read but it actually says that when n is equal to a specific number and the inlock value which was the Boolean is different than zero then the proof will fail so this is how the interactive debugger would actually look like it's in the command line currently but uh I think it would be nice in as a vs code extension so on the left hand side we have all the nodes in the control flow graph and on the right hand side we have the configuration the constraints and the source code of the test that is executing so it's nice because you can follow the execution you can identify the state in which the program is failing and you can also remove a node stop the execution stop the execution remove a node and then continue from that point further so you don't have to rewrite the star restart the entire process from the ground up and so this is the simplified control flow graph of the execution basically it will run the setup function then after 800 steps it will start the actual test and then it will reach the first branching Point whether the N is equal to that number so if if it's not then the test will pass but if the end is actually that number it will go to the next branching point and it will check that the Boolean value is true or false so it will be able to identify the counter example and return this path condition first so yeah this was my talk on the right hand side we have this uh we just released a guide on how you can use the KVM Foundry integration and we also have a Discord Community where you can join and ask questions so thank you for um everything