Glow Formal Verification Stage 2

Background

Smart contracts have much stricter security requirements than many other programs: there is often real money at stake, and the immutable nature of the blockchain can make it difficult to upgrade code after deployment. This means that more effort, time, and money must be spent ensuring correct contracts ahead of time, and this has inhibited the popularity of smart contracts in many industries.

MuKn's solution to this problem was to build a domain-specific language for smart contracts, which we call Glow. We released our initial version on the Cardano KEVM in February 2021 with first-class abstractions for accounts, participants in an interaction, and cryptographic operations. Although Glow has many safety features built-in (e.g., accounts must balance, escrow is automatically released on timeout, etc.), its safety guarantees can be substantially augmented by having the contract developer state propositions that should be true of the program as a whole (e.g., there must be a winner of a game, some statement must be reached by all participants, etc.), encode them as assertions in a meta-language (an assert statement), and automatically prove or disprove them. This process is known as formal verification, and it lets developers write safer contracts in less time.

It does this by allowing developers to ask: does the business logic of our contract really make sense? In particular:

• Am I really implementing what I intended to?
• Can I guarantee that each participant will be always able to do what was specified?
• Am I sure that all participants won't be able to trigger any undesirable outcome?
• Am I sure we don't accidentally transfer funds to the wrong account?
• Am I sure that the amounts transferred between accounts is fair?

We jump-started development of our Formal Verification Engine for Glow with help from Catalyst 5 funds: thanks to the backing of voters, we now have a working proof-of-concept. It is currently able to verify a limited set of assertions about a Glow program, but we want it to do more!

After testing several different versions of syntax and semantics of assertions, and with our initial implementation in place, we are ready to begin the project's next stage. This phase will expand the capabilities of the Formal Verification Engine, introduce a new tool for Glow programmers, and employ cutting-edge formal verification techniques to ensure the correctness of critical parts of the Glow Formal Verification Engine itself.

Our proposal will make formal verification tools more readily available to teams of all sizes. All Glow code and all of the Formal Verification Engine code is licensed under the Apache 2 license. 

Deliverables

We expect to deliver the following after three months:

Glow programmers will be able to express important properties of the contract inside Glow program source code.

They will be able to add special lines to their code directly describing both desired and undesired outcomes of the contract, and the Glow compiler will make sure that the program always executes accordingly.

This functionality will allow developers to:

Write assertions about the:

1. value of variables:

• a == 3

• b > 2

2. reachability of specific parts of Glow program

• reach(pointX)

3. account balances of the contract account and those of the participants

• gain(participantA) > 0

• gain(participantA) == loss(participantB) + x

For each assertion, the Glow developer will be able to specify for each participant:

• Game-theoretic directives expressed by inclusion to one of the groups:

• Cooperating participants: who will benefit from the validity of assertion and are expected to act in its favor.

• Adversarial participants: who will benefit from the invalidity of assertion and are expected to act against it.

• Assumptions about the honesty of their execution environment.

Combine assertions with logical connectives to express fine-grained rules:

• reach(pointX) =>
        (reach(pointY)
                && (gain(participantA) > gain(participantB)))

If the formal verification engine detects an inconsistency during compilation, the compilation process will be interrupted, preventing the developer from compiling and deploying a faulty contract. In that case, a human-readable output will be produced to help the developer address the issue.

Budget and Resources Required

We anticipate this work taking the efforts of a senior architect, a senior support engineer, and a junior support engineer. whose combined cost is $25,333.00 per month.

Implementation strategy

A working proof of concept of this system—capable of automatic checks of assertions—was implemented with the help of a Catalyst Fund 5 grant. With the funds from this Catalyst Fund 7 grant, we will be able to ship production-ready implementations and perform formal verification of some of its key parts.

Our system uses the Z3 Theorem Prover to produce proofs over propositions generated by our compiler. Some models and meta-models will be written in the dependently typed language of the proof assistant Agda. Using these off-the shelf components allows integration with third-party developer tools and even independent Glow compiler implementation.

Future

In the next steps (not funded by this current proposal), we will broaden the scope of verifiable Glow programs and assertions about them by integrating additional external tools like LTL and CTL model checkers and Computer Algebra System. Since our model is well suited to future modifications, one of our key goals will be to express assertions about randomness and the basic properties of cryptographic functions. We expect to deliver this after about six months.

In the longer run, we will implement automated economic analysis of contracts.

Completion of the grant will also result in the formalization of the specification of Glow Language. This will be an important step on the way to proving the correctness of our implementation in the future.

We have already begun planning for these future steps; please see our attached Outline of large-scale plan for applying Formal Methods to Glow ecosystem.