金融科技公开课回顾 北大教授孙猛讲授《区块链形式化验证8月27日晚，由北京大学大数据分析与应用技术国家工程实验室和睿智合创（北京）科技有限公司（简称“睿智科技”）联合举办的金融科技公益公开课第三期线上开课。北京大学数学科学学院信息与计算科学系教授、博士生导师孙猛为大家带来了《区块链形式化验证》课程，受到了广大网友的热烈欢迎。课程在直播平台小鹅通及北大校友平台i1898同步直播，在线观看人数共计上万人次。

　　该系列公开课于5月7日面向全网免费开课，首期课程为睿智科技首席战略官、摩根大通银行原董事总经理、美国运通公司原首席信贷官林晴带来的《美国金融危机背景下的中国启示录》。第二期课程为北京大学数字金融研究中心副主任，北京大学国家发展研究院副教授、博士生导师，斯坦福大学经济学博士黄卓带来的《金融科技时代的中国财富管理》。

　　“很多人以为比特币跟区块链两者就是一个东西，实际上比特币只是第一个成功的区块链应用。你可以把区块链理解成智能手机，那么比特币只是手机上一个做的非常好的App。”孙猛表示，区块链是一种分布式账本技术，通过共识机制发动节点共同记账，为了防止共识信息被篡改，通常采用链式数据结构，使用密码学技术进行数据存储。

　　众所周知，信用是所有金融活动的根基。传统金融行业里的所有机构（包括金融机构、金融科技公司、监管机构、中介机构等）的所有金融活动都是为了解决信任问题。在孙猛看来，区块链最大的创新是第一次用技术解决了人类的共识问题，把密码学、分布式系统、博弈论、P2P协议等诸多技术有机组合到一块，通过理性的技术为人类建立信任提供了方法，为我们提供了一个很好的解决信任问题的途径，也构成了目前金融科技领域最核心的技术之一。

　　“通过区块链，人们可以不需要借助第三方的信任背书完美世界官网首页csgo，就能进行点到点的交易、支付等金融活动，区块链在金融行业已经得到了非常广泛的应用。”孙猛表示，但另一方面，一行小的代码错误或可能导致巨大损失，此外金融领域巨大的经济利益也吸引着大量黑客攻击。“如何保证区块链的安全性问题也变得越来越重要。”

　　“区块链技术目前也面临着一些挑战，主要包括可扩展性、安全性、隐私保护和监管等等问题。”孙猛认为，“形式化验证技术对于保障复杂的区块链系统的安全性、可信性至关重要。为了应对这方面的挑战，我们已经做了一些工作，当然距离真正应用还有一定的距离。”

　　“我们前两天刚刚过了七夕节，有一句非常应景的诗来形容这个情况，就是‘金风玉露一相逢，便胜却人间无数’。当区块链和形式化技术两者碰到一块，得到的结果绝对是1+1远远大于2的。”孙猛对此很有信心。

　　孙猛介绍道，目前市场上做区块链形式化验证的项目相对较少，已知的项目有UIUC的Grigore Rosu教授团队提供智能合约形式化验证的平台——Runtime Verification；耶鲁大学的邵中教授和哥伦比亚大学顾荣辉教授创立的Certik验证框架；成都链安科技的Verification as a Service（VaaS）是一个同时支持EOS和以太坊区块链的形式化验证平台。

　　“这些大部分还处于早期阶段，在区块链验证里头还有很多可以做的工作。”孙猛表示，他的团队目前在做的工作，主要的想法是把形式化验证和测试结合起来，用在安全的以太坊虚拟机实现的开发上，并且可以在字节码的层次上对智能合约进行验证。

　　“我们的定义包括类型、指令和解释器定义。”孙猛介绍道，“然后可以对经过验证的EVM进行部署。我们定义一系列的driver来从WhyML程序中抽取Ocaml程序，抽取之后，EVM的OCaml实现被封装成一个静态库，可以被Rust中的虚拟机调用。在我们的框架里，Rust和Why3可以进行交互，经过验证的模型可以直接在production environment中执行，并且可以被进一步测试。”

　　孙猛团队还在做一些区块链形式化验证的工作，包括对块同步协议、共识协议的形式化建模、以及对相关的性质在模型检查工具UPPAAL里面做的形式化验证。

　　在课程的后一阶段，孙猛就网友关心的几个问题进行了回复。这些问题有：为什么形式化验证对金融领域特别重要？现在在区块链验证方面也已经有一些相关的工具和平台，你们的工作和他们相比有什么优点或者不同之处？现在的人工智能、大数据、深度学习等技术对区块链的安全性保障方面有没有什么帮助？

　　孙猛，北京大学数学科学学院信息与计算科学系教授、博士生导师，曾任联合国大学国际软件技术研究所客座研究员，荷兰数学与计算机科学研究中心研究员，主要研究领域为软件理论和形式化方法。

　　近年来的工作主要包括：协调模型和语言，余代数理论及其应用，形式化建模，软件验证与测试，信息物理融合系统，面向服务与云计算，区块链智能合约的建模与验证，大数据分析，机器学习与深度学习的理论基础及相关技术在形式化验证中的应用。

　　北大-睿智金融科技公益公开课系列课程由北京大学大数据分析与应用技术国家工程实验室和睿智合创（北京）科技有限公司（简称“睿智科技”）联合举办。

　　北京大学大数据分析与应用技术国家工程实验室由国家发展和改革委员会批复组建，整合了数学科学学院、信息科学学院和前沿交叉学院大数据科学中心的优势研究力量和学科资源，是承担原创大数据理论和技术的应用开发和成果转化的创新平台，致力于面向企业一线技术需求的数学基础研究与工程应用交叉融合发展以及大数据和人工智能学科的人才培养。

　　睿智科技是一家以“打破金融信息非对称”为使命，为广大金融机构提供大数据洞察力系列产品、一站式科技赋能、智能导流三大核心业务的智能金融科技企业。睿智科技依托大数据洞察力和人工智能技术，致力于成为连接亿万消费者的金融需求与千百家金融机构信贷供给的智能金融枢纽，为促进中国金融繁荣与普惠做出贡献。返回搜狐，查看更多