[Formal Verification] Certora Prover Tool

When I deep dived into the blockchain ecosystem, I had a trait for demystifying the implementations of the protocol. For example, when I understood that Uniswap v2 was one of the most used DeFi protocols, I simply took a look into the smart contracts. Then, I had an attraction to security. So, firstly, I learned the basic vector attack at swcregistry.io. In the meantime, I tried to learn how to write unit tests for smart contracts and how to use tools like Echidna or Slither. During my learning session, I watched this video Martin Lundfall: “Smart contracts as inductive systems”. This sparked my interest in formal verification. ...

As mentioned in the previous article, Certora creates software called Certora Prover. It allows verifying your specifications or finding bugs in your compiled smart contracts. The Certora tutorials is a course to start writing specifications in Certora’s spec language. Today I will share my understanding and my opinion on lessons 0 to 2. Let’s dive in! Lesson 0 In this lesson, you have three resources: a video, a quiz (answers), and books (introduction to logic, discrete mathematics). ...

Hello everyone ! Today will be a quick recap about what I learned. This lesson is not about the certora verification language (CVL). The subject is SMT — Satisfiability Modulo Theories, one of the cores of the certora prover. The role of the SMT is to decide whether a property, expressed as a set of logic expressions, can be proved or disproved. - Lesson 3 I recommend having done Lesson 0 (more precisely introduction to logic). We will only use Z3 Playground for the exercise and this tab: ...

Hello everyone, after a pretty long pause. It’s time to go back in order to finalize the project. This lesson is pretty wide, it will cover some theoretical course and the syntax CVT (Certora Verification tool). How to Think of Systems as State Machines: Here are the resources: Watch the video from 48:58 to 1:02:45 — Link https://youtu.be/8FWfmvj3HYw https://www.cs.cornell.edu/courses/cs211/2006sp/Lectures/L26-MoreGraphs/state_mach.html After reviewing these videos and articles, I understand the core concept of state machines. Correct me if I’m wrong, but a blockchain is monolithic. A block is composed of transactions that are executed one at a time. If we abstract the system, a blockchain “is a state machine”. Every protocol built on a blockchain is constrained to think of a state machine system. Otherwise, there will be some problems. ...

How are you doing? I hope pretty well! Today we will discuss lesson 5. Additional Useful Flags Follow the instructions on ScriptExercise2: We are only using two flags on this part. Personally, the most useful flag is --method, as it allows you to avoid rerunning all your rules when you are debugging the specification files. About the flag --send_only, it can be useful if you don’t want to analyze the result on your terminal. ...

Everything is clear for the moment? Good because today will be a theoretical lesson on the mindset of how analyzing a bunch of smart contracts. This lesson can be helpful not only in the formal verification sector but also for auditors. Let’s start ^^ A Guide For Thinking About Properties First of all, I recommend you to have a quick check on the introduction of the lesson. I will try to recap with my words. ...

Bonjour ! Comment allez-vous ? The lesson of the day will once again include a lot of theory. Don’t worry, it’s interesting. Let’s start ! Inductive Reasoning Pre-conditions and post-conditions Blog post by Mátyás Lancelot Bors In this post, Mátyás Lancelot Bors offers a definition for pre-conditions and post-conditions. A precondition is a condition, or a predicate, that must be true before a method runs for it to work. In other words, the method tells clients, “this is what I expect from you”. So, the method we are calling is expecting something to be in place before or at the point of the method being called. The operation is not guaranteed to perform as it should unless the precondition has been met. ...

How it’s going? Last lesson we had a theoretical course on inductive reasoning and invariants. This time we will deep dive into how to implement invariants properly. Let’s start! New Concepts Associated With Invariants Pre-conditions Vs. Valid States In the previous lesson (lesson 7), we mentioned the over-approximating state of CVT for reaching full coverage. This can bring some false negatives due to infeasible states that can never occur at runtime. To address this, we use pre-conditions to restrict the set of reachable states. ...

What’s up? We are almost at the end of the lessons. The subject of the day will be quick. Indeed, we will see a phenomenon that can be recurring when writing rules, but the core concept is simple. Let’s start! Vacuous Rules When the Certora tool verifies a rule, CVT will follow the script inside the rule. Let’s create a situation where we call a function, and this one reverts every time regarding the parameters given. Then the test of the rule is useless, and we weren’t able to test the final assertion. For the CVT, there is nothing to signal because there is no assertion returning false. This is what we call a vacuous rule; it’s when a rule creates a false proof of the properties. Don’t be afraid; there are three methods for checking if a rule is vacuous. ...

Hi, it’s me again. Today, we are here for our last lesson! It will be on how to handle loops in the smart contract with the Certora verification tool. In most programming languages, loops are accompanied by possible computational problems. Certora identifies two main problems. The first one is the significant increase of commands execution in the programs depending on your conditions for the iterations, it can considerably affect your programs. The second one is the halting problem. In brief, if you have a Turing machine, loops can break the rules of determinism. For these problems, the EVM chooses to establish the concept of gas to avoid infinite computation. ...