By Joanne Fuller
I want to begin by saying that I am writing this blog post in the hope that others can experience the epiphany moment that I had while learning Dafny as part of my exploration into formal methods. Further, it is my hope that this post will act as a catalyst for others to consider formal methods as a critical and necessary skill within the arsenal of anyone who writes code. As part of the Automated Verification Team within R&D at Consensys, I am using Dafny in the formal verification of the Ethereum 2 Phase 0 specification, and I want to share why I find it useful.
My background
I should make it clear that I am not a software developer, but rather I consider myself to be a mathematical programmer with some knowledge of software development. I first learnt to write programs as part of my maths class during my final year of high school and I probably should mention that although I quite liked using computers at that time, the prospect of learning how to program scared me to the point where I almost dropped that particular maths class. Having decided to face my fear of failure (with respect to learning to program and potentially ruining my result in this class), I went on to experience my first epiphany moment in the context of programming. I can still vividly remember sitting in class and having the realisation that writing a program to solve a maths problem wasn’t some magical and mysterious process, it was almost like writing down how I would work through a problem in my head. There was no looking back after that!
Programming has been an important aspect of everything that I have done since. My PhD in cryptography relied heavily on an ability to develop algorithms and then program optimal implementations. My programs were written for experimentation and, although I didn’t undertake what we would now refer to as formal testing, I would informally check bounds and test cases using logical reasoning about the intended output. I also worked for many years as an academic undertaking research in the field of finance and economics. Again this included writing programs, and again I used my own techniques to informally test and reason about their correctness.
It is fair to say that although I had an appreciation for the fact that testing would always be incomplete in the sense that it was impossible to test every case; that I was reasonably confident that my mathematical way of thinking was pretty good when it came to informally testing in a rigorous manner. As such I definitely did not have a full appreciation of the difference between testing and proving correctness, nor the consequences of such! During my career prior to joining Consensys I was content to rely on my own informal techniques for determining what I thought was correctness via testing.
My background is therefore part of the story, as I am myself somewhat surprised that I did not discover formal methods earlier. I consider myself to be a mathematician; I love maths, algorithms and logic. It now seems crazy to simply rely on incomplete testing, but also it seems crazy for anyone who programs to not at least have some appreciation of what formal methods can offer and the potential consequences of missing a bug given the many ways in which computer programs are integrated into our lives. Formal methods allow us to go beyond testing, to prove that a program is correct against a specification that includes pre and post conditions.
A first Dafny example
As a simple example consider the integer division of a non-negative dividend n by a positive divisor d;
n / d
shown below:
Although in a typed programming language we can somewhat restrict the input parameters, it is not always sufficient. In this example the specification of n and d as natural numbers means that both inputs must be non-negative integers but it doesn’t provide for the restriction of d to being a positive integer. The use of a pre-condition by way of the requires statement provides for such a restriction and means that this method can only be called if d > 0. Hence if any other part of the program would cause div to be called without such a pre-condition being satisfied, then the program will not verify. The ensures statement then provides the post condition and provides a formal specification of what the method output must satisfy.
This example is written using Dafny: “A language and program verifier for functional correctness” and brings me to my next point, that is, why I am such a fan of Dafny. I think it is fair to say that for many programmers, the thought of using “formal methods” to verify program correctness is somewhat scary and is often perceived as being “too” hard. Whether this is because of a lack of exposure to the techniques, a lack of appreciation of the benefits, or even a lack of training in this area; whatever the reasons may be, I believe that Dafny has the ability to allow any programmers to quickly achieve success in applying formal methods in their work. Looking at the code snippet above, I would expect anyone with some programming knowledge to be able to read this Dafny code; Dafny is very much a programmer friendly language. Once you learn a little bit of Dafny it is very easy to start experimenting and then basically learn as you go. And if you are interested in learning Dafny, a great place to start is the tutorial series by Microsoft. The site also includes an online editor, so it is very easy to try out the tutorial examples. The Verification Corner YouTube channel is another source of useful references.
My epiphany moment
Finally I wanted to share my epiphany moment from when I was learning Dafny. I have certainly heard stories about short and simple pieces of code, from large reputable companies, having bugs that were missed and ultimately costing many millions of dollars; but I think it is only when you realise yourself how easy it would be to unintentionally create a bug in a simple function that it all makes sense! The moment when you say to yourself “Oh, it would be so easy to make that mistake!”
My moment came while watching one of the Verification Corner videos.
In this tutorial Rustan Leino goes through a SumMax method that takes two integers, x and y, and returns the sum and max, s and m, respectively. This example is relatively straightforward and the Dafny code is shown below.
The inputs x and y are specified as integers through typing and no other preconditions are required. The three post conditions provide checks that the output does indeed meet the specifications, namely that s does equal x + y, and that m is equal to either x or y and that m does not exceed x and y. The SumMaxBackwards method is then presented as an exercise and this is where it gets more interesting. The specification is the reverse of SumMax, i.e. given the sum and maximum return the integers x and y. Ok, so a first attempt might be with the same postconditions; as the relationships between the inputs and outputs still hold. If we let x be the maximum then a quick bit of algebra tells us that y should equal the sum minus the maximum. Putting this into the online editor gives the following.
It doesn’t verify. So what went wrong? We are told that a postcondition didn’t hold and specifically the postcondition on line 3 (ensures x<= m && y <= m) may not hold. Looking more closely we see that this post condition specifies that x <= m and y <= m. Well, we know that x is less than or equal to m as we set x equal to m, so this means that the y <= m part doesn’t verify. How can this happen? Our algebra told us that y := s - m. Let’s say s is 5 and m is 3, then y = 5 - 3 = 2 which ensures y <= m; but let’s say we call this method with s equal to 5 and m equal to 1. Nothing will stop us from calling the method with these input parameters but to do so will cause a problem as y = 5 - 1 = 4 and then y > m. Basically what we are seeing here is that even though the input parameter is meant to be the maximum of two integers that creates the sum s, there isn’t anything to stop us trying to call the method with an input that isn’t valid. Unless a precondition is included to restrict the inputs of s and m to valid integers that will result in outputs x and y that meet the specification, then our method can produce incorrect results. What relationship do we need between s and m to provide valid inputs? A bit more algebra shows us that s <= m * 2 for there to be a valid solution of x and y. If we add this as a precondition, Dafny is now able to verify the code as shown below.
This was the example where I could see just how easy it is to introduce a bug into code. Just because we call the input parameters ’s’ for sum and ‘m’ for maximum, doesn’t mean that the method will be called appropriately and as such as part of some larger program, there could be many unintended consequences that follow from this type of bug. I hope it is useful for anyone else learning about Dafny or formal methods more generally.
What I am working on now
Well that brings me to the end of my post. If you would like to see what I am currently working on with Dafny then check out this GitHub repo. I am part of the Automated Verification Team within R&D at Consensys and we are using Dafny in the formal verification of the Ethereum 2 Phase 0 specification. The use of formal methods in the blockchain space is an exciting new area of research that has been embraced by Consensys and I would encourage anyone interested in learning more about Eth 2.0 to look at the resources available within our project repo.