Formal method tools are key productivity aids for authoring correct smart contracts

In What properties must an enterprise smart contract language have?, Simon and Neil stated that “for a contract to be guaranteed to perform as intended, it must be amenable to formal verification methods.” In this blog post, we first discuss what formal methods are and why good language design greatly simplifies the task of applying formal methods. We then present the formal methods tools in use at Digital Asset for our contract modeling language, Daml.

Readers with a strong background in formal methods may jump directly to the second part.

Formal methods — what are they and why do we need them?

A smart contract is a program–and like every program, it is a concise description of what will happen when we run the program on a computer. The program’s behavior is what we can observe during its execution. Different program inputs produce different behaviors, and these behaviors additionally depend on the environment, e.g., thread scheduling in a concurrent application. Any given program can exhibit a myriad of behaviors, possibly infinitely many. When we write a smart contract, we want to be confident that we understand all possible behaviors.

Program testing can be a very effective way to show the presence of bugs, but is hopelessly inadequate for showing their absence. 

Edsger W. Dijkstra, one of the most influential computer scientists of the 20th century

A fundamental limitation of testing, which is all about observing individual program runs, is that it can never encounter all possible behaviors of a program–there are just too many. Testing cannot guarantee that when the code is shipped, someone won’t discover an outlying behavior — a corner case — that had not been covered by the tests. For example, this was the case for Intel’s Pentium floating-point division (FDIV) error in 1994, for which Intel had to set aside $475M USD to cover the cost of remediation ($800M in today’s dollars). In the blockchain domain, the DAO incident is just one example where the monetary cost of an erroneous smart contract was significant.

Formal methods circumvent this limitation by not relying at all on the running of the program; instead, they reason mathematically about the program code itself. This reasoning is grounded in a formal semantics of the programming language, i.e., a mathematical description of how all the language primitives behave and how they interact. Such semantics turn a piece of code into a mathematical object. Fortunately, we do not need to be mathematicians to apply formal methods — formal method tools codify all the required reasoning in their analysis algorithms.

The gold standard of formal methods is formal verification, which is the act of proving or disproving the correctness of the code with respect to specific formal properties. This form of quality assurance builds a mathematical proof that all execution paths satisfy the given properties–not unlike how algebra is used to solve equations.

For example, financial markets often use netting to improve efficiency and lower capital costs of settlement by consolidating the value of multiple positions or payments to be exchanged between parties into the fewest possible number of actual transactions. One property of the settlement algorithm, therefore, is that it must ensure that before and after netting the aggregated amounts remain the same for all (pairs of) parties. Such a property is simpler to understand than the behavior of the code itself — and therefore easier to correctly specify — because it focuses on essential characteristics of the code and can elide irrelevant behavioral aspects.

Every analysis tool supports only a certain class of properties, and the expressiveness varies a lot between the tools employed. Proof assistants likeIsabelle/HOL and TLA+ can handle very general mathematical properties, but their usage requires expert knowledge and substantial manual effort. At the other end of the spectrum, fully automatic formal method tools analyze the code only for very specific properties, but are usable by many programmers. For example, a type checker can ensure type-safe execution. In this case, the burden on programmers is minimal: they simply declare the types of program variables and functions, and the checker takes care of the rest. Between the two extremes, we can find a wealth of formal methods techniques, e.g., static analysis, symbolic execution, and model checking.

Techniques across the whole spectrum are being put to good use in industry, e.g., at Intel, ARM, Microsoft, Facebook, and Amazon. And it is not always about large-scale system verification — employing the automated tools during the specification and development of software systems can greatly reduce the programmer’s burden in writing correct code. Also before coding, at the design stage, formal methods can support building simpler and clearer designs.

However, formal methods are not a panacea; testing and validation remain necessary. The following diagram illustrates why. Although formal methods construct mathematically precise proofs, these proofs are based on the formal semantics, which is just a model of the real world. Like every model, such a semantics formalizes only certain aspects of the full behavior.

For the proof to be meaningful, we must ensure that the semantics faithfully models the real world, e.g., using traditional validation techniques. Moreover, we must also be confident that the formalized property actually captures the intended property–in particular, that the model covers all relevant aspects, which is especially important for security properties. Again, validation and testing can help establish confidence. Nevertheless, formal methods can significantly increase productivity: while we must run the formal analysis on every program, the semantics’ validation need only be done once for the model — not for every program, like with traditional testing. The same applies to the validation of properties that apply to many programs, e.g., type-safe execution.

Formal methods go hand in hand with good language design

How difficult it is to employ formal methods at development time is directly related to the language’s design; a language that was not designed with formal methods in mind can present a number of complications to the programmer as they strive to produce correct code. And a poorly designed language does not just make it hard to write correct code during development — it makes it virtually impossible to formally verify that code because its semantics abounds with corner cases.

Following are just two classes of issues exposed by some programming languages being used for smart contract development today that can inhibit the use of formal methods.

Too many corner cases. For every unit of code, it should be clear and easy-to-understand what that code does. If the behavior fans out into many cases, hackers have a better chance to exploit poorly understood corner cases.

For example, consider the relatively simple expression x + 1. In a statically typed language with overflow checking (such as C#, with checking enabled), if x is an integer, x + 1 denotes the next integer larger than x or raises an overflow exception if x was already the largest integer that fits into the range. In contrast, in a language such as JavaScript — where there is no strong type system and the + operator is overloaded — the expression x + 1 results in

• A string appended with the character 1, if x is a string. This holds even if xis a string of digits, perhaps because the programmer forgot to first convert the string into a number.
• x, if x was sufficiently large (say, 2 to the power of 53 — this post on safe integers in JavaScript explains why).
• Additional behaviors, if x is neither a string nor a number (e.g., an array or an object).

This is rather unintuitive; and when working with such a language, programmers must keep all this complexity in mind! In practice, most programmers only consider the most frequent cases and ignore the corner cases.

A simple example from geometry helps to illustrate these complications: drawing a triangle on paper using a pen and a drawing tool.

A well-designed language is like the upper straightedge, which you can easily use to draw the three sides of a triangle without having to worry about anything except the angles between the sides–it even protects against accidentally drawing beyond the end of the straightedge (think of overflow checking for integers). In contrast, programming in a poorly designed language with many corner cases is more like drawing a triangle with the lower ‘straightedge’. Of course, it is possible to draw a nice triangle with such a tool, but you constantly have to watch out to avoid getting caught in the irregular areas, i.e., the language’s corner cases.

In the DLT domain, Ethereum’s language Solidity is a good example of a contract language that suffers from such special cases. For example, when a function calls a function of another smart contract, the callee itself may call back the first function such that it executes again. In combination with the mutable state of Ethereum accounts, this mechanism opens the door to reentrancy attacks, one of which caused the DAO incident.

Certainly, formal methods can force consideration of all the corner cases. But just imagine how many checks and case distinctions would be necessary with a poorly designed language–so why choose such a language in the first place? Look for a type-safe language with proper checks to make development simpler.

Loss of abstraction. In A new language for a new paradigm: smart contracts, Ben and Edward discussed how programmers use abstraction to write clean code. If a language does not support the right level of abstraction for the task at hand, the programmer must manually encode these ideas using lower-level primitives — as well as analyze to what extent the encoding achieves the desired abstraction, and under what circumstances it may break down. While this may produce functionally correct code, such encodings impose an unnecessary burden on the programmer–and on formal methods tools alike, as they have to infer the abstraction and their high-level property from the low-level encoding.

Returning to the world of geometry for illustration, imagine you were given the task of writing a program to draw a triangle but were only given a grid of pixels and a pen to blacken individual pixels. A programmer can, of course, implement a line drawing algorithm to obtain a triangle like the following. But without the abstract concept of a line, it’s basically impossible to verify geometric constraints for such an assortment of pixels.

In this example, a good language is like a well-designed vector graphics library. It directly encapsulates the required abstractions once and for all, such that programmers can readily use them and apply analysis tools to reason about them. Look for a language that supports the right abstractions for the task at hand-writing contracts.

Formal methods at Digital Asset

Daml avoids these issues — and many more — because it was designed with formal methods in mind. A few examples:

• As Daml is a functional language, Daml programmers have the full toolbox of functional programming available for structuring their code and modeling their data, e.g., parametric polymorphism, higher-order functions, and algebraic data types.
• Treating contract concepts as native to Daml gives programmers the level of abstraction they need to write contracts without concern for DLT implementation details like synchronization and cryptography.
• Having Daml store contract data on the ledger using the structured data model, as Edward and Ben pointed out, “frees programmers from the burden of hand encoding their data into an ill-fitting backend storage system”. In comparison, writing programs in Ethereum’s instruction language is like programming in assembler, where memory is an unstructured sea of bytes and programmers must not forget to validate their encodings — or risk attacks such as short addresses.

For the Daml developer, we currently offer two analysis tools for Daml smart contracts, described next. Both are integrated into the development tooling to give Daml developers instant and continuous feedback on the code they are writing.

Daml has a strong type system tailored for enterprise agreements. Functional languages with a strong type system and clean semantics, such as OCaml, Haskell, ML, and F# are amenable to formal analysis in part because the types reliably document how a piece of code may be used. Daml is similarly built on a sound, static type system with type inference. The Daml type system distinguishes between pure functions and updates to the ledger, which supports the programmer in keeping the program logic separate from ledger updates. Such separation of pure and impure parts improves code quality in general. Just like contracts can be smart, type systems can be smart, too!

Daml checks authorization. In their blog post, Simon and Neil pointed out that for the consequences of a contract to be compulsory, entrance must be voluntary. Then, as described by Martin and Jost, Daml makes the signatories to a smart contract explicit, and a runtime authorization check ensures that every ledger update has been authorized by the relevant parties–directly or indirectly through delegation. To prevent the possibility of a smart contract getting stuck on the ledger due to lack of authorization, the Daml SDK provides a static analysis based on abstract interpretation that flags potential lack of authorization in workflows, e.g., because the programmer forgot to specify that a party must agree to some smart contract being created.

At Digital Asset, formal methods do not stop at this level. We have also formally verified core parts of the DA Platform using interactive proof assistants including Isabelle/HOL and TLA+. For example, we have formalized Daml’s authorization and privacy models, and verified the enforcement algorithms.

Throughout the course of this blog series, we have taken an in-depth look at Daml: a language of contracts; a language of privacy; a language of ledgers; and a functional language. Although we are already using Daml to build some very sophisticated projects (see, for example, our work with the Australian Securities Exchange), it is still, as of this writing, in Developer Preview as we systematically deliver on our roadmap. Our approach with respect to formal methods tooling has been to deliver this tooling in stages, beginning with support for the development process and folding in more formal methods tooling at later stages.

In the long run, it is our intent to take formal methods to the next level, where Daml and the Digital Asset Platform are not only engineered and tested following best practices, but their critical parts are formally verified.

Read Part 9: Smart contract code: when what you don’t write is as important as what you do

New to this series about Daml? Click here to read from the beginning!

Join the community and download the Daml SDK.

This story was originally published 7 August 2018 on Medium

About the author

Andreas Lochbihler, Ph.D., Formal Methods Engineer — Language Engineering, Digital Asset. http://www.andreas-lochbihler.de/

Andreas joined Digital Asset’s Zurich team in early 2018 to work on emerging systems architecture, and formal methods for Daml. Prior to joining DA, he was a senior researcher in the Information Security Group at ETH Zürich, where his research revolved around the formal verification of cryptographic constructions. His framework CryptHOL brought to cryptography the expressiveness and rigor of higher-order logic and coalgebraic methods as implemented in the proof assistant Isabelle/HOL. Before joining ETH, he was a member of Programming Paradigms Group at the Karlsruhe Institute of Technology and of the Software Systems Group at the University of Passau.

Andreas holds a Ph.D. in computer science from Karlsruhe Institute of Technology. His thesis on the semantics of concurrent Java involved building and formally analyzing a model of Java concurrency which covers source code, bytecode, a virtual machine, the compiler, and the Java memory model.