Formally Verifying YUL Level Static Analyses and Optimization with Coq

Transcript

It works. Yeah. Okay. Thanks. Uh, okay. So, I'm Samir and I will be uh just briefly overviewing the 4U projects that aims at formally verifying level static analysis and optimization with proof assistant uh rock. Okay. So, the context of this work is formal guarantees for compiler correctness. Since compilers rely heavily on static analysis and optimizations and these implementations the implementations of these tools can have implementation bugs even if the underlying theory is is correct the correctness of the entire compilation process depends on the uh on these components being being correct. So our

goal is to provide formal mathematical guarantees that uh that these tools are are correct and we want to do it with formal uh verification. So uh formal verification of programs of correctness of programs can be done in uh in several ways. One popular way is to use a proof assistant. So in this context you have uh a language that is usually a functional language with uh with algebraic data types and you can write programs and then write statements about these programs. uh the statements are written in some logic that is supported by by the uh by the proof assistant and then the proof assistant will help you to prove the correctness of these of these theorems a step by

step where every step is verified to be uh to be correct. So if you want to use this approach to verify a static analysis tool the tool must be written in this language of the uh proof assistant which is not realistic because uh these tools are not usually written in some in some other uh languages. So what we can do we can build a model that represents the static analyzer. We can build it in the language of the drove assistant and then uh write proofs and statements about the correctness of this of this model. The challenges here is that first we have to trust that the model really represents the behavior of the static analyzer. So this is something that we have we have to accept. Uh also static analysis tools typically use um external tools as SMT

solvers. So either you model them or you have to trust that they are correct and also writing proofs at this scale is very complex because the tools are are very uh very large. So an alternative approach that instead of verifying the uh analyzer itself we can verify the results that it generates. So in this approach uh we have a program we run the tool that is the static analyzer and then we get the result and when we pass the program and the result to a checker that we write and the checker tells me if the results are correct or not. So the idea is that this checker is much simpler than the tool itself and we can write it directly in the language of the proof assistance and then we can write formal statements about the correctness of the checker which means if the

checker tells me that the results are correct then they are really uh really correct. Okay. and we develop the proof for this statements in the in the proof assistant. So this approach is is a bit more realistic than than the uh the other one. Okay. So it doesn't matter which approach you take verifying the tool or verifying the results in order to uh uh write formal statements about programs or about properties of programs we need to uh model the behavior of programs mathematically. And here comes the role of semantics. So we have to develop a semantics in the proof assistant that represents the semantics of the the programming language that we are dealing with and we have part of the the

semantics that also we have to represent data types and states and everything has to be defined in the proof in the proof assistant. Okay. The semantics that we usually use is operational semantics which describe uh discrete execution steps. How from one state we can move to the next state. uh and this operational semantics can be defined either as an executable function. So you can execute the semantics like writing an interpreter or it can be defined as a relation. Similarly you define a a logical relation that defines relation between a state and the next state. And in this in this case the transitive closure of the relation represents the uh executions.

Okay. Um so apart from operational semantics we can also define other kind of semantics. This depends on the property that we are interested in uh in verifying. So the vario project is exactly about this is about developing uh semantics for the ule intermediate language uh in order to uh use it with a with a long-term goal term is to use it to verify static analysis results in in the solidity uh compiler. So we have developed this uh formal semantics for uh for ule and in the proof assistant coke. The semantic is parametric in the dialect and we have the AVM dialect implemented almost executable when when possible. The current semantics works at

the level of the controller flow graphs not at the level of the SST and uh for a future work we plan to also de develop a similar semantics for the AS proof of concept. We have verified the results of the livveness analysis in the solidity compiler like we have developed a checker to check that the results of the livveness analysis that has been presented before uh is is correct. Okay. So let me just briefly describe the components of the semantics that we have. So here we have the interface for the dialect. So if you want to implement the dialect you have to provide a type for the uh basic values like 256 bits.

You have to provide a type for the op codes that are supported like add sub and so on. And you have to provide a type for the state which is in the EVM it would be a combination of memory and the store and you have to provide an a method a function execute or define a corresponding relation which says how you execute op codes in this uh in this in this dialect. Okay. So the this function receives a state op code a list of input values and returns output values and new state and the status. The status can be for example still running, reverted, an error and so and so on.

Uh smart contract the type for a smart contract is this one. So a smart contract has a name. It has a list of functions and the name of the main function. Uh the function is represented as a collection of blocks that represent a control flow graphs. So a block includes uh includes uh instruction of this form, assignment, a call to a dialect or a call to a function. Uh blocks also have information on their kind like if they are normally blocks, branching blocks or uh return blocks and also blocks have um support for the feed function in case you want to represent SSA uh SSA, CFG like the CFGs that we have. they do not

assume SSA but you can you can also represent SSA cfg. So a state at the u level is uh is a record of a call stack like in any other language where every frame in the stack is uh corresponds to the execution of a function. So it has information on which instruction it's currently executing. It has information about the values of the uh of the the values of the variables, the current values for the variables, the status of the execution, if it's running, reverted, terminated and so on. And also a component that represents the state uh of the dialect which is managed entirely by the dialect model. Then the semantic scam is defined uh as two

functions. The first one is a step which is a say which describes how from one state I move to the next state. And eval is just a loop calling steps and end times. So those can be defined as an executable functions or that like what we have them or they can also be defined as as relations. They don't have to be really uh executable. Okay. So as a proof of concept we have used uh these semantics to verify the results of the liveness analysis. So livveness is um we say that a set of variables is live at the beginning of a block. if uh any execution starting from DC block is not affected by any variable that is not in that set. Okay. So uh we have developed a checker for the uh for for the

livveness which takes a program and lives information and and tell us if it's if um if if the result are correct or not and uh so the checker is implemented in the proof assistant uh rock and uh it is also formally verified. So the statement that we have proved is this statement which basically says if you start from a state ST1 and you and in execution steps you get into a new state ST1 prime then if you start from an equivalent state up to the value of a variable that is not live you will also be able to make an execution step and arrive to a state that is equivalent to the uh previous uh to the previous one.

Uh okay so to wrap up is uh so the success in verifying the livveness information or or in this liveness checker somehow confirms the feasibility of this of this approach. Uh we have applied it currently to a small limited of smart contracts just for testing the the checker. Uh we will apply it for to a broader range of of smart contracts. We also plan to extend it to more static analysis uh that are uh like conceptive propagation but maybe this will be delayed until we define the semantics at the level of the a because many of the static analysis are at the level of the a semantics and we plan also to improve the usability of the uh of the tool by building friendly user interfaces like

to use it from a command line from a shell a library and so on and of course to build corresponding semantics at the level of the tasty. That's Thanks a lot. >> Thank you so much, Samir. Uh that would be uh that was a super insightful talk. We have one question for you. Why rock out of the options? >> Uh because um I have more experience in rock.

>> Pretty straightforward answer. Um if you folks have any more questions for Samir. Yeah, >> great talk. Thank you. Uh can this uh framework in Iraq can be used to formally verify contracts like to translate them into you and prove properties about them? >> Uh so sorry can you repeat again? I >> uh so can you use this framework in U to prove properties about smart contracts in U >> about smart contract? Yeah. Yes. I mean you you can you can you can do it also about smart contracts. But then the problem if you want to verify properties of a of a specific smart contract then a better approach is to model your smart

contract in coke and try to prove the property like this would not be really appropriate for a single smart contract. It will be appropriate for um for a tool that receives as input a smart contract like a static analysis. >> Thank you. Thank you so much. Um that will be it for you Samir. Thank you so much for your talk.