Formal verification for the blockchain
Testing has been around for a long time and is the most common way to make sure your software runs correctly. Developers have it drilled into their heads to test everything to make sure that their code quality is reasonably bug-free. This is 100% a satisfactory practice for regular applications because if you make a mistake, worst-case scenario, you can just roll back your application to a previous state. This is not the case in blockchain. If a hacker finds a loophole in your application they will take all the money and there is very little anyone can do about it. Game Over. However, there is another option: Formal Verification. Formal Verification has its downfalls too, but at Reach, we have been working hard at making Formal Verification accessible to the traditional developer.
The difference between testing and formal verification is that with testing you provide values into the piece of code you test and you test that the result equals what you expect it to. With formal verification, you mathematically prove that no matter what values you put into the code you want to prove correct it will always provide you the expected outcome.
There are many types of testing. Unit, End to End, Regression, and others. The problem with testing is that “Testing shows the presence, not the absence of bugs” — Edsger Dijkstra. For example, if you have a thousand tests, then what do you know about your program? If one test fails, then you know either (a) the program is incorrect, (b) the test is incorrect, or © both are incorrect. This is valuable information that helps you improve your software. On the other hand, what if every test passes, then what do you know? You know that if your program is incorrect, you haven’t thought of the right situation that leads to the flaw being exposed. You know that if you deploy your program, and it is used only in the ways your thousand tests predicted, then it will have the expected behavior. This is an unlikely scenario for most programs, which have dramatically larger state spaces than can feasibly be explored in the number of tests engineers can write by hand.
However, there is another option, Formal Verification. Formal Verification uses a kind of “algebra of programming” to reason about all possible behaviors a program may exhibit all at once. It is not a new technique: the first computer-generated proof was created in the 50s; indeed, early computer scientists were primarily concerned with performing formal verification, not playing PacMan or even simulating nuclear explosions. and we’ve come a long way since then. There are many forms of formal verification: interactive theorem proving, SMT solving, model checking, static analysis, manual Hoare logic-style proofs, and so on. Each of these techniques has multiple specialized domains where they are commonplace. However, formal verification is rarely applied to general-purpose programs
The reason why we don’t formally verify everything is that it is extremely difficult. Most techniques require great expertise (i.e PhDs and special training) and drastically increase the development time (some studies suggest by up to 100x). This is why most developers have no experience with it. Actually, this is not quite true; most developers are familiar with type systems, such as those found in Java or Haskell. These type systems are examples of the cheap application of formal verification techniques: a type system automatically checks a program to determine if certain categories of errors are missing, and only if it can verify that they are, then the program is allowed to run. We don’t normally think of type analysis as formal verification, because it is so automatic and in the background to most software engineering. Reach is deploying a different kind of formal verification in the same way.
One of the great things about blockchain networks is that they are much more limited by design than traditional applications. Because of this, we at Reach have designed a development platform that automatically formally verifies many common mistakes that a blockchain developer would make, and made it very easy to insert custom assertions for their specific applications. This platform is analogous to a more advanced type system that allows the cheap specification of basic correctness properties of a program. Reach allows a traditional developer, with no special training, to take advantage of a tool that is 100% necessary in a world that if you make a mistake it means game over.
When a developer writes their applications with Reach they receive:
Guaranteed Security: If code is law, it’s completely convoluted law that is extremely difficult to understand. Reach’s proofs give you easily understood laws that their users can rely on, because the properties it verifies are specified inside of the program in terms of the basic data of the program, not a separate abstracted model of how the program runs.
Reliable Security: If after a long security audit a developer wants to change a couple of lines of code there is a reasonable chance that the change will break all the security guarantees that the audit provided. With Reach, you don’t have that problem, because the security properties are embedded in the program and will be automatically checked every time you modify or recompile.
Blockchain has limitless opportunities, but those opportunities come with a lot of risks. We are still working on Reach, but we invite you to check out our progress and join our community so you can help us make the right decisions as we move forward.
Reach Github: https://github.com/reach-sh/reach-lang
Reach Telegram: https://t.me/reach_sh
Reach Website: https://reach.sh
Resources:
https://en.wikipedia.org/wiki/Formal_methods
http://gauss.ececs.uc.edu/Courses/c626/lectures/Intro/std.pdf
https://www.eeweb.com/profile/adarbari/articles/a-brief-history-of-formal-verification
