首届国际理论计算机联合大会（International Joint Conference on Theoretical Computer Science，IJTCS）于2020年8月17日-22日在线上举行，主题为“理论计算机科学领域的最新进展与焦点问题”，由北京大学与中国工业与应用数学学会（CSIAM）、中国计算机学会（CCF）、国际计算机学会中国委员会（ACM China Council）联合主办，北京大学前沿计算研究中心承办。  

 

　　8月20-22日，大会“区块链技术”分论坛如期举行，纽约州立大学石溪分校陈婧助理教授主持。小编为大家带来论坛精彩回顾。

 

Formal Design, Implementation and Verification of Blockchain Languages
Grigore Rosu, University of Illinois at Urbana-Champaign

 

　　随着区块链编程语言和虚拟机的快速发展，对于这些语言和虚拟机的形式化分析和验证工具也需要尽快提出。这篇报告提出了基于重写的可执行语义框架 K，该框架可以使用配置、计算和规则来定义编程语言、类型系统和形式分析工具，以对区块链语言进行自动化形式设计和验证。将给定的某种语言的形式语义作为输入，K 框架可以生成各种形式的执行和分析工具，包括解释器、编译器、符号执行等。

 

　　K 框架可使用的语言不仅包括 C、Java、JavaScript 等主流语言，也包括 Solidity、EVM 等区块链编程语言和虚拟机，这些新兴语言每隔一段时间就会定期修改，因此语义框架似乎是最有效的形式验证工具。作者认为在区块链领域，这样独立于语言/范式，并且实现自动化验证的语义框架将获得极大发展。

 

Can a Blockchain Keep a Secret
Shai Halevi, Algorand Foundation

 

　　作者提供了一个用区块链系统实现可信秘密共享技术的方案。秘密共享是分布式计算中的重要技术之一，其思想是将秘密以适当的形式拆分并给予不同的参与者管理，仅当若干个参与者一同协作时才能恢复这条秘密消息。该论文实现了在 PoS 区块链，不超过1/4坏结点的动态敌手模型下的高效可扩展秘密共享方案。在此方案下，秘密将随机的共享到一个小的匿名委员会中，并保证该秘密只会在满足条件时释放。

 

　　在技术层面上，该方案巧妙地解决了秘密共享问题中可扩展性与动态敌手模型二者间的矛盾，即可扩展性要求共享秘密的参与者不能过多，但动态敌手模型又可以主动的去腐化参与者的问题。在该方案中，作者首先使用了密码学自选举的方式保证了每轮参与者的保密性。其次，为了解决不同轮之间参与者进行秘密传输的问题，作者引入了名为目标匿名通道的新工具，在其中信息发送者将无法得知信息接收者的身份。在区块链系统中，作者在每轮中引用了一个新的提名委员会去实现目标匿名通道的功能。由此，每轮秘密共享的参与者均为完全匿名的，巧妙地在实现可扩展性的同时保证了秘密共享的安全性。

 

基于区块链的社区医疗管控系统
欧嵬，中国工业与应用数学学会区块链专业委员会

 

　　至2018年底，我国已建成全球规模最大的法定传染病疫情和突发公共卫生事件网络直报系统，但仍有诸多问题；2020年初爆发的疫情，对公共卫生服务提出了更高的要求。本次报告旨在利用区块链技术对社区医疗进行管理与管控，对实现智慧化社区公共卫生管理体系提出了新构想。利用基于 Fabric 技术框架搭建的联盟链，通过层级的职能划分，实现数据的实时采集、交互与智能结构化，将医疗账本实时同步至疾控部门，以便迅速发现、控制病情，实现对确诊患者的信息的网络报告与随访管理。通过国密算法有效保护患者的数据隐私安全。

 

　　该基于区块链的平台将政府、医疗卫生机构、居民等多方用户需求考虑在内，完善了传统医疗平台的功能，提高了医疗平台的可扩展性、可维护性，提高了系统与用户隐私的安全性。在实验和功能测试中表现良好。最后，报告对未来区块链技术在医疗系统的应用作出展望。

 

Correctness Conditions for Cross-Chain Deals
Maurice Herlihy, Brown University

 

　　在现代分布式数据管理系统中，一个分布式交易通常被认为需要拥有原子性、一致性、独立性以及持续性的特点。其中，原子性是指交易的中间步骤将全部发生或全部不发生，一致性要求货币数量均衡，独立性指两笔交易的处理应互相独立，而持续性要求交易一经完成就应不能再更改。然而，在区块链跨链环境中，随着参与者可能产生各种偏离协议的攻击行为，分布式跨链交易的性质需要进行重新定义。

 

　　本文作者考虑了在多条区块链交互的新环境下，跨链交易应当拥有哪些新的性质。相比于传统的分布式环境，多条区块链的环境没有任何公共可信结点，其网络结构也更加复杂。作者主要考虑了在协议受到攻击时参与者可能存在的几种状态，并利用博弈论的思想，将整个交易行为看作各节点之间的博弈。之后，作者从博弈策略入手，重新解释并拓展了跨链交易中原子性、一致性、独立性和持续性的定义。最后，作者说明了在网络强连接可以使协议做到强纳什均衡，同时还强调了智能合约资产锁定在跨链交易中的重要性。

 

Security Analysis Techniques for Blockchain Smart Contracts
陈钟，北京大学

 

　　智能合约是运行在区块链系统中的应用程序，拥有着公开透明以及任何人可验证的特点，是区块链发展中最重要的技术之一。然而，随着智能合约在区块链中的广泛应用，逐渐有黑客开始利用代码漏洞恶意攻击智能合约，并造成了重大的财产损失。因此，如何检测智能合约的安全性，修补智能合约的安全漏洞以防止其被恶意攻击成为了目前智能合约发展的一大难题。

 

　　为了解决这一难题，讲者设计出了三种发现智能合约安全漏洞的技术，可以满足漏洞检测、漏洞预测和漏洞搜索这三种不同场景的应用需求。同时，讲者汇总了智能合约执行异常的分类和发生机理，并对大规模真实交易数据进行了实证研究，总结出了运行期异常的特征和主要原因，并由此提出了针对智能合约运行期异常的诊断技术。最后，讲者还设计并实现了S-Secure智能合约安全分析工具集，并使用真实的智能合约数据验证了该工具的有效性。

 

NC-Max: Breaking the Throughput Limit of Nakamoto Consensus
张韧，秘猿科技

 

　　在区块链共识技术的发展中，中本聪共识（Nakamoto Consensus）作为首次在比特币中实现的共识协议，对整个加密货币的发展具有着重要意义。所谓中本聪共识是比特币最原始的共识协议，其中包含比特币的挖矿方式，主链确认方式等多个部分。然而，中本聪共识协议在安全性和效率上进行了权衡，因此其虽然保证了安全性和良好的激励机制，却同时因为低效性导致比特币功能极大受限。为了解决这一问题，近年来人们提出了各种共识协议，希望能够在不降低安全性的同时提高共识协议的执行效率。

 

　　在本篇论文中，作者将中本聪共识进行改进，提出了拥有更高吞吐量且能够充分利用带宽的 NC-Max 协议。在技术层面上，NC-Max 协议将一笔交易的确认和同步过程分离开来，从而消除了对于块大小的限制。其次，在此协议中还使用了更加精确的挖矿难度调整机制，通过用无效区块验证出块速度，实现更灵敏地根据网络状况调节吞吐量。作者证明了改进后的协议相比于原始的中本聪共识协议能够更有效的防止自私挖矿攻击（Selfish Mining）。同时作者还通过实验证实了新协议的吞吐量相比于原始协议有显著提高，并且有效降低了无效区块的数量。

 

An Overview of Recursive Proofs
Alessandro Chiesa, University of California, Berkeley

 

　　随着区块链技术的发展，为了进一步高效地实现区块链系统中的隐私性和可证明性，近年来零知识证明方案，非交互式证明等技术正逐渐走进人们的视野。本次演讲者主要介绍的便是其中的递归证明方案技术，该技术在近两年来有多项优质论文发表，被认为是证明方案在区块链应用上最合适的方法之一。与传统的证明方案中证明者需要在交互协议中向验证者证明完整的计算过程不同，递归证明方案可以使证明者每次交互只证明部分计算执行的正确性，之后再利用多轮的方式实现完整证明，因此非常适用于应用在区块链系统之上。

 

　　讲者首先介绍了简洁的非交互式论证系统（SNARGs），能够非交互式的为一个复杂计算的正确性提供一个比原计算量小得多的证明，使验证者所需的计算量大大降低。其次，讲者讲述了如何从简洁的非交互式论证系统构造出递归证明方案的增量可验证计算性，即怎样通过先前的有效证明来继续生成新的步骤证明。最后，讲者在说明递归证明方案的普适性和有效性的同时，还强调了其在实际应用中非常复杂和昂贵，如何构造更简单实用的递归证明系统也是目前亟待解决的问题。

 

A Mechanism Designer's View of Cryptocurrencies
Matt Weinberg, Princeton University

 

　　本次报告主要介绍了讲者基于自身的研究领域，对加密货币的看法。他通过一个从实际问题中抽象出来的数学模型，简单地介绍了数字货币的原理，讲者认为在这些假设下的结果对于实际问题是很有价值的参考。

 

　　首先，讲者介绍了自私挖矿攻击（Selfish Mining），这里提到了 Eyal 和 Sirer 提出的定理：当个人的计算能力大于总计算能力的1/3，且其他人选择最长的链协议时，个人选择最长的链协议并不是最优的。进而可以通过定理得到一些额外的结论。相对应的是另一个定理：当计算力大约小于30%时，选择最长链协议是最优的。Weinberg 教授提出基于当前现实情况，自私挖矿攻击并未在比特币中发现，但是这并不代表以后也不会发生。

 

　　其次介绍的是交易费用问题（transaction fees）。当前交易费用是非常低的，几乎为0，而且是不稳定的；相对于交易费用，区块奖励正以每四年减半的速率衰减，最终也会趋于0。当矿工只能依靠交易手续费时，他们的收入就变得不稳定，此时矿工就可能会从富裕的块中窃取交易费用。从这个角度看，矿工最终会依赖交易费用作为收入，并且随着区块奖励的逐渐减少，自私挖矿攻击现象也会加剧。因此为了区块链的安全性与稳定性，保持交易费用的上涨与稳定是一个重要的话题。

 

　　最后，讲者对权益证明（Proof-of-stake）进行了介绍。他比较详细地解释与证明了前面的结论。

 

　　由于时间原因，讲者只提出了三条最终结论：一是激励很重要。激励机制最好用简单、易于操作的模型来分析；二是可以以自私挖掘攻击为视角分析最长链变化，三是激励权力下放（incentivizing decentralization）是一个很艰难的过程。

 

Direct Evidence of Bitcoin Wash Trading
李家荪，George Mason University

 

　　迄今为止，对于加密货币存在清洗交易，只有一些文献中有间接推论，但是作者对此提供了直接证据。作者使用黑客从比特币交易所泄露的数据，发现所有交易中有2%至33%的交易是清洗交易。清洗交易是一种市场操纵手段，交易者可以自己“制作”交易。作者还研究了清洗交易的特点：虽然并不会对比特币价格产生重大影响，但是会增加交易费，增加交易所的收入。同时，通过增加表面交易量，交易所可以增强对客户的吸引力。

 

　　作者还从之前暴露的清洗交易的交易执行者和交易所内部人士的参与中找到了一致的证据，并且进一步使用直接证据来评估文献中提出的间接推理技术。

 

分布式密钥技术在区块链中的基础性作用
高承实，中国工业与应用数学学会区块链专业委员会

 

　　非对称密码技术是构建区块链应用的基石，其在区块链交易过程中的用户标识、操作校验、验证资产所有权都起到重要作用。然而，传统的非对称密码技术无法有效实现对分布式和去中心化系统的支持，这主要是因为在区块链系统中，没有任何一个公共可信的节点可以实现密钥创建和分发工作。为了解决这一问题，讲者介绍了分布式密钥技术，并从工业界的角度对该技术在区块链中的应用进行了详细的阐述。

 

　　所谓分布式密钥技术，即使用安全多方计算将原来中心化的非对称密码技术变为分布式实现，其相比于传统的多签名技术或秘密分享技术拥有着诸多优势。首先，相比于多签名技术，分布式密钥技术可以使不同签名者拥有对资产的不同权限，能够为区块链系统监管提供底层的技术支持。而相对于秘密分享技术，分布式密钥技术不仅不需要先生成一个完整私钥再进行拆分，还可以实现更加丰富的业务逻辑，能够在区块链底层就实现对用户业务角色的定义和区分。总而言之，采用分布式密钥技术能够在区块链系统中进行有效监管的同时保证用户隐私，并且支持更丰富的业务逻辑实现。