Factual inaccuracies of “Facebook Libra is Architecturally Unsound”

A post by Stephen Diehl about Facebook Libra is making the rounds this morning. It makes a number of claims about flaws in the software. Many of these claims are factually inaccurate. I consider it to be a gish gallop that bombards you with a bunch of negative claims, many of which are false or at best, specious.

For context, I am a contributor to OpenLibra, a group independent of Facebook (or should I say “FACEBOOK”) who are experimenting with operating the Libra software. My company also operates other BFT-based cryptocurrencies, such as the Cosmos Network which is based on Tendermint BFT. Prior to that I worked extensively in credit card processing at companies like Square and LivingSocial, also doing card processing integrations at several companies before that.

This post, like the original, is intended to be purely technical, and if it were to talk about my opinions of a hypothetical production Libra network, they wouldn’t be positive: the day Libra came out and I was first able to review the papers and code, my tl;dr was “some interesting looking tech with terrifying social implications”.

That said, allow me to review some of the technical claims:

Libra’s byzantine tolerance on a permissioned network is an incoherent design. #

The claim is that Libra is a centralized, “permissioned” network, and therefore doesn’t need BFT.

This claim would be a good one, but ignores some properties of the Libra software: it supports running in either a permissioned or permissionless mode as one of the settings in the configuration. I suspect Facebook’s longer term plans, were they to actually launch Libra, are to move to a permissionless proof-of-stake model much like the one used by Cosmos (which managed to launch in a fully permissionless mode).

Libra HotStuff BFT is not capable of achieving the throughput necessary for a payment rail #

This section throws a few numbers out: it claims the UK Bacs system does 580,000,000 transactions a month, or about 223 transactions per second.

Curiously it claims Libra can’t do this, but posts no numbers about Libra’s throughtput. Libra’s throughput target is 1,000 transactions/sec (see Section 8: Performance in the Libra paper) with 10 second latencies on consensus time. I don’t think that number is unrealistic, and some of the testnets we are running for other BFT protocols are operating at those performance levels or above.

As another data point: the Open Libra testnet has been running for about a day and has made nearly 100,000 blocks (i.e. approximately 1/6th the number in the 10+ year history of the Bitcoin blockchain), operated by volunteers on the open Internet. Though I didn’t take the time to do so for this post, I would love to measure the transaction throughput we’re able to achieve on this testnet.

Libra’s Move language is unsound #

The core argument of this section is the Move language claims to use linear types, but the Move IR compiler contains no prover to assert the soundness, ala something like the Rust borrow checker.

This is true, but also highly misleading: the Move IR compiler does not perform these checks, and can emit bytecode which is unsound, however that code is immediately checked by a bytecode verifier which asserts these properties, including reference safety. To me this provides better guarantees than doing these checks in the Move IR compiler alone: it ensures all bytecode is checked, regardless of what compiler emitted it.

Is it actually sound? I don’t know, it’s brand new and looks unfinished to me, and even if it were finished I’m unqualified to make that assertion, but it’s certainly quite a bit more existing machinery than the original blog post would lead you to believe.

Beyond that, they have experimental support for translating their bytecode to Boogie IVL in order to facilitate formal verification.

Libra’s cryptography engineering is unsound #

And… here we get to the part of the post which really takes the cake. Stephen Diehl doesn’t understand cryptography, but sure has a lot to say about it.

It is impossible to say whether the dependencies on the following tools are secure or not as none of these libraries have had security audits nor do they have standard practice disclosure policies. Several core libraries in particular are indeterminate about their vulnerabilities to side channel and timing attacks.

  1. ed25519-dalek
  2. curve25519-dalek

My goodness, where to begin. I guess the part where the claims that these libraries have never had a security audit are completely incorrect: these libraries have been audited by both Quarkslab and NCC group, with only minor findings (the Quarkslab audit is public, the NCC audit is not but was paid for by a former employer of mine and had only minor findings).

Shortly before that, the post extolls the virtues of formally verified cryptography:

The tools to build verifiable primitives exist today and while expensive to do, are certainly not outside the economic capacity of Facebook to build. Yet the team has chosen not to on a project stated to be reliable for global finance.

False. The Calibra fork of curve25519-dalek is integrating formally verified implementations from the fiat-crypto project.

That said, formally verified cryptography is limited in application and scope: it can’t prove code is free of sidechannels, for instance, because those are a property of the combined software-hardware physical system, not a property of the formal model.

This harkens back to the famous Don Knuth quote: “Beware of bugs in the above code; I have only proved it correct, not tried it.” While I’m a fan of formal verification and will soon be attending a seminar on formally verifying cryptographic code, it has a number of limitations. Personally I’ll be sticking with upstream curve25519-dalek, despite the lack of formal verification (in absence of that the field arithmetic contains prose proofs of correctness in the comments).

The library gets even more experimental and ventures quite outside the Cryptography Standard Model

This sounds like Facebook has ventured straight into the realm of YOLO cryptography! But really it’s a meaningless claim: the standard model is not a particularly useful one, and much of the cryptography we rely on every day uses constructions proven in different but still rather boring models such as the random oracle model. Protocols like TLS rely on several constructions which are proven in the random oracle model: without it we wouldn’t have things like digital signatures, message authentication codes, or transcript hashing needed to build a secure authenticated key exchange.

I guess this is where I should point this out (and also that I get a hostname verification error accessing the site over HTTPS):

Screen Shot 2019-11-05 at 9.59.14 AM.png

Anywho… back to the post. For some context on that “Cryptography Standard Model” stuff:

The library gets even more experimental and ventures quite outside the Cryptography Standard Model by folding in very novel techniques like verifiable random functions, bilinear pairings and threshold signatures.

Verifiable Random Functions (VRFs) are effectively a type of non-malleable signature which are secure in the random oracle model. While they are poorly known, I find them to be simultaneously a very powerful and very boring construction. If anything, they provide better security properties than typical digital signatures across the board, such as the afforementioned non-malleability and message preimage resistance from an attacker who holds both a public key and a VRF output.

Regarding bilinear pairings and threshold signatures: Libra doesn’t use these for either consensus or transaction signing, and instead uses Ed25519 for this purpose. This is about the most boring way you can build a BFT blockchain like Libra today, and is the same approach used by Tendermint. Ed25519 is quite boring: it was selected by the IRTF CFRG as the next-generation signature algorithm for TLS, and NIST’s latest draft of FIPS 186-5 now includes Ed25519 as a soon-to-be recommended algorithm.

Ironically, one of the things the things the post complained with earlier was the lack of transaction privacy. This is something I agree with and care about, however the reference to bilinear pairings is ostensibly in regard to the BLS12-381 elliptic curve. There are a few different ways they could potentially use this, such as for BLS threshold signatures, but the main way the BLS12-381 curve is leveraged today is as part of the Zcash Protocol for private/shielded transactions expressed as zero-knowledge proofs. I sure would love to see Libra integrate something like that.

The section concludes:

These techniques and libraries might be sound, but the amalgamation of all of them into one system should raise some serious concerns about attack surface area. The combination of all of these new tools and techniques makes the burden of proof much higher.

The core Libra protocol is computing additions to a Merkle tree constructed using SHA-3 with Ed25519 signatures from validators. To me that is an extremely boring construction and works the same way as several other production proof-of-stake blockchains such as Cosmos.

Yes, there’s some wild “next gen crypto” in their cryptography library, but it’s not being used by the core protocol (or practically anything in their codebase) yet, and its purpose may very well be to experiment with solving issues like transaction privacy.

That brings us to our last section…

Libra has no capacity for consumer protection mechanisms #

This section is talking about payment reversal mechanisms like chargebacks. Right now Libra is missing many features of other proof-of-stake blockchains like governance, however these mechanisms can be used to implement things like payment reversals.

We can imagine a model where a Libra partner brokered some transactions they want to reverse, and have determined they were fraudulent as part of an existing disputes process. They can put this reversal to a governance vote, and if it passes reverse the desired transactions.

While it’s true Libra doesn’t have these features, it’s being worked on, and it certainly has “the capacity” for them.

Conclusion #

Stephen Diehl’s ends with “the final conclusion one must take away after doing technical due diligence on this project is this simply that it would not pass muster in any respected journal on distributed systems research or financial engineering.”

Well, that’s more or less how I feel about his blog post. His post is filled with a number of accusations and claims which are completely wrong.

There are a lot of reasons not to like Libra, and in particular there are reasons to worry about the social impact of a Libra network operated by Facebook.

But from a technical perspective, I find Libra to be one of the best enterprise grade BFT-based blockchain systems in development today.

 
1,955
Kudos
 
1,955
Kudos

Now read this

Introducing Miscreant: a multi-language misuse resistant encryption library

For the past several months I have been hacking on not just one, but five encryption libraries in five different languages (Go, Python, Ruby, Rust, and TypeScript). Tall order, I know. And worse, these libraries implement what I believe... Continue →