符号执行 + BMC
概述
什么是符号执行?
符号执行(Symbolic Execution)是一种静态分析技术,用于推导程序在所有可能输入情况下的行为。它是一种自动化的程序分析方法,通过以符号形式代替具体的输入值来执行程序,并跟踪程序中的符号约束,以推导出程序的各种路径、条件和状态。
在符号执行中,程序的输入被表示为符号值,而不是具体的数值。这些符号值可以代表变量、表达式或内存位置等。通过符号执行引擎,程序可以在不实际运行的情况下,通过处理符号值和符号约束来探索不同的路径和可能的行为。
符号执行的主要目标是发现程序中的漏洞、错误、不变量和不一致性。通过执行所有可能的输入路径,符号执行可以发现潜在的错误情况,如空指针解引用、整数溢出、数组越界、死锁等,并生成相应的测试用例或错误报告。
关键思想:不需要具体测例值,用符号沿着程序执行
为什么需要符号执行?
比如检查程序的某些安全属性是否对任何可能的使用场景都成立: 若采用随机生成的测例?——后门可能在特定输入才会被触发,难以随机生成,而符号执行为该问题提供了一个优雅的解决方案,不需要具体的输入,将输入表示为符号来探索所有可能的执行路径,即使用符号而不是实际的值沿着程序执行。具体而言,维护两个公式:
Path condition,路径条件——执行到当前分支(路径)需要满足的条件
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值只能选择一条路径,但可以通过不断符号化通过不同的路径条件求解,能不断求解出新的路径初始值,提升路径覆盖率
挑战
语义建模 需要对所有语句编码形式化的语义——编码语句执行为一阶逻辑公式需要仔细考量
对于C语言,怎么编码指针、数组?
对于除0问题,是否可以认为两个语句是一样的?
对于函数int func(int a) return a/a和return 1
语句数目——需要对每条语句逐一编码和测试
约束求解
现有的SMT求解器能够求解一定规模一阶逻辑公式,但支持的规模还不够大
路径爆炸
嵌套if语句产生的路径是指数增长的
无上界的循环——无限嵌套的if语句,难以使用有限资源探究所有可能
初步解决无界模型的符号执行——> BMC
限界模型检测——Bounded Model Checking
基于循环展开技术将无界模型(程序)转化为有界模型,从而缓解路径爆炸问题
例如将循环展开5次——变成5个嵌套if
此方法能够保证有限资源下对于无界模型的符号执行成为可能,作为trade-off,该方案不保证限界外模型的安全性,从另一个视角来看,该方案能够给出模型在限界内是安全的保证。
现有的工具:CBMC https://arxiv.org/pdf/2302.02384.pdf 对于C语言进行限界模型检测