2020 最具“战略性”的编程语言:C 语言?还是 C# 、 Python 、Swift?

编程语言是人们指导或控制机器的工具,其开发目的在于让操控机器的过程更加简单和顺畅。正因如此,数百种编程语言应运而生。然而,它们的命运却各不相同。一些语言已不复使用,或将在未来几年淘汰。相应地,一些语言将会被充分使用,还有一些崭新的编程语言正在逐渐被人们所接受。

“虽然程序漏洞的检测和验证已经引起业界的高度重视,但在区块链行业内,安全问题仍旧频繁发生。如果只检测已经存在的漏洞的话,永远存在被黑客抢先一步的风险。既然这样,我们有没有办法直接开发出一个没有程序漏洞的、可以完全被信赖的智能合约呢?”

CertiK 联合创始人顾荣辉在开发者大会上提到了智能合约安全的源头问题。

DeepSEA 项目为了攻克这些更加底层可能出现的问题与隐患而诞生。

前天发布的【宅在家里最适合看的编程,C++、Java 还是……沈从文?】已经简单介绍了 DeepSEA 的基础概念,那么现在让我们来了解一下 DeepSEA 的运行机制和执行过程。DeepSEA 是一种灵活且兼容的语言,可以使用 Coq 创建具有高度抽象和推理功能的安全程序。它旨在提供使用 Coq 证明助手来进行形式化验证的智能合约功能属性的方法。

现如今许多关于智能合约验证的工作都是围绕自动证明(例如 Z3)建立的。这种功能可以简单陈述一个定理,并尝试证明这一定理。对于以下相对简单的证明、算术表达式和数据结构(如数组),这种功能最为有用。在该定理自定义甚至陈述状态的情况下,自动工具往往会卡顿。Coq 是一个交互式证明助手,它不会证明定理:用户必须同时编写定理陈述和证明,然后 Coq 会检查证明是否正确。这将涉及更多的工作,但它同时也可以处理任意高级数学问题。

为了推理出 Coq 中合约的正确性,需要定义一个正在执行的模型,该模型可以加载到 Coq 证明助手中。现在 CertiK 团队研发的方法是使用相当小的编程语言(DeepSEA 语言)编写合约。DeepSEA 编译器不仅将合约编译为 EVM 字节码,还输出可以加载的表示形式进入 Coq。从而可以推断出合约的高级表示形式。由于技术人员还验证了 DeepSEA 编译器的正确性,所以可以确保生成的 Coq 合约表示形式与已编译的 EVM 字节码的工作相契合。

2020 最具“战略性”的编程语言:C 语言?还是 C# 、 Python 、Swift?

示例: 使用 Coq 验证通证合约

DeepSEA 语言受 ML 和 Coq 本身等功能语言的启发。下面的代码显示了通证合约的总体外观,以它为运行示例。

2020 最具“战略性”的编程语言:C 语言?还是 C# 、 Python 、Swift?

下图显示了将通证合约编译为 EVM 的过程。编译过程首先要解析合约并对其进行类型检查,然后生成一组相应的 Coq 文件。技术团队将这些文件与经过验证的编译器后端链接,然后使用 Coq 的提取工具将其编译为 OCaml,从而生成 EVM 程序集。最后,打印机通道(未经验证,用 OCaml 编写)可以将程序集转换为实际的字节码。即可通过将合约部署到 Ganache 实例中并调用函数来演示合约的运行过程

2020 最具“战略性”的编程语言:C 语言?还是 C# 、 Python 、Swift?

为了方便起见,CertiK 开发了一个 DeepSEA 编译器,它被编译为单个 OCaml 可执行文件,用户无需在计算机上安装 Coq 即可运行它。这用(未经验证的) OCaml 代码替换了用 Coq 编写的某些编译器,因此可信度较低,并且不会生成合约的 Coq 表示形式。下图显示的编译器正在运行,它能生成与上面 Coq 版本相同的字节码。我们还可以打印出中间语言表示形式或 EVM 汇编助记符。

2020 最具“战略性”的编程语言:C 语言?还是 C# 、 Python 、Swift?

现在我们可以将合约表示形式加载到 Coq 中,并开始编写有关它的证明。合约表示为用 Coq 的内置编程语言“ Gallina”编写的功能,如下所示。由于这是用户将在证明中使用的版本,因此我们希望它以清晰的方式与输入程序相对应并实现大部分的功能。这一点可以通过使用 Gallina 语言(不是 DeepSEA 语言)以及 monadic 组合器编写来实现。

如果我们查看细节,那么从某种角度来说,Coq 表示实际上比输入程序更高级,更易于推理。虽然已编译的以太坊哈希值无法跟踪存储在程序中的密钥,但在 Coq 版本中,我们可以使用 Int256Tree 数据表示余额,该数据类型表会储存其密钥。尽管可执行程序使用的是 256 个整数,但表示形式可使用的整数是无限的,因此表示形式可以用普通算术实现。(下文将会讨论如何处理整数溢出。)

2020 最具“战略性”的编程语言:C 语言?还是 C# 、 Python 、Swift?

下图显示了使用 Coq 证明助手来证明合约的 transfer 方法保留了余额中存储的代币。换句话说,其中没有可以创建或销毁通证的漏洞。(有可能出问题的地方就是代码检查整数溢出,并检查发送和接收帐户是否不同的环节。如果忘记了其中一个 if 语句,则该定理将不可证明。) Coq 是一个交互式操作:计算机不断显示要证明的内容,程序员输入一系列命令,将定理分解为更简单的语句。

2020 最具“战略性”的编程语言:C 语言?还是 C# 、 Python 、Swift?

除了最终合约之外,DeepSEA 系统还生成了一组附带条件,必须证明这些附带条件对合约是有效的,且多数情况下不存在整数溢出。在 Solidity 语言中,程序员通常使用“安全机制”库,并在该库中添加证明语句,以在发生整数溢出时还原合约调用函数的过程。DeepSEA 提供了插入语句,在这种情况下,附带条件显得微不足道。通过一些措施,目前可以证明 transfer 方法中的整数不会溢出。

证明(下图中的摘录)余额中存储值的不变性有关,所以实际上整个过程并不需要安全保证性语句。这是一个用程序验证如何提高效率的例子,它帮助程序员去使用更多编程技术,使它们可操作性和安全性都得到保证。

2020 最具“战略性”的编程语言:C 语言?还是 C# 、 Python 、Swift?

在接下来的几周和几个月中,CertiK 将发布更多项目,例如下载编译器,语言手册草案,更多示例证明以及最终实现案例等。

DeepSEA 正式上线,复制链接【https://certik.org/research/deepsea/】至浏览器即可查看 DeepSEA 上线产品。

2020 最具“战略性”的编程语言:C 语言?还是 C# 、 Python 、Swift?

了解更多

General Information: info@certik.org

Audit & Partnerships: bd@certik.org

Website: certik.org

Twitter: @certik.org

Telegram: t.me/certik.org

Medium:medium.com/certik

币乎:bihu.com/people/1093109

往期回顾

*热点追踪 | 疫情肆虐,“围城”中的区块链

*## 宅在家里最适合看的编程,C++、Java 还是……沈从文?

*## 疫情抗击:武汉红会被问责,如何防止慈善变成伪善

*## 安全聚焦 | CertiK 已经完成对 BetProtocol 通证智能合约的审计

*## 安全聚焦 | CertiK 已完成对 The Sand box 旗下 SAND 以及 LAND 通证合约的审计

*## 干货分享 | 详情回顾:倪兆中博士深度解答如何构建安全的区块链生态

*## 安全聚焦 | CertiK 已完成对 FrenchICO 的安全审计

*## 公司动态 | 金色讲堂预告 : 如何构建安全的区块链生态?倪兆中为您深度解答

*## 公司动态 | CertiK 荣获金色财经“与时共创”最佳安全服务机构大奖!

*## 业内干货 | 以太坊销毁价值 135 万美元的 PAX?代币销毁是什么?

*##

请点击“阅读原文”访问 CertiK 官方网站