Symbolic Execution学习

学习记录
,

0x00: 前言

学习的时候做个记录，看过什么，踩过什么坑之类的。

0x01: 资料

1. paper && 不错的文章

《All You Ever Wanted to Know about Dynamic Taint Analysis and Forward Symbolic Execution (but Might Have Been Afraid to Ask)》

《Symbolic execution for software testing: three decades later》

符号执行入门

2. 项目

KLEE

Z3

Angr

3. 一些资源

3.1 z3

主要是解决一些CTF题目。

  1. Z3一把梭：用约束求解搞定一类CTF题

  2. 使用z3约束器解决CTF中的题目

  3. z3-stuf

3.2 angr

  1. angr-doc

    使用angr解决一些ctf题目，这部分直接参考angr-doc里的examples就好了。

  2. angr-ctf

    很好的入门资料，各种基础用法都有demo，注释很全面，跟着学习就好了。
    环境建议：Linux + virtualenv

  3. 关注各大ctf中wp

4. 实践demo
1. mini mc

This directory contains a “minimal” implementation to demonstrate
the basic ideas of symbolic execution and concolic execution, using
Z3’s Python interface.