兩年後，我回到部落格上發表了一篇與通常有關 Haskell 和數學的無聊講座不同的文章。過去幾年我一直在歐盟研究金融科技，現在似乎是時候寫一個很少被科技媒體關注的話題了。
Facebook 最近發布了一個名為 Libra 的「新金融服務平台」。它被定位為基於一籃子國際貨幣的數位結算系統，這些貨幣在「區塊鏈」上管理並儲存在瑞士管理的資金池中。該計畫的目標雄心勃勃，並會產生大規模的地緣政治後果。
В и 有很多關於擬議金融體系背後不健全的貨幣和經濟假設的明智文章。但能夠從技術角度進行分析的專家還不夠多。沒有多少人致力於金融基礎設施並公開談論他們的工作，因此該項目在科技媒體上沒有得到太多報道，儘管它的內部結構向世界開放。我的意思是儲存庫中的開源 и .
向世界開放的是一個建築上精神分裂的工件，聲稱是全球支付基礎設施的安全平台。
如果您深入研究程式碼庫，系統的實際實現會完全偏離既定目標，並以最奇怪的方式偏離。我確信這個專案有一段有趣的公司歷史。因此，可以合理地假設它是經過一番精心設計的，但實際上我看到了一組非常奇怪的架構決策，它們破壞了整個系統並使用戶面臨風險。
我不會假裝對 Facebook 這家公司有客觀的看法。 IT界很少有人用同情的眼光看她。但將其聲明與已發布的程式碼進行比較，清楚地表明其所聲明的目的從根本上是具有欺騙性的。簡而言之，這個計畫不會賦予任何人權力。他仍將完全處於一家公司的控制之下，該公司的廣告業務深陷醜聞和腐敗，以至於該公司別無選擇，只能嘗試使其支付和信用評分多樣化以求生存。明確的長期目標是充當消費者基於個人社交媒體數據獲得信貸的數據經紀人和中介。這是一個絕對恐怖和黑暗的故事，沒有得到應有的關注。
這個故事唯一的優點是，他們創造的神器非常不適合手邊的任務，只能被視為傲慢的行為。該專案存在幾個主要的架構錯誤：
解決存取控制網路中的拜占庭將軍問題是一種不一致的設計
拜占庭將軍的問題是分散式系統研究的一個相當狹窄的領域。它描述了網路系統承受隨機組件故障同時採取對系統運作至關重要的糾正措施的能力。一個有彈性的網路必須能夠抵禦多種類型的攻擊，包括重啟、中斷、惡意負載和領導選舉中的惡意投票。這是Libra架構的主要決定，完全沒有意義。
這個額外結構的時間複雜度開銷取決於演算法。有許多關於解決拜占庭將軍問題的 Paxos 和 Raft 協議變體的文獻，但所有這些結構都會帶來額外的通訊開銷 
以維持法定人數。對於Libra，他們選擇了一種通訊成本盡可能最高的演算法 如果領導失敗。跨多種類型的網路故障事件可能會重新選舉領導者，從而產生額外的開銷。
對於在高度監管的跨國公司聯盟內運行的系統來說，所有用戶都有 Facebook 簽署的程式碼，對網路的存取也由 Facebook 控制，因此在共識層面考慮惡意參與者根本沒有意義。目前還不清楚為什麼這個系統甚至可以解決拜占庭將軍的問題，而不是簡單地維護一致的審計追蹤來檢查合規性。萬事達卡或 Andressen Horrowitz 運行的 Libra 節點突然開始運行惡意程式碼的可能性是一個奇怪的規劃場景，只需確保協議完整性和非技術（即法律）手段即可更好地解決這種情況。
國會證詞將該產品稱為微信、支付寶和 M-Pesa 等新國際支付協議的競爭對手。然而，這些系統都不是為了在驗證者池上運作來解決拜占庭將軍問題而設計的。它們只是在傳統的高頻寬總線上設計的，該總線根據一組固定的規則進行佈線。這是設計支付系統的自然方法。 設計精良 支付系統根本不會遇到雙花和分叉的問題。
共識演算法的開銷並不能解決任何問題，只是限制了系統的吞吐量，除了公共區塊鏈的貨物崇拜之外，沒有任何原因，這不適用於此用例。
Libra沒有交易隱私
根據文檔，該系統的設計考慮到 假名，即協議中使用的地址是從橢圓曲線上的公鑰獲得的，不包含有關帳戶的元資料。然而，在組織治理結構的描述或協議本身中，沒有任何地方表明交易中涉及的經濟數據將如何隱藏驗證者。該系統旨在將交易大規模複製給一系列外部各方，根據現有的歐洲和美國銀行保密法，這些外部各方不應了解經濟細節。
各國的資料政策很難協調，特別是考慮到不同司法管轄區的法律法規不同，對資料保護和隱私的文化觀點也不同。該協議本身默認對聯盟成員完全開放，這是一個明顯的技術缺陷，不符合其設計要求。
Libra HotStuff BFT 無法達到支付系統所需的吞吐量
在英國，BAC 等清算系統每月能夠處理約 580 億筆交易。同時，Visa 等高度優化的系統每天可以處理 000 筆交易。效能因交易大小、網路路由、系統負載和 （反洗錢、洗錢計畫）。
隨著民族國家在過去十年中對其清算基礎設施進行了現代化改造，Libra 正試圖解決對國內轉帳來說並不是真正問題的問題。對歐盟的零售消費者來說，轉移資金根本不是問題。在傳統基礎設施上，這可以透過標準智慧型手機在幾秒鐘內完成。對於大型企業轉賬，有與轉移大量資金相關的各種機制和規則。
除了相關司法管轄區之間的規則和要求存在差異之外，沒有任何技術原因導致跨境支付無法即時處理。如果在交易鏈的不同階段執行多次必要的預防措施（客戶盡職調查、制裁檢查等），則可能會導致交易延遲。然而，這種延遲純粹是監管立法和合規性的結果，而不是技術的結果。
對於消費者來說，英國的交易沒有理由不會在幾秒鐘內清算。歐盟的零售交易確實正在放緩 政府和監管機構施加的（了解你的客戶）和反洗錢限制，同樣適用於 Libra 支付。即使 Facebook 要克服跨境傳輸和私人資料傳輸的障礙，所提出的模型距離全球交易吞吐量還有數百人年的距離，並且可能需要從頭開始重新設計。
Libra Move 語言不正確
該白皮書大膽宣稱一種名為「Move」的新的、未經測試的語言。從程式語言理論（PLT）的角度來看，這些陳述是相當可疑的。
Move 是一種新的程式語言，用於在 Libra 區塊鏈上實現自訂交易邏輯和智能合約。由於 Libra 的目標是有一天為數十億人服務，因此 Move 的設計將安全性作為首要任務。
Move 的一個關鍵功能是能夠使用受線性邏輯啟發的語意來定義任意資源類型。
在公共區塊鏈中，智慧合約面臨公共網路的邏輯，存在託管帳戶、洗錢、OTC 代幣發行和賭博等問題。所有這一切都是透過一種名為 Solidity 的設計極其糟糕的語言完成的，從學術的角度來看，這使得 PHP 的作者看起來像個天才。奇怪的是，Facebook 的新語言似乎與這些技術無關，因為它實際上是一種腳本語言，旨在用於模糊的企業目的。
在私人分散式帳本中，智慧合約是顧問拋出的術語之一，而不太考慮明確的定義或目的。企業軟體顧問通常透過模糊性賺錢，而智能合約是企業蒙昧主義的典範，因為它們實際上可以被定義為任何東西。
在聲明其安全性之後，我們必須看看該語言的語義。程式語言理論中的正確性通常由兩個不同的證明組成：“進步”和“保存”，它們決定了語言評估規則的整個空間的一致性。更具體地說，在類型論中，如果函數恰好使用其參數一次，則該函數是「線性」的；如果最多使用一次，則該函數是「仿射」的。線性類型系統透過為所有函數子表達式分配類型並追蹤呼叫位置，提供靜態保證，確保聲明的線性函數是真正線性的。這是一個需要證明的微妙屬性，並且對於整個程式來說並不容易實現。線性類型仍然是一個非常學術的研究領域，受到 Clean 中類型唯一性實現和 Rust 中類型所有權的影響。有一些關於向 Glasgow Haskell 編譯器添加線性類型的初步建議。
Move 關於使用線性類型的聲明似乎是對編譯器的無根據的深入研究，因為 。據了解，白皮書引用了Girard和Peirce的經典文獻，而實際實施中並沒有類似的內容。
此外，所謂的安全語言的形式語義在實作或文件中都沒有出現。語言足夠小，可以在 Coq 或 Isabelle 中找到正確語義的完整證明。實際上，使用過去十年發明的現代工具很有可能實現將證明轉移到字節碼的端到端完整轉換編譯器。我們知道該怎麼做，首先 時間回到1996年。
從程式語言理論的角度來看，不可能檢驗 Move 是一種可靠且安全的語言的說法，因為這些說法純粹是擺手和行銷，而不是實際證據。對於一個需要處理數十億美元交易的語言項目來說，這是一個令人震驚的情況。
Libra 密碼學有缺陷
建立安全的密碼系統是一個非常困難的工程問題，最好以健康的偏執態度來處理危險代碼。這個領域有重大突破，例如微軟珠穆朗瑪峰項目，它正在建立一個可驗證的安全平台 。已經存在創建可驗證原語的工具。雖然這很昂貴，但顯然並沒有超越 Facebook 的經濟能力。然而，該團隊決定不參與該項目，該項目被宣佈為全球金融體系的可靠基礎。
天秤座項目 來自幾個相當新的庫，用於創建最近幾年才出現的實驗性密碼系統。不可能說對以下工具的依賴是否安全，因為這些庫都沒有經過審計，也沒有標準的揭露政策。特別是，對於一些核心庫來說，對於側通道攻擊和定時攻擊的防護並不確定。
Libra 庫變得更具實驗性並且超越 ，應用非常新技術，例如可驗證隨機函數（VRF）、雙線性對和閾值簽名。這些方法和庫可能是合理的，但將它們全部組合到一個系統中會引起對攻擊面區域的嚴重擔憂。所有這些新工具和技術的結合大大增加了證明安全性的複雜性。
應該假設整個加密堆疊容易受到各種攻擊，除非另有證明。 Facebook 著名的「快速行動，打破常規」模型無法應用於處理客戶財務資料的加密工具。
Libra 未能落實消費者保護機制
此支付系統的一個顯著特徵是，如果支付因訴訟而取消或導致意外或系統故障，則能夠回滾交易。 Libra 系統被設計得“完整”，不包含支付取消的交易類型。在英國，所有 100 英鎊至 30,000 英鎊之間的付款均須遵守《消費者信貸法》。這意味著，如果所購買的產品出現問題或付款接收者不提供服務，支付系統將與賣家共同承擔責任。類似的規則也適用於歐盟、亞洲和北美。
Libra 目前的設計不包括遵守這些法律的協議，也沒有創建協議的明確計劃。更糟糕的是，從架構角度來看，基於 Merkle 驅動器狀態的核心已驗證資料結構的最終性不允許任何機制在不重新設計核心的情況下創建此類協定。
在對該專案進行技術審查後，我們可以得出結論，它根本無法通過任何受人尊敬的分散式系統研究或金融工程期刊的審查。為了嘗試改變全球貨幣政策，需要做大量的技術工作來創建公眾和監管機構可以信任的可靠網路和安全處理用戶資料。
我認為沒有理由相信 Facebook 在設計中做了必要的工作來克服這些技術問題，或者它比目前的基礎設施有任何技術優勢。說公司需要監管靈活性來探索創新並不能成為不先進行創新的藉口。
來源： www.habr.com