HoRStify：智能合约的可靠安全分析
密码学与安全
2023-02-01 v1
摘要
加密货币以太坊是应用最广泛的智能合约执行平台。智能合约是分布式应用，管理金融资产，因此可实现去中心化交易所或自治组织（DAO）等高级金融工具。其金融属性使智能合约成为极具吸引力的攻击目标，大量针对流行合约的漏洞利用导致数百万美元财务损失便证明了这一点。这种无处不在的攻击风险催生了对可靠静态分析工具的需求，以协助智能合约开发者在部署前消除合约漏洞。对 EVM 合约而言，既可靠又具洞察力的漏洞评估是一项艰巨挑战，因为合约在极大未知且潜在敌意的执行环境中运行低级字节码。迄今为止，尚不存在可证明可靠的自动化分析器能够基于程序依赖验证安全属性，尽管主流攻击类别正属此类。在本工作中，我们提出 HoRStify，首个基于可靠静态分析的以太坊智能合约依赖属性自动化分析器。HoRStify 将其可靠性证明建立于一个静态程序切片的形式化证明框架之上，我们将其实例化到 EVM 字节码语义。我们展示了 HoRStify 足够灵活，可可靠地验证时间戳依赖等著名攻击类别的缺失，同时性能足以分析真实世界智能合约。
引用
@article{arxiv.2301.13769,
title = {HoRStify: Sound Security Analysis of Smart Contracts},
author = {Sebastian Holler and Sebastian Biewer and Clara Schneidewind},
journal= {arXiv preprint arXiv:2301.13769},
year = {2023}
}
备注
Accepted for CSF 2023