拿到binary时的步骤:
- file
- strings
- ltrace/strace
- gdb/OD
- IDA
- …
angr
符号执行
符号执行 (Symbolic Execution)是一种程序分析技术。其可以通过分析程序来得到让特定代码区域执行的输入。使用符号执行分析一个程序时,该程序会使用符号值作为输入,而非一般执行程序时使用的具体值。在达到目标代码时,分析器可以得到相应的路径约束,然后通过约束求解器来得到可以触发目标代码的具体值。
符号模拟技术(symbolic simulation)则把类似的思想用于硬件分析。符号计算(Symbolic computation)则用于数学表达式分析。
angr简介
angr是一个多架构的二进制分析平台,具备对二进制文件的动态符号执行能力和多种静态分析能力。
angr的简要过程:
- 将二进制程序载入angr分析系统
- 将二进制程序转换成中间件语言(intermediate representation, IR)
- 将IR语言转换成语义较强的表达形式,比如,这个程序做了什么,而不是它是什么。
- 执行进一步的分析,比如,完整的或者部分的静态分析(依赖关系分析,程序分块)、程序空间的符号执行探索(挖掘溢出漏洞)、一些对于上面方式的结合。
1 | # 不需要命令行参数的情况 |
z3
Z3 is a theorem prover from Microsoft Research
Z3 is a Satisfaiability Modulo Thories(SMT) solver
z3 Types
- BitVec:指特定大小的数据类型
- BitVec(“x”,32)对应c语言中的int
- BitVec(“x”,8)对应c语言中的char
- Int(整型)
- Real(实数)
- Bool(布尔值)
- Array
- ……
Tips
- z3中没有signed/unsigned类型
- 使用<,<=,>=,/,/%,>>操作signed类型变量
- 使用ULT,ULE,UGT,UGE,UDIV,Uremand,LShR操作unsigned类型变量
- 将BitVec的大小设成运算过程中最大的
模板
1 | from z3 import * |
例子:
1 | // Soup Meat Tea (SMT) (TM) |
z3求解:
1 | from z3 import * |
You are welcome to share this blog, so that more people can participate in it. If the images used in the blog infringe your copyright, please contact the author to delete them.