Automated Bug-finding for Plutus

[GENERAL] Summarize your solution to the problem.

We have already built Yogo, a semantic search and bug-finding tool for C, Java, and Python based on automated reasoning techniques, published in PLDI 2020. We will add Haskell/Plutus support.

[GENERAL] Summarize your relevant experience.

Already built this tool for C, Java, and Python. Leader has a Ph. D. in programming languages from MIT, specializing in multi-language programming tools.

[GENERAL] Requested funds in USD.

[IMPACT] Please describe your proposed solution.

We have previously built Yogo, which uses automated reasoning to find buggy code in multiple languages. Yogo allows a user to write rules that allow Yogo to recognize many different forms of a high-level concept such as “user-specified value,” and then write queries based on these concepts such as “find any place where a user-specified value is used to choose a currency.” The upshot is that, from a short query, Yogo can find nearly every place in a codebase that semantically exhibits a certain class of buggy behavior, even when it bears no syntactic resemblance. For example, in our PLDI 2020 paper introducing Yogo, we used it to find a bug in Oracle’s Graal codebase (1.2 million lines of Java) which had been missed by a custom static-analyzer designed to find that exact type of bug.

With this grant, we will bring Yogo to Haskell and Plutus, and develop rules and queries for finding common bugs and vulnerabilities in smart contracts.

Yogo is built on the Cubix multi-language infrastructure, which currently supports C, Java, JavaScript, Lua, and Python. We will add Haskell support to Cubix, then add Haskell support to Yogo, and then write several bug-finders using Yogo.

[IMPACT] Please describe how your proposed solution will address the Challenge that you have submitted it in.

Fund Statement:

How can we create a positive developer experience that helps the developer focus on building successful apps?

Having vulnerabilities in apps and needing to buy weeks of auditor time to find them detracts from a positive experience.

Yogo will be able to discover common vulnerabilities and flaws in a fraction of the time of traditional audits.

[IMPACT] What are the main risks that could prevent you from delivering the project successfully and please explain how you will mitigate each risk?

There are three phases to the project: adding Haskell support to Cubix, adding Haskell support to Yogo, and writing bug-finding static analyses using Yogo. Each carries its own technical risks. We give a brief overview of the risks and mitigations, and then a highly technical description .

LESS TECHNICAL DESCRIPTION

Haskell and Plutus are substantially different from the languages previously supported by Cubix and Yogo. While there is no concern that they cannot be extended to support Haskell and Plutus, there is a risk that it will be able to share much less work with the existing languages than expected. However, there is always the option of only providing partial support to a language, focusing on getting a large enough subset to cover many smart contracts.

There is also a risk that some classes of bugs will be very difficult to encode into Yogo queries.

HIGHLY TECHNICAL DESCRIPTION

The primary concerns when adding Haskell support to Cubix are its differences from other languages in scoping. We will likely need to implement a new generalize scoping system for Cubix so that it can capture the commonalities between variable declarations in Haskell and other languages while still remaining faithful to each.

The primary concern when adding Haskell support to Yogo are in the use of recursion instead of loops, the use of higher-order functions, and the simultaneity of variable declarations. These all require encodings different from any of Yogo’s prior supported languages. For recursion in particular: The key insight behind program expression graphs (PEGs), the representation used by Yogo, is to create a single “loop” node which represents infinitely many states of the program. It is expected that this insight will generalize to recursion, but not yet proven. It should at least be applicable to the most common subsets of recursion found in smart contracts (which should not be doing unbounded computation).

The primary concern with Plutus in particular is the reliance on exceptions in validators. Yogo currently has poor support for exceptions. However, Ross Tate in his thesis did explain how to elegantly handle exceptions in PEGs, the representation used by Yogo.

For building bug finders: Yogo is very good at finding things which are present, but less good at finding things which are absent. It can still be done, but it is much clumsier and slows development. However, many bug-finders rely on showing that things are absent.

[FEASIBILITY] Please provide a detailed plan, including timeline and key milestones for delivering your proposal.

Months 1-2: Addition of Haskell support to Cubix

Months 3-4: Addition of Haskell support to Yogo

Months 5-6: Development of bug-checkers using Yogo, empirical evaluation, refinements to Yogo’s Haskell support

[FEASIBILITY] Please provide a detailed budget breakdown.

James Koppel: 460 hours at $130/hour. (Full rate is $260/hour; company will pay other half)

— 80 hours, GHC 9 upgrades

— 160 hours, adding Haskell support to Cubix

— 100 hours, initial Haskell/Plutus support in Yogo

— 120 hours, refinement of Haskell/Plutus support in Yogo to better handle higher-order functions, Plutus-specific quirkss

Nils Eriksson: 105 hours at $80/hour. (Full rate is $160/hour; company will pay other half)

— 45 hours: Researching common bugs in Plutus smart contracts

— 60 hours: Development of at least 10 different custom bug-checkers in Yogo

[FEASIBILITY] Please provide details of the people who will work on the project.

Dr. James Koppel is a world expert in programming tools development with 10 years of experience working in Haskell. His audit of the blockchain voting app “Voatz” garnered national media attention (see, e.g.: https://www.nytimes.com/2020/02/13/us/politics/voting-smartphone-app.html ), and directly caused the state of West Virginia to discontinue its use. He completed his undergrad at the age of 20 with two degrees from Carnegie Mellon University, was named a “20 Under 20” Thiel Fellow in 2012, and holds a Ph. D. in programming languages from MIT. Through his company Mirdin (formerly James Koppel Coaching, LLC), he has personally trained 250 software engineers in how to write code more flexibly and with fewer bugs.

Nils Eriksson is a senior software engineer with 10 years of experience. He previously worked as a Tech Lead at Discover Networks, where he built core software used in their coverage of the Tokyo Olympics.

Nils Eriksson is a senior software engineer with 7 years of experience in functional programming, and a recent Plutus Pioneer (proof). He previously spent several years as a Tech Lead at Discover Networks, where he built the core software and managed the tech teams responsible for delivering the Tokyo Olympics, Discovery+, Dplay Nordics, Eurosport, and Discovery+ India

[FEASIBILITY] If you are funded, will you return to Catalyst in a later round for further funding? Please explain why / why not.

This grant will create a complete, self-sustaining bug-finding tool for Plutus. It is possible we will return to Catalyst for smaller improvements, such as upgrades for new versions of Plutus TX, support for new libraries/languages such as Plutarch, and new bug-finders built on top of Yogo.

[FEASIBILITY] Are you or any member of your team working on any other proposals in this Fund9?

[FEASIBILITY] Are you or your team working on any other proposals from previous Funds?

[AUDITABILITY] Please describe what you will measure to track your project's progress, and how will you measure these?

We will measure:

• Number of bug-finding queries built with Yogo
• Proportion of vulnerabilities detected in a corpus of code with known vulnerabilities
• Proportion of API misuse flaws detected in a corpus of code with known flaws
• False positive rate

As a non-quantitative measure, we will also construct a “challenge corpus” featuring vulnerable code snippets with varying levels of indirection and obfuscation. Yogo’s ability to find vulnerabilities even in the face of deliberate obfuscation will be strong evidence of its general utility.

[AUDITABILITY] What does success for this project look like?

Success means that developers will be able to use it to get near-instantaneous reports on flaws and vulnerabilities in their code.

Our reach goal is for Yogo to be able to automatically flag more than 2/3 of double satisfaction, resource limit, and clone-script attack vulnerabilities in a corpus of vulnerable code obtained from past audits, as well as more than 1/2 of API misuses in a similar corpus.

[AUDITABILITY] Please provide information on whether this proposal is a continuation of a previously funded project in Catalyst or an entirely new one.

Entirely new.