After two years, I returned to the blog for a post that differs from the usual boring lectures about Haskell and mathematics. I've been working on fintech in the EU for the past few years and it seems like the time has come to write about a topic that has received little attention from the tech media.
Facebook recently released what it calls a “new financial services platform” called Libra. It is positioned as a digital settlement system based on a basket of international currencies that are managed on a “blockchain” and stored in a money pool managed from Switzerland. The goals of the project are ambitious and entail large-scale geopolitical consequences.
В и Lots of sensible articles about the unsound monetary and economic assumptions behind the proposed financial system. But there are not enough specialists capable of analysis from a technical point of view. Not many people work on financial infrastructure and talk publicly about their work, so this project doesn't get much coverage in the tech media, although its innards are open to the world. I mean open source in repositories и .
What is open to the world is an architecturally schizophrenic artifact with claims to be a secure platform for the global payment infrastructure.
If you dive into the code base, 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. So it's logical to assume that it was designed with some diligence, but in reality I see a really strange set of architectural decisions that break the entire system and put users at risk.
I will not pretend to have an objective opinion about Facebook as a company. Few people in the IT industry look at her with sympathy. But a comparison of its statements and the published code clearly shows that the stated purpose is fundamentally deceptive. In short, this project does not empower anyone. He will remain entirely under the control of a company whose advertising business is so mired in scandal and corruption that it has no choice but to try to diversify its payments and credit scoring to survive. The clear long-term goal is to act as a data broker and intermediary in consumers' access to credit based on their personal social media data. This is an absolutely horrific and dark story that doesn't get the attention it deserves.
The only saving grace of this story is that the artifact they created is so hilariously unsuited to the task at hand that it can only be seen as an act of hubris. There are several major architectural errors in this project:
Solving the Byzantine Generals Problem in an Access Control Network is an Inconsistent Design
The problem of the Byzantine generals is a rather narrow area of research of distributed systems. It describes the ability of a network system to withstand random component failures while taking corrective actions critical to the operation of the system. A resilient network must withstand several types of attacks, including restarts, outages, malicious loads, and malicious voting in leadership elections. This is the main decision for the Libra architecture, and it is completely meaningless here.
The time complexity overhead of this additional structure depends on the algorithm. There is a lot of literature on variants of the Paxos and Raft protocols solving the Byzantine generals problem, but all these structures introduce additional overhead for communication over 
to maintain quorum. For Libra, they chose an algorithm with the highest possible communication cost in case of failure of leadership. And there is additional overhead from potential re-election of leaders across multiple types of network failure events.
For a system operating within a consortium of highly regulated multinational corporations, where all users have code signed by Facebook and access to the network is controlled by Facebook, it simply does not make sense to consider malicious participants at the consensus level. It is not clear why this system would even solve the problem of Byzantine generals, rather than simply maintaining a consistent audit trail to check compliance. The possibility of a Libra node run by Mastercard or Andressen Horrowitz suddenly starting running malicious code is an odd scenario to plan for and is better addressed by simply ensuring protocol integrity and non-technical (i.e. legal) means.
Testimony to Congress billed the product as a competitor to new international payment protocols such as WeChat, Alipay and M-Pesa. However, none of these systems are designed to run on validator pools to solve the Byzantine generals problem. They are simply designed on a traditional high-bandwidth bus that makes wiring according to a fixed set of rules. This is a natural approach to designing a payment system. Well designed the payment system simply will not encounter the problem of double spending and forks.
The overhead of the consensus algorithm does not solve any problem and only limits the throughput of the system 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 governance structure for the organization or in the protocol itself does it indicate how the economic data involved in transactions will be hidden from validators. The system is designed to replicate transactions on a large scale to a range of external parties who, under existing European and US bank secrecy laws, should not be privy to the economic details.
Data policies across countries are difficult to coordinate, especially given disparate laws and regulations in different jurisdictions with different cultural views on data protection and privacy. The protocol itself is by default completely open to consortium members, which is a clear technical shortcoming that does not meet the requirements for which it is designed.
Libra HotStuff BFT is unable to achieve the throughput required for a payment system
In the UK, clearing systems like BAC are capable of handling around 580 transactions per month. At the same time, highly optimized systems like Visa can process 000 transactions per day. Performance varies depending on transaction size, network routing, system load, and (anti-money laundering, money laundering schemes).
Libra is trying to solve problems that are not really problems for domestic transfers, as nation states have modernized their clearing infrastructure over the past decade. For retail consumers in the European Union, moving money is not a problem at all. On traditional infrastructure, this can be done with a standard smartphone in seconds. For large corporate transfers, there are various mechanisms and rules associated with moving large amounts of money.
There is no technical reason why cross-border payments cannot also be processed instantly, other than differences in rules and requirements between the relevant jurisdictions. If the necessary preventive measures (customer due diligence, sanctions checks, etc.) are performed multiple times at different stages of the transaction chain, this may result in a delay in the transaction. However, this delay is purely a function of regulatory legislation and compliance, not technology.
For consumers, there is no reason why a UK transaction would not clear in a matter of seconds. Retail transactions in the EU are indeed slowing by (Know Your Customer) and AML restrictions imposed by governments and regulators, which apply equally to Libra payments. Even if Facebook were to overcome the obstacles to cross-border transfers and private data transfers, the proposed model is hundreds of person-years away from global transaction throughput and would likely need to be redesigned from scratch.
Libra Move language is incorrect
The white paper makes bold claims about a new, untested language called Move. These statements are quite dubious from the point of view of programming language theory (PLT).
Move is a new programming language for implementing custom transaction logic and smart contracts on the Libra blockchain. Because Libra aims to one day serve billions of people, Move is designed with security as a top priority.
A key feature of Move is the ability to define arbitrary resource types with semantics inspired by linear logic.
In public blockchains, smart contracts face the logic of public networks with escrow accounts, money laundering, OTC token issuance, 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 seems to have nothing to do with these technologies, since it is actually a scripting language intended for obscure enterprise purposes.
In private distributed ledgers, smart contracts are one of those terms thrown around by consultants without much regard for clear definition or purpose. Enterprise software consultants typically make money from ambiguity, and smart contracts are the apotheosis of corporate obscurantism because they can be defined as literally anything.
After making claims about its security, we need to look at the semantics of the language. Correctness in programming language theory typically consists of two different proofs: “progress” and “preservation”, which determine the consistency of the entire space of evaluation rules for the language. More specifically, in type theory, a function is "linear" if it uses its argument exactly once, and "affine" if it uses it at most once. The linear type system provides static guarantee that a declared linear function is truly linear by assigning types to all function subexpressions and keeping track of where calls are made. This is a subtle property to prove and is not easy to implement for an entire program. Linear typing is still a very academic field of study, influenced by the implementation of type uniqueness in Clean and type ownership in Rust. There are some preliminary proposals for adding linear types to the Glasgow Haskell Compiler.
Move's statement about using linear types seems like an unwarranted dive into the compiler, since there . As far as one can tell, the whitepaper cites canonical literature from Girard and Peirce, and there is nothing similar in the actual implementation.
Additionally, the formal semantics of the supposedly secure language appear nowhere in the implementation or document. The language is small enough to find a complete proof of correct semantics in Coq or Isabelle. In reality, an end-to-end full conversion compiler with proof transfer to bytecode is quite possible to implement with modern tools invented in the last decade. We know how to do it, starting with back in 1996.
From a programming language theory perspective, it is impossible to test the claim that Move is a reliable and secure language, since these claims amount to pure hand-waving and marketing rather than actual evidence. This is an alarming situation for a language project that is being asked to process billions of dollars of transactions.
Libra cryptography is flawed
Building secure cryptosystems is a very difficult engineering problem, and it's always best to approach working with dangerous code with a good dose of healthy paranoia. There are major breakthroughs in this area, like the Microsoft Everest project, which is building a verifiable secure . Tools already exist to create verifiable primitives. Although this is expensive, it is clearly not beyond Facebook's economic capabilities. However, the team decided not to participate in the project, which was announced as a reliable foundation for the global financial system.
libra project from several fairly new libraries for creating experimental cryptosystems that have 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 have been audited and do not have standard disclosure policies. In particular, for some core libraries there is no certainty regarding protection against side-channel attacks and timing attacks.
The libra library becomes even more experimental and goes beyond , applying very new techniques such as verifiable random functions (VRFs), bilinear pairs, and threshold signatures. These methods and libraries may be reasonable, but combining them all into one system raises serious concerns about attack surface area. The combination of all these new tools and techniques greatly increases the complexity of proving security.
It should be assumed that this entire cryptographic stack is vulnerable to various attacks until proven otherwise. Facebook's famous 'Move Fast and Break Things' model cannot be applied to cryptographic tools that process customer financial data.
Libra fails to implement consumer protection mechanisms
A distinctive feature of the payment system is the ability to roll back a transaction if the payment is canceled by a lawsuit or leads to an accidental or system failure. The Libra system is designed to be "complete" and does not include a transaction type for payment cancellation. In the UK, all payments between £100 and £30,000 are subject to the Consumer Credit Act. This means that the payment system shares responsibility with the seller in the event of a problem with the purchased product or if the recipient of the payment does 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 creating one. Even worse, from an architectural perspective, the finality of the kernel's authenticated data structure, based on the state of the Merkle drive, does not allow for any mechanism to create such a protocol without redesigning the kernel.
After conducting a technical review of this project, we can conclude that it simply will not pass muster in any respected distributed systems research or financial engineering journal. To try to change global monetary policy, a huge amount of technical work needs to be done to create a reliable network and secure processing of user data that the public and regulators can trust.
I see no reason to believe that Facebook has done the necessary work in its design to overcome these technical problems or that it has any technical advantages over the current infrastructure. Saying that a company needs regulatory flexibility to explore innovations is not an excuse for not doing them first.
Source: habr.com