运行时会说:“我看到了这个交易中心,我看到了他们想要使用的所有对象。我正在检查他们是否实际拥有这些对象,或者它们拥有一个可以中转拥有它们的对象,以便他们有权使用它们。我们要求程序员进行的许多权限检查最终都在We Run Time中发生,这些检查是不可能忘记的。我认为这非常重要,因为最难保护的是程序员没有告诉你的规范。这些规范很容易被忘记,使用静态分析或其他方法很难捕捉到它们,因为你总是需要一些人来确定哪些规范很重要。
主持人 Sonal Chokshi:顺便说一句,在远期或近期的长期规划方面,当人们以这种方式更多地合作时,企业规模会发生什么,我认为这将非常有趣,因为它显然是分布式的,不仅仅是一个公司,有时人们会合作。但我的意思是,当你考虑现在的老旧方式,你有像开发人员和所有这些最佳实践和所有这些方法。然后你有这些非常不同的思维方式来做事情,我们还没有完全在这个世界中将所有这些正式化,这还为时过早,但我非常好奇这种事情会是什么样子。
a16z Noah:现在EVM的工具很好用,那么Move的工具怎么样呢?还需要进行哪些重大改变吗?
Sui CTO Sam Blackshear :我认为我们的工具还处于很早期的阶段。我们正在开发一个包管理器,可以跨链使用,像Create.io或npm一样。Move的模型系统非常适合这种事情,我们正在努力实现这个目标。这个包管理器可以让开发者轻松分享他们的代码,这在Solidity中很难做到,因为在Solidity中,只能通过复制粘贴的方式来分享代码。我们还在最初的时候就专注于正确性工具的研发,我们有很多这样的工具,但我认为我们还有很多事情要做,使它们更易用。我们有一个单元测试框架,我们可以直接在Move中编写测试。我们也开发了Move prover,用来辅助我们做形式化验证。
Move Prover 的重要性
主持人 Sonal Chokshi:能否简单谈一下形式化验证以及为什么Move Prover很重要?
Sui CTO Sam Blackshear :形式化验证很具有挑战性,通常需要专家或者博士来使用。我们正在努力将它推广到每一个日常开发者,而不需要专业知识。目前还不清楚这个目标能否实现,但我们看到了一些很有前途的项目。比如,最近有人将一个智能合约的所有规范提交到了一张文件中,之后只需要为新函数写规范,这就使得形式化验证变得非常容易。不过,形式化验证还有很多需要改进的地方,包括提高易用性和功能强大程度。
还有像fuzzer这样的工具,虽然不如形式化验证好用,但对于一些重要的正确性检查非常有帮助,特别是当你需要写一些非常复杂的代码时。我们也有一些学术界的库在研发这些工具。除此之外,我们也正在研究如何让编写程序变得更容易,比如支持更多集成开发环境、程序合成和人工智能等。
主持人 Sonal Chokshi:如何使用Move Prover?如果我想试试它怎么办?
Sui CTO Sam Blackshear :首先你需要拿到你已经测试过的程序。验证不是测试的补充。然后你可以编写一些很难测试或很难检查的内容。这可能是一些简单的函数前后条件。比如说,如果我的函数输入满足这个条件,那么输出应该满足那个条件。你还可以编写数据不变量,比如你有一个计数器,你想证明它总是在增加,你可以编写一个规范,将其附加到计数器结构中,以检查它是否成立。然后它会查看所有的函数,并确保这些规范都成立。
还有更高级的用法,比如全局存储和变量。你可能想说,这个对象始终只有一个,或者这个对象有两个,然后有三个。以及这个对象的字段和那个对象的字段之间的关系。这些规范很大程度上取决于应用程序。Move语言可以避免很多基本的错误,但对于你作为程序员来说,总会有一些特定于你的应用程序的正确性条件。规范语言使编写这些条件变得容易,可以在编写代码之后或某些情况下甚至在编写代码之前编写它们,并确保它们在所有可能的程序执行和所有可能的函数调用中都成立。因此,现在,规范语言与编译器集成,因此您可以在任何这些模式下提取它并尝试使用它。它还与构建系统集成。您只需要执行move build -prove,它就会检查这些规范。
a16z Noah:酷!Prover能理解Sui 对象模型和Sui交易系统吗?比如,我能否证明关于跨交易的一些可能修改全局状态的内容?
Sui CTO Sam Blackshear :它还没有完全理解,但它并不需要完全理解。例如,如果你想证明计数器始终在增加,这是一个Sui对象,但是它不需要完全理解Sui就可以证明。即使在核心Move的prover中,它也真正考虑对象和全局存储的层面,而不是像交易这样的概念。因此,今天它确实只能考虑函数和事务的层面,这也能够正常工作。但我想我们将来可能会在Sui方面做更多的事情,特别是关于父子关系和异构对象映射。
编程语言的治理
主持人 Sonal Chokshi:我们可以谈谈编程语言的治理吗?编程语言的演进有着悠久的历史,但是在区块链和加密货币的背景下,治理话题显然更加重要,因为有许多其他方面需要考虑,如分权、开源、分布式社区、令牌和经济学资产等,这有时作为激励计划的一部分参与其中。
a16z Eddy Lazzarin:特别是因为它们是开源的,能在许多不同的上下文中使用,它们被视为公共物品,但它们不同,需要设计和细节的关注。编程语言应该如何发展?今天有很多编程语言似乎都有不同的治理方式,如我所想到的前两个是C++委员会和WG21委员会,还有一些非常复杂的名称。
然后像Python,Guido是它的生命之恩人,拥有 benevolent dictator for life。那么,您认为什么是现代化的编程语言治理方式?特别是在加密货币领域,这是一种独特的情况,因为这些编程语言可能与层一相连,这是一种依赖于编程语言的不同类型的东西,它是一种公共物品,但是它有利益相关者,它有大量的资本附加值,有许多价值正在传递。也许有一些编程语言的治理模式更适合区块链。我对思考编程语言应该如何治理或更好地说,移动如何发展,考虑到所有巨大的利益相关者和设计语言保护其安全性质的重要性非常感兴趣。
Sui CTO Sam Blackshear :嗯,我不会认为我的见解适用于其他编程语言。但对于Move来说,我有一个非常具体的看法,就是这种跨平台的愿望。Move 被设计为一种跨平台语言,其中一些链EDM 的基本功能仍应适用,并且覆盖了智能合约开发能手和Web2新人,极具灵活性。除了对程序员和平台设计者的好处外,治理是另一个原因,几乎所有区块链语言中的有争议的决定,例如:我们应该增加这个限制吗?或者我们应该支持这种签名方案吗?或者我们是否应该拥有这个库?我们试图将其设置在适配器层,即构建在语言形式之上的平台,而核心语言非常简洁。简洁性是我们语言的关键设计原则之一,非常不依赖于区块链。
因此,如果我们要与社区的利益相关者进行辩论,它不会像“我们应该增加gas限制”这样的问题。而是像“我们应该拥有电子邮件”这样的问题,这是一个更纯粹的设计问题,可以受到来自一个或多个Move平台的问题或用例的影响,但不太可能朝着对某个利益相关者有利而对其他人不利的方向发展。到目前为止,这种模式一直运作得很好,但我们还需要看看未来会发生什么。
基本上,Move语言的治理方式是,最初,Move是在Facebook开发的,没有真正的治理。它只是我们使用它的方式,虽然我们有这些设计原则。现在,团队分散了一些,我们有很多来自不同机构的成员。有些人在我们这里,有些人在其它地方。有一些来自学术界、安全社区的第三方贡献者,还有一些Move链的星际币等其他机构。我们每个星期四都会开会。我们会讨论Move的设计问题,我们非常谨慎地扩展语言。简洁性是主要的东西,但我们会积极地扩展它。
比如,添加这个东西会使在Move之上的这些层次的实验更容易进行。一旦我们看到这些实验的结果,或者每个人似乎都在做同样的事情,那么我们就会将其移到核心语言中。因此,我们对治理的答案是:尽可能避免治理,通过让有争议的事情发生在Move之上的层次,以及将简洁性作为核心原则之一,使我们在仅当每个程序员都需要某个东西时,才添加新的内容。
主持人 Sonal Chokshi:你们作为程序员,对于另一面的事情,比如Noah,你们真的在乎吗?比如说你选择使用什么工具,怎样参与?你们在意社区或者编程语言的治理吗?还是只在乎你们获取所需的工具?
a16z Noah:我认为在一定程度上是有关系的,比如你想使用一个被很多人使用的语言,这样你就可以得到更多的贡献者,对吧?你也想要一个不会被抛弃的语言,对吧?那些应该是主要的考虑因素。但是,我并不在意Python是由独裁统治还是委员会治理,只要能够达成目标就好。尽管我认为很多人不在意,但是有很多争论表明由委员会治理已经破坏了很多编程语言,我想。
主持人 Sonal Chokshi:是啊,我一直觉得很有趣。
Sui CTO Sam Blackshear :我认为这很重要。我有一些技术上的设想,比如跨平台的程序和资源,以及这些东西应该有的大致想法。但是这是一个社区项目。很多贡献者为设计的很多方面做出了贡献,我并不是Move或任何其他东西的独裁者。但是,我认为我的角色是策展人,确保每个人都在同一页面,并确保在想法涌现时,我们根据这些原则进行评估,这些想法可以来自任何人。但是最重要的是我们有共同的愿景。每种语言都略有不同。我认为它们固有地反映了它们的用途、创建者和社区的个性等等因素。所以肯定不会有一种适用于所有的规则。
主持人 Sonal Chokshi:对,完全没问题,这很有道理。
Sam怎么进入Move的
所以在我们结束前的最后几个问题里,我突然意识到我们从来没有听过Sam怎么来到Move的。我主要感兴趣的不仅仅是因为我想听你的故事,我相信它很棒,但我更感兴趣的是你是如何通过思考去解决问题的。所以你能快速分享一下这个过程吗?当然可以。
Sui CTO Sam Blackshear :我开始作为一名编程语言研究员来进行职业生涯。我从事静态分析和程序验证的工作,这意味着我花了很多时间看真实的程序,寻找漏洞,并尝试弄清楚程序员经常犯的错误类型是什么,以及导致这些错误的原因是什么。是语言的基本问题使得某些类型的错误过于容易?是他们使用的框架的问题?还是仅仅是有关人类心理学,使得某些类型的错误比其他错误更容易被发现?
基本上,在我的博士期间,我花了很多时间研究真实的程序,查找漏洞,然后构建这些工具,试图在不运行代码的情况下查看代码并尝试在之前捕捉这些错误。而这种事情在一般情况下是无法解决的。你在进行静态分析时,总是在与停机问题作斗争,但在实践中,你可以无限地接近完美的结果,而不是在理论中得出平均结果。所以我花了很多时间做这件事,看了所有经典类型的漏洞,如空引用、缓冲区溢出、安全问题等等。我真的很享受这个工作,但是很难找到这些例子和很多人真正关心的数据集。但是在我博士的最后阶段,我在Facebook实习。这是在2013年到2014年左右,他们正在从Web世界向移动世界过渡,并且发现当我将漏洞发布到移动应用中时,它会在那里存在两周,而在Web中,我可以立即修复它。
当我加入后,Android上的分裂问题是造成问题最严重的问题,因为这会导致无法修复的漏洞。他们在静态分析技术上进行了大量投资。他们从我的领域收购了一个研究小组,我有机会与他们一起工作,并继续我真正喜欢的工作。但是,与其结束于单个程序的漏洞修复,我开始思考如何设计一种语言来使这种漏洞更难以产生。
我对语言设计和程序安全方面的兴趣越来越大,开始产生一些关于如何构建更安全的语言的想法。后来,我在2018年加入了Libra项目,这是一个构建基于区块链的全球支付网络的项目,我被征用为编程语言方面的专家。这个项目需要一个新的编程语言,因此我开始着手构建Move语言,并使用我之前的经验来解决一些语言设计上的挑战,例如如何确保Move智能合约的安全性和正确性。
主持人 Sonal Chokshi:所以Libra 也被重命名为diem,这是今天很多人可能知道的。还有一个快速的提醒,你的博士论文的实际主题是什么?
Sui CTO Sam Blackshear :我的博士论文主要研究目标导向的静态分析。通常,在进行静态分析时,你会查看整个程序并构建有关程序的事实数据库,然后通过获取该事实数据库来查找漏洞。这种方法很有效,但对于非常大的程序而言,不太容易扩展,因为你必须查看整个程序并做所有事情。而你可能有一个非常具体的问题,只关注程序中的一个特定部分。例如,如果你正在运行分析器,并且在CI中报告漏洞,你真的想要报告在该pull request中发生的漏洞。对程序中的其余部分不是很关心。
本文采摘于网络,不代表本站立场,转载联系作者并注明出处:http://www.longfuchaju.com//chuangye/qiuzhi/6604.html