获得 IBM 和以太坊基金会科研奖金的编程语言 DeepSEA 究竟是什么？

以太坊基金会（Ethereum Foundation）刚刚宣布了第五批科研奖金名单，共有 7 个项目被授予资金支持，包括：
1） The Matter，一项应用了 zkSNARK 技术的 Plasma 扩容方案；
2） LeapDAO，Plasma 扩容方案「Leap」的新版设计；
3） Py-libp2p，ibp2p 的 Python 语言实现，可以应用于 Eth2.0 研究；
4） Ethereum on ARM ，在 ARM 设备等资源受限设备上运行以太坊客户端的方案；
5） Goerli 测试网，一种跨各种客户端的以太坊测试网；
6） Shadowlands，Python 语言开发的全文字界面以太坊 DApp 平台；
7） DeepSEA，一共用于编写已验证智能合约的编程语言。

其中第七个项目「DeepSEA」值得关注。DeepSEA 由安全服务商 CertiK 研发团队、耶鲁大学和哥伦比亚大学科研团队进行相关研究。在获得以太坊基金会的科研奖金资助之前，这个项目还已经获得了 IBM-哥伦比亚数据中心和量子链（Qtum）授予的科研经费。这次又获得以太坊基金会的资金支持，体现出业内对区块链安全体系建设的重视程度，以及推动跨行业应用场景实现的强烈愿景。

链闻了解到，DeepSEA 项目由 CertiK 两位联合创始人耶鲁大学计算机系主任邵中教授与哥伦比亚大学计算机系顾荣辉教授共同主导，是一种针对智能合约的函数式智能合约编程语言。

CertiK 团队告诉链闻，他们开发 DeepSEA 这个智能合约编程语言，是希望让开发者在智能合约中引入交互式形式化验证技术，让智能合约能够被编译成函数定义导入 Coq （一种辅助证明工具），并且被自动放入相应的 DeepSEA 规范层（Specification Layer）中，从而用数学方式完全证明。

换句话说，DeepSEA 的诞生，让多种用于编写智能合约的高级语言能够被编译到例如以太坊虚拟机（EVM）或超级账本（Hyperledger）等机器语言中，并能够保证编译过程不会产生任何漏洞。这会对跨平台智能合约的功能整合和安全验证起到了举足轻重的作用。

CertiK 联合创始人、哥伦比亚大学计算机系顾荣辉教授曾经提到：虽然区块链程序漏洞的检测已经被业界高度重视，但智能合约安全事件仍旧频繁发生，因此 CertiK 团队产生了一个想法：「是否可以从源头处解决区块链的安全问题？是否可以通过设计新的智能合约语言在开发阶段消灭安全漏洞？」

带着这个想法，CertiK 团队开始了 DeepSEA 项目的研发工作，他们通过 DeepSEA-Blockchain 框架构建跨平台的、可信赖的智能合约框架，为 Hyperledger、EVM 等平台上的开发者提供一个值得信赖的开发环境。

据顾荣辉教授介绍，DeepSEA 是一种「无漏洞的编译器」，该编译器可以证明源代码无漏洞，同时被编译后的机器码不会存在漏洞。同时，DeepSEA 源代码中的程序规范可以被手动导入 Coq 证明辅助器中，开发者可以在 Coq 中对程序进行手动或者半自动证明。

DeepSEA 架构示意图

DeepSEA 框架的独特属性表明该语言可以有效处理编程中的“固有冲突”，详述如下：
“如今的主流操作系统和虚拟机管理程序仍然是用类似 C 的底层语言编写的。我们发现，高级的形式化推理和底层系统编程之间似乎存在固有的冲突：前者依赖于高抽象级别的丰富理论，而后者必须操纵和管理低级别的影响和硬件资源。”

顾荣辉教授表示，DeepSEA 项目将帮助 CertiK 公司进一步探索形式化验证技术在区块链领域的应用，从而更好的保护用户的数字资产安全。为了让 DeepSEA 项目在实际场景中更好地应用，研究人员的目标是设计和实现一个“工具链”。该工具链将会被应用于“构建经认证的操作系统内核”。CertiK 将有机会把 DeepSEA 工具链纳入其现有的形式化验证科技中，实现更完善的智能合约和区块链生态安全验证，从而更好地保护用户的数字资产安全。

CertiK 是一个由计算机科学领域的自身教授创立的公司，团队核心成员包括耶鲁大学教授邵中、哥伦比亚大学教授顾荣辉，该项目通过形式化验证技术，提供规模化智能合约验证服务，来保证智能合约和区块链系统的安全性。根据 CertiK 团队披露，CertiK 在 2018 年间共保护了价值 12 亿美金的数字资产免受损失，这一数字在新的一年中还在持续增长。

—-

编译者/作者：项目动态

玩币族申明：玩币族作为开放的资讯翻译/分享平台，所提供的所有资讯仅代表作者个人观点，与玩币族平台立场无关，且不构成任何投资理财建议。文章版权归原作者所有。