论文标题
智能合约控制流的反应性合成
Reactive Synthesis of Smart Contract Control Flows
论文作者
论文摘要
智能合约是小但容易出错的计划，可以在多方之间实施协议。我们提出了一种自动构建智能合约状态机器的反应性综合方法。为此，我们将时间流逻辑（TSL）扩展到无限域上具有普遍量化的参数。参数化的TSL是指定时间控制流的方便逻辑，即正确的交易顺序以及合同字段的数据流。我们开发了一种两步方法，即1）合成 - 一般而言 - 无限状态系统的有限表示，以及2）将系统拆分为紧凑的层次结构，以实现状态机的实现。我们在原型工具scsynt中实现了该方法，该方法在几秒钟内自动构造实现指定控制流的固体代码。
Smart contracts are small but highly error-prone programs that implement agreements between multiple parties. We present a reactive synthesis approach for the automatic construction of smart contract state machines. Towards this end, we extend temporal stream logic (TSL) with universally quantified parameters over infinite domains. Parameterized TSL is a convenient logic to specify the temporal control flow, i.e., the correct order of transactions, as well as the data flow of the contract's fields. We develop a two-step approach that 1) synthesizes a finite representation of the - in general - infinite-state system and 2) splits the system into a compact hierarchical architecture that enables the implementation of the state machine in Solidity. We implement the approach in our prototype tool SCSynt, which - within seconds - automatically constructs Solidity code that realizes the specified control flow.
