建筑性精神分裂症Facebook天秤座

两年后,我回到博客上发表了与通常无聊的Haskell和数学讲座不同的文章。 在过去的几年中,我处理了欧盟的金融技术,似乎是时候写一篇技术媒体很少关注的话题了。

Facebook最近发布了名为“天秤座”的“新金融服务平台”。 它被定位为基于一篮子国际货币的数字支付系统,这些国际货币在“区块链”上进行管理,并存储在瑞士管理的现金池中。 该项目的目标雄心勃勃,并带来大规模的地缘政治后果。

金融时报》《纽约时报》在提议的金融体系的核心部分有很多关于不合理的货币和经济假设的合理文章。 但是从技术角度来看,没有足够的专家来进行分析。 在金融基础设施上工作并公开谈论其工作的人并不多,因此,尽管该项目的内部对全世界都是开放的,但该项目并未在技术媒体上进行过多报道。 我的意思是天秤座Calibra组织存储库中的开源。

向世界开放的是一种精神分裂症的建筑假象,声称具有全球支付基础设施的安全平台的作用。

如果您沉迷于代码库,那么系统的实际实现将以最奇怪的方式完全不同于所声明的目标。 我确信这个项目有一段有趣的公司历史。 因此,可以合理地假设它是出于某种热情而开发的,但实际上,我看到了一套非常奇怪的体系结构解决方案,它们破坏了整个系统并危及用户。

我不会对Facebook作为一家公司发表客观观点。 IT行业中很少有人会同情她。 但是,将她的陈述与已发布的代码进行比较可以清楚地表明,所述目的是一个根本的骗局。 简而言之,该项目无法赋予任何人权力。 他将完全受一家广告公司的控制,该公司的广告业务陷入丑闻和腐败,以至于他只能选择使付款和信用评分多样化以生存。 一个明确的长期目标是充当数据经纪人和中介,让消费者根据他们在社交网络上的个人数据获得信贷。 这是一个完全恐怖而令人沮丧的故事,没有引起应有的重视。

这个故事唯一可以挽救的恩典是,他们创造的人工制品太有趣了,以至于无法完成任务,只能视为一种骄傲。 此项目中存在几个基本的体系结构错误:

使用访问控制解决网络中的拜占庭将军问题是不一致的设计


拜占庭将军的任务是分布式系统研究的一个相当狭窄的领域。 它描述了当采取对系统功能至关重要的纠正措施时,网络系统承受任意组件故障的能力。 弹性网络必须能够抵御多种类型的攻击,包括重新启动,故障,恶意负载和领导选举中的恶意投票。 这是Libra架构的主要解决方案,在这里完全没有意义。

来自此附加结构的时间复杂度的开销取决于算法。 关于Paxos和Raft协议的变种,有很多文献都提出了解决拜占庭将军问题的方法,但是所有这些结构都带来了额外的通信开销成本, On2维持法定人数。 对于Libra,我们选择了通讯成本最高的算法 On2如果领导失败。 对于几种类型的网络故障事件,潜在的重新选举领导者还会带来额外的开销。

对于在高度管制的跨国公司财团中运行的系统,其中所有用户都有一个Facebook签名的代码,并且由Facebook控制对网络的访问,以共识级别考虑恶意参与者根本没有意义。 目前尚不清楚为什么该系统通常能解决拜占庭将军的问题,而不仅仅是维护一致的审核记录以验证合规性。 由万事达卡(Mastercard)或安德森·霍洛维茨(Andressen Horrowitz)管理的天秤座主机突然开始运行恶意代码的可能性是一个奇怪的计划方案,只需确保协议和非技术性(即合法)手段的完整性,就可以更好地解决。

在国会的证词中,该产品被宣布为新的国际支付协议的竞争对手,例如微信,支付宝和M-Pesa。 但是,这些系统都没有设计用于验证者库来解决拜占庭将军的问题。 它们仅在传统的高吞吐量总线上进行设计,该总线根据一组固定的规则进行布线。 这是设计支付系统的自然方法。 精心设计的支付系统根本无法解决重复支出和分叉的问题。

共识算法的开销无法解决任何问题,仅出于公共区块链的货物崇拜而没有任何理由限制系统吞吐量,这不适用于此用例。

天秤座没有交易隐私


根据该文档,系统在设计时考虑了假名 ,即协议中使用的地址是从椭圆曲线上的公钥获得的,并且不包含有关帐户的元数据。 但是,在组织的管理结构的描述中或协议本身中,都没有任何地方指示验证者如何隐藏参与交易的经济数据。 该系统旨在为许多外部方进行大规模交易复制,根据现有的欧洲和美国银行保密法,不应将其用于经济细节。

不同国家/地区的数据政策难以协调,尤其是考虑到不同司法管辖区的法律法规不同,这些国家对数据保护和隐私具有不同的文化观点。 协议本身默认情况下对财团成员完全开放,这是一个明显的技术缺陷,不符合开发协议的要求。

Libra HotStuff BFT无法达到支付系统所需的带宽


在英国,BAC之类的清算系统每月能够执行约5.8亿笔交易。 同时,高度优化的系统(例如Visa)每天可以处理150,000,000笔交易。 性能取决于交易规模,网络路由,系统负载和AML检查 (反洗钱,洗钱方案)。

天秤座试图解决的问题是,对于国内转移而言,这并不是真正的问题,因为过去十年来,各民族国家对其清算基础设施进行了现代化改造。 对于欧盟的零售消费者而言,转移资金根本不是问题。 在传统基础架构上,这可以使用标准智能手机在几秒钟内完成。 对于大型公司转移,存在与大量资金转移有关的各种机制和规则。

没有技术原因也无法立即进行跨境付款,不同司法管辖区之间在规则和要求上存在差异。 如果在交易链的不同阶段多次执行必要的预防措施(客户的尽职调查,制裁确认等),则可能导致交易延迟。 但是,这种延迟纯粹是监管法律及其执行的功能,而不是技术。

对于消费者而言,没有理由在几秒钟之内不会清除英国的交易。 欧盟的零售交易确实在放慢KYC (了解您的客户) 检查和政府和监管机构施加的反洗钱限制,这些限制同样适用于Libra付款。 即使Facebook克服了国际转移和私人数据转移的障碍,但从全球交易的吞吐量来看,所提出的模型仍需要数百个工年,并且可能会从头开始处理。

天秤座移动语言不正确


白皮书对名为Move的未经验证的新语言进行了大胆的陈述。 从编程语言理论(PLT)的角度来看,这些陈述令人怀疑。

Move是一种新的编程语言,用于在Libra区块链上实现自定义交易逻辑和“智能合约”。 由于天秤座的目标是一天为数十亿人提供服务,因此Move的设计重点是安全性。

Move的一个关键功能是能够利用线性逻辑启发的语义来定义任意类型的资源。

在公共区块链中,智能合约通过代管账户,洗钱,发行场外代币和赌博而进入公共网络的逻辑。 所有这些都是通过一种称为Solidity的,设计极差的语言完成的,从学术的角度来看,这使PHP的作者看起来像个天才。 奇怪的是,Facebook的新语言似乎与这些技术没有任何关系,因为它实际上是一种为晦涩的公司任务设计的脚本语言。

在私人分布式分类帐中,智能合约是顾问分散使用的术语之一,而无需过多关注明确的定义或目标。 公司软件顾问通常会因模棱两可而赚钱,而智能合约是公司默默无闻的典范,因为它们可以从字面上定义为任何事物。

在声明了其安全性之后,我们应该查看该语言的语义。 编程语言理论的正确性通常包含两个不同的证明:“进行”和“保存”,它们确定了语言评估规则整个空间的一致性。 更具体地说,在类型论中,如果函数仅使用一次自变量,则该函数为“线性”,如果使用不超过一次,则为“仿射”。 线性类型系统为声明的线性函数真正是线性提供了静态保证,将类型分配给函数的所有子表达式并跟踪调用位置。 这是一个微妙的证明性质,对于整个程序而言,实现起来并不容易。 线性类型化仍然是一个非常学术的研究领域,受Clean类型的唯一性和Rust中类型所有权的影响。 对于向Glasgow Haskell编译器添加线性类型,有一些初步建议。

关于线性类型使用的Move语句在编译器中似乎是不合理的,因为没有这样的类型检查逻辑 。 据人们判断,该技术文档引用了吉拉德和皮尔斯的经典文献,在实际的实现中,没有任何东西。

此外,在实现或文档中都找不到所谓安全语言的形式语义。 该语言小到足以在Coq或Isabelle中找到语义正确性的完整证明。 实际上,可以使用过去十年中发明的现代工具来实现将证据转换为字节码的完整转换的端到端编译器。 我们知道如何做到这一点,始于1996年George Nekula和Peter Lee工作

从编程语言理论的角度来看,无法验证“ Move是一种可靠且安全的语言”的说法,因为这些说法纯属挥舞和推销,而不是实际证据。 对于正在提议委托数十亿美元进行交易处理的语言开发项目,这是一个令人震惊的情况。

天秤座密码学不正确


建立可靠的密码系统是一个非常复杂的工程问题,以大量健康的偏执狂来对待危险代码总是更好。 该领域有重大突破,例如Microsoft Everest项目,该项目构建了可验证的安全TLS堆栈 。 已经存在用于创建可验证原语的工具。 尽管价格昂贵,但显然并没有超出Facebook的经济可能性。 但是,团队决定不参加该项目,该项目被宣布为全球金融体系的可靠基础。

这个天秤座项目依赖于几个相当新的库来创建实验性密码系统,这些才出现在最近几年。 无法确定对以下工具的依赖项是否安全,因为这些库均未经过审核且没有标准的披露政策。 特别是,对于一些主要的图书馆,尚无法确定如何防范第三方渠道的攻击和时间攻击。

  1. ed25519-dalek
  2. 曲线25519-达力克

天秤座库具有更大的实验性,它使用非常新的方法超越了标准模型,例如可验证的随机函数(VRF),双线性对和阈值签名。 这些方法和库可能是合理的,但是将它们全部组合在一个系统中会引起对攻击表面积的严重关注。 所有这些新工具和技术的结合大大增加了安全证据的复杂性。

应当假定,整个加密堆栈容易受到各种攻击,除非有其他证明。 著名的Facebook模型“快速移动和破坏事物”不能应用于处理客户财务数据的加密工具。

天秤座无法实施消费者保护机制


付款系统的一个显着特征是,如果诉讼取消付款或导致意外或系统故障,则可以回滚交易。 天秤座被设计为“完全完成”,并且不包括用于取消付款的交易类型。 在英国,从100英镑到30,000英镑的所有付款都受《消费者信贷法》的约束。 这意味着,如果购买的商品有问题或收款人未提供服务,则支付系统与卖方共同承担责任。 类似的规则适用于欧盟,亚洲和北美。

Libra的当前设计没有包含遵守这些法律的协议,并且没有明确的创建计划。 从体系结构的角度来看,更糟糕的是,基于Merkle驱动器状态的经过身份验证的内核数据的结构的最终性,不允许在不重新设计内核的情况下创建这种协议的任何机制。



在对该项目进行技术检查之后,我们可以得出结论,它根本不会通过任何有关分布式系统研究或金融工程的著名期刊的测试。 为了尝试更改全球货币政策,需要做大量的技术工作来创建可靠的网络并安全处理用户数据,这是公共和监管机构可以信任的。

我没有理由相信Facebook在其项目中做了必要的工作来克服这些技术问题,或者与现有基础架构相比,它具有某些技术优势。 一家公司需要监管灵活性来了解创新的主张并不是没有首先创造创新的借口。

Source: https://habr.com/ru/post/zh-CN475022/


All Articles