How serious? Hard to say. For bitcoin, seriosity is hard to judge anyway, but here it’s more about the combination, using formal methods for blockchain & co. When preparing the lecture, brushing up the introductory slides of Chapter 1, I stumbled upon this perhaps less obvious playground for formal methods.
Advocates of formal methods will concede that formal methods may not be used everywhere and may not be useful everywhere, but there are areas where they have or should have their place. Areas like safey-critical applications come to mind, avionics, space missions, embedded systems in critical infrastructure …
But there is also at least one crypto-currency, of all things, flying the flag for formal methods. But then again, ``bitcoin’’ is about money of sort (or at least money laundering…) and about financial systems, so it’s critical software. BTW: when saying ``bitcoin’’ here, I mean all kinds if crypo-currencies. Indeed, there is no dearth of those; see that list for a compilation of the more bizzare ones. There is also a virtual cementry or memorial where deceased coins rest in peace.
Cardano
Cardano is one of many crypto-coins. As obvious from the lists linked in above, there are genuinely bizzare coins out there. Cardano seems intended as a more respectable enterprise, and according to a current ranking of market capitalization of different ``coins’’, it’s actually ranked number 5.
Its official webpage, under the topic ``Why Cardano?’’, invokes formal specification and verification as argument for investing in it! Besides that, Cardano has also a wonderfully evangelical motto ``Making the world work better for all’‘.
The text about verification is an interesting read. It mentions challenges and limitations for formal verification in general and for Cardano or crypo-currencies in particular. The texts sees the use of formal methods resp. the extent to which one should use it as a ``judgement call’’ and ``compromise’’, a compromise to which extent (parts of) the software (and the software stack, and the hardware) should or can be tackled formally. In particular, due to the fact that distributed software and distributed problems (such as the underlying block-chain) are subtle and notoriously hard to get right, the text pitches the need for machine-checked proofs and verification. Not just pen-and-paper argumentation, as formal is that may be.
The text is a bit vague about what actually has been done for Cardano. Understandably so, it’s basically marketing material, but some technical hints are given. They mention concrete verification techniques, tool and languages like Isabelle/Hol on the one hand, and LiquidHaskell with SMT-solving on the other, all pretty up-to date stuff. There are many SMT-solvers around and used, including used in industry. SMT solving via the refinement types of LiquidHaskell is a natural choice, given that part of Cardano is implemented in Haskell.
The theorem prover is intended to machine-check proofs of designs and algorithms that were orginally done with pen-and-paper and human insight. Additionally, the document states that they intend ``on gradually adding Liquid Haskell to all production code in Cardano’s implementation throughout 2017 and 2018’’. It’s unclear what the current status is (the text was last updated 2020).
``Blockchain’’ as a concept or data structure has many aspects that makes it a challenging target for formal argumentation. It’s based on some very hard distributed problems like distributed consensus or byzantine agreement. Algorithms for such problems are pretty subtle and hard to understand. And given that some bitcoin apostles believe and hope that soon all financial transactions and everything else will and should be ``on the blockchain’’, it can’t hurt that someone makes the effort and studies some of its foundations in a rigourous manner.
The Cardano webpage does not refer to published material or source codes of the proofs they claim have been done. I guess the target audience of the webpage is not overly interested in studying mathematical proofs, anyway…
There are some published works tackling the Cardano consensus proof-of-stake protocol (called Ouroboros) and the ledger data structure. See for example here or here. Publically available is also Cardano ledger specification, including Isabelle code for ledger verification. The blog here is not intended as a systematic overview over formal verification efforts for bitcoin, blockchain & co, not even for Cardano alone, it’s just intended at pointing to formal verification in unexpected corners, so I leave it at that.
Formal method help making bitcoin&co more safe?
If we count bitcoin among the financial systems and ``money’’ as part of critical infrastructure in the general sense, then blockchain etc is a safety critical piece of software. Even more so, if everything else that can conceivably be block-chained ends up sooner or later on the blockchain. And there is no lack of things (material or otherwise) that have been been proposed to be blockchained.
Now, what role do formal methods play there, if any? Before I give my two cents in that, let have a look at some known incidents where bitcoin&co proved ``unsecure’’ in some way.
Some security breaches in connection with bitcoin, blockchain & co?
It is just a short list of a few more well-known incidences. Some of them with quite a colorful background story, like the mother of all crypto-heists, the Mt.Gox robbery from 2014 (at some point that exchange was hosting 60% (!) of the world-wide bitcoint trading). There had been numerous similar incidents, for instance, one even larger one, netting $500+ Mio and one with a size $60 Mio, both ``in’’ Tokio.
Another interesting one is the attack on the ``DAO’’. It exploited some ill-programmed smart contracts; see for instance the early analysis here, or see also here.
Interestingly, the vulnerability came from from issues with reentrancy (or recursion). Other problems and vulnerabilities include the good old race conditions (actually, reentrancy, in a way, is a form of race-condition, only without concurrency). One remedy for that particular vulnerability (proposed at the same analysis of the problem) is using mutexes (or locks) a standard concurrency control mechanism. It prevents, when used correctly, concurrent shared access, i.e., assuring mutual exclusion.
Probably those whose wallets were syphoned off found no humor in the irony that the weaknesses were exploited in a language called solidity executing smart contracts….. The vulnerability is astonishing insofar that races are known as one one the most pernicious programming errors. The effects of races in concrete software and hardware are exceedingly hard to study. Years and years of hard effort have not been able, for instance, to come up with a satisfactory (memory) memory model for instance for C++ or Java, i.e., a memory model that describes the behavior of programs including those with races. One thing that is commonly agreed is that in racy programs, bad things can happen. Like in the DAO-attack. It’s not just that it’s a potential danger of bad things. In this particular case, something like 60 million dollar actually vanished (if you believe that one can attach a price-tag in traditional currency and actual money to Ethereum).
As said, it’s known that races must be avoided (in really almost 100% of cases). If you ever were exposed to a beginner’s course of concurrent or parallel programming, that’s really the 101. And which example is used in many courses to illustrate and warm up for the bad effects of race conditions? It’s an example so simplistic and intuitive that even beginners to the topic can immediatel grasp, even non-specialists.
So, which example am I talking about? The good old bank transfer example! It’s of course not identical with what happened at the DAO, but the message and the essence is the same: manipulating a bank account (or data in general) ``simultaneously (in the DAO case via recursion) without protection or synchronization is a bad idea, so bad indeed, that one should learn about it in lession 1.
It’s sometimes difficult to say what, besides criminal energy, enabled this or that incident (and there are many more), and what counter-measures, including formal methods, could have prevented it.
It should be noted that the target of the thefts seem to have been mostly the exchanges, i.e., electronic trading platforms, not the coin implementations themselves. Disciples of crypto-currency could stress that the coin itself is (somehow) safe. Whether that argument, even if perhaps true to some extent, offers much consolation to the suckers that lost their fortune small or large on an exchange or on the DAO, one may doubt:
Sorry about your financial loss, but you should know: your coins are safe, that’s mathematically proven. It’s just the wallet and the platform which was compromised, the coins themselves are just safely in the hand of someone else now.
What about formal methods?
Coming back to the question from the beginning, what role do formal methods play here. As described, Cardano advocates formal verification and seems to use it (to which extent is a bit unclear). In that, I believe, Cardano is more or less unique, as far as crypto-currencies is concerned. So will the verification efforts done for Cardano make it (more) safe?
Sure, if some core parts (like the ledger data structure) has undergone a verification, even if only the concept and not the actual code, it makes it more robust.
But still it’s a very long way, seeing the big picture. The few attacks mentioned above targeted, as said, mostly surrounding infra-structure, like exchanges. Indeed, early exchanges were known (afterwards) for their piss-poor security.
``Are my crypto-coins secure?’’ asked by an individual has many aspects, and probably whether the underlying byzantine-agreement version has been formally verified or not is the least of one’s concerns. Of course, that’s not a counter-argument against verifying underlying algorithms and data structures. Having one’s fortune fall through the cracks of a faulty implementation of a Merkle-tree is not better than having them robbed at gunpoint (and that happened, too). Or what if the exchange provider shuts down the exchange (with or without running away with the coins). That’s actually very common, it’s called an ``exit scam’’. For all of those risks, formal verification cannot protect anyone
Indeed, there are very many aspects of security, also outside blockchains, some potentially addressable via formal methods, some sure not. That includes legal issues, like can I go to court to get lost money back? If you know where the court house is, sure, everyone can go to court. The question is does it help (probably not). Can I go to the police to get it back if someone steals it? Same answer. Maybe the legal system does not even accepts the crypto-currency as property that has been stolen. Many other things can affect the security of ``coins’’ negatively in the sense of that one looses money (if that’s the core security property of a crytpo-currency in a broad sense). That can includes future regulations (or even bans) of a crypto-currency, the fact that it simply dies or falls out of favor, because a even more interesting one takes over, or it looses quite a portion of its value when the Chinese government (or some other) withdraw its tolerance, or simply just by a random tweet by Elon Musk.
Anyway, formal verification techniques have been used for Cardano, the extent of which concretely is a bit foggy. But one thing is for sure, and that’s remarkable in itself and says something about formal methods.
Cardano developers do have used formal methods for marketing, as argument to pitch their crypto-currency to investors as being secure and safe!
What has it all to do with the lecture?
Technically not too much. It’s more to point out, as part of the motivation and introductory remarks, that one can stumble upon formal methods also outside areas which are the usual suspects like safety-critical systems.
A connecting point is that the lecture focuses on techniques for concurrent and distributed systems, and blockchain is one such system, resp. a concept for such system. The particular techniques mentioned above, like theorem proving and SMT solving will not be much discussed in the lecture. Technically, we will focus more on what is known as model checking, perhaps also run-time verification.