Formal Verification of Smart Contracts: Short Paper

ABSTRACT

提出将使用F*框架用于编写代码

1. INTRODUCTION

本文目的：通过静态分析方式查找漏洞

字节码(Byte-code)是一种包含执行程序，由一序列 op 代码/数据对组成的二进制文件，是一种中间码。

将智能合约的验证分为双端方式：（基于语言的方式来证明）

1.直接对Solidity编程语言转换成F*语言 *

Solidity*
Runtime error就是在运行期间出现的错误,运行时错误不同于炸弹或系统垮掉,运行时错误一般不影响操作系统运行*.）时的安全性

2.将EVM字节码部分转换成F*语言

EVM* 将EVM字节码反编译为F*语言。
允许我们分析低级别的属性，例如完成呼叫或交易所需的气体量上限

文章目的：

未来验证可靠性编译器的正确性

2. FROM SOLIDITY TO F*

提供的方式：

提出工具将Solidity转换为F* 语言，并提供了嵌入式F*的自动分析样本

研究中不包含循环语句

2.1具体的转换

合约转换为F模块——类型声明转换——合同属性打包成状态记录——合同方法转换成F?* 的功能——判断分支是返回还是抛出——赋值的转换——内置的方法调用被库调用替换

2.2检验易受攻击的模式

Solidity程序的缺陷：

其他运行时错误（如气体耗尽或调用堆栈溢出）都会触发异常。但在使用send函数时send and its variants are not guaranteed to succeed (send returns a bool).

3.字节码反编译码为F*

EVM*?作为EVM字节码的反编译器，用于分析Solidity源代码不可用的合约，并用于检验合约的低级属性

反编译器基于符号执行进行堆栈分析，以识别程序中的跳转目的地，并检测堆栈不足和溢出

4.结论

利用F* 来验证智能合约：

1.可以灵活捕捉并验证合同的程序的相关属性

2.便于利用其他静态工具进行验证

3.利用符号执行来进行验证

未来方向：