DEVCON2：康奈尔大学Phillip Daian论智能合约研究三步走策略

作者：Lydia

Phillip Daian提到康奈尔大学，也是IC3的成员。IC3是一个研究中心。康奈尔大学、康奈尔理工大学等学校组成的联合倡议。智能合约五大挑战表现在扩展性能、正确性、保密性、安全性和合规性。和关键性安全软件进行比较如电网，软件的错位问题会损失资金，让从业人员非常难过。安全性和正确性的关联性更高，攻击者会检测错误。同时有非常独特的监测环境，我们用的还是开放的代码，在飞机上汽车上都能访问。

对此方向的研究，他提出了三步走的策略：

1、工具（形式化验证和分析模式）：最热门的话题。形式化验证用严密的规定低层的东西如EVM，规约非常好，可以更好的解决写正确代码的问题。一个程序的形式化规约可以成为形式化规约，帮助找到错误，生成合约。新加坡大学会采用EVM的语意，以太坊白皮书可以了解。Y3的后端，solidity合约允许取出一些股份，确保合约的余额，也满足了规约。写完整的规约非常困难，总是会错失一些东西。一些性能如激励机制还有一些高级的性能是很难说明的，如果有说明会有一些信任的工具进行证明，任何工具都需要低级的语言审计，系统会和语意一致。还有一些不完整无法决定的结果，因此需要更多工作才能确保完整性。

这些系统可以不需要，认为参与，验证和赏金失败的话需要备用机制让人参与进来。

Marino是一个律师，写了以太坊库，研究以太坊差距。

2、EScape Hatches后的复原：可能被滥用，坏人可以利用这个，这个问题也需要注意。之前会有一些合约提供一些机制转移注意力，所有的钱都被取出来了。一旦出现灾难性的问题，就需要用到备用架构。

3、错误赏金：激励架构如果没有赏金是没用的。破坏的成本是否低于获得的好处，因此必须付出赏金维护体系，不然通过意志维护系统是不够的。

攻击者很困难会在预测市场上有自己的仓位。还有传统的方法解决这个问题。让社区破坏这个合约才能解决这个问题。在学术界我们对于escape有许多解决方法，对于错误赏金方法还有很多方法。如何建立无需信任的赏金和付款，我们也不希望信任合约的作者来付款，如果赏金高攻击者本身也可以报告错误，如何避免这种情况发生。

合约中也有缺陷，不能解决所有问题。建议大家在写高价值合约要考虑所有方面，生态系统会提高最好的工具。错误赏金可以提供一个非常好的检验方法。Phillip Daian表示大家如有问题，可以咨询他们。

作者：Lydia | 来源：Chainb