espritoxyz/tsa

TSA (TON Symbolic Analyzer) 是一款基于符号执行并专为 [TON blockchain](https://ton.org/) 上的智能合约设计的静态分析工具。 ### 快速开始 要安装 TSA，请遵循[指南](docs/getting-started.md)。 想了解更多关于 TSA 的用例，请阅读[以下文档](docs/modes/use-cases.md)。 使用 TSA 最简单的方法是生成测试。例如，[请参见此处](docs/modes/test-gen-mode.md)。 ### 语言支持 TSA 工作在 TVM 字节码层面，因此可以分析用任何语言编写的智能合约，只需将其编译为 BoC 格式即可。 ### 用途 TSA 的设计目的如下： - 检测潜在的 TVM 运行时错误：查找在处理整数（溢出/下溢、除以零）和切片/构建器（读取或写入错误数量的位、类型不正确等）时可能出现的异常行为。 - 生成回归测试：TSA 能够根据发现的执行路径生成基于 Blueprint 的测试，从而允许修复预期的行为并发现错误的执行。 - 蜜罐检测：TSA 可以检测并报告旨在欺骗用户的恶意合约。 ### 资助 TSA 由 [TON Foundation grant](https://github.com/ton-society/grants-and-bounties/issues/489) 资助，并根据 [8 个月路线图](https://questbook.app/dashboard/?proposalId=667ee6b9b59d3e9ae042d6c9&chainId=10&role=builder&isRenderingProposalBody=true&grantId=65c7836df27e2e1702d2d279) 进行开发。 ### 灵感 TSA 受到 [Universal Symbolic Virtual Machine(USVM)](https://github.com/UnitTestBot/usvm) 的启发并积极使用该技术—— 这是一个支持多种编程语言的符号核心引擎。 USVM 和 TSA 本身也广泛使用了 [KSMT](https://github.com/UnitTestBot/ksmt) 库—— 这是一个用于 SMT 求解器的 Kotlin/Java API，并针对 TON 区块链进行了一些优化。 非常欢迎您为这两个项目做出贡献。 ### 许可证 MIT © Esprito Tech QFZ LLC

标签：Blueprint测试框架, BoC格式, Formal Verification, IPv6支持, JS文件枚举, Kotlin, KSMT, SMT求解器, TON区块链, TVM字节码, USVM, Web3安全, 云安全监控, 密码管理, 形式化验证, 整数溢出, 智能合约, 溢出检测, 符号执行, 自动化测试生成, 蜜罐检测, 误配置预防, 配置审计, 错误检测, 除零错误, 静态分析