符号执行 + BMC

概述

什么是符号执行？

符号执行（Symbolic Execution）是一种静态分析技术，用于推导程序在所有可能输入情况下的行为。它是一种自动化的程序分析方法，通过以符号形式代替具体的输入值来执行程序，并跟踪程序中的符号约束，以推导出程序的各种路径、条件和状态。

在符号执行中，程序的输入被表示为符号值，而不是具体的数值。这些符号值可以代表变量、表达式或内存位置等。通过符号执行引擎，程序可以在不实际运行的情况下，通过处理符号值和符号约束来探索不同的路径和可能的行为。

符号执行的主要目标是发现程序中的漏洞、错误、不变量和不一致性。通过执行所有可能的输入路径，符号执行可以发现潜在的错误情况，如空指针解引用、整数溢出、数组越界、死锁等，并生成相应的测试用例或错误报告。

关键思想：不需要具体测例值，用符号沿着程序执行

为什么需要符号执行？

比如检查程序的某些安全属性是否对任何可能的使用场景都成立： 若采用随机生成的测例?——后门可能在特定输入才会被触发，难以随机生成，而符号执行为该问题提供了一个优雅的解决方案，不需要具体的输入，将输入表示为符号来探索所有可能的执行路径，即使用符号而不是实际的值沿着程序执行。具体而言，维护两个公式：

1. Path condition，路径条件——执行到当前分支(路径）需要满足的条件

2. Symbolic Memory，符号内存——变量当前的值

路径条件和符号内存通常都使用一阶逻辑公式来表达，因为使用逻辑符号而不是具体的值来表示，因此被称为符号执行。

• 名词解释:SMT求解器——用于求解一阶逻辑公式是否是可满足的求解器（类似于应用于布尔逻辑的SAT求解器)，全称Satisfiability Modulo Theories Solver

一个小例子

在执行到assert(x-y != 0)时调用smt solver，返回验证结果

动态符号执行

动态符号执行混合了具体执行和符号执行，给定一些具体值（即可以确定下本次执行的path路径），比如通过给的值能确定第一次执行不走入if(z==x)的路径

由于已经走过了不等的路径，于是再求解希望得到一个能走入if语句的值，得到一个x=2,y=1值，根据这个值动态执行会走入一个相等的路径，就会走入第一个if语句

第二次执行的路径条件的第二步再反一下，希望能求解得到进入第二个if语句的路径，于是求解得到一个可能的结果：x=22,y=11，再作为输入，这样会走入第二个if语句，于是之前隐藏的ERROR被触发

动态执行每次concrete值只能选择一条路径，但可以通过不断符号化通过不同的路径条件求解，能不断求解出新的路径初始值，提升路径覆盖率

挑战

1. 语义建模 需要对所有语句编码形式化的语义——编码语句执行为一阶逻辑公式需要仔细考量

   • 对于C语言，怎么编码指针、数组?

   • 对于除0问题,是否可以认为两个语句是一样的?

   • 对于函数int func(int a) return a/a和return 1

   • 语句数目——需要对每条语句逐一编码和测试

2. 约束求解

   现有的SMT求解器能够求解一定规模一阶逻辑公式，但支持的规模还不够大

3. 路径爆炸

   • 嵌套if语句产生的路径是指数增长的

   • 无上界的循环——无限嵌套的if语句，难以使用有限资源探究所有可能

初步解决无界模型的符号执行——> BMC

限界模型检测——Bounded Model Checking

基于循环展开技术将无界模型（程序)转化为有界模型，从而缓解路径爆炸问题

• 例如将循环展开5次——变成5个嵌套if

  

此方法能够保证有限资源下对于无界模型的符号执行成为可能，作为trade-off，该方案不保证限界外模型的安全性，从另一个视角来看，该方案能够给出模型在限界内是安全的保证。

现有的工具：CBMC https://arxiv.org/pdf/2302.02384.pdf 对于C语言进行限界模型检测