查看原文
其他

DeepSEA编译器1.1版本,正式发布!

CertiKFoundation CertiK 2021-02-05
继CertiK主网正式上线后,DeepSEA编译器进行了两项重大更新,目前DeepSEA编译器的1.1版本已正式发布。

此次发布中的重大更新内容:

1. DeepSEA的WebAssembly后端现已完备支持所有的语言特性。

2. 现在DeepSEA的整个编译后端均可作为一个独立的库来使用在任何人的项目中。

你可以在Github发布页面下载可执行文件及使用案例:

https://github.com/CertiKFoundation/deepsea/releases


对以太坊2.0 WebAssembly的完备支持

DeepSEA 1.0对于Ethereum 2.0 WebAssembly的支持仅限于不包含哈希操作的语言特性(也就是除了事件、数组、结构之外的操作)。

在这次的发布中,DeepSEA已将1.0未能支持的特性补齐。也就是说,目前DeepSEA已完备支持所有特性。

另外,CertiK还将以太坊环境接口(Ethereum Environment Interface)融合进了CVM中,这意味着DeepSEA的WebAssembly后端(以太坊2.0 eWasm)现在可以在CertiK上使用了。

在神荼测试网或者CertiK主网上部署一个DeepSEA WebAssembly合约,你只需要在使用 `certikcli deploy` 命令式加上 `--ewasm` 参数即可。

如果部署的合约中不包含任何的初始化代码,那么则需要再加上 `--runtime` 参数。

以下是一个在虚拟机中运行编译到DeepSEA以太坊2.0版本WebAssembly的多层智能合约的例子:


独立的编译器后端

1.1版本另一个重大改进是DeepSEA编译器后端现已可以作为一个可以被用来制作其他任意语言编译器的库。
如同其他很多编译器,DeepSEA当前的实现分为前端和后端。前端负责解析语法树、类型检查、将抽象数据类型转换为具体的底层表示,以及DeepSEA特定的诸如对象或者层的语言特性。
总体来说,前端将DeepSEA程序转换成了一个简单的中间语言MiniC,然后后端再将MiniC程序转换成为EVM或者是eWasm。
MiniC语言的设计就像它的名字所表达的那样,基本上是C语言的简化版本。
因此MiniC很适合作为任意编程语言的编译对象。生成MiniC并且使用DeepSEA后端比直接生成EVM字节码要容易得多。并且因为DeepSEA后端经过了形式化验证,所以基于它的其他编译器的漏洞风险将会更低,保障程序按照其设计初衷正确执行的可能性也将大大增加。
DeepSEA 1.1版本的发布中有两个不同版本的后端:一个作为可执行文件,另一个作为软件库。
首先是一个独立的可编译MiniC的命令行程序,然后是一组可以被直接链接到任意Ocaml程序中的Ocaml文件。
如果你的编译器是使用Ocaml便携的,那么使用DeepSEA后端将会大大增加使用便捷性。
想要更多关于MiniC以及如何使用后端库的细节,请阅读DeepSEA的参考手册:

https://github.com/CertiKFoundation/deepsea/blob/master/DeepSEA language reference.pdf

在此,CertiK尝试加入了一个新的可以用于便携以太坊智能合约的编程语言OpenSC:
https://github.com/certikfoundation/deepsea/tree/master/src/OpenSC
这个语言最初是作为哥伦比亚大学编译器课程中的小组项目创作出来的。经过创作小组的学生成员许可后,CertiK将此语言发布。
OpenSC是一个和DeepSEA完全不同的语言,但是测试表明它可以成功使用DeepSEA的后端。
此案例是一个信号:通过使用DeepSEA编译器后端的情况下,编写区块链编程语言将不再是一个困难的过程。
DeepSEA项目被专门设计用来编写可认证的正确代码,它同时为保护代码提供了有效的解决方案。
CertiK相信,在智能合约编程语言这个底层技术支撑中,不同的安全实现方式,将会给我们的应用带来不同的安全保障。
复制链接【https://certik.org/research/deepsea/】至浏览器即可查看DeepSEA最新信息。

往期回顾

CertiK Chain主网已正式上线!

CertiK DeepSEA编译器支持蚂蚁链,加码可信区块链

历时2的10次方,CertiK主网即将上线!

一站式降低风险:CertiK安全预言机、CertiKShield

预测市场“头号玩家”PlotX,已通过安全审计

CertiKShield正式启动,最高可获得100,000美元的资产损失理赔!

币安智能链上快速扫描、预言机及CertiKShield操作指南

币安智能链与CertiK合作,联合保卫DeFi交易安全

Yearn.finance新项目Eminence攻击事件漏洞分析

CertiK工程师专访 | 程序员第一人,是个漂亮妹子?


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

    您可能也对以下帖子感兴趣

    文章有问题?点此查看未经处理的缓存