Osiris：Hunting for Integer Bugs in Ethereum Smart Contracts

论文题目：（2018-ACSAC）Osiris: Hunting for integer bugs in ethereum smart contracts ——在以太坊智能合约中寻找整数错误

论文引用：Torres C F, Schütte J, State R. Osiris: Hunting for integer bugs in ethereum smart contracts[C]//Proceedings of the 34th Annual Computer Security Applications Conference. 2018: 664-676.

代码开源：https://github.com/christoftorres/Osiris

一、主要内容

本文的研究重点是与整数错误（integer bugs）相关的安全漏洞，这类漏洞是由以太坊虚拟机与Solidity编程语言的一些特性而导致的，所以难以避免。文章针对这类漏洞提出了OSIRIS工具，该工具是一个将符号执行与污点分析相结合的漏洞检测框架，旨在精确地寻找以太坊智能合约中整数错误导致的安全漏洞。

该工具针对EVM字节码自动化检测与整数错误相关的安全漏洞，目前覆盖了三种不同种类的整数错误：

算术错误（arithmetic bugs）
截断错误（truncation bugs）
符号错误（signedness bugs）

分析了495个以太坊代币智能合约并且在一些合约中发现了未知的安全漏洞，同时针对与整数错误相关的安全漏洞提出了对EVM与Solidity编译器的修改防护方案；本文使用OSIRIS工具对截至2018年1月所有已经部署在以太坊区块链中的智能合约进行了自动化检测，发现其中有42,108个智能合约至少存在有一种上述与整数错误相关的安全漏洞；

二、设计实现

2.1 Background

2.1.1 以太坊虚拟机

矿工使用以太坊虚拟机（EVM）执行智能合约，EVM是用于执行EVM字节码的基于栈的虚拟机。

2.1.2 Solidity编程语言

Solidity的语法虽然与C和JavaScript相似，但是Solidity存在一系列专门针对智能合约开发的独有概念。Solidity是静态类型语言，整数分为有符号整数与无符号整数，宽度最低为8bit，最高为256bit。然而在EVM中，所有的整数均以256bit大端补码的形式存放。也就是说，Solidity中的整数类型系统与EVM中的整数类型系统存在不一致，这极有可能导致严重的编码错误。

2.1.3 以太坊智能合约中的整数错误

本文描述了三种类型的整数错误，这些整数错误有可能导致恶意用户窃取以太币或者更改智能合约的执行路径。

算术错误

算术错误包括整数上溢、整数下溢、除数为零和模数为零这四种错误。值得注意的是，EVM与Solidity针对越界行为的处理方式是不完全相同的，而且在EVM和Solidity旧版本（0.4.0之前）除数为零和模数为零只会导致运算结果为0，并不会触发异常。

截断错误

将一个整数类型数据转换为宽度更短的整数类型数据，可能会导致精度的丢失

符号错误

将一个有符号整数类型数据转换为相同宽度的无符号整数类型数据，可能会导致一个负数变为一个很大的整数（反之亦然）。

2.2 METHODOLOGY

2.2.1 类型推断

整数的类型信息，例如宽度和符号，通常只能从智能合约的源代码中直接获得，而不能从字节码中获得。尽管如此，通过分析Solidity编译器在编译过程中引入的代码优化规则，人们依旧能够根据特定代码优化规则从智能合约字节码中间接地推测整数的类型信息。

对于无符号整数，编译器会使用AND操作符屏蔽不在整数宽度范围内的bit，例如编译器会将uint32数据与位掩码0Xffffffff进行AND操作。

对于有符号整数，编译器会使用SIGNEXTEND操作符对数据进行符号扩展，数据的宽度可以根据SIGNEXTEND操作符的第一个参数i的值计算获得，即8 * (i + 1)。

2.2.2 寻找整数错误

算术错误

对于每一条可能导致整数上溢或者整数下溢错误的算术指令，作者检查在当前的路径条件下指令是否有可能违反Table 1中所列举的各条边界检查要求，如果指令可能违反任意一条边界检查要求，则该指令存在算数错误。

截断错误

Solidity分别使用AND和SIGNEXTEND指令截断有符号整数和无符号整数。作者检查每一条AND指令和SIGNEXTEND指令的输入是否大于指令的输出，以判断指令是否存在截断错误。

此外，为了检测并忽略Solidity编译器有意引入的截断，例如address类型数据的转换以及storage中变量的压缩存储，作者还对于检测得到存在截断错误的指令进行了进一步的筛选。

符号错误

作者根据特定指令的符号限制对所有整数类型数据的符号信息进行推断。所有数据的初始标记为”Top“；如果一个数据被当做有符号整数使用过，则将该数据标记为”Signed“；如果一个数据被当做无符号整数使用过，则将该数据标记为”Unsigned“；如果一个数据既被当做有符号整数使用过，又被当做无符号整数使用过，则将该数据标记为”Bottome“，表示该整数类型数据存在符号错误。