Formal Verification in Cryptocurrencies
What is Formal Verification?
Formal verification or formal proof is a formal proof of compliance or non-compliance of the subject of verification with its formal description.
Verification consists in creating an abstract mathematical model that is related to the technical characteristics of the product (eg, algorithm, hardware chip), while the formal methods used to create the model are mainly based on the theoretical foundations of computer science.
Mathematician Martin Davis is credited with developing the first computerized mathematical proof as early as 1954. In the 1960s, this concept began to be used to check the correctness of computer programs in Pascal and Java. After a series of high-profile computer bugs, such as the Pentium FDIV bug in 1994, the notion that formal verification should be ubiquitous became widespread.
The use of formal verification has become extremely important in hardware systems, where it is used by almost all major hardware manufacturers to ensure the reliability of their products. However, its use is not as common in software as it is in hardware, mainly due to the commercial nature of hardware manufacturing.
Formal verification can be used to verify systems such as source code software, cryptographic protocols, combinational logic circuits, digital circuits with internal memory. Formal verification is carried out by Windows and MacOS kernels, space rocket control systems, nuclear power plant software and other software systems, where an extra gap can cause billions of dollars in losses.
However, this dynamic is starting to change with the advent of blockchains and cryptocurrencies, where money transfers are done autonomously through a decentralized network. With more value at stake than in traditional systems, the correctness of smart contracts has become a pressing issue.
What Is Formal Verification in Cryptocurrencies?
Every year, the use of smart contracts is increasing more and more in various areas of the digital industry: banking, legal organizations, logistics companies, exchanges. These are areas in which the theory of smart contracts can greatly simplify the interaction of two or more parties.
A smart contract is a computer algorithm for generating, managing and providing information about the ownership of something. In a narrower sense, a smart contract is a set of functions and data located at a specific address in the blockchain.
In other words, a smart contract is an agreement between several parties on the establishment of legal rights and obligations that are written in the form of a program code and executed in a special software environment.
The main application of smart contracts is related to the implementation of distributed registries, the blockchain, the semantic basis of which is the absence of an intermediary between the parties signing a smart contract. Nevertheless, it is very likely that with the development of digital technologies, smart contracts will be able to become the main guarantor of the execution in the broadest sense of the legal conditions for the execution of an agreement concluded between two or more parties.
Smart contracts have the following properties:
The structure of smart contracts is based on a cycle: “If … then”, “If <<contract execution condition>>, “then” <<operation>>. After the execution of the contract, the result of the operation is recorded in the distributed ledger.
Example: if a horse wins at a horse race, the smart contract performs the operation of transferring the winnings to the contract participants according to the conditions specified in the contract in advance.
Smart contracts are contracts implemented in a programming language, which minimizes the possibility of different / incorrect interpretation of the contract by the participants in the interaction.
The environment for launching and executing smart contracts provides a reliable environment that ensures the transparency of interaction and the authenticity of tracking transactions/operations.
The technology of smart contracts is based on working with a decentralized registry, any participant can access the distributed registry and check the correct functioning of the smart contract, according to the previously described conditions of the concluded agreement. This ensures the integrity of the data, and also prevents the falsification of data and the terms of the contract agreement.
All this makes the use of smart contracts quite convenient and attractive tools for the interaction of the parties, when control over the execution of the terms of the contract and transparency of interaction are required.
However, smart contracts have a number of disadvantages:
- Smart contracts are based on program code, any error in the code leads to incorrect execution of the contract, this imposes high requirements on the accuracy of the contract description, as well as increased responsibility on the developer of the program code.
- When crating a complex smart contract that must take into account the behavior of several parameters of the conditions for the execution of a contract at once, the contract developer needs to control the behavior of several conditions of a complex multicomponent contract system at once. This makes the process of creating a contract a difficult task that not all developers are ready to take on.
- The impossibility of reviewing the result of the execution of a smart contract and making changes after accepting the terms of the agreement between the parties. At the moment, there is a discussion on introducing the possibility of a smart contract having a third independent party, with a confirmed legal status and the right to make changes to the program code of the smart contract, which would allow not to recreate a new contract, but to correct an existing one, if in the process of interaction of the parties to the contract came to the understanding that the conditions for the execution of a smart contract need to be reviewed.
- Uncertainty of the legal status of the smart contract. At the moment, the smart contract does not have a legal status, primarily due to the impossibility of revising the conditions for its execution.
These shortcomings require us to think about the introduction of additional verification / testing of the smart contract program code to increase the reliability and correctness of the conditions for its execution.
One way to solve this problem is to use formal verification of smart contracts.
Formal verification can be perceived as a type of testing, if roughly – we guarantee that the system will work according to the described scenario and will not fail in logic.
Also, formal verification can serve as a bridge for understanding between the developer of the contract and its customer. Often, customers want to be sure that a fixed smart contract performs exactly the actions and according to the conditions agreed upon by the parties to the contract. But how can you be sure of this if the parties to the contract do not know programming languages?
One of the solutions is to build automata and diagrams based on the formal smart contract model. Diagrams and graphs regarding the program code have a lower threshold for perception, they are easier to read and it becomes clearer and faster to understand what exactly and how the smart contract does.
Thus, formal verification performs two functions at once: verification of the logic and basic functions of a smart contract and an image of the operation of a smart contract using a state flow diagram, state machines.
It should be noted that the formal verification of smart contracts can play the role of a kind of auditor in the modern digital industry.Obviously, additional verification is required, especially when it comes to financial transactions or other actions, the cost of errors of which is quite high. Auditing and testing is commonplace in economics and engineering. The technology of smart contracts stands at the intersection of these areas, so it is quite logical to apply to it increased requirements for the reliability and security of operations.
The stage of formal verification of smart contracts can be compared with the presence of an intermediary institution that checks the correctness of the logic and validates the correctness of the stated contract conditions.
The use of formal verification and formal modeling can greatly reduce the time costs of developing contracts by checking their correctness at the early stages of contract development.
Current Applications of Formal Verification
Several platforms are either already integrating formal verification or planning to do so soon. Assessing the security of the smart contracts that run on these platforms will be vital to assess their effectiveness in mitigating critical vulnerabilities.
Zilliqa
Zilliqa is a high performance blockchain designed to host scalable and secure decentralized applications (dapps). Several Zilliqa developers were the authors of an earlier study that revealed thousands of weaknesses in smart contracts.
Zilliqa uses a new programming language called Scilla developed by members of the Zilliqa team and some other affiliates. Scilla is an intermediate level language built into Coq Proof Assistant. It is intended to be translated into higher level languages to perform analysis and validation before compiling contracts into bytecode.
Tezos
Tezos is written in OCaml and its smart contract language is Michelson which is based on OCaml. OCaml was chosen for its functional programming offerings for speed, unambiguous syntax and semantics, and formal proof implementation capabilities. Tezos also uses Coq Proof Assistant to formally validate smart contracts.
Arthur Breitman – the co-founder of Tezos – posted details about verifying some of Michelson’s Coq contracts, including a multi-signature contract on his testnet last year. Tezos was launched relatively recently, so its application of formal verification should provide an excellent indicator of the state of increased security of smart contracts using this method. Whether the exploits that targeted Solidity contracts will work in Tezos will take some time to uncover, but assessing how secure smart contracts are becoming in Tezos could be very indicative of a continuing trend.
Cardano
Cardano is written in Haskell and its smart contract language is Plutus, which is based on Haskell. Cardano is designed with the Cardano Computing Layer (CCL) which consists of 2 layers:
- Formally specified virtual machine and language environment.
- Officially specified languages that facilitate verification of the smart contract code.
The goal is to create an environment that streamlines the process of ensuring that the contract functions as intended without catastrophic vulnerabilities. Notably, Cardano does not use a limited stack design like the Ethereum EVM, so without worrying about stack arithmetic flow, it can formally validate smart contracts much more easily.
Ethereum
Ethereum has been exploring the possibility of including formal verification for quite some time, and several projects are exploring its potential. One such publication focuses on smart contract bugs and suggests ways to fix them, including improving the operational semantics of Ethereum to allow for formal verification.
Ethereum gas limits make formal verification difficult. Also, the only way to find out the meaning of a Solidity program is to compile it into bytecode. The compiler changes quickly, so verification tools must also adapt to the speed of change.
Conclusion
Smart contracts should be implemented in a language that is easy to verify. Therefore, functional languages like Haskell or OCaml are more suitable for smart contract code than imperative languages like C/C++, Java, and JavaScript, because the architecture of functional languages is easier to justify and formally verify. Of course, most programmers are more familiar with JavaScript, but in this case, between ease of use and security, you need to make a choice in favor of the latter.
On the other hand, it must be remembered that formal verification has certain limitations. It is not fully automatic and still requires human intervention. In addition, formal verification can only prove the characteristics that we intended to test; if you mistakenly check for the wrong functions, vulnerabilities may remain open. However, if implemented correctly, it will be a step in the right direction.
Formal verification is a very complex and time-consuming task. Despite this, it has become a universal standard in the hardware industry and is likely to continue gaining momentum in the software field. Blockchains and cryptocurrency networks, where large transfers are common, will undoubtedly accelerate this effect. Measuring the positive impact of formal smart contract verification will likely take a few years as we see only the beginnings of what should become a much broader industry trend.