据IT外包 www.pc626.com报道:自2014年比特币交易所运营商XX遭攻击破产倒闭以来，至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愿景为在世界范围内实现透明、公平、安全的区块链生态。作为耶鲁大学的终身教授，邵教授在过去二十多年来，致力于利用数学证明的方法开发形式化验证过的软件系统。