5 ms·

Bitcoin is at a point in valuation where a huge effort should be put into using formal verification: a bug can worth hundreds of billions of dollars. One proble

Bitcoin is at a point in valuation where a huge effort should be put into using formal verification: a bug can worth hundreds of billions of dollars. One problem is that it's already written in C++, which is a language with incredibly complex semantics for program verification (and now it's too hard to move away, so the C++ program has to be proven to be correct). The main blocker is what others have written as well: it's very hard to do the formal verification.

xvilka 8y ago
This is why currencies like Cardano were created.
- xiphias2 8y ago
  Cardano's proof of stake model has stronger assumptions than proof-of-work (if it wouldn't be the case, and the authors could prove it, they could work on improving Bitcoin itself...but I think they preferred to make money). New altcoins just don't solve the problem of increasing the security of Bitcoin. Schnorr signatures are are great example of not making the cryptographic assumptions stronger (actually making them weaker) while improving the scalability of the system.
DoctorOetker 8y ago
Almost 10 years ago on bitcoin dev IRC channel I was asking the devs to consider having the reference specification to be formally specified, so that all clients, are at least supposed / expected to comply with it. They were not interested...
- xiphias2 8y ago
  The problem is that there's no such thing as a formal specification when running C++ code, and I believe Coq runs too slow to be practical. We have Rust now as an alternative language, but it's too late to rewrite the consensus code, so we have to work with legacy code.
dranov 8y ago
I agree, and there are efforts to develop formally verified implementations of Nakamoto consensus (which I'm involved in). We've published a paper a year ago about our efforts and first results and I'm currently extending that work for my Master's thesis. Others are also building on top of that work [3]. We're nowhere near having a verified Bitcoin implementation (much less verifying the existing C++ implementation), but we're making steady progress. One could reasonably expect having a verified, deployable implementation in 3-4 years if people continue working on it. It remains to be seen whether people would switch to that from Core (very unlikely) or Core would adopt it as a component to replace its existing consensus code (interesting possibility, but also unlikely). [1] - https://github.com/certichain/toychain https://github.com/certichain/toychain [2] - http://pirlea.net/papers/toychain-cpp18.pdf http://pirlea.net/papers/toychain-cpp18.pdf [3] - https://popl19.sigplan.org/track/CoqPL-2019#program https://popl19.sigplan.org/track/CoqPL-2019#program
- iso-8859-1 8y ago
  First you mention Nakamoto consensus, then you mention "existing consensus code". Are you including Bitcoin script when you say consensus? It seems like a huge task to formally model the whole consensus system, including OP_CODESEPARATOR. How would you replicate something like the BIP-0050 problem? https://github.com/bitcoin/bips/blob/master/bip-0050.mediawiki https://github.com/bitcoin/bips/blob/master/bip-0050.mediawi...
  - dranov 8y ago
    > Are you including Bitcoin script when you say consensus? Currently, no. Our model considers "consensus" to be agreement on the ordering of transactions. We don't yet interpret the transactions. However, agreement on the state follows directly provided nodes have a function (in the "functional programming" sense), call it `Process`, that returns the current state given the ordered list of transactions. If all nodes have the same the function, they will have the same state. The BIP-0050 issue (in my understanding) is that different Bitcoin versions had different consensus rules, i.e. their `Process` functions were different. As far as I know, Bitcoin script is deterministic, so it should be possible to define it functionally. We haven't begun looking at this, though, and I don't know of anyone that has -- some people are working on verified implementations of the EVM, however. > It seems like a huge task to formally model the whole consensus system, including OP_CODESEPARATOR. It is a huge task, yes, but it can be done modularly such that reasoning about script interpretation can be almost entirely separated from reasoning about Nakamoto consensus. (This is a bit subtle, since the fork choice rule needs to check if blocks are valid, which relies on script interpretation.) I don't really understand OP_CODESEPARATOR. As long as it is deterministic, it shouldn't be an issue.

xvilka 8y ago

This is why currencies like Cardano were created.

xiphias2 8y ago
Cardano's proof of stake model has stronger assumptions than proof-of-work (if it wouldn't be the case, and the authors could prove it, they could work on improving Bitcoin itself...but I think they preferred to make money). New altcoins just don't solve the problem of increasing the security of Bitcoin. Schnorr signatures are are great example of not making the cryptographic assumptions stronger (actually making them weaker) while improving the scalability of the system.

DoctorOetker 8y ago

Almost 10 years ago on bitcoin dev IRC channel I was asking the devs to consider having the reference specification to be formally specified, so that all clients, are at least supposed / expected to comply with it. They were not interested...

xiphias2 8y ago
The problem is that there's no such thing as a formal specification when running C++ code, and I believe Coq runs too slow to be practical. We have Rust now as an alternative language, but it's too late to rewrite the consensus code, so we have to work with legacy code.

dranov 8y ago

I agree, and there are efforts to develop formally verified implementations of Nakamoto consensus (which I'm involved in). We've published a paper a year ago about our efforts and first results and I'm currently extending that work for my Master's thesis. Others are also building on top of that work [3]. We're nowhere near having a verified Bitcoin implementation (much less verifying the existing C++ implementation), but we're making steady progress. One could reasonably expect having a verified, deployable implementation in 3-4 years if people continue working on it. It remains to be seen whether people would switch to that from Core (very unlikely) or Core would adopt it as a component to replace its existing consensus code (interesting possibility, but also unlikely). [1] - https://github.com/certichain/toychain https://github.com/certichain/toychain [2] - http://pirlea.net/papers/toychain-cpp18.pdf http://pirlea.net/papers/toychain-cpp18.pdf [3] - https://popl19.sigplan.org/track/CoqPL-2019#program https://popl19.sigplan.org/track/CoqPL-2019#program

iso-8859-1 8y ago
First you mention Nakamoto consensus, then you mention "existing consensus code". Are you including Bitcoin script when you say consensus? It seems like a huge task to formally model the whole consensus system, including OP_CODESEPARATOR. How would you replicate something like the BIP-0050 problem? https://github.com/bitcoin/bips/blob/master/bip-0050.mediawiki https://github.com/bitcoin/bips/blob/master/bip-0050.mediawi...
- dranov 8y ago
  > Are you including Bitcoin script when you say consensus? Currently, no. Our model considers "consensus" to be agreement on the ordering of transactions. We don't yet interpret the transactions. However, agreement on the state follows directly provided nodes have a function (in the "functional programming" sense), call it `Process`, that returns the current state given the ordered list of transactions. If all nodes have the same the function, they will have the same state. The BIP-0050 issue (in my understanding) is that different Bitcoin versions had different consensus rules, i.e. their `Process` functions were different. As far as I know, Bitcoin script is deterministic, so it should be possible to define it functionally. We haven't begun looking at this, though, and I don't know of anyone that has -- some people are working on verified implementations of the EVM, however. > It seems like a huge task to formally model the whole consensus system, including OP_CODESEPARATOR. It is a huge task, yes, but it can be done modularly such that reasoning about script interpretation can be almost entirely separated from reasoning about Nakamoto consensus. (This is a bit subtle, since the fork choice rule needs to check if blocks are valid, which relies on script interpretation.) I don't really understand OP_CODESEPARATOR. As long as it is deterministic, it shouldn't be an issue.