ksluckow/awesome-symbolic-execution

# Awesome Symbolic Execution [](https://github.com/sindresorhus/awesome) ## 目录 * [论文](#papers) * [课程](#courses) * [视频](#videos) * [工具](#tools) ## 论文 * [符号执行与程序测试](https://doi.org/10.1145/360248.360252), James C. King. * [一个生成测试数据并符号执行程序的系统](https://doi.org/10.1109/TSE.1976.233817), L. A. Clarke. * [关于动态污点分析与前向符号执行你想知道的一切（但可能不敢问）](https://doi.org/10.1109/SP.2010.26), Edward J. Schwartz, Thanassis Avgerinos, David Brumley. * [软件测试中的符号执行：三十年后](https://dl.acm.org/doi/10.1145/2408776.2408795), Cristian Cadar and Koushik Sen * [符号执行技术综述](https://arxiv.org/pdf/1610.00502.pdf), Roberto Baldoni, Emilio Coppa, Daniele Cono D’Elia, Camil Demetrescu, and Irene Finocchi. * ***符号执行论文合集：** [XMUsuny/symbolic-execution-papers](https://github.com/XMUsuny/symbolic-execution-papers)* ## 课程 * [哈佛大学符号执行课程](http://www.seas.harvard.edu/courses/cs252/2011sp/slides/Lec13-SymExec.pdf)。 * [爱荷华州立大学符号执行课程](http://web.cs.iastate.edu/~weile/cs641/9.SymbolicExecution.pdf)。 * [马里兰大学符号执行课程](https://www.cs.umd.edu/class/spring2013/cmsc631/lectures/symbolic-exec.pdf)。 ## 视频 * [MIT 符号执行课程](https://www.youtube.com/watch?v=mffhPgsl8Ws)。 * [符号执行课程（Coursera 软件安全课程的一部分）](https://www.coursera.org/learn/software-security/lecture/agCNF/introducing-symbolic-execution)。 * 斯图加特大学 Michael Pradel 教授的程序分析课程 * [符号与混合测试（第 1 部分，符号）](https://youtu.be/wOO5jpoFIss) * [符号与混合测试（第 2 部分，挑战）](https://youtu.be/K_Q32ar1g6g) * [符号与混合测试（第 3 部分，混合）](https://youtu.be/TlEjgqSXYNE) * [符号与混合测试（第 4 部分，应用）](https://youtu.be/WSL0Oac2VNc) ## 工具 ### Rust * [Owi](https://github.com/OCamlPro/owi) - 基于 WebAssembly (Wasm) 构建的并行（动态）符号执行引擎，可以运行 Rust 代码。 ### Java * [Symbolic PathFinder (SPF)](https://github.com/SymbolicPathFinder/jpf-symbc) - 基于 [Java PathFinder](https://github.com/javapathfinder) 构建的符号执行工具。支持多种约束求解器、惰性初始化等。 * [JDart](https://github.com/psycopaths/jdart) - 基于 [Java PathFinder](https://github.com/javapathfinder) 构建的动态符号执行工具。使用 [JConstraints](https://github.com/psycopaths/jconstraints) 支持多种约束求解器。 * [CATG](https://github.com/ksen007/janala2) - 使用 [ASM](http://asm.ow2.org/) 进行插桩的混合执行工具。使用 CVC4。 * [LimeTB](http://www.tcs.hut.fi/Software/lime/) - 使用 [Soot](https://github.com/soot-oss/soot) 进行插桩的混合执行工具。支持 [Yices](http://yices.csl.sri.com/) 和 [Boolector](http://fmv.jku.at/boolector/)。支持分布式混合执行。 * [Acteve](https://code.google.com/archive/p/acteve/) - 使用 [Soot](https://github.com/soot-oss/soot) 进行插桩的混合执行工具。最初用于 Android 分析。支持 [Z3](https://github.com/Z3Prover/z3)。 * [jCUTE](http://osl.cs.illinois.edu/software/jcute/) - 使用 [Soot](https://github.com/soot-oss/soot) 进行插桩的混合执行工具。支持 [lp_solve](http://lpsolve.sourceforge.net/)。 * [JFuzz](http://people.csail.mit.edu/akiezun/jfuzz/) - 基于 [Java PathFinder](https://github.com/javapathfinder) 构建的混合执行工具。 * [JBSE](http://pietrobraione.github.io/jbse/) - 使用自定义 JVM 的符号执行工具。支持 CVC3, CVC4, Sicstus 和 Z3。 * [Key](https://www.key-project.org/) - 定理证明器，使用 Java 建模语言 (JML) 编写的规范。 * [SWAT](https://github.com/SWAT-project/SWAT) - 松耦合动态符号执行工具，使用 [ASM](https://asm.ow2.io) 进行插桩，使用 [JavaSMT](https://github.com/sosy-lab/java-smt) 生成公式，目前使用 [Z3](https://github.com/Z3Prover/z3) 作为求解器。 ### LLVM * [KLEE](http://klee.github.io/) - 基于 LLVM 构建的符号执行引擎。 * [Cloud9](https://dslab.epfl.ch/research/cloud9) - 基于 KLEE 构建的并行符号执行引擎。 * [Kite](http://www.cs.ubc.ca/labs/isd/Projects/Kite/) - 基于 KLEE 和 LLVM。 * [SymCC](https://github.com/eurecom-s3/symcc) - 一个编译器包装器，在编译期间将符号执行嵌入到程序中，以及相关的运行时支持库。 * [GenSym](https://github.com/Generative-Program-Analysis/GenSym) - 用于基于并行 fork 的符号执行的编译器。 * [Owi](https://github.com/OCamlPro/owi) - 基于 WebAssembly (Wasm) 构建的并行（动态）符号执行引擎，可以运行 LLVM 代码。 ### .NET * [PEX](http://pex4fun.com/About.aspx) - .NET 的动态符号执行工具。 * [VSharp](https://github.com/VSharp-team/VSharp) - .NET 程序集的符号执行引擎。 ### C * [CREST](https://github.com/jburnim/crest) - 是一个用于 C 程序混合测试的开源工具。 * [Otter](https://bitbucket.org/khooyp/otter/) - 是一个纯源码级的 C 语言符号执行器，可用于测试程序。 * [CIVL](http://vsl.cis.udel.edu/civl/) - 一个包含 CIVL-C 编程语言、模型检查器和符号执行工具的框架。 * [Owi](https://github.com/OCamlPro/owi) - 基于 WebAssembly (Wasm) 构建的并行（动态）符号执行引擎，可以运行 C 代码。 ### JavaScript * [Jalangi2](https://github.com/Samsung/jalangi2) - JavaScript 动态分析框架。 * [SymJS](https://doi.org/10.1145/2635868.2635913) - JavaScript Web 应用程序的自动符号测试。 ### Python * [CrossHair](https://github.com/pschanely/CrossHair) - 用于验证 Python 函数属性的符号执行工具。 * [PyExZ3](https://github.com/thomasjball/PyExZ3) - Python 函数的符号执行。[NICE](https://code.google.com/archive/p/nice-of) 项目符号执行工具的重写版。 * [APEX](https://github.com/allexdav2/apex) - 支持覆盖率引导测试生成的 Python 混合执行引擎。使用 Rust 构建。 ### Ruby * [Rubyx](https://www.cs.umd.edu/~avik/papers/ssarorwa.pdf) - Ruby on Rails Web 应用的符号执行工具。 ### Android * [SymDroid](http://www.cs.umd.edu/~jfoster/papers/cs-tr-5022.pdf) - 用于识别 Android 应用程序中活动权限的符号执行器。 ### 二进制 * [Mayhem](http://dx.doi.org/10.1109/SP.2012.31)。 * [SAGE](https://patricegodefroid.github.io/public_psfiles/ndss2008.pdf) - 针对 X86 Windows 应用程序的白盒文件模糊测试工具。 * [DART](https://doi.org/10.1145/1064978.1065036) - 是第一个结合动态测试生成的混合测试工具。 * [BitBlaze](http://bitblaze.cs.berkeley.edu/) - 用于计算机安全的二进制分析。 * [PathGrind](https://github.com/codelion/pathgrind) - 针对 32 位程序的基于路径的动态分析。 * [FuzzBALL](http://bitblaze.cs.berkeley.edu/fuzzball.html) - 基于 BitBlaze Vine 组件构建的符号执行工具。 * [S2E](http://s2e.systems/) - 支持 x86, x86-64 或 ARM 软件栈的符号执行平台。 * [miasm](https://github.com/cea-sec/miasm) - 逆向工程框架。包含符号执行。 * [pysymemu](https://github.com/feliam/pysymemu/) - 支持 x86/x64 二进制文件。 * [BAP](https://github.com/BinaryAnalysisPlatform/bap) - 二进制分析平台，提供编写程序分析工具的框架。 * [angr](http://angr.io/) - 用于分析二进制文件的 Python 框架。包含符号执行工具。 * [Triton](https://triton.quarkslab.com/) - 动态二进制分析平台，包含动态符号执行工具。 * [manticore](https://github.com/trailofbits/manticore) - 用于二进制文件（x86, x86_64 和 ARMV7）和 Ethereum 智能合约字节码的符号执行工具。 * [MAAT](https://github.com/trailofbits/maat) - 低级符号执行工具，使用 Ghidra 的 p-code。 * [BinCAT](https://github.com/airbus-seclab/bincat) - 二进制代码静态分析器，集成 IDA。执行值和污点分析、类型重构、释放后使用和双重释放检测。 * [Sydr-Fuzz](https://sydr-fuzz.github.io/) - 面向安全开发生命周期的持续混合模糊测试与动态分析。 * [SymEx-VP](https://github.com/agra-uni-bremen/symex-vp) - 针对带有精确 SystemC 外设模型的 RISC-V 嵌入式固件的符号执行。 * [Owi](https://github.com/OCamlPro/owi) - 基于 WebAssembly (Wasm) 构建的并行符号执行引擎。 ### 其他 * [Symbooglix](https://github.com/symbooglix/symbooglix) - Boogie 程序的符号执行工具。 * [OSS-Sydr-Fuzz](https://github.com/ispras/oss-sydr-fuzz) - 针对开源软件的混合模糊测试

标签：AI工具, Fuzzing, pocsuite3, SMT求解器, TruffleHog, 二进制安全, 云安全监控, 云资产清单, 可配置连接, 学术论文, 形式化验证, 程序分析, 符号执行, 约束求解, 课程资源, 路径遍历, 软件测试, 逆向工程, 防御加固, 静态分析