智能合约是一种在达成约定条件时自动执行特定行为的计算机程序，在在线交易中被认为比传统合约更安全，但它们并非无误的。宾州州立大学信息科学与技术学院的研究人员作为一个多机构合作项目的一部分，开发了一个全面的基于模型的框架，以替代传统的编程代码，使智能合约的开发、验证和使用更加容易、更加安全。

他们在《IEEE可靠与安全计算交易》上发表了他们的提案。

与大多数软件一样，编写智能合约的代码容易出错和存在漏洞。项目着重解决了涉及验证代码是否按预期执行的重要技术挑战，特别是与其他智能合约互动时。

智能合约存储在类似于存储比特币等虚拟货币的区块链平台上。区块链平台旨在使智能合约（通常处理相当有价值的资产）免受篡改。但是，虽然该平台可以保证智能合约能够正确执行，但它不能验证合约的代码是否正确。

当智能合约的预设条件满足时，特定操作在区块链上执行并更新，以确保交易不可更改。然而，当智能合约的行为与预期不符时，确定问题可能具有挑战性。

对于使用编程语言手动编写的智能合约进行验证是具有挑战性的。软件错误可能直到智能合约部署后才被检测到，在此时可以被利用。

以在线拍卖为例：拍卖代码中写入的要求是，拍卖一旦结束后就不能再进行更多的竞价。然而，在部署后，拍卖允许最高出价者在拍卖结束后被替换。部署后的验证工具可能会确定指令（编程语言）是错误的，但它们不能准确地指示问题出在哪里，程序员需要怎么修复它。

近年来的安全漏洞——攻击者恶意从智能合约中提取资产或完全破坏合约——证明开发人员需要更高效的验证工具来确保智能合约能够满足其要求。

学术界和行业界都有很多针对编程语言和机器代码的验证工具，也有公司可以聘请来执行合约审计。但是这些工具和服务提供的反馈可能是底层的，不一定是有用的。

类似安全漏洞的事件经常利用了多个智能合约之间的交互，但之前关于智能合约验证、漏洞发现和安全开发的研究通常只考虑单个合约。

为了解决这个差距，我们引入了一个我们称之为VeriSolid的框架，用于使用基于抽象状态机的模型对合约进行形式化验证，该模型按照约定方式执行合约。这种方法使开发人员能够在高层抽象上思考和验证一组相互作用合约的行为。

研究人员表示，这个变化始于开发阶段。一个高层抽象模型可以让开发人员以简单、用户友好的方式表达合约的工作方式。

“我们相信，相对于编程语言的代码行，人类更容易使用抽象概念进行工作，”拉斯卡说。“如果验证工具在模型中发现有错误，我们可以提供在更高层次的抽象中识别问题的反馈。”

对于在线拍卖的情况，模型的验证反馈将直接指导开发人员找到问题所在：竞标功能在拍卖结束后仍然可用，导致最高出价者发生变化。

通过我们提出的模型，智能合约可以在部署之前进行验证。此外，工具还可以从模型中生成源代码，以便部署在区块链上，就像开发人员手动编写编程语言一样。

研究人员使用VeriSolid生成Solidity代码——一种用于在区块链平台上实现智能合约的编程语言。

这段代码在功能和行为上与验证的模型相等，使得可以创建正确设计的智能合约。此外，我们还引入了一种名为部署图的图形符号，用于指定合约类型之间的可能互动。