So you have a project built on smart contracts, and it needs to be perfect. Blockchains, after all, are distributed trust scenarios, so any problem in the contract will erode investors’ trust. Whatever you’re writing today will eventually end up out there, in the wild, ready to be exploited by unscrupulous actors—and once it’s released, there’s nothing you can do. That kind of pressure can cause many sleepless nights.
Few lines of computer code carry as much weight as smart contracts. Millions of dollars are on the line, and the federal government provides no forgiveness or protection if things go awry. Trying to anticipate all the ways your contract might fail and designing protocols to avoid those vulnerabilities can be daunting.
Fortunately, a little expertise and formal proof that your protocols are secure can help you sleep while other contract authors sweat.
Where does risk live?
Risk in smart contracts comes in four layers:
Protocol-level vulnerabilities
Implementation errors
Security breaches
Blockchain errors
These risks are listed in order of importance, as well as in the order of threat intensity. Let’s take a closer look at each layer.
Protocol-level vulnerabilities
Remember a perfect blockchain, with security invulnerable code, flawlessly implementing a vulnerable protocol, is just perfect execution of a vulnerable protocol that will be exploited. These exploits are unintended consequences of the protocol design. For example, as a protocol author, it’s possible to fail to account for the implications of complex rules interacting, such that a bad actor can exfiltrate funds.
Ideally, smart contract projects formally verify their protocols before a single line of code is written—even better if a theorem prover generates a portion of the code. However, this is rarely, if ever, seen in the wild. Instead, many projects involve a more standard approach, where code is written to completion and then tested for exploits.
The standard approach works as a stop-gap, but it doesn’t replace the need for formal proofs that the protocol itself can be trusted—even if no known exploits are found. These tests are necessarily limited to the imagination of the tester, as in the tester can only test for things they are aware of. Testing the code and showing that some instances work as expected will never prove that ALL cases work as expected, so formal verification is still needed.
Implementation errors
This is good, old-fashioned, incorrectly implemented code, also known as bugs. You are almost guaranteed to have some of these. Luckily, it’s much easier to catch and fix these bugs if your protocol is proven. Furthermore, suppose your smart contracts are coded in a language like Haskell. In that case, you get the static guarantees of GHC’s glorious type system and, likely, property tests, making correctness much easier to achieve.
Even better, if the protocol is proven in Coq, you can code generate part of the smart contract code to maximize the value of the proofs and demonstrate that portions of code are free from error. Few techniques engender trust quite like outputing your smart contract code directly from a theorem prover.
Regardless, code review and tests are needed on the implementation to ensure it faithfully follows the protocol. Therefore, manual testing is also recommended. This is where smart contracts are put into a testing environment, and various “flows” of the protocol are exercised and observed to match the results expected from the formalized protocol.
This way, we can deliver a high degree of confidence that the smart contract code reliably represents the protocol. And since the protocol is formally verified, that same infallibility can now be attributed to the implementation itself.
Security breaches
Even with a proven protocol and a perfectly implemented smart contract, security issues may still exist. Penetration testing is required to overcome these issues. Mitigating security risks involves identifying potential exploits and threat vectors, along with attempting to hack the smart contract in a running test environment.
The exploits used in penetration testing are not common and typically exist due to flaws in shared software protocols. However, penetration testing should still hold someplace in verifying your smart contract project. While a zero-day exploit may still exist, the process of penetration testing is more than sufficient to demonstrate your smart contract system is resilient against attacks.
Blockchain errors
The level of rigor from blockchains varies wildly. On one extreme rests Ethereum’s error-prone results; on the other, Cardano’s proven Pi-Calculus. How much trust you can put in your substrate depends on what blockchain you have chosen. Is it proven technology? And is it well written?
These errors are the least likely to occur but should still be considered. Perhaps your smart contract implementation can work around a bug in the blockchain itself without sacrifice, perhaps not. Either way, getting a code review from a member of the blockchain team is worthwhile if possible, as they may have intimate knowledge of where blockchain errors might arise. But as this is the least likely and lowest impact risk to occur, such a review can typically be delayed or avoided altogether.
Getting Your Protocols Verified
The formal verification process takes the following form. First, the protocol must be formalized into a precise mathematical specification. A qualified logician should perform this step in close cooperation with the protocol author. The communication here is essential, as formalization itself can uncover inconsistencies or incoherence in the protocol. Additionally, it’s vital that the logician formalize the protocol precisely as the author envisions it. There is little value in formalizing a misunderstanding of the desired protocol.
When done correctly, formalization results in a beautiful series of precise mathematical expressions representing the correct execution of the protocol. This stage is the hardest to predict timing and effort, but it rarely takes longer than a few months.
Once the protocol is formalized, logicians can begin constructing proofs against this specification. This process defines the exact properties the protocol must hold. For example, what does it mean that “no one can exfiltrate funds maliciously”? Once you have the formalism, a logician can make such statements precise and prove true or false. This stage is much more predictable and takes much less time than formalization.
Coq ensuring correctness in the blockchain
Types of proofs
There are two forms of proofs used to verify smart contracts: classical proofs and computer-checked proofs. Classical proofs are more flexible than computer checked proofs, as not all proofs can be constructed on a computer. However, they may contain errors that a computerized theorem prover would catch. Peer review is sufficient to mitigate this risk, as classical proofs may be the only option to prove specific properties due to the limitations intrinsic to computers.
Computer-checked proofs are typically done in a theorem-proving language such as Agda, Coq, or Athena. Computer-checked proofs require an additional step: translating the mathematical specification into the theorem-proving language of choice, at Platonic.Systems we recommend using Coq. It offers excellent quality and ergonomics, as well as the ability to output raw Haskell code. That’s right! Since Coq can provide reliable code generation, you can output correct, proven code directly from Coq for use in your smart contracts!
There are great reasons to choose one proof type over the other or even use both to get the assurances you want. The choice is simply a matter of taste and requirement. There is nothing wrong with peer-reviewed classical proofs as the only means of formal verification. There is nothing wrong with relying on Coq. The choice is about the specific things you wish to prove and what you wish to do with these proofs. Luckily, proofs can be delivered faster by parallelizing multiple logicians’ work, unlike formalization, which a single person typically performs.
Achieving infallibility
With the combination of a formally verified protocol, well-tested and reviewed code, penetration testing, and blockchain implementer review, your smart contracts will be as close to infallible as possible. No higher degree of confidence can be achieved.
The beauty of this process is that you can expose it to your community for an independent check once you have your third-party verification. Nothing inspires confidence like performing your own peer review! And inviting scrutiny can only bring good things. Either your community finds no issues, which compounds confidence, or some brilliant member manages to break the verification—to which you can simply thank them and fix the problem.
Moving your smart contract project from keeping you up at night to strengthening your confidence is where Platonic.Systems shines. Contact us for a free consultation, and let us get you the peace of mind (and deep sleep) you deserve.