Category: MythX

Abstract Smart contracts facilitate the transfer of value and help determine digital asset behavior. This results in a higher need for formal proofs and computer-aided checks compared to traditional software which does not typically perform these functions. 0x is an open protocol that enables the peer-to-peer exchange of assets on the Ethereum blockchain. It is one of the largest open protocols with over 30 projects building on top of it, amassing over 713,000 total transactions, and a volume of $750 million.

Contract invariants are properties of the program program state that are expected to always be true. In my previous article I discussed the use of Solidity assertions to check contract invariants. This article expands on the use of invariants and provides a couple of additional examples. An interesting feature of invariant checking on the bytecode level is that it allows you to detect low-level issues, including issues caused by compiler optimisation or idiosyncrasies of the programming language, by defining high-level rules.

In previous posts, we introduced Harvey, a fuzzer for Ethereum smart contracts, and presented two techniques to boost its effectiveness: input prediction and multi-transaction fuzzing. Harvey is being developed by MythX in collaboration with Maria Christakis from MPI-SWS. It is one of the tools that powers our smart contract analysis service. Sign up for our free plan to give it a try! In this post, we summarize our upcoming ICSE 2020 paper and provide a high-level overview of how we use online static analysis to guide Harvey.

This is the third and last post in the MythX series on integrating security analysis of smart contracts into your Continuous Integration (CI) system. In the first part we built a CircleCI configuration. In the second part we built a small and beautiful Travis CI configuration. “But I am using a completely different CI system!” - You, maybe. Fret not. The avid reader might have noticed a common pattern in the past two posts: In setups we used the MythX CLI and a basic Python runtime.

The MythX platform leverages several internal components to provide the best possible analysis results. One of these components is available open-source; the symbolic executor Mythril. In this article, I’ll demonstrate how you can use Mythril to analyze a set-up of multiple smart contracts. By default, Mythril will analyze a contract in isolation. Interactions with external contracts are generalized so that we capture all possible vulnerabilities. Sometimes, this means we find a weakness in your smart contract that might not affect your particular setup.

In the second part of this series on continuous integration, we will build an easy first integration of the MythX API into the Travis continuous integration platform. Other posts in this series: Part 1: CircleCI Part 2: Travis Part 3: (Coming soon) This three-part series is about integrating MythX into Continuous Integration systems. In the first part of this series I have shown how to automatically check for smart contract vulnerabilities in CircleCI.

In the first post of a new series, we discuss integrating security considerations to a continuous integration pipeline, starting with CircleCI. Conveyor belts. Because continuity. Get it? Continuous testing of applications can be hard to figure out. While it is difficult to measure CI/CD adoption, the blockchain ecosystem offers a great opportunity to adopt in-depth testing and continuous delivery pipelines where they make sense: right from the start. At MythX we don’t mind which technologies you are using to get things done.

We’re introducing new plans offering the highest confidence in the correctness of your code, and allowing payment via credit/debit cards for the first time. We’re excited to announce some changes to our MythX plans that will be going live on January 31, 2020. Now, whenever a team announces “exciting changes” it’s often code word for something bad, but in this case, these changes should positively affect (as far as we can predict) absolutely all of our known users.

Leveraging security tools for verification can help you increase confidence in the correctness of smart contract code. Examples are given here using the MythX plugin for Remix. Whether you are a smart contract developer or auditor you might wonder if there’s any value in using an automatic smart contract analysis tool. Assuming you know what you’re doing, will these tools tell you anything you don’t already know? In this article I’ll describe how you can leverage security tools to increase confidence in the correctness of smart contract code and potentially detect issues that are not easily apparent.

We recommend using MythX through every stage of the smart contract development life-cycle, before, during, and after deployment. (Note: This post was originally published in June 2019 and has been updated.) We talk a lot here on the MythX team about the importance of regular, routine analysis of your smart contracts prior to deployment onto the blockchain. The reason for this is simple: once the contract is deployed, it is immutable.