自2014年比特币交易所运营商MT.Gox遭黑客攻击破产倒闭以来，至2018年1月日本另一家数字资产交易所CoinCheck价值约5.3亿美元资产失窃；从2016年The DAO因代码漏洞致五千万美元以太币失窃，到2017年11月Parity过亿美元以太币被冻结，在迅猛的发展势头下，日益壮大的数字资产市场一直摆脱不了安全事故频发的阴影，安全问题成为了区块链这一新兴技术寻求突破、实现大规模落地最为主要的阻碍之一，业内正集体呼唤着，解决这一痛点的可靠技术方案出现。
在上世纪九十年代概念被首次提出后，由于缺乏可信执行环境，智能合约这一概念一直被看作是空中楼阁的设想。直到支持图灵完备的脚本语言的以太坊的诞生，支持可编程合约的数字系统和区块链技术的发明让尼克·萨博的这一技术设想真正落地。但由于智能合约代码编写难度极高，编译器缺少代码库和漏洞导致的系统崩溃等技术问题随着区块链发展历程的推进被不断放大，对于提升智能合约安全性的各种方案的探讨也逐渐成为了业内探讨的技术热点。
早在2016年以太坊开发者大会（Devcon2）上，形式化验证就成为了社区的热门话题。但用数学算法验证软件程序，在确保不同的网络元件接受指令并以用户的身份模拟执行预定程序的过程中，本身就有着需要人工输入等技术限制，如何运用各种工具包来整合形式化验证，存在着诸多制约。
由耶鲁大学计算机科学系教授邵中（详见雷锋网(公众号：雷锋网)此前报道：《最牛华人“程序员”邵中，全世界程序员的命运都可能因他而变》）及其弟子、哥伦比亚大学计算机系助理教授顾荣辉带领的形式化验证智能合约项目CertiK，在耶鲁大学数十年的研究成果的基础上，致力于为现有所有的区块链应用提供最先进的安全性服务（官网：certik.org）。
在以往，基于区块链去中心化的思想和技术特性，智能合约一旦提交至链上，合约的源代码无法再被更改。正因为这一点，当黑客发现并利用其存在的漏洞来窃取资金时，唯一制止这种不法行为的方法只有硬分叉（hard forking）：将链强行分叉，并且使之前所有的交易信息作废，还需所有社区里的用户升级其本地的区块链。以太坊（ETH）和以太坊经典（ETC）即为一个最具说服力的前车之鉴，其通过硬分叉追讨回失窃资金后使得社区内部分裂，遭致违背去中心化的技术信仰的声讨，爆发的争执蔓延至今，仍影响着社区的稳定和发展。
面对这样巨大的安全风险和不确定性，区块链上的财富似乎可以被轻易攫取，也能被轻易掠夺。对此，顾荣辉教授表示，“区块链建立于信任之上，但是它却并不安全，它的代码实现和所有的复杂系统一样，都可能存在漏洞。甚至区块链因为其去中心化的特性，在其上编写代码极易发生错误，却很难更正代码漏洞。”
从这一现实痛点出发，邵教授认为区块链安全性问题亟需得到解决，在他看来，一旦所有的区块链的代码在上链前全部被形式化的数学证明验证后，开发者和用户们就无须再为区块链上的系统遭受黑客攻击而担心，区块链的安全性问题能够真正得到解决。
2018年3月7日，耶鲁大学在其官网上发表新闻称，Certik项目的顺利实施，对区块链的安全问题提供了可靠的保障，使其在迈向落地应用的过程中大大提高了可行性。文章提到，CertiK提供的首创性的安全服务，能够帮助区块链上的每笔交易避免程序错误（bug-free），并且无法被黑客所攻破（hack-resistent）从而造成用户的资金损失，而这将会改变整个区块链行业的规则和未来走向。
据透露，CertiK目前的首要目标是实现比特币、以太币等数字货币交易的完全安全性；而在远期的宏大目标上，CertiK愿景为在世界范围内实现透明、公平、安全的区块链生态。作为耶鲁大学的终身教授，邵中教授在过去二十多年来，致力于利用数学证明的方法开发形式化验证过的软件系统。
雷锋网此前曾报道，这位计算机程序语言设计的权威专家已经研发了经形式化验证过的无漏洞、无法被黑客攻破的操作系统：CertiKOS，而CertiK正是CertiKOS研究的一个延伸，利用数学证明的形式化验证方法开发完全可信经过验证的智能合约与区块链生态体系。
顾荣辉教授：CertiK构建安全性编程社区打人类知识数据库
而CertiK在大大提高各种丰富多样的区块链应用的可行性、改善区块链应用生态的同时，目光也放得更为长远，不仅仅将自己定位为一个提升区块链交易安全性的科技初创公司，更是一个致力于建设安全性编程社区的基金会，如顾教授所言，这其实是在建立一个经过形式化验证的人类知识数据库。
具体来看，是如何一步步构建这个如此宏大的数据库？顾教授透露，基金会将首先会为社区的开发者们提供大量的形式化验证的教程。他表示，CertiK的验证过程体现了化整为零的解题思想，将一个难以证明的大问题拆分为许多容易证明的小问题，然后再将证明过的小问题重新组合回分解之前的较难的大问题，并且保证其中从端到端的正确性（end-to-end guarantees）。
在这个过程中，前述所有的这些小问题都将发送给整个社区，社区的开发者们可以利用CertiK提供的方法，也可以运用自己的算法来证明这些问题。一旦某个问题通过多方独立的开发者的验证，那么其便可以用来作为建立其他理论的依据，从而形成互助协作的技术机制和良好的社区氛围。
可编程化区块链塑造理想世界:商业业务迁移上链杜绝人为错误
展望未来，邵教授认为：“可编程化的区块链拥有超越互联网的潜力”，他为我们勾画了这样一个理想世界：在这个世界里，包括保险、银行、法律、会计等在内的越来越多重要的服务，都将会移植到不用担心人为错误的网络世界，人们将在区块链上完成各项商业活动。“
他特别强调：
“在未来，或许虚拟世界将会扮演比现实世界更为重要的角色。“
而在丹华资本董事总经理Judy Yan看来，一旦安全性问题被解决，将没有任何东西能够阻碍区块链的扩张。作为CertiK的早期投资者，其表示：“比特币仅为一条区块链，还有其他更多的公链和私链。目前有很多金融机构和相关团体都想打造自己的区块链，但无论如何，他们都需要解决区块链的安全性问题。“
来自学界同行的评测同样对CertiK寄予了厚望。斯坦福大学物理系的JG Jackson and CJ Wood教授张首晟表示：“CertiK 是第一批提出利用数学证明的形式化验证方法来检查工程系统和智能合约安全性的团队。这将是区块链技术领域、甚至是科学领域的一大跨越式进步。”
一直以来，耶鲁大学合作研究办公室（Yale Office of Cooperative Research,OCR）都与邵教授和顾教授有着紧密的合作，来寻求研究成果的商业化之路。OCR的高级业务发展经理Richard Anderson称：“目前的区块链技术社区，极其容易受到黑客的攻击，但是耶鲁的这项技术将会改变世界。”
。
原创文章，作者：ItWorker，如若转载，请注明出处：https://blog.ytso.com/80803.html