符号执行
2021-10-07 20:36:56 1 举报AI智能生成
符号执行概述
作者其他创作
大纲/内容
Example
S，语句，包括赋值，顺序，分支，循环
，符号存储，保存符号状态
π，路径约束，true or false
span class=\"equation-text\" contenteditable=\"false\" data-index=\"0\" data-equation=\
Symbolic choice
Symbolic iteration
Symbolic Execution
1. 处理：程序应能在不超过给定资源的情况下进行任意长时间的工作。由于庞大数量的控制流路径，内存消耗是特别关键的问题。
2. 避免重复工作：不应该重复执行工作，避免为分析可能有共同前置的不同路径，从一开始就多次重启一个程序。
3. 分析结果重用：以前运行的分析结果应该尽可能地重复使用。特别是，应避免调用消耗很大的SMT求解器来求解之前解决过的路径约束。
符号执行的设计原则
DFS:占用内存更小，受到包含循环和递归调用的路径的阻碍
BFS:占用内存更大，能快速的遍历早期行为，需要更长时间完成特定路径的探索
最大覆盖率；
最短距离：与程序中特定点的距离；
buggy-path优先策略；
loop exhaustion策略：探索访问循环的路径，很多溢出；
Fitness function：衡量探索路径到达目标测试覆盖的距离，优先考虑可能更接近特定分支的路径。例如目标分支|a-c|==0，路径的接近度被定义为|a-c|，越小越接近。----适应度函数类似于优化策略；
启发式探索
路径选择
IRs实现解释器比直接为机器代码实现符号解释器容易得多。
解释IR比相应二进制执行速度慢。
基于IR的符号执行
执行未修改的机器代码。
一般机器指令较多，没有基于IR的符号执行实现简单。
无IR的符号执行
符号执行实现的两种方案
将所有变量映射到实际值
实际状态
只映射那些有非实际值的变量
符号化状态
Concolic 执行
符号执行过程会占用较多资源，在线符号执行可能会降低目标程序的性能。
通常程序在执行过程中会存在并发情况及一些不确定事件，这可能会给在线符号执行带来一些不可预料的问题。
如果目标程序中采用了代码混淆、加壳等保护技术，混合符号执行很可能无法正常运行。
在线符号执行
离线符号执行
Java：Symbolic Path Finder
Prefix
angr 工具
KLEE
SAGE
工具
JDart - Dynamic symbolic execution tool built on Java PathFinder. Supports multiple constraint solvers using JConstraints.
CATG - Concolic execution tool that uses ASM for instrumentation. Uses CVC4.
LimeTB - Concolic execution tool that uses Soot for instrumentation. Supports Yices and Boolector. Concolic execution can be distributed.
Acteve - Concolic execution tool that uses Soot for instrumentation. Originally for Android analysis. Supports Z3.
jCUTE - Concolic execution tool that uses Soot for instrumentation. Supports lp_solve.
JFuzz - Concolic execution tool built on Java PathFinder.
Key - Theorem Prover that uses specifications written in Java Modeling Language (JML).
Java
KLEE - Symbolic execution engine built on LLVM.
Cloud9 - Parallel symbolic execution engine built on KLEE.
Kite - Based on KLEE and LLVM.
LLVM
PEX - Dynamic symbolic execution tool for .NET.
.net
CREST.
Otter.
C
Jalangi2.
SymJS.
Java script
Mayhem.
SAGE - Whitebox file fuzzing tool for X86 Windows applications.
DART.
BitBlaze.
PathGrind - Path-based dynamic analysis for 32-bit programs.
FuzzBALL - Symbolic execution tool built on the BitBlaze Vine component.
miasm - Reverse engineering framework. Includes symbolic execution.
pysymemu - Supports x86/x64 binaries.
BAP - Binary Analysis Platform provides a framework for writing program analysis tools.
angr - Python framework for analyzing binaries. Includes a symbolic execution tool.
Triton - Dynamic binary analysis platform that includes a dynamic symbolic execution tool.
Binaries
symbolic execution tools
符号执行
0 条评论
回复 删除
下一页
