I don't have a formal protocol verification background, but I have a proposal related to specification that may aid in creating formal verification, and would be helpful in its own right.
Specifications are usually in the form of a document, but of Bitcoin it's often said that its only protocol (consensus) specification is the Bitcoin Core client software (although it's a de facto, not authoritative specification; the latter doesn't exist). But the difficulty in verifying its correctness, or for readers to understand it, is that it (appropriately) includes so much non-protocol complexity and optimization (both CPU and memory). Also, it's written in C++, which is very efficient, but is not easy to understand.
With that background, my proposal is to write a full consensus protocol specification in the form of working code in its simplest possible form. Human language is amgibuous, but code is precise; it answers all possible questions (unless it uses undefined behavior (UB) aspects of the programming language, or is asynchronous. Optimization is not the goal (it's even an anti-goal); understandability and obviousness are the only goals, as well as, of course, correctness -- faithfulness to the consensus protocol implemented by Bitcoin Core.
It would not be necessary to create consensus-valid blocks or transactions, only to check (verify) them.
It would need to be aware of the history of soft forks (activation height) and verify accordingly.
This code would also be helpful when proposing consensus upgrades; the author could describe the necessary changes using code more precisely than in text. The BIP could link to a version of this specification program modified to implement the needed consensus changes.
I propose writing this code in Python, since I believe most programmers agree that it's the easiest well-known language to understand. This is why, for example, the Bitcoin Core functional tests are written in Python; in test code, performance is secondary to ease of understanding; readers must be convinced that the test is testing what is intended to be tested. Another advantage of Python is that there's a lot of open-source Bitcoin-related code written in Python. Python has good debugger support. If a validation failure occurs, one could run the code using a debugger and see exactly why the failure is happening.
The result of this project is a standalone Python script, let's call it bc-protocol-check.py for now (there may be a better name). Internally, it would be structured as a main (executable) and a library, so it could be used in other by other libraries or programs. It would read standard input, expecting a series of blocks in raw hexidecimal form. It would deserialize and check each block (including all contained transactions) for validity. It would print a clear error message and halt if it encountered an invalid block.
It will be able to verify the existing mainnet blockchain. A small program (probably in Python) could make sequential (by block height) getblock RPCs to a local bitcoind node, and pipe the hex to bc-protocol-check.py. (This project would include that small program.) Or, one could pipe in blocks from any other source. (The program can detect when it's verifying the real mainnet chain, in which case it will apply the activation rules; otherwise, the current (latest) rules will be in effect.)
This project will include a set of invalid block sequences (test vectors) and the expected form of failure. These would demonstrate various kinds of consensus failures and would also help test the correctness of bc-protocol-check.py.
I want to get this tool committed to the Bitcoin Core repository, probably within the contrib/ directory (miscellaneous tools). Like the doc directory, this tool's functionality would, at every repository commit, match that commit's consensus protocol rules.
This would put an additional burden on developers who make consensus changes, but I think it will be considered worth the effort, especially since soft forks are becoming more rare with time. It may also help the developer understand the change more clearly.
The bc-protocol-check.py executable would be simpler than a real Bitcoin client in several ways:
- no P2P interface
- no mempool (no standalone transactions)
- no wallet
- no RPC or similar (ZMQ, REST,
bitcoin-cliequivalent) - no creation of consensus-dependent entities (transactions, blocks), only verification
Given the large amount of existing open-source Python bitcoin-related code, a few options are available:
- import a library that does something we need
- copy and paste the code from that library (with attribution)
- reimplement from scratch
These decisions will be made on a case-by-case basis. If the library provides exactly what we need and not much more, then it makes sense to import it. (An example might be the ECDSA algorithms.) If the library provides code segments that we need but is also bound up with features and functionality that we don't need, then the second option is a better choice. If the library does what we need but in a complex indirect way, then we'd probably go for the third option.
This tool will be able to track chain reorgs and determine the best tip at all times, since this is part of consensus. Probably the program should act similar to a pruned node (so re-orgs that are too deep would cause a failure), because storing the entire block history would require too much storage (currently, over 600 GB).
To validate all of mainnet, some form of backend (on-disk) storage will be needed for the UTXO set (currently 12GB) and recent block history (for re-orgs), despite being contrary to the goal of ASAP (as simple as possible). If bc-protocol-check.py keeps the these in memory, then when it quits, all state is lost, which would require re-doing a lot of work to get back to that state. Also, that would require a lot of memory, limiting where this program can be run. Some good database candidates are: shelve, dbm, plyvel, or PickleDB.
With this backend storage, one can pipe some blocks into bc-protocol-check.py (it exits on EOF), then pipe more blocks into another instance of the program, and that's equivalent to piping both sets of blocks into a single run of the program.
It would be helpful to report validation failures in a way that makes it clear to the user exactly where the problem is. For example, if the 6th input of a block's 3th transaction fails consensus, it would be good to get an error that points directly to that input. Python has some mechanisms to help with this (or, a simple error stack can be implemented directly).
- Build the most basic framework, a Python program that reads stdin line by line and stores it in the local backend database.
- Research existing Python bitcoin codebases, become familiar with what they provide. For the remaining steps, use existing library code where appropriate.
- Add parsing of block hex, make block hash the lookup key in the backend database, with the block data as the value (so we can look up blocks later by block ID)
- Add block checks (difficulty adjustment algorithm, block timestamp)
- Add transaction parsing.
- Add transaction validation (there would be sub-steps here for each of the transaction types).
- Add enhanced consensus failure reporting
- Adjust validation processing for soft-fork activations (based on block heights)
- Write a small program to get mainnet blocks from a local
bitcoindand pipe them tobc-protocol-check.py. - Successfully parse the mainnet blockchain
- Write a small tool to convert between block hex and JSON (this will help with the next step)
- Write test vectors (fake blocks that will trigger validation failures)
- Add re-org logic (determining best chain tip)
- Write mailing list or Delving post announcing the project (probably earlier, when there's enough for others to look at)
- Possibly create a presentation for (for example) the Brink developer meeting.
- Write a PR to get this tool reviewed and merged to the
contribpart of the Bitcoin Core repo.
As is often the case, it's hard to say! I'm available to work on this about 32 hours per week; at that rate, it would probably take me about 9 months. (I'm fairly good with Python, but would want to learn the best ways as I go along.) If it's not done by then and looks promising (making good progress and with many people thinking it's a good idea), I could ask for another grant (I'd be available after the initial period is over).
Is the scope of this proposal correct? It's aimed at specifying the onchain consensus rules, but protocol also refers to the P2P network. Is it possible to construct a code version of the P2P protocol specification, and would that be useful?
I think, inititally, an emphasis on the onchain protocol is appropriate, because if there are errors at this level, the result could be a chain split (as has happened in the past). If there's a P2P protocol bug, the most likely outcome would be a node gets kicked off the network. But one might imagine a bug affecting every node on the network at the same time (for example, due to receiving a malformed P2P message), and that would be nearly as disasterous. On the other hand, such a message wouldn't be relayed very widely. But an attacker could release it from many locations at the same time.