Formal Methods: Correctness in Blockchain Design
2023-03-06 by
zoe
Formal methods use mathematical processes to pinpoint and test the components of a system, and the functionality of each of them. 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 helps DApp developers to achieve this by using formal methods.
The topic of formal methods can be further divided into the following 2 major subtopics:
Formal specification: A process used to define the functionality of a system’s components
Formal verification: A process used to prove or disprove the correctness of the functionality of the algorithms that make up a system
Formal methods for the blockchain
Multiple hacks continue to hit the blockchain and decentralized applications.
Smart contracts have stricter security requirements than many other types of programs. There is often real money at stake, and the immutable nature of the blockchain can make it difficult to upgrade code after deployment.
Securing can be achieved by properly defining each component from the start of the system’s design and continuously proving their absence throughout their development.
Formal verification does just that, adding mathematical proofing rigor to the “shift left” concept, commonly associated with the DevSecOps movement.
MuKn Offerings
Mutual Knowledge Systems (MuKn) offers formal verification consulting services.
Our implementation of formal verification allows 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?
Design principles of Glow, our domain specific programming language for decentralized applications clearly define functionality, such as:
- Cryptographic specification
- Tracking of accounts, balances and transactions, and confirmation of their proper execution
References / Further Reading
[/vc_column_text][/vc_column][/vc_row]