程序验证方法
https://blog.csdn.net/m0_37714470/article/details/109380215
1）Ad-hoc Testing（随机测试）
随机测试是没有书面测试用例、记录期望结果、检查列表、脚本或指令的测试。主要是根据测试者的经验对软件进行功能和性能抽查。其需要花费的代价低，不过相应的其能提供的可信度也很低。
（2）Concolic Testing（混合测试）& Whitebox Fuzzing（白盒模糊测试）
混合测试是具体的符号执行测试，是具体执行和符号执行相结合，后面可能会单独写一篇文章进行介绍。【先立个flag在这hhhh】
模糊测试是一种通过向目标系统提供非预期的输入并监视异常结果来发现软件漏洞的方法，可分为黑盒模糊测试、白盒模糊测试和灰盒模糊测试，后面可能也有单独写文章介绍模糊测试。【第二个flag】
（3）Symbolic Execution（符号执行）
定义
符号执行 （Symbolic Execution）是一种程序分析技术，它可以通过分析程序来得到让特定代码区域执行的输入。顾名思义，使用符号执行分析一个程序时，该程序会使用符号值作为输入，而非一般执行程序时使用的具体值。在达到目标代码时，分析器可以得到相应的路径约束，然后通过约束求解器来得到可以触发目标代码的具体值。
符号执行的代价高于前两种工具，但相应的可信度也提升了，可以实现全路径覆盖，也能发现一些其他工具发现不了的BUG。
工具举例：KLEE
（4）Extended Static Checking
（5）Static Analysis（静态分析/程序分析）
（6）Verification（验证）
1.2 使用符号执行的原因
1.2.1 黑盒测试的困难性
考虑下方代码什么时候会触发 “DivdieByZero” 异常？
int foo(int x, int y){
if(x32467289)
return x/y;
else
return 0;
}
根据代码可知，当 x 32467289 && y == 0 时，会触发 除零 异常。
当看不到源代码时，如何发现代码中的这一漏洞？
考虑黑盒模糊测试，即随机生成整型的输入值：
Foo(1, 1) √
Foo(1, 0) √
Foo(0, 0) √
……
直到 Foo(32467289, 0) 才会触发这个异常，所以采用模糊测试触发这个异常的概率为：1 / (2^64)
这一结果显示，黑盒测试发现异常非常艰难。
1.2.2 白盒测试的困难性
考虑下方代码，如果我们可以证明：无论怎么给 x、y 赋值，都不会触发 assert(x-y != 0)，那么就可以对代码改写，将该句代码删除掉。
void foo(int a, int b){
int x = 1, y = 0;
if(a != 0){
y = 3+x;
if(b == 0)
x = 2*(a+b);
}
assert(x-y != 0);
}
当采用下方测试用例进行测试时：
输入：a = 0, b =0；输出：x = 1, y = 0；
输入：a = 1, b = 0；输出：x = 2, y = 4；
输入：a = 1, b = 1；输出：x = 1, y = 4；
……
需要有较多测试用例，比较麻烦。
上述结果表明，在没有理论指导进行测试的情况下，白盒测试可能也很难发现代码中的错误。
1.2.3 自动生成测试用例
关键思想：对于给定的程序，是否有一个方法或者工具可以自动生成一组测试用例，要求效率要高，并且测试用例要满足一定的性质。
所以考虑 符号执行（Symbolic Execution）。
2 符号执行原理及理解
2.1 符号执行原理
符号执行是一种程序分析技术，它可以通过分析程序来得到让特定代码区域执行的输入。
当使用符号执行分析一个程序时，该程序会使用符号值作为输入，而非一般执行程序时使用的具体值。
在达到目标代码时，分析器可以得到相应的路径约束，然后通过约束求解器来得到可以触发目标代码的具体值。
2.2 符号执行理解
以下方代码为例：
int foo(int x, int y){
int z = x+y;
if(x==32467289)
return x/y;
else
return 0;
}
1 构造符号值作为函数输入，符号值常用变量名称
此处为：
变量 值
x x
y y
2 使用“符号输入”执行程序，保持符号程序状态
2.1 对于普通语句，直接执行
执行完语句“int z = x + y”后，符号程序状态如下：
变量 值
x x
y y
z x + y
2.2 对于分支语句，向各个分支添加相应的“路径条件”
即：
if (x == 32467289) 路径条件：x == 32467289
return x/y;
else 路径条件：x != 32467289
return 0;
3 根据路径条件和属性，我们可以生成约束
约束为可能触发异常的路径条件和属性。
如上图所示，右分支不可能触发异常；左分支在 y== 0 时会触发除零异常，所以约束为：
x == 32467289 /\ y == 0
即：
if (x == 32467289) 路径条件：x == 32467289
return x/y; y == 0
else 路径条件：x != 32467289
return 0;
4 将生成的约束馈送到某个求解器（例如Z3），以检查可满足性
The model:
[x = 32467289, y==0]
5 验证步骤
将求解器中的模型用作具体输入，看是否会触发异常。
2.3 符号执行架构
上述执行过程如下图所示：
symbolic executor：相当于Z3
path conditions：路径条件
solver：求解器，例如Z3
model：模型 如果是UNSAT，则表明程序中不存在bug；如果是SAT，则需要将其作为具体输入执行程序看是否会触发bug。
3 符号执行实例
符号执行下方程序：
void foo(int a, int b){
int x = 1, y = 0;
if(a != 0){
y = 3+x;
if(b == 0)
x = 2*(a+b);
}
assert(x-y != 0);
}
如果对于所有的 x、y，都不存在 x == y 的情况，则最后一句"assert( x - y != 0) 可以删除，那么我们需要判断的就是 x-y == 0。
所以约束为：路径条件 /\ x - y == 0。
构造符号值：
变量 值
a a
b b
x 1
y 0
对于第一个分支：if( a != 0 )
（1）路径条件：a == 0
变量 值
a a
b b
x 1
y 0
约束为：a == 0 /\ 1 - 0 == 0，显然UNSAT。
（2）路径条件：a != 0
变量 值 语句
a a /
b b /
x 1 /
y 4 y = x + 3
a. 路径条件：b ! = 0
变量 值
a a
b b
x 1
y 4
约束为：a != 0 /\ b != 0 /\ 1 - 4 == 0，显然也是UNSAT。
b. 路径条件：b == 0
变量 值 操作
a a /
b b /
x 2 * (a + b) x = 2 * (a + b)
y 4 /
约束为：a != 0 /\ b == 0 /\ 2 * (a + b) - 4 == 0
将约束馈入Z3，得到 model [ a = 2, b = 0 ]。
将 [ a =2, b = 0 ] 代入源程序，发现确实 x - y == 0。
现代符号执行技术
现代符号执行技术的关键要素之一是它们混合具体(Concrete)执行和符号(Symbolic)执行的能力。
混合执行测试（Concolic testing）
当给定若干个具体的输入时，Concolic testing动态地执行符号执行。Concolic testing会同时维护两个状态：
精确状态(concrete state): maps all variables to their concrete values.
符号状态(symbolic state): only maps variables that have non-concrete values.
不同于传统的符号执行技术，由于Concolic testing需要维护程序执行时的整个精确状态，因此它需要一个精确的初始值。举例说明，还是之前这个例子：对于图1中的示例，concolic执行将生成一些随机输入，比如{ x = 22; y = 7} 并具体和象征性地执行程序。具体执行将在第7行采用“else”分支，符号执行将沿具体执行路径生成路径约束 x0 != 2y0。Concolic测试否定路径约束中的合取并解决x0 = 2y0以获得测试输入{x = 2; y = 1}; 执行采用与前一个不同的路径 - 第7行的“then”分支，现在在此执行中获取第8行的“else”分支。与前面的执行一样，concolic测试也沿着这个具体的执行执行符号执行，并生成路径约束。Concolic测试将生成一个新的测试输入，强制程序以及之前未执行的执行路径。在第三次执行程序之后，concoic测试报告已经探索了程序的所有执行路径并终止了测试输入生成。
执行生成测试（Execution-Generated Testing (EGT)）
由EXE和KLEE工具实施和扩展的EGT方法的工作原理是区分程序的具体和符号状态。EGT在执行每个操作之前，检查每个相关的值是精确的还是已经符号化了的，然后动态地混合精确执行和符号执行。如果所有的相关值都是一个实际的值（即精确的，concrete），那么，直接执行原始程序（即，操作，operation）。否则（至少一个值是符号化的），这个操作将会被符号执行。举例说明，假设之前那个例子，第17行改成y=10。那么，在调用twice时，传入的参数是concrete的，返回的也是一个concrete value，因此z也是一个concrete value。第7、8行中的z和y+10也会被转换成concrete vaule。然后再进行符号执行。
Concoic测试和EGT是现代符号执行技术的两个实例，其主要优势在于它们混合具体和符号执行的能力。 为简单起见，在本文的其余部分，我们将这些技术统称为“动态符号执行”。
动态符号执行中的不精确性(imprecision) vs.完整性(completeness)
不精确性: 代码调用了第三方代码库（由于种种原因无法进行代码插装），假设传入的参数都是concrete value，那么就像EGT中的一样，可以全部当作concrete execution。即使传入的参数中包含符号，动态符号执行还是可以对符号设一个具体的值。Concolic和EGT有不同的解决方法，后面再介绍。除了调用外部代码，对于难以处理的操作数（如浮点型）或是一些复杂的函数（solver无法解决或需要耗费大量时间），使用concrete value可以帮助符号执行环节这种impression。
完备性: 动态符号执行通过concrete value可以简化约束，从而防止符号执行get stuck。但是这也会带来一个新问题，就是由于这种简化，它可能会导致一些不完整性，即有时候无法对所有的execution path都能生成input。但是，当遇到不支持的操作或外部调用时，这显然优于简单地中止执行。
动态符号执行使用具体值简化约束的能力有助于为符号执行卡住的执行路径生成测试输入，但这需要注意：由于简化，它可能会失去完整性，即它们可能无法生成测试 某些执行路径的输入。 例如，在我们的示例中，动态符号执行将无法为路径true，false生成输入。 但是，当遇到不支持的操作或外部调用时，这显然优于简单地中止执行。
主要挑战和解决方案
接下来我们将讨论符号执行中的关键挑战，以及为响应它们而开发的一些有趣的解决方案。
路径爆炸(Path Explosion)
描述:
首先，要知道，符号执行implicitly过滤两种路径：
不依赖于符号输入的路径；
对于当前的路径约束，不可解的路径。
但是，尽管符号执行已经做了这些过滤，路径爆炸依旧是符号执行的最大挑战。
解决方案:
利用启发式搜索搜索最佳路径
目前，主要的启发式搜索主要focus在对语句和分支达到高覆盖率，同时他们也可被用于优化理想的准则。
方法1：利用控制流图来guideexporation。
方法2：interleave 符号执行和随机测试。
方法3（more recently）：符号执行结合演化搜索(evolutionary search)。其中，fitness function用于drive the exploration of the input space。
利用可靠的(sound)程序分析技术来减小路径爆炸的复杂度
方法1：静态地合并路径，然后再feed solver。尽管这个方法在很多场合都有效，但是他把复杂度转移给了solver，从而导致了下一个challenge，即约束求解的复杂度。
方法2： 在后续的计算中，记录并重用low-level function的分析结果。
方法3 ： 自动化剪枝
约束求解(Constraint Solving)
描述:
约束求解是符号执行的技术瓶颈。因此，对于solver的优化（提高solver的求解能力）成了解决这个技术瓶颈的手段。
解决方案:
去除不相关的约束
一般来说，程序分支主要依赖于一小部分的程序变量。也就是说，程序分支依赖于一小部分来自于路径条件(path condition)的约束。因此，一种有效的方法就是去掉那些与当前分支的输出不相关的路径条件。例如，现有路径条件：(x+y>10)(z>0)(y<12)(z-x=0)。假设我们现在想生成满足(x+y>10)(z>0)^¬(y<12)，其中我们想建立对¬(y<12)（与y有关）的feasibility。那么，(z>0)和(z-x=0)这两个约束都可以去掉，因为与y不相关。
递增求解
核心思想就是缓存已经求解过的约束，例如(x+y<10)^(x>5)=>{x=6,y=3}。对于新的约束，首先判断这个新约束的搜索空间是缓存里约束的超集还是子集。如果是新的约束的搜索空间是缓存的约束的子集，那么，就把缓存中的约束去掉多余的条件后继续求解。如果是超集，那么直接把解代入去验证。
内存建模(Memory Modeling)
描述:
程序语句转化成符号约束的精度对符号执行的覆盖率有很大的影响。例如，内存建模是用一个具体的数值去近似一个固定位数的整数变量可能会很有效，但是另一方面，它也会导致imprecision，比如丢失一些符号执行的路径，或探索一些无用的解。另一个例子就是指针，一些工具如DART[3]只能处理精确的指针。
解决方案:
precision和scalability是一个trade-off。需要考虑的因素有：
a) 代码是high level的application code还是low-level的system code。
b) 不同的约束求解器的实际效果。
并发控制(Handling Concurrency)
描述:
大型真实世界的节目通常是并发的。 由于这些程序固有的非确定性(non-deteminism)，测试是非常困难的。 尽管存在这些挑战，但动态符号执行已经有效地用于测试并发程序，包括具有复杂数据输入，分布式系统和GPGPU程序的应用程序。
符号执行工具
动态符号执行已经由学术界和研究实验室的几个工具实现。 这些工具支持多种语言，包括C / C ++，Java和x86指令集，实现几种不同的内存模型，针对不同类型的应用程序，并使用几种不同的约束求解器和理论。
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.
JavaScript
Jalangi2.
SymJS.
Python
PyExZ3 - Symbolic execution of Python functions. A rewrite of the NICE project’s symbolic execution tool.
Ruby
Rubyx - Symbolic execution tool for Ruby on Rails web apps.
Android
SymDroid.
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.
Misc
Symbooglix - Symbolic execution tool for Boogie programs.