Solidity 智能合约安全性相关的资源

OKO: 通过交易 Hash 分析内部调用的网址

🔗 https://oko.palkeo.com/

Oko 是以太坊上专注于智能合约的分析网站，它是用户 etherscan 上智能合约相关信息不够的一个补充。颗粒度非常细。

原理是：获取已验证合约的源代码和 ABI，并使用 Panoramix 对无代码合约进行反编译。它还尝试解释所有对合同的调用的输入数据，以一种可理解的形式显示它。

搜索框。您可以输入：

合约地址 : 查看合同的源代码或反编译，从/到它的调用。
交易哈希 : 查看事务引起的状态修改，以及在此期间进行的调用树。
块号 : 查看关于区块的基本信息，以及其中包含的交易列表。

合约已知漏洞及利用情况

SlowMist
ConsenSys：已知的智能合约攻击 : 针对最重要的合约漏洞提供适合初学者的解释，多数案例提供了代码示例。
SWC 注册表 : 适用于以太坊智能合约的常见缺陷枚举 (CWE) 的精选项目列表。
Rekt : 定期更新的著名加密领域黑客攻击和漏洞利用范例刊物，不提供详细的事后分析报告。

测试工具和库

单元测试工具
- Solid-coverage : 适用于测试智能合约的 Solity 代码覆盖工具。
  - GitHub
- Waffle : 高级智能合约开发和测试框架（基于 ethers.js）。
- Remix 测试 : 用于测试 Solidity 智能合约的工具。在 Remix IDE 的“Solidity Unit Testing”插件下工作，该插件用于编写和运行合约的测试用例。
  - 相关文档
  - GitHub
- OpenZeppelin Test Helpers : 用于以太坊智能合约测试的断言库。确保你的合约按预期运行！
  - GitHub
  - 相关文档
- Truffle 智能合约测试框架 : 自动化测试框架让你的合约测试变得轻而易举。
  - 相关文档
  - 网站
- Brownie 单元测试框架 : Brownie 利用 Pytest，一个功能丰富的测试框架，让你可以编写具有最少代码的小型测试，有效地扩展以用于大型项目，并保持高度可扩展性。
  - 相关文档
  - GitHub
- Foundry 测试 : Foundry 提供了 Forge，这是一个快速灵活的以太坊测试框架，能够执行简单的单元测试、燃料优化检查和合约模糊测试。
  - GitHub
  - 相关文档
- Etheno : 全栈式以太坊测试工具，包括 JSON 远程过程调用多路复用器、分析工具包装器和测试集成工具。 Etheno 消除了在大型多合约项目中设置 Manticore 和 Echidna 等分析工具的复杂性。
  - GitHub
静态分析工具
- Mythril : 以太坊虚拟机字节码评估工具，用于使用污染分析、concolic 分析和控制流检查来检测合约漏洞。
  - GitHub
  - 相关文档
- Slither : 基于 Python 的 Solidity 静态分析框架，用于查找漏洞、增强代码理解以及为智能合约编写自定义分析。
  - GitHub
- Rattle : 以太坊虚拟机字节码静态分析框架，旨在处理已部署的智能合约。
  - GitHub
动态分析工具
- Echidna : 快速合约模糊器，用于通过基于属性的测试来检测智能合约中的漏洞。
  - GitHub
- Harvey : 自动化模糊测试工具，用于检测智能合约代码中的属性违规行为。
  - 网站
- Manticore : 用于分析以太坊虚拟机字节码的动态符号执行框架。
  - GitHub
  - 相关文档
更多测试介绍

形式化验证工具

用于验证智能合约中的函数正确性和检查不变量的工具。

用于制定形式化规范的规范语言
- Act：Act 允许存储更新、前置条件/后置条件、合约不变量的规范。其工具套件也具有证明后端，可通过 Coq、SMT 求解器或 hevm 证明许多属性。
  - GitHub
  - 相关文档
- Scribble : Scribble 把 Scribble 规范语言中的代码注释转换为检查规范的具体断言。
  - 相关文档
- Dafny : Dafny 是一种可直接验证的编程语言，依赖于高层次注释来推理和验证代码的正确性。
  - GitHub
用于检查正确性的程序验证器
- Certora Prover : Certora Prover 是一种检查智能合约代码正确性的自动形式化验证工具。它使用 CVL（Certora 验证语言）编写规范，并组合使用静态分析和约束求解检测属性违反。
  - 网站
  - 相关文档
- Solidity SMTChecker : Solidity 的 SMTChecker 是一个基于 SMT（可满足性模理论）和 Horn 求解的内置模型检查器。它在编译期间确认合约源代码是否符合规范并静态检查是否违反了安全属性。
  - GitHub
- solc-verify : solc-verify 是 Solidity 编译器的扩展版本，它可以使用注释和模块化程序验证对 Solidity 代码执行自动形式化验证。
  - GitHub
- KEVM : KEVM 是以太坊虚拟机 (EVM) 的形式化语义，用 K 框架编写。 KEVM 是可执行的，并且能够使用可达性逻辑证明某些与属性相关的断言。
  - GitHub
  - 相关文档
定理证明的逻辑框架
- Isabelle - Isabelle/HOL 是一个证明助手，允许使用形式化语言表示数学公式并且提供工具来证明这些公式。主要应用于数学证明的形式化，特别是形式化验证，它包括证明计算机硬件和软件的正确性以及证明计算机语言和协议的属性。
  - GitHub
  - 相关文档
- Coq - Coq 是一种交互式定理证明器，让你可以使用定理来定义程序并以交互方式产生经机器检查的正确性证明。
  - GitHub
  - 相关文档
用于检测智能合约中易受攻击模式的基于符号执行的工具
- Manticore : 一种基于符号执行的工具，用于分析以太坊虚拟机的字节码分析工具。
  - GitHub
  - 相关文档
- hevm : hevm 是一种面向以太坊虚拟机字节码的符号执行引擎和等价性检查器。
  - GitHub
- Mythril - 一种符号执行工具，用于检测以太坊智能合约中漏洞
  - GitHub
  - 相关文档
更多测试介绍

智能合约审计服务

为以太坊开发项目提供智能合约审计服务的组织的列表。

漏洞奖励平台

协调漏洞奖励并对发现智能合约中重大漏洞的负责人进行奖励的平台。

监测工具

OpenZeppelin Defender Sentinels : 一种用于自动监测和响应智能合约中事件、函数和交易参数的工具。
Tenderly Real-Time Alerting : 一种在智能合约或钱包发生异常或意外事件时，为你获取实时通知的工具。

合约的安全管理工具

OpenZeppelin Defender Admin : 进行智能合约管理的管理界面，包括控制访问、升级和暂停功能。
Safe : 在以太坊上运行的智能合约钱包，需要最少人数批准交易后交易才能进行 (M-of-N)。
OpenZeppelin Contracts : 用于实现管理功能的合约库，包括管理合约所有权、升级、访问限制、治理、可暂停等功能。

合约安全学习难点

Awesome BlockSec CTF : 精选区块链安全攻防、实战、夺旗竞赛和解决方案的文章列表。
Damn Vulnerable DeFi : 通过实战演练学习去中心化金融智能合约的攻击性安全，并培养漏洞搜查和安全审计方面的技能。
Ethernaut : 基于 Web3 和 Solidity 的实战演练，其中每个等级都是一个需要“攻破”的智能合约。

确保智能合约安全的最佳做法

ConsenSys：以太坊智能合约安全最佳实践 : 保护以太坊智能合约安全的完整指南列表。
Nascent：简单的安全工具箱 : 智能合约开发的实用安全指南和检查清单的集合。
Solidity 模式 : 面向智能合约编程语言 Solidity 的安全模式和最佳实践实用合集。
Solidity 文档：安全性注意事项 : 用 Solidity 编写安全智能合约的准则。
智能合约安全验证标准 : 旨在确立智能合约安全性标准的第十四部分检查清单，面向开发者、架构师、安全审核者和供应商。