标签：Short 字节 验证 Contracts Solidity send Paper 合约 EVM

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.利用符号执行来进行验证

未来方向：

标签：Short,字节,验证,Contracts,Solidity,send,Paper,合约,EVM
来源： https://blog.csdn.net/qq_42932021/article/details/118726360

本站声明： 1. iCode9 技术分享网（下文简称本站）提供的所有内容，仅供技术学习、探讨和分享；
2. 关于本站的所有留言、评论、转载及引用，纯属内容发起人的个人观点，与本站观点和立场无关；
3. 关于本站的所有言论和文字，纯属内容发起人的个人观点，与本站观点和立场无关；
4. 本站文章均是网友提供，不完全保证技术分享内容的完整性、准确性、时效性、风险性和版权归属；如您发现该文章侵犯了您的权益，可联系我们第一时间进行删除；
5. 本站为非盈利性的个人网站，所有内容不会用来进行牟利，也不会利用任何形式的广告来间接获益，纯粹是为了广大技术爱好者提供技术内容和技术思想的分享性交流网站。