Architectural Schizophrenia Facebook Libra

Two years later, I returned to the blog for a post that differs from the usual boring lectures on Haskell and math. The last few years I have been engaged in financial technology in the EU, and it seems that the time has come to write on a topic that the technical media paid little attention to.



Facebook recently released what it calls the “new financial services platform” called Libra. It is positioned as a digital payment system based on a basket of international currencies that are managed on a “blockchain” and stored in a cash pool managed from Switzerland. The objectives of the project are ambitious and entail large-scale geopolitical consequences.



The Financial Times and New York Times have a lot of reasonable articles about unreasonable monetary and economic assumptions at the heart of the proposed financial system. But there are not enough specialists capable of analysis from a technical point of view. Not many people work on the financial infrastructure and publicly talk about their work, so this project is not too covered in the technical media, although its insides are open to the whole world. I mean open source in the Libra and Calibra Organization repositories.



What is open to the world is an architectural schizophrenic artifact with a claim to the role of a secure platform for the global payment infrastructure.



If you plunge into the code base, then the actual implementation of the system completely diverges from the stated goal, and in the most bizarre ways. I am sure that this project has an interesting corporate history. Therefore, it is logical to assume that it was developed with some zeal, but in reality I see a really strange set of architectural solutions that break the entire system and endanger users.



I will not claim an objective opinion about Facebook as a company. Few people in the IT industry look at her with sympathy. But a comparison of her statements and the published code clearly shows that the stated purpose is a fundamental hoax. In short, this project does not empower anyone. He will remain completely under the control of a company whose advertising business is so entangled in scandals and corruption that he has no choice but to try to diversify payments and credit scoring in order to survive. A clear long-term goal is to act as a data broker and intermediary in consumer access to credit based on their personal data on social networks. This is a completely terrifying and gloomy story, which does not pay the attention that it deserves.



The only saving grace of this story is that the artifact they created is so funny that it doesn’t fit the task that it can only be seen as an act of pride. There are several major architectural errors in this project:



Solving the Byzantine generals problem in a network with access control is an inconsistent design



The task of the Byzantine generals is a rather narrow field of research of distributed systems. It describes the ability of a network system to withstand arbitrary component failures when taking corrective actions critical to the functioning of the system. A resilient network must withstand several types of attacks, including restarts, failures, malicious loads, and malicious voting in leadership elections. This is the main solution for the Libra architecture, and it is completely pointless here.



The overhead of time complexity from this additional structure depends on the algorithm. There is a lot of literature on the varieties of the Paxos and Raft protocols with the solution of the Byzantine generals problem, but all of these structures introduce additional communication overhead charges over O(n2) to maintain a quorum. For Libra, we chose an algorithm with the highest possible cost of communication O(n2) in case of leadership failure. And there is additional overhead from potential re-election of leaders for several types of network failure events.



For a system operating in a consortium of highly regulated multinational corporations, where all users have a Facebook-signed code, and access to the network is controlled by Facebook, it simply does not make sense to consider malicious participants at a consensus level. It is unclear why, in general, this system solves the problem of Byzantine generals, and not just maintains a consistent audit trail to verify compliance. The possibility that the Libra host, managed by Mastercard or Andressen Horrowitz, suddenly starts to run malicious code, is a strange planning scenario and is better solved simply by ensuring the integrity of the protocol and non-technical (i.e. legal) means.



In testimony for Congress, the product is declared a competitor to new international payment protocols such as WeChat, Alipay and M-Pesa. However, none of these systems is designed to work on pools of validators to solve the problem of Byzantine generals. They are simply designed on a traditional high-throughput bus that makes wiring according to a fixed set of rules. This is a natural approach to the design of a payment system. A well-designed payment system simply does not meet the problem of double spending and forks.



The overhead of the consensus algorithm does not solve any problem and only limits the system throughput for no reason other than the cargo cult of the public blockchain, which is not intended for this use case.



Libra has no transaction privacy



According to the documentation, the system is designed taking into account pseudonymity , that is, the addresses used in the protocol are obtained from public keys on elliptic curves and do not contain metadata about accounts. However, nowhere in the description of the management structure for the organization or in the protocol itself does it indicate how the economic data participating in transactions will be hidden from validators. The system is intended for large-scale replication of transactions for a number of external parties, which, in accordance with existing European and American bank secrecy laws, should not be devoted to economic details.



The data policies of different countries are difficult to coordinate, especially given the disparate laws and regulations in different jurisdictions that have different cultural views on data protection and privacy. The protocol itself is by default completely open to consortium members, which is a clear technical flaw that does not meet the requirements for which it was developed.



Libra HotStuff BFT is not able to achieve the bandwidth required for the payment system



In the UK, clearing systems like BAC are capable of carrying out about 580 million transactions per month. At the same time, highly optimized systems like Visa can process 150,000,000 transactions per day. Performance depends on transaction size, network routing, system load and AML checks (anti-money laundering, money laundering schemes).



Libra is trying to solve problems that for domestic transfers are not really problems, as nation states have modernized their clearing infrastructure in the last decade. For retail consumers in the European Union, moving money is not a problem at all. On a traditional infrastructure, this can be done with a standard smartphone in seconds. For large corporate transfers, there are various mechanisms and rules related to the movement of large volumes of money.



There are no technical reasons why cross-border payments also cannot be made instantly, with the exception of differences in rules and requirements between the respective jurisdictions. If the necessary preventive measures (due diligence of the client, verification of sanctions, etc.) are carried out several times at different stages of the transaction chain, this may lead to a delay in the transaction. However, this delay is purely a function of regulatory law and its enforcement, not technology.



For consumers, there is no reason why a deal in the UK will not clear out in seconds. Retail transactions in the EU are really slowing down on KYC (Know Your Customer) checks and AML restrictions imposed by governments and regulators that are equally applicable to Libra payments. Even if Facebook overcomes the obstacles to international transfers and transfer of private data, the proposed model is hundreds of man-years from the throughput of global transactions and is likely to be processed from scratch.



Libra Move language is incorrect



The white paper makes bold statements about a new unverified language called Move. These statements are rather doubtful from the point of view of the theory of programming languages ​​(PLT).



Move is a new programming language for implementing custom transaction logic and “smart contracts” on the Libra blockchain. As Libra aims to one day serve billions of people, Move is designed with top priority on security.


A key feature of Move is the ability to define arbitrary resource types with semantics inspired by linear logic.


In public blockchains, smart contracts clash with the logic of public networks with escrow accounts, money laundering, the issue of over-the-counter tokens, and gambling. All this is done in a stunningly poorly designed language called Solidity, which from an academic point of view makes the author of PHP look like a genius. Oddly enough, the new language from Facebook does not seem to have anything to do with these technologies, since it is actually a scripting language designed for obscure corporate tasks.



In private distributed ledgers, smart contracts are one of those terms that consultants scatter without special attention to clear definitions or goals. Corporate software consultants usually make money on ambiguity, and smart contracts are the apotheosis of corporate obscurantism because they can be defined literally as anything.



After statements about its safety, we should look at the semantics of the language. The correctness in the theory of programming languages ​​usually consists of two different proofs: “progress” and “preservation”, which determine the consistency of the whole space of evaluation rules for a language. More specifically, in type theory, a function is “linear” if it uses its argument exactly once, and “affine” if it uses it no more than once. The linear type system provides a static guarantee that the declared linear function is truly linear, assigning types to all subexpressions of functions and tracking call locations. This is a subtle property for proof, and it is not easy to implement for the entire program. Linear typing is still a very academic area of ​​research, influencing the uniqueness of types in Clean and the ownership of types in Rust. There are some preliminary suggestions for adding linear types to the Glasgow Haskell Compiler.



The Move statement about the use of linear types seems unreasonable immersion in the compiler, since there is no such type checking logic . As far as one can judge, the technical document cites canonical literature from Girard and Pierce, and in the actual implementation there is nothing of the sort.



In addition, the formal semantics of a supposedly safe language are nowhere to be found either in the implementation or in the document. The language is small enough to find complete proof of the correctness of semantics in Coq or Isabelle. In reality, the end-to-end compiler of the complete conversion with the transfer of evidence to bytecode can be implemented using modern tools invented in the last decade. We know how to do this, starting with the work of George Nekula and Peter Lee back in 1996.



From the point of view of the theory of programming languages, it is impossible to verify the statement that Move is a reliable and safe language, since these statements come down purely to waving and marketing, and not to actual evidence. This is an alarming situation for a language development project that is being asked to entrust billions of dollars worth of transaction processing.



Libra cryptography is incorrect



Building reliable cryptosystems is a very complex engineering problem, and it is always better to treat dangerous code with a good dose of healthy paranoia. There are major breakthroughs in this area, like the Microsoft Everest project, which builds a verifiable secure TLS stack . Tools already exist for creating verifiable primitives. Although it is expensive, it clearly does not go beyond the economic possibilities of Facebook. However, the team decided not to participate in the project, declared as a reliable foundation for the global financial system.



The libra project relies on several fairly new libraries for creating experimental cryptosystems, which only appeared in the last few years. It is impossible to say whether the dependencies on the following tools are safe or not, since none of these libraries has been audited and does not have standard disclosure policies. In particular, for some major libraries there is no certainty regarding protection against attacks on third-party channels and time attacks.



  1. ed25519-dalek

  2. curve25519-dalek


The libra library becomes even more experimental and goes beyond the scope of the standard model using very new methods such as verifiable random functions (VRF), bilinear pairs and threshold signatures. These methods and libraries may be reasonable, but combining them all in one system raises serious concerns about the attack surface area. The combination of all these new tools and techniques greatly increases the complexity of the evidence of security.



It should be assumed that this entire cryptographic stack is vulnerable to various attacks until proven otherwise. The well-known Facebook model 'Move Fast and Break Things' cannot be applied to cryptographic tools that process clients' financial data.



Libra cannot implement consumer protection mechanisms



A distinctive feature of the payment system is the ability to roll back the transaction if the payment is canceled by a lawsuit or leads to an accidental or system failure. Libra is designed to be “fully completed" and does not include a transaction type for canceling a payment. In the UK, all payments from £ 100 to £ 30,000 are governed by the Consumer Credit Act. This means that the payment system shares responsibility with the seller in case of a problem with the purchased goods or if the payee did not provide the service. Similar rules apply in the EU, Asia and North America.



The current design of Libra does not include a protocol to comply with these laws and does not have a clear plan for its creation. Even worse, from an architectural point of view, the final structure of authenticated kernel data, based on the state of the Merkle drive, does not allow any mechanism for creating such a protocol without redesigning the kernel.






After conducting a technical examination of this project, we can conclude that it simply will not pass the test in any respected journal on the study of distributed systems or financial engineering. To try to change the global monetary policy, a huge amount of technical work needs to be done to create a reliable network and secure processing of user data, which the public and regulatory authorities could trust.



I see no reason to believe that Facebook in its project did the necessary work to overcome these technical problems or that it has some technical advantages over the existing infrastructure. The assertion that a company needs regulatory flexibility to learn about innovations is no excuse for not making them first.



All Articles