作为比特币的一项关键底层技术，近些年区块链成为了非常火爆的概念和趋势，而且构成了目前金融科技领域最核心的技术之一。通过区块链，人们可以不需要借助第三方的信任背书，就能进行点到点的交易、支付等金融活动，实现了在金融行业的广泛应用。但要警惕的是，区块链中一行小的代码错误就可能会导致金融行业的巨大损失，金融领域巨大的经济利益也会吸引大量的黑客攻击，因此，如何保证区块链的安全性问题也变得越来越重要。

《区块链安全性形式化验证研究》正是在此背景下所进行的课题，该课题也是北大-睿智Fintech联合实验室第一期结题项目之一。近日，项目负责人、北京大学数学科学学院信息与计算科学系教授孙猛进行了结题汇报。来自北京大学、睿智合创（北京）科技有限公司（简称“睿智科技”）的各位专家委员会成员参加了评审会议。

项目负责人、北京大学数学科学学院信息与计算科学系教授孙猛

孙猛介绍，以太坊平台有很多深的漏洞，如短地址攻击、拒绝服务攻击等，实际上很多漏洞通过形式化方法都能找出来。“而要保证智能合约的正确性、安全性，就要求我们确保这些漏洞完全被检测。形式化验证（Formal Verification)提供了很好的解决方案。”

图片来源：《区块链安全性形式化验证研究》课题

形式化方法是基于严格数学基础，对计算机系统进行形式规约、开发和验证的技术。形式验证是证明不同形式规约之间的逻辑关系，这些逻辑关系反映了在开发不同阶段产品之间的需要满足的各类正确性需求。

图片来源：《区块链安全性形式化验证研究》课题

“我们这个项目最初的计划是完成三项研究，一是使用WhyML作为中间语言，给出以太坊虚拟机EVM的形式化定义，并实现到OCaml语言上的转换，从而可对以太坊上的智能合约安全性进行形式化验证；二是选取1?2种比较典型的区块链架构，使用定理证明和模型检查技术对区块链上的协议进行形式化描述和验证。”孙猛表示，希望初步形成区块链形式化建模和验证的方法论，为后续进一步研究打下基础。

“目前看，原计划各部分工作均已顺利完成，共发表及录用国际会议论文4篇，并开发了智能合约验证的原型工具，初步形成了相关的方法框架。”孙猛表示。

学术委员会成员、睿智科技CTO苏明富，学术委员会成员、睿智科技模型研发总监刘洋博士分别就“隐私计算”“联邦学习”“数据分层与处理”等问题与孙猛进行了交流。

最后，该项目通过学术委员会的投票，顺利完成结题。

左起：睿智科技CTO苏明富

项目负责人、北京大学数学科学学院信息与计算科学系教授孙猛

睿智科技联席总裁兼CFO黄建

睿智科技模型研发总监刘洋博士

关于北大-睿智Fintech联合实验室

2019年9月，大数据分析与应用技术国家工程实验室与睿智科技联合发起的北大-睿智科技Fintech联合实验室在北京大学静园六院正式成立。该联合实验室将探索产学研结合的新模式，推动大数据和人工智能等前沿技术在金融科技行业中的应用和发展，助力传统金融行业的数字化转型。

联合实验室的课题研发面向北大师生开放申请。同时，北大师生如有金融科技领域的前沿课题，也可以向联合实验室提交单独的申请报告，待学术委员会审核通过后将予以实施并提供经费支持。