符号执行
2021-10-07 20:36:56 1 举报AI智能生成
符号执行概述
作者其他创作
大纲/内容
Example
Symbolic Execution
S，语句，包括赋值，顺序，分支，循环
，符号存储，保存符号状态
π，路径约束，true or false
Symbolic choice
Symbolic iteration
符号执行的设计原则
1. 处理：程序应能在不超过给定资源的情况下进行任意长时间的工作。由于庞大数量的控制流路径，内存消耗是特别关键的问题。
2. 避免重复工作：不应该重复执行工作，避免为分析可能有共同前置的不同路径，从一开始就多次重启一个程序。
3. 分析结果重用：以前运行的分析结果应该尽可能地重复使用。特别是，应避免调用消耗很大的SMT求解器来求解之前解决过的路径约束。
路径选择
DFS:占用内存更小，受到包含循环和递归调用的路径的阻碍
BFS:占用内存更大，能快速的遍历早期行为，需要更长时间完成特定路径的探索
启发式探索
最大覆盖率；
最短距离：与程序中特定点的距离；
buggy-path优先策略；
loop exhaustion策略：探索访问循环的路径，很多溢出；
Fitness function：衡量探索路径到达目标测试覆盖的距离，优先考虑可能更接近特定分支的路径。例如目标分支|a-c|==0，路径的接近度被定义为|a-c|，越小越接近。----适应度函数类似于优化策略；
符号执行实现的两种方案
基于IR的符号执行
IRs实现解释器比直接为机器代码实现符号解释器容易得多。
解释IR比相应二进制执行速度慢。
无IR的符号执行
执行未修改的机器代码。
一般机器指令较多，没有基于IR的符号执行实现简单。
Concolic 执行
实际状态
将所有变量映射到实际值
符号化状态
只映射那些有非实际值的变量
在线符号执行
符号执行过程会占用较多资源，在线符号执行可能会降低目标程序的性能。
通常程序在执行过程中会存在并发情况及一些不确定事件，这可能会给在线符号执行带来一些不可预料的问题。
如果目标程序中采用了代码混淆、加壳等保护技术，混合符号执行很可能无法正常运行。
离线符号执行
工具
Java：Symbolic Path Finder
Prefix
angr 工具
KLEE
SAGE
symbolic execution tools
Java
JPF-Symbc - Symbolic execution tool built on Java PathFinder. Supports multiple constraint solvers, lazy initialization, etc.
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.
JBSE - Symbolic execution tool that uses a custom JVM. Supports CVC3, CVC4, Sicstus, and Z3.
Key - Theorem Prover that uses specifications written in Java Modeling Language (JML).
LLVM
KLEE - Symbolic execution engine built on LLVM.
Cloud9 - Parallel symbolic execution engine built on KLEE.
Kite - Based on KLEE and LLVM.
.net
PEX - Dynamic symbolic execution tool for .NET.
C
CREST.
Otter.
CIVL - A framework that includes the CIVL-C programming language, a model checker and a symbolic execution tool
Java script
Jalangi2.
SymJS.
Binaries
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.
S2E - Symbolic execution platform supporting x86, x86-64, or ARM software stacks.
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.
manticore - Symbolic execution tool for binaries (x86, x86_64 and ARMV7) and Ethereum smart contract bytecode.
0 条评论
下一页
