文章

OKTC & CertiK Chain 生态合作规划方案

欧易

发布于 2020年6月02日

更新于 2024年4月25日

关于CertiK

CertiK是业内领先的区块链安全公司，总部位于纽约，由耶鲁大学和哥伦比亚大学的顶级形式验证专家，携数十年科研成果共同创立，是最早进入区块链安全领域的公司之一。团队技术实力雄厚，曾完成了世界上第一款防黑客操作系统内核，并将核心技术成功应用于区块链安全领域。与传统的安全检测方法不同，CertiK尝试在数学层面上证明区块链生态系统与智能合约具有抗黑客能力并且安全无漏洞。目前，CertiK的主要业务包括智能合约的形式化验证、渗透测试及公链安全定制等服务。

CertiK由Binance Labs、DHVC、FBG、光速中国、经纬中国、比特大陆、策源创投等全球领先的投资者共同孵化投资，已与Binance、Kucoin、欧易和Huobi等世界顶级数字资产交易所，以及NEO、ICON、Terra和QuarkChain等公链建立了战略合作伙伴关系。截至目前，CertiK已经累计保护了超过60亿美元的资产免受损失。CertiK已经对BNB, Terra, Crypto.com，TUSD和USDK等多个主要项目进行了安全审计。未来，CertiK将继续保护区块链安全。

合作方案

CertiK Chain和 OKTC拥有相通的设计理念和开发计划，可以更好地激发未来的协同效应。CertiK Chain会在以下独特的几个方面为 OKTC 生态联盟增加价值，实现CertiK Chain和OKTC的跨链合作。

一、用CVM为 OKTC 赋能

与 OKTC 类似，CertiK是基于Tendermint-BFT开发共识，愿景是通过CertiK独有的虚拟机和DeepSEA编程语言构建一个无边界的跨链生态。

CertiK虚拟机（CVM）是个由CertiK Chain开发的智能合约平台。在1.0版本中，它主要实现的场景是在添加了安全相关的扩展功能以外提供完整的EVM兼容性。将来的版本将会提供WASM和综合的代码支持，CVM可以被搭载在Cosmos核心模块上，被 OKTC 所直接使用。

虽然CVM支持经诸如Solidity等经典编程语言，这些语言却无法为形式化验证提供理想的支持。因此，我们会通过CVM将DeepSEA语言指向 OKTC 。

二、用DeepSEA为 OKTC 赋能

因其资金相关性，分布式金融应用有着严格的安全要求，不同开发者写出的智能合约的交互行为往往非常精细而微妙，这其中可能就会产生漏洞。目前，大多数现有的形式化验证解决方案只能分开证明某一个合约的性质，这样的证明过程（例如：通过给每一个这个合约里的函数注明运行前后的规范）是一个“链下”的过程，没有传统软件开发环境中即时的权限控制或者检测反馈。另一方面，这些证明工具经常带有被假设可信任的代码，而这些假代码有可能存在漏洞。 OKTC 的愿景是想要构建无边界的公链生态、并且拥有流畅的数据、资产以及价值流通，然而现有的安全等级无法给予有效保障。

DeepSEA编程语言的目标是使用Coq定理证明助手去从头到尾的验证合约的正确性。DeepSEA系统语言的组成部分有：一个新的编程语言，一个已被验证的编译器，和一个能将合约代码翻译成可被Coq证明助手加载的形式化模型的编译机制

CertiK正在开发一个经验证的编译器，该编译器可以将DeepSEA语言翻译成字节码。由于编译器本身已经通过了Coq辅助证明工具的验证，该编译器不存在任何可能破坏合约安全属性的漏洞。换句话来说，用户不仅可以在源代码层面证明程序的安全性，并且这个安全性和用户直接使用字节码的形式化规范进行推理得出的安全保障一样严格可靠。并且，由于验证证明不会有大量控制流或者数据表示的问题，整个证明过程将会变得更为便捷。而编译器通过了安全验证这一事实也意味着所有通过编译的程序都满足某些运行时安全性质，并且这些性质是可验证的，比如：类型安全、没有整数溢出，等等。

DeepSEA是一个模块化的系统，因此DeepSEA变成语言可以被编译到不同的目标架构中，并且经过验证的编译器后端可以被不同的前端语言重复使用。在未来，团队可以将这些后端重新用于领域特定语言（DSL）上（例如特别用于开发金融合约的语言），而这些DSL都可以拥有和其他语言相同的正确保障。

DeepSEA编译器会将合约翻译到一个可被加载到辅助证明工具中的库中，在那里将会执行对于高级的正确属性的证明。能够使用功能完整的交互式证明助手意味着用户可以定义任意复杂定理的陈述和模型，并且不会被证明工具本身的限制所影响。举个例子，当证明一个金融程序的时候，用户可以写出一些博弈论的定义（就像数学书里面一样）并证明预期协议确实是一个占优策略。

另外一个例子也能够证明辅助证明助手的功能非常强大：跨链应用。跨链应用包含了很多存在于不同的链上的并且进行异步通信的智能合约上。这是另外一个DeepSEA能够为 OKTC 生态赋能的好方式。在这个环境下，DeepSEA工具可以针对每个单独合约自动输出一个经过验证的模型，然后开发人员可以使用辅助证明助手去定义该智能合约怎样与别的合约进行交互，改对延迟进行怎样的假设等等。DeepSEA可以被编译到不同的链上运行，比如说CertiK Chain， OKTC ，Ethereum，这也同样可以为用户写一套标准的用于桥接的合约提供帮助，然后在一个单独的DeepSEA开发中将它们全部验证，为跨链交流提供坚实基础。

DeepSEA 论文发表于程序语言顶级会议 OOPSLA’19 ，DeepSEA语言白皮书 0.9版与编译器预览版也已公开发布。

三、用区块浏览器为 OKTC 赋能

CertiK区块浏览器是一个CertiK Chain的网络前端，极大程度地被链的用户所依赖，用以追踪他们的交易记录以及探索整个区块链平台的信息。在诸如BTC, ETH, BCH等传统区块链中，区块浏览器仅仅为他们自身的链而工作。举个例子：一个用户永远不能使用一个ETH区块浏览器浏览比特币的信息。

基于相同的愿景——创建无边界的区块链生态和更加高效和透明的资产、数据和价值流转， OKTC 和CertiK Chain正在设计高协同程度的集成和同步，包括他们的链前端和顶端的去中心化应用。CertiK团队目前正在开发CertiK区块链对 OKTC 的兼容支持，从一个安全增强的角度，为 OKTC 提供数据交叉检验，和数据验证等功能。带有多种区块浏览器选择的 OKTC 会使得未来的用户在链上活动中具备更加多权限和易用性。

四、用DeepWallet为 OKTC 赋能

DeepWallet是一个易用性极高的去中心化网络钱包应用，能够让多种数字资产在基于Cosmos的不同区块链上进行交互。DeepWallet为用户提供以下几种主要功能支持：

在基于Cosmos的协议中拥有易用的多资产管理；
交易和链上活动的历史记录追踪；
更方便快捷地发送和接收数字资产；
在钱包中可进行质押，让用户能够通过质押支持的POS通证得到奖励；
基于浏览器的Solidity & DeepSEA语言编译功能、部署智能合约，以及合约交互；

五、用NoOps为 OKTC 赋能

NoOps是CertiK团队设计及开发的“架构及服务”平台，用企业级别的基础架构运行区块链节点。使用NoOps的区块链用户可以节约下巨大的管理运营成本并关注更多在自身的商业实现。CertiK团队正在装载一批知名区块链协议的架构搭建和配置，用以促进相关的生态发展。

NoOps平台会为 OKTC 提供集成服务，让用户能够便捷地使用以下功能：

如果用户参与了OKTC的质押，则可以在NoOps平台上主办他们自身的运营节点；
通过CertiK主办的节点查询OKTC的数据，获取有价值的信息；
CertiK团队深度理解链上数据对于去中心化交易所的重要性。基于团队对区块链和智能合约监控系统的专业知识，团队相信NoOps平台能够提供便捷、安全以及稳定的OKTC数据访问；

功能重点：

1.符合用户需求的基础架构

可扩展的基础架构栈根据客户需求打造，并且一如既往地保持着行业标准。这些架构栈通过云服务提供方和本地数据中心进行部署和运维，致力于为用户传递最好的服务，无论身在何方。

2. 防患于未然的安全等级

NoOps的系统部件在构建时就充分考虑了物理和逻辑的包围隔离等措施，防止潜在的黑客攻击。CertiK团队是用户基础架构的守护者，让用户能够成为自身财产的托管方。在这样的环境下，用户的资产安全也就得到了绝对的保障。

3. 供数据情况的监控

每一个节点群会拥有单独的监控，用以收集数据记录和系统日志，频度大约为1秒。实时分析和报告会基于共识和机器等级传递到用户，用以提供更好的运营能见度和洞察能力。

4. 从市场角度完善用户节点

NoOps团队的线上市场列出了范围宽广的一批领先的区块链协议，让用户可以从持续的更新中自由选择，并支持最新发行的协议。任何增添的功能和测试网配置也能够被方便地使用，可以保证便捷的延展功能。