Author: Palina Tolmach This blog post serves as the second installment of a two-part series exploring the concept of symbolic execution for smart contracts. For background information on symbolic execution and an overview of existing tools for Ethereum smart contracts verification, be sure to check out part one! In this post, we will dive into the topic of symbolic testing. The first half of this post will provide a comprehensive review of existing tools that support symbolic testing for EVM smart contracts. In the second half, we'll share our own experience of integrating EthBMC—one of the top-performing tools from part one—with the Foundry development framework to enable symbolic testing. What is symbolic testing? Symbolic execution provides an effective way to identify potential vulnerabilities in smart contracts by analyzing multiple execution paths simultaneously. However, it can also be limited by scalability and usability problems. Symbolic testing partially addresses these issues by analyzing tests using symbolic inputs rather than systematically examining all possible sequences of function calls made to the smart contract. Symbolic testing also allows reusing existing unit or fuzz tests for formal analysis, removing the necessity to separately define specifications, a labor-intensive blocker for adoption. Last but not least, symbolic testing also takes advantage of the setUp() function that is usually supported by testing frameworks such as Foundry, which helps (concretely) set up the initial state for the analysis; this feature is particularly useful for symbolic execution tools like hevm and EthBMC that analyze runtime bytecode, which does not include constructor logic. Let's consider a simple smart contract example from the previous post. The contract is based on the code included in an issue from the Foundry repository titled condition not caught by invariant/fuzzer. We're interested in the assert on line 15, which should fail if the function is called with x being equal to 6912213124124532 (6912213124124531 + 1).

Author: Palina Tolmach Formal verification techniques are widely regarded as a trustworthy, although complicated, way to rigorously ensure security and correctness of smart contracts. One such technique is symbolic execution, which allows users to check whether an execution of a program can violate a certain property or reach a vulnerable state. Symbolic execution is in the spotlight lately, with many tools available, including established ones like Mythril or Manticore, or newer ones like Halmos. In this blog post we introduce symbolic execution and explore the existing bytecode-level symbolic execution tools for Ethereum smart contracts. We discuss our experiments with some of these tools and highlight their strengths and limitations. We also conveniently provide shell commands for you to reproduce every experiment! This post is the first of two on the topic of symbolic analysis of smart contracts. The link to part 2 covering symbolic testing will be here once it's ready, so check back later! We publish a small smart contract benchmark in this post, and an extended version is to come in the later one. For now, enjoy part 1! What is symbolic execution? If you know the answer to that question, feel free to skip to the next section :)

Authors: Kurt Barry (MakerDAO), Uri Kirstein (Certora) Introduction "It ain’t what you don’t know that gets you into trouble. It’s what you know for sure that just ain’t so." - Mark Twain Multi-Collateral DAI, the stablecoin managed by MakerDAO, is one of the largest cryptocurrencies. Launched in November 2019, it has, as of May 2022, a market cap of roughly 6.5B$ backed by about 10B$ of collateral. Ancient by crypto standards, if its smart contracts contained any bugs, they should have been found long ago. Surprisingly, it was discovered that a relationship between system quantities considered to be an invariant, known since 2018 and even thought to be mathematically provable, did not hold. This anomaly was found using the Certora Prover. Fortunately, no funds were or are at risk. This finding is an important reminder that one must be very careful to distinguish between things that are likely true and those that are actually proven (keeping in mind that proofs can contain mistakes too!). The Certora Prover To keep DAI and its backing collateral safe, the MakerDAO Protocol Engineering Core Unit (PECU) uses a variety of processes and technologies. Code changes undergo extensive internal review and must pass unit and integration tests. Mistakes are searched for via red teaming, fuzzing, and external audits. MakerDAO also has an Immunefi bug bounty program.