没有合适的资源?快使用搜索试试~ 我知道了~
理论计算机科学电子笔记267(2010)17-27www.elsevier.com/locate/entcs使用SAT的Edd Barrett1,2和Andy King3肯特大学计算机学院英格兰摘要符号决策树并不是唯一的方法来关联标记和数值变量之间的关系。布尔公式也可以表示这样的关系,其中整数变量用命题变量的位向量建模。布尔公式可以被组合以表达块和程序状态,但它们很难处理,因此需要计算它们的抽象。本文展示了如何增量SAT可以适用于派生范围和设置抽象的位向量,都受到布尔公式的约束。保留字:抽象域,数值域,值域,满意度求解。1介绍虽然抽象解释的基本思想在三十多年前就已经形成[5],但抽象解释直到最近才进入工业化阶段[6]。这一新阶段的特点不仅是更加注重工具和系统构建,而且还包括设计和实现新的抽象领域。例如,用于提高可伸缩性的域即弱关系域类[15,19],以及更好地匹配真实程序结构的域,即将状态标记和数值变量之间的关系关联起来的符号决策树[1]。这篇文章的重点是将状态标记与范围和集合的数字抽象联系起来。Blanchet等人 [1]用下面给出的伪代码1作者要感谢Thomas Schilling对SAT求解的评论,Ralph Corderoy对CNFconnversion的支持,JüorgBrauer对最小化位向量的讨论,MartinEllis的代码审查和Stephen Fendyke分享他的插值软件知识。我们也感谢匿名评论者的评论。2电子邮件:e. kent.ac.uk3电子邮件:a.m. kent.ac.uk1571-0661 © 2010 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi:10.1016/j.entcs.2010.09.00318E. 巴雷特,A.King/Electronic Notes in Theoretical Computer Science 267(2010)17(X=0);if(!B)Y:=1/X;这个代码是正确的,在这个意义上,它不给除以零错误,如果X = 0,但是为了推导出这一点,有必要跟踪B和X之间的关系。提交人指出:“为了精确地处理这些例子,我们实现了一个简单的关系域,它包含一个决策树和一个算术抽象域。通过对布尔变量进行排序和对子树进行机会共享来简化决策树。这种方法的唯一问题是,决策树的大小可以是布尔变量数量的指数,并且代码包含数千个全局变量在二进制逆向工程中,将布尔值与数值联系起来的问题尤为严重,尽管在这种情况下,布尔值是CPU状态标记。二进制逆向工程是从程序的可执行文件中找出程序的作用的问题例如,当对许可限制阻止访问源代码的代码执行安全审计时,这是一个必要的步骤。受这些安全问题的启发,最近人们对从二进制恢复控制流图(CFG)感兴趣[12]。这里的问题是所谓的鸡和蛋问题[8]:为了导出CFG,必须跟踪寄存器中出现的值和间接地址。但是,为了跟踪寄存器中的值,需要CFG。Kinder通过应用常数传播分析结合自身随分析进行而单调增长的CFG来解决这种循环依赖性[12]。他用一种理想化的汇编语言来说明这些思想。在实践中,这个问题相当难解决,部分原因是将状态标记与范围联系起来的问题。为了说明,考虑以下用于开关表的x86汇编代码[ebp-0x8];eax:=*(ebp-8)subeax,0x2;eax:=eax-2cmpeax,0x5;CF:=(0=eax5);ZF:=(eax=5)ja0xd8;JMPifCF=0anddZF=0jmp [0x8048a0c + eax *4]为了确定CFG,有必要确定当达到间接跳跃时eax∈[0,5]。该范围信息和表本身允许CFG被过度近似。然而,推断eax本身的范围需要仔细推理进位(CF)和零(ZF)标记的值-这是一个类似于Blanchet等人 [1]解决最近,已经展示了如何应用布尔公式来推导用于AVR微控制器代码范围分析的传递函数[2]。在这项工作中,代码块的语义被表示为布尔公式,然后用八边形[15]和一个布尔方程[11]进行抽象,以便导出一个传递函数,该传递函数是一个保护更新系统在本文中,我们将展示如何布尔E. 巴雷特,A.King/Electronic Notes in Theoretical Computer Science 267(2010)1719i=0n−1公式可以以类似于决策树的方式直接应用于分析本身然而,与决策树方法不同,我们不强制规范表示,从而解决了与此类数据结构相关的大小问题[3]。相反,我们将块的语义表示为单个命题公式,该公式可以很容易地用比特爆破技术导出[13]。这个公式对所有寄存器和所有状态标记之间的所有关系进行编码,尽管是位级粒度。然后将抽象应用于公式以提取每当遇到块时总是保持的范围不变量,最终允许恢复控制流。此外,我们可以在块的入口处施加范围信息,并在出口处观察范围,同样通过应用抽象。这在精神上类似于最好的变压器[18],但从一个命题的立场。本文主要研究如何抽象布尔公式表示区间信息。具体而言,我们作出以下贡献:• 我们展示了如何有效地提取由布尔公式约束的位向量的范围信息,其中该向量被解释为整数。准确地说,我们展示了如何计算包括整数可以假设的所有值的最小范围,从而获得最佳过近似。• 我们展示了如何细化范围抽象技术,以发现范围内的边界,将其划分为一组范围。该技术依赖于以交替的方式计算向量的过近似和欠近似。这个过程最终收敛到一个集合S上,它精确地描述了向量的值。然而,如果需要,该过程可以在n个步骤之后预先终止,以计算近似向量值的集合。准确地说,如果n是奇数,则计算过近似(S的超集),否则如果n是偶数,则找到欠近似(S的子集)。• 我们展示了这些技术如何与增量SAT相吻合,并提供了实验结果,表明该技术是可行的。2范围抽象为了推断位向量x在受给定布尔公式f这可以通过将SAT求解器与分块子句结合使用来实现。例如,假设SAT求解器被应用于找到f的解,在该解下,命题变量x=fx0, . ,xn−1 个向量都与真理valuesb0, . ,bn−1∈{0,1}. 一个blocking子句c=yi的定义是 , 如果bi=0,y i = x i,否则yi=<$xi。 我们有一个新的解决方案,从真理valuesb0, c d ,bn-1,至少有一个bi。这样做的结果是公式f ∈ c排除了先前找到的解。通过重复这种技术,可以枚举所有的解决方案,因此x可以假设的所有值,从中可以提取最大值和最小值。这种技术的局限性在于,求解器的调用次数与解的数量(可能很大)成线性关系,此外,SAT实例的大小会随着阻塞子句的添加而增加。20E. 巴雷特,A.King/Electronic Notes in Theoretical Computer Science 267(2010)17(1)函数minimum(f,x,s)(2)k ←时间,n ← |X|(3)当(|K|
下载后可阅读完整内容,剩余1页未读,立即下载
![application/pdf](https://img-home.csdnimg.cn/images/20210720083512.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
安全验证
文档复制为VIP权益,开通VIP直接复制
![](https://csdnimg.cn/release/wenkucmsfe/public/img/green-success.6a4acb44.png)