CertiK Chain： DeepSEA语言的原生链

与传统金融业相比，由于去中心化和开源等特性，区块链生态系统因可能遭受极大损失而会更加规避风险。当用户有能力在区块链上共享有价值的高风险数据时，安全性是至关重要的。然而，即便拥有了最佳设计的系统和规则，区块链系统仍然可能会失效，甚至被黑客攻击。

而CertiKChain 给区块链的安全注重带来了彻底的变革。它在系统的每一层面上都确立了可靠的安全性，使得任何在此之上构建的软件都能够保证区块链的可靠性。从操作系统一直到内置形式化验证支持的智能合约，CertiK Chain都给出了前所未有的安全性保证。

正因为有了这些安全性保证，CertiK Chain自然而然地成为了DeepSEA语言的原生链。DeepSEA是一个函数式编程语言，能够对智能合约进行高度抽象的严谨推理，并能够生成可信代码及其可被机械化检验的数学证明。

DeepSEA非常独特。和其他编程语言不同的是，它是被专门设计用来编写可认证的正确代码的。

今天，几乎所有的智能合约都是用未被设计支持形式化验证的语言写出来的。即使那些支持形式化验证的语言，也只是针对一些简单的情况。

DeepSEA则利用了交互式高阶逻辑辅助定理证明工具，从而能够对诸如跨链、投票这样的复杂程序进行灵活的证明。DeepSEA的编译器不仅能生成可执行的字节码，同时还能生成和这些字节码对应的可形式化验证的模型，从而使得这些代码在数学意义上的正确性可以由开发者们用辅助定理证明工具验证。

如果你想了解有关DeepSEA的更多信息，可以查看之前的文章【宅在家里最适合看的编程，C++、Java还是……沈从文？】以及【2020最具“战略性”的编程语言：C语言？还是C# 、 Python 、Swift？】来了解。

通过对DeepSEA的整合，CertiK Chain能够不折不扣地将安全作为第一要务。在使用DeepSEA写智能合约时，部署者（或其他用户）可以基于编译器的输出构造出关于程序正确性的证明，并且将其推送到链上。接下来证明将会得到检验，并被发表，从而完成对于合约的认证。长远而言，用户和合约都可以根据某合约的认证及相关证明信息而决定是否与其进行互动。

DeepSEA编译器有一个经过验证的后端来生成与以太坊虚拟机（EVM）兼容的字节码。而这些字节码和Solidity的二进制应用接口（ABI）也同样兼容。所以任何使用Solidity编写的合约都可以调用使用DeepSEA写的合约，反之亦然。

DeepSEA程序可以被部署到以太坊之上。但由于CertiKChain的虚拟机（CVM）也和EVM兼容，它们也能在CertiK Chain上执行。重要的是，与传统的以太坊合约不同，在CertiK Chain上运行的DeepSEA合约有一些额外的能力：

• CertiK Chain支持记录一个程序是否通过形式化验证满足了特定形式化规范
• 合约在运行时可以查询特定地址上的合约是否满足特定规范

DeepSEA编译器会输出用高阶逻辑表述的代码规范，并且其可以在链上被注册。DeepSEA程序也可以查询特定地址是否被形式化验证过。例如，这将能够让程序只与那些已经证明没有回调（callback-free）的合约交互。

在以上的系统中，每个用户只有两个选项：要么自己检查一遍证明，要么相信一个第三方来检查。然而，这两者都有可能出错，因为这需要非常熟悉证明工具以及相关的库，以确保没有误用任何错误的假设。除此之外，智能合约在运行时仍然无法查询证明。

为了解决这个问题，CertiK Chain将把证明的检验作为链的核心功能之一。一段冗长的证明可以被切分成很多小段，而每一小段证明都会被多个验证节点（verifier node）检查。当所有的验证节点就一段证明的正确性达成了共识，证明所对应的定理将被写入链的下一个区块，记录为已证明。

这意味着CertiK Chain将会建立世界第一个记录已验证声明的共识机制。每当一个新的定理被写入链中，所有人都能精确了解这个定理做出了哪些假设。所有用户都可以在自己的形式化验证的开发中，放心地使用此定理，而智能合约则也可以在运行时随时进行定理的证明查询。

DeepSEA可以直接通过命令行工具CLI部署，也可以通过DeepWallet网页界面来进行。

CLI会调用DeepSEA的编译器，然后获取生成的字节码和二进制应用接口（ABI）。部署一个DeepSEA合约和部署一个Solidity合约一样，他们使用同样的命令，非常简洁：

certikcli tx cvm deploy <ckt><filename>  

开发者们也可以自行编译字节码（以及ABI，如果想要的话），把字节码存到一个文件里，然后使用同上的命令来部署（如果有ABI的话再加上--abi的flag）。使用DeepSEA和Solidity部署的函数都可以被同样的命令调用：

certikcli tx cvm call <address><ckt> <function>

DeepSEA也可以通过DeepWallet部署。DeepWallet是一个允许用户发送、收取、以及质押CTK的安全钱包应用，同时，它还支持使用DeepSEA（以及Solidity）开发、部署、使用安全智能合约于CertiK Chain之上。通过DeepWallet友好的用户界面，用户可以直接与DeepSEA交互。

安全显然是任何区块链系统实现透明及信任的基础。正是因为区块链的安全要求如此之高，这些要求最终只可能被可机器检查的安全数学证明所满足。

DeepSEA的开发工作部分由哥伦比亚-IBM区块链中心和以太坊基金会资金支持。DeepSEA以任何其它语言都无法企及的安全性让我们距离构建安全区块链生态系统的愿景更近了一步。CertiK Chain和DeepSEA的整合让所有的区块链用户都将能在终极的信任和证明的基础之上开发全新的杀手级应用，以天马行空的想象力筑建安全区块链生态的无限可能。

如果想要获得更多讯息请复制后方链接至浏览器或点击文章底部蓝字【阅读原文】访问邮件列表来收取更多细节和未来公告：

https://mailchi.mp/certik/chain-signup

了解更多

General Information: [e-mail]

Audit & Partnerships: [e-mail]

Website: certik.org

Twitter: @certik.org

Telegram: t.me/certik.org

Medium:medium.com/certik

币乎：bihu.com/people/1093109

往期回顾