您好、欢迎来到现金彩票网!
当前位置:2019欢乐棋牌 > 指称语义 >

抽象解释论文

发布时间:2019-07-27 05:45 来源:未知 编辑:admin

  基于抽象解释的程序分析及其应用 周洁 (桂林电子科技大学 计算机学院 广西 桂林541004) 摘要: 摘要:在计算机普遍应用的现代社会,软件特别是大型实时安全攸关软件的可靠 性成为计算机界和整个社会都非常关注的问题。 现有的形式化软件验证工具都不 得不通过近似来处理复杂问题中的计算, 抽象解释作为一种在数学模型间进行可 靠近似的理论, 为各类自动验证工具中不同的近似方法建立起一个统一的形式化 框架。抽象解释理论在程序分析和验证研究领域得到了广泛的关注与应用,其应 用范围涵盖了程序静态分析、程序变换、程序调试、程序水印等方面。本文分析 了现有程序分析和验证典型形式化方法的不足, 描述了基于程序不动点语义的抽 象解释理论框架,介绍了 Galois 连接、Widening 算子、Narrowing 算子,指出 了基于抽象解释理论的程序验证的主要研究方向。 并对其近年来的应用现状进行 了较为全面的介绍, 最后给出了抽象解释理论中尚存在的一些问题及可能的研究 方向。 关键字: 关键字:抽象解释;Galois 连接;Widening 算子;Narrowing 算子;程序验证 Program verification techniques and application based on the abstract interpretation Zhoujie 【 Abstract 】 : In a highly computer-dependent society , reliability of software , especially of big real-time safety critical ones , gains farranging attention from computer community and the rest of the world.Existing tools for formal program verifying have to deal with complex computation through approximating to some extent.Abstract interpretation is a theory for sound approximation between mathematic models , and constructs a unifying formal framework for different approximate methods of different program verification tools.Abstract interpretation is discussed and applied widely in several program analysis and verification fields,including static analysis,program transform, debugging, program watermarking, so on. This paper analyzes and the shortcomings of the existing typical formalism method of the program analysis and verification , introduces Galois connection 、 Widening operator 、 Narrowing operator , describes the theory framework of abstracting program’s fixpoint semantics,and then introduces its state of the art and future challenges. 【 keyword 】 : Abstract interpretation ; Galois connection ; Widening operator;Narrowing operator;program verification 引言: 1 引言: 随着计算机技术在各行各业应用的日益普及, 工作在我们身边的各种计算机 系统由于其中的软件系统失效经常表现的不尽人意,呈现出脆弱、难以信任的特 征,甚至造成不可挽回的损失,因此研究相关的可信软件关键技术以提高软件系 统的可信性已经成为十分迫切的需求。 在程序可信性分析和验证的研究过程中中,模型检验、定理证明是能够自动 化实现的典型形式化方法。模型检验通过遍历系统所有状态空间,能够对有穷状 态系统进行自动验证,并自动构造不满足验证性质的反例。对于无穷状态系统或 状态数目超出现有计算机处理能力的非常复杂的有穷状态系统,模型检验方法难 以解决状态空间爆炸问题。 定理证明方法能够应用于解决无穷状态系统的验证问 题,但是模型检验是一种自动验证有穷状态系统的技术,其基本思想是通过遍历 系统模型的状态空间老检验系统模型是否满足给定的性质。 模型检验面临状态空 间爆炸的难题,定理证明方法也受到一阶逻辑半可判定性的限制,因为一阶逻辑 是半可判定的,理论分析结果表明,机械化的定理证明过程并不能保证停机。 计算机科学理论和大规模软、 硬件系统的发展需要一种能够处理计算机科学 中不可判定问题和非常复杂问题的有效方法,抽象解释理论就是其中一种有效的 解决方法,它为计算机科学中的不可判定问题和复杂问题的逼近求解提供了系统 性的构造方法和有效算法。 抽象解释理论是sot和R.Cousot于1977年提出的 程序静态分析时构造和逼近程序不动点语义的理论。程序指称对象域上的计算, 程序语义(操作语义或者指称语义)描述了对象域上的计算过程或结果。程序的 抽象解释就是指使用另一个抽象对象域上的计算抽象逼近程序指称的对象域 (具 体对象域)上的计算,使得程序抽象执行的结果能够反映出程序真实运行的部分 信息。抽象解释本质上是在计算效率和计算精度之间取得均衡,以损失计算精度 求得计算可行性,再通过迭代计算增强计算精度的一种抽象逼近方法。基于抽象 解释理论的形式化方法是对大规模软、 硬件系统进行自动化分析与验证的有效途 径之一,已被广泛地应用于大型软、硬件系统的验证研究中。本文描述完备格、 Galois连接、完备格上的Widening/Narrowing算子等基本概念,以及程序语义基 于Galois连接的抽象解释理论框架。 后面主要集中于描述基于抽象解释的典型应 用研究,主要包括基于抽象解释的程序变换、基于抽象解释的程序安全性性质验 证和程序活性性质验证。 基础知识: 2 基础知识: 完备格) 定义 1(完备格):设﹤L,?﹥是一个偏序,﹤L,?﹥称为一个完备格当且仅 当:L中任何一个子集均存在最小上界和最大下界。特别地,用⊥=??=?L表示L中 最小元素,用?=??=?L表示L中最大元素,其中,?和?表示最小上界算子和最大下 界算子,完备格﹤L,?﹥一般表示为﹤L,?,?,?,⊥,?﹥。 定义2 连接) 定义2( Galois 连接 ): 设﹤P,≤﹥和﹤Q,?﹥是两个偏序集合, α :P→Q 和 γ :Q→P是两个映射,序偶﹤ α , γ ﹥称为一个Galois连接当且仅当:?x∈P,? y∈Q, α (x)?y 当且仅当x≤ γ (y),其中,映射α称为抽象算子, γ 称为具体算 子。 由Galois 连接的定义,容易验证抽象算子 α 和具体算子 γ 具有如下性质: (1) ?x∈P,x≤ γ ( α (x)); (2) ?y∈Q, α ( γ (y))?y; (3) α 和γ单调递增。 抽象算子 α 和具体算子 γ 具有的上述性质与Galois连接的定义等价。 可以从 上界和下界两个方向抽象逼近对象集合。抽象偏序集﹤Q,?﹥中的对象集合p 可 以上界抽象逼近具体偏序集﹤P,≤﹥中的对象集合P′当且仅当P′≤ γ (p) γ , (p)是P′的上界保证抽象逼近的可靠性;理论上,P′存在最优上界抽象逼近∩ {pP′≤(p)}。抽象算子 α 刻画了具体对象域和抽象对象域之间的最优上界抽 象逼近映射关系,即抽象分析时 α (P′)作为P′的抽象逼近。首先, α (P′) 是P′的一个上界抽象逼近(?x∈P,x≤ γ ( α (x)));其次,若p 是P′的任 意一个上界抽象逼近,即P′≤ γ (p)。由Galois连接的定义,则有 α (P′)?p 近 (?x∈P,?y∈Q,x≤ γ (y)当且仅当 α (x)?y),表明 α (P′)是P′的最优 上界抽象逼近。 容易验证,Galois连接的运算具有如下性质: (1) 两个Galois连接的合成是Galois连接; (2) Galois连接的广义笛卡尔乘积是一个Galois连接; (3) 设P表示一个程序,用S[[P]]表示P 的语义,如果S[[P]]可以通过计算 语义泛函F[[P]]的最小不动点得到,即S[[P]]= lfp F[[P]],若? α , γ ?是一个 Galois 连 接 , 定 义 语 义 泛 函 F ′ [[P]]= α ? F[[P]] ? γ , 则 S[[P]] 的 抽 象 α (S[[P]])= lfp F′[[P]]。 Galois 连接的上述运算性质表明对程序语义可以连续地进行抽象,直到抽 象对象域上的抽象计算满足计算复杂度的要求为止。 程序不动点语义的计算过程不收敛(不终止)是引起程序验证过程中状态空 间爆炸的另一个原因。设?L,?,?,?,⊥,??是一个完备格,程序P的指称语义(操作 语义与指称语义具有语义等价性)可以由L上的一个单调语义泛函F[[P]]:L→L 来刻画,在最理想的情况下,即F[[P]]是完备格L上的连续函数,并且?{F[[P]]n (⊥)n∈N}在有限步迭代计算后收敛,则容易得到F[[P]]的最小不动点 lfp (F[[P]])=?{F[[P]]n(⊥)n∈N};否则,(?{F[[P]]n(⊥)n∈N})不一定 收敛,即使(?{F[[P]]n(⊥)n∈N})收敛,也不一定收敛于 lfp (F[[P]])(因 为F[[P]]不一定是连续函数)。在抽象解释理论框架中,Widening 算子可以给出 lfp (F[[P]])的一个上界逼近,Narrowing 算子给出 lfp (F[[P]])更精细的一 个上界逼近。 定义3 算子) 定义3(Widening 算子):设?L,?,?,?,⊥,??是一个完备格,算子?:L×L→L 称为Widening 算子当且仅当: (1) ?是一个上界算子(即? l1 , l2 ∈L, l1 , l2 ? l1 ? l2 ); ? ? (2) 对于任意的递增链( ln )n,递增链( ln )n都收敛,其中,( ln )定义 ? ? ? 为:如果n=0,则( ln )=ln;否则, ln =( ln ?1 )? ln 。 偏序集合可以扩张成为完备格,然后可以为完备格定义Widening算子。 例如, 区间抽象域可以扩张成为完备格,对于扩张得到的完备格?L,?,?,?,⊥,??,定义 如下的Widening算子?: 如果m2m1,并且n2≤n1,则[m1,n1]?[m2,n2]=[⊥,n1];如果m1≤m2,并且n1n2,则 [m1,n1]?[m2,n2]=[m1,?]; 如果m2m1,并且n1n2,则[m1,n1]?[m2,n2]=[⊥,?];如果m1≤m2,并且n2≤n1,则 [m1,n1] ? [m2,n2]=[m1,n1] ; 对 于 区 间 构 成 的 无 穷 递 增 链 [0,1],[0,2],…,[0,n],…,Widening 算子?使该递增链迅速收敛到[0,?]。 设程序P的单调语义泛函F[[P]]:L→L 定义在完备格?L,?,?,?,⊥,??上,并且?是 完备格?L,?,?,?,⊥,??上的一个Widening 算子,定义序列(F[[P]] n )n为: ? 若n=0,则F[[P]] n =⊥; ? n? n? 若n0,并且F[[P]]( F[[P]] n?1 )?F[[P]] ? 1 , 则F[[P]]?n = F[[P]] ? 1 ; ? n? n? 否则, F[[P]] n =F[[P]] F[[P]] ? 1 ) (F[[P]] ? 1 ) 可以证明序列 ( ? 。 (F[[P]] n ) ? ? n 收敛,并且存在m0,使得F[[P]]( F[[P]] m )? F[[P]] m ,F[[P]]在F[[P]] m ? ? ? 处是收缩的(reductive),由Tarski 不动点定理, lfp (F[[P]])? F[[P]] m , ? 即F[[P]] m 是 lfp (F[[P]])的一个上界逼近, F[[P]] m 对 lfp (F[[P]])逼近的 ? ? 精度取决Widening 算子?。 定义4 算子) 定义4(Narrowing 算子): 设﹤L,?,?,?,⊥,?﹥是一个完备格,算子 Δ:L×L→L称为Narrowing 算子当且仅当: (1)? l1 , l2 ∈L,若 l2 ? l1 ,则 l2 ?( l2 Δ l1 )? l1 ; ? ? (2) 对于所有的递降链( ln )n,递降链( ln )n收敛;其中,( ln )定义 ? ? ? 为:如果n=0,则( ln )= ln ;否则,( ln )=( ln ?1 )Δ ln 。 设 Δ 是 完 备 格 ﹤ L, ? , ? , ? , ⊥ , ? ﹥ 上 的 一 个 Narrowing 算 子 , 定 义 序 列 ([F[[P]] ? n )为: ? 若n=0,则([F[[P]] n )=(F[[P]] m ); ? 否则,([F[[P]] ? )=([F[[P]]] ??1 )ΔF[[P]]([F[[P]]] ??1 )。 n n n ? 可以证明 lfp(F[[P]]) (F[[P]] n(F[[P]] m ) ? ? ) ([F[[P]]] n ) ?F[[P]] m , ? ? ? ? ? 并且([F[[P]]] n ) n 收敛,即存在m′0,使得([F[[P]]] m )=([F[[P]]] m +1 )。 ? 取([F[[P]]] m )作为 lfp (F[[P]])的上界逼近,显然,它是比F[[P]] m 更精细的 ? 一个 lfp (F[[P]])的上界逼近。 连接的抽象解释理论框架: 3 程序不动点语义基于 Galois 连接的抽象解释理论框架: Galois连接、 完备格上的Widening/Narrowing算子是抽象解释理论中的基本 概念。 Galois连接中的具体算子保证抽象解释中抽象对象域和具体对象域之间逼 近关系的可靠性,抽象算子建立两者之间的最优逼近关系。完备格上的Widening 算子用于使程序不动点语义的计算过程收敛或用于加速其收敛,Narrowing算子 对程序不动点语义计算结果进行精化。程序通常描述为迁移系统,基于抽象解释 理论对迁移关系进行抽象,可以构造具有不同精细程度的程序抽象语义。抽象解 释理论从抽象对象域、Widening算子、程序抽象语义3个方面建立起程序不动点 语义抽象逼近计算的理论框架。基于抽象解释理论的程序验证的基本思想是,在 保证抽象逼近可靠性的前提下,对程序不动点语义计算过程的各个层次进行抽象 逼近,使得计算过程收敛或加速其收敛,然后依据逼近计算的不动点语义验证系 统需要满足的性质,若验证过程中出现虚假反例,则对抽象过程进行精化。 基于抽 象解释理论的形式化验证的特点是可靠但不完备的,如果验证结果表明抽象系统 满足验证性质,则抽象解释理论保证原系统也满足验证性质;若验证结果表明抽 象系统不满足验证性质,则原系统可能满足验证性质(表明抽象过程中出现了不 满足验证性质的虚假反例),可能不满足验证性质(原系统存在不满足验证性质 的真实反例),需要更精细的抽象分析。 3.1程序语义基于Galois连接的抽象解释理论框架 程序语义基于Galois连接的抽象解释理论框架 Galois 程序通常表示为迁移系统,迁移系统 τ =﹤Σ,Σi,t﹥是一个三元组,其中,Σ 为状态集合,Σi?Σ为初始状态集合,t?Σ×Σ为状态之间的迁移关系。程序迁 移关系的复杂性也是引起程序验证过程中状态空间爆炸的原因之一,对迁移关系 进行抽象解释得到迁移系统的4种语义:部分踪迹语义、自反传递闭包语义、可达 性语义、区间语义,这4种语义具有不同的抽象逼近层次。 (1)迁移系统的部分踪迹语义 迁移系统 τ 的部分执行踪迹是状态的有穷序列s0 s1…sn,其中,s0 ∈Σ,﹤ si,si+1 ﹥∈t,in。所有部分执行踪迹构成的集合称为 τ 的部分踪迹语义,记作 ∑τ ∑τ ? n , ∑τ = ∪n ≥0 ∑τ ,其中, ∑τ 表示长度为0的部分执行踪迹集合,即空集, 表示长度为 n 的部分执行踪迹的集合。 部分踪迹语义精确地描述了迁移系 ? n 0 统的行为。 (2)自反传递闭包语义作为部分踪迹语义的抽象 在验证与中间计算步骤无关的程序性质时,部分执行踪迹语义过于精确,对 迁移系统 τ 的部分执行踪迹集合,X定义如下的抽象: a(X)={ a (﹤s0s1…sn﹥)s0s1…sn∈X}, 其中, a (﹤s0s1…sn﹥)=﹤s0,sn﹥,即对X中的任意一条踪迹σ=s0s1… sn, a 将迁移关系﹤s0s1…sn﹥抽象为σ的初始状态s0 与最终状态sn之间的迁移关系。 由a(X)的定义,对于迁移系统 τ 的部分踪迹语义 ∑τ , a ( ∑τ ) 是迁移关系 t 的 自 反传递闭包 t ? 。 设Y是初始状态和最终状态之间迁移关系构成的集合,定义 ={s 容易证明,a (X) ?Y当且仅当X? γ (Y) α , γ ,﹤ γ (Y) 0s1…sn﹤s0,sn﹥∈Y}。 ? ? ﹥Galois 连接,表明自反传递闭包语义是部分踪迹语义的最优上界抽象逼近。 (3)可达性语义作为自反传递闭包语义的抽象 迁移系统 τ =﹤Σ,Σi,t﹥的可达性语义表示为{s′?s∈Σi:﹤s,s′﹥∈ t ? },是初始状态可达的所有状态组成的集合。 定义post[r]Z={s′?s∈Z:﹤s,s′﹥∈r},a (Y)=post[Y]Σi={s′?s ∈Σ i :﹤s,s′﹥∈Y},则迁移系统的可达性语义{s′?s∈Σ i:﹤s,s′﹥∈ t ? }=post[ t ? ]Σi= a ( t ? ), 定义 γ (Z) ={﹤s,s′﹥s∈Σi, 且s′∈Z},则a (Y) ?Z当且仅当Y? γ (Z) , 因而,﹤ α , γ ﹥是一个Galois 连接,表明可达性语义是传递闭包语义的最优上界 抽象逼近。 (4)区间语义作为可达性语义的抽象 迁移系统 τ =﹤Σ,Σi,t﹥的状态如果能用全序排序,其中以-∞和+∞作为 极值,或者更一般地,迁移系统 τ =﹤Σ,Σi,t﹥的状态集合构成一个完备格,则 τ 的区间语义为位于某一区间的可达状态集合。 定义 α H (Z)=[minZ,maxZ],minZ 和maxZ 分别是集合Z的最小值和最大值, 定义 α H ([ l , h ])={s∈Σ l ≤s≤ h },并定义抽象蕴涵[ l , h ]?[ l , h ]为 γ H ([ l , h ])? γ H ([ l , h ]),则有 α H (Z)?[ l , h ]当且仅当Z? γ H ([ l , h ]),因而, ﹤ α H , γ H ﹥是一个Galois连接,表明区间语义是可达性语义的最优上界抽象逼 近。 在抽象解释理论框架中,程序语义划分为标准语义、集合语义、抽象语义3 个抽象层次,程序的标准语义是指程序的操作语义或指称语义,集合语义是对标 准语义进行抽象得到的与程序验证性质相关的语义部分,对集合语义进一步抽象 构造得到抽象语义,程序验证时使用抽象语义。 基于抽象解释的程序验证技术: 4 基于抽象解释的程序验证技术: 4.1 基于抽象解释理论的程序变换 程序变换是程序的语法变换,它将程序变换为与其语义等价的另外一个程序, 本质上是保持程序语义的程序设计语言上的映射,语法变换导致程序语义的变换, 因而可以将程序变换视为等价变换后的程序语义的反编译过程。 程序语义比程序 包含了更多的信息。 例如,程序中包含了变量及它们的类型信息,但是不包含程序 语义中具有的程序运行时对变量连续赋值的信息,程序描述了构成程序的语句的 序列,但是没有程序语义所描述的程序语句的执行序列。 不同于程序,程序语义中 包含了程序的运行时信息。 例如,程序语义能够反映程序的执行时间,但是程序运 行性能在程序中却无法体现。依据P.Cousot的观点,可以将程序视为程序语义的 抽象。 抽象解释理论为程序变换提供了一个简单而自然的实现框架:首先,基于抽 象解释理论对程序的语义进行抽象(抽象解释保证语义等价性),得到程序的抽 象语义;然后,对程序的抽象语义再进行抽象(程序可以视为程序语义的抽象, 即对程序语义的反编译过程),构造得到的程序就是程序变换的结果。特别地, 如果程序P 的程序语义可以由计算单调的程序语义泛函F[[P]]的最小不动点得 到,并且﹤ α , γ ﹥是一个Galois连接,定义语义泛函F′[[P]]= α ? F [[P]]? γ ,则程序P的变换程序t[[P]]= lfp F [[P]]。基于抽象解释理论的程序变换提 供了由一种语义模型构造另外一种语义模型的构造方法。 Bruno Blanchet基于Horn逻辑的安全协议模型及其验证方法是基于抽象解 释理论的程序变换在安全协议验证领域的一个典型应用。 安全协议是建立在密码 体制基础上的一种通信协议,它运行在计算机网络或分布式系统中,借助于密码 算法为在网络环境中实现密钥分配、身份认证、电子商务交易等任务的各方约定 任务的执行步骤和执行规则。 安全协议是解决互联网络安全问题最有效的手段之 一,它满足的基本安全性质有保密性和认证性。Cervesato,Durgin等人提出了基 于线性逻辑的安全协议模型,它是安全协议基于状态迁移的一种精确模 型,Blanchet证明了基于线性逻辑的安全协议模型经过抽象解释、Skolem化带存 在量词的公式、 程序变换,可以得到基于Horn逻辑的安全协议模型,给出了保密性 的验证方法,同时,通过一组变换规则将基于进程代数的安全协议模型转换为基 于Horn逻辑的安全协议模型,并给出了认证性的验证方法。 具体地说,基于线性逻 辑的多集重写语义,Blanchet对基于线性逻辑的安全协议模型的踪迹(接收消息 动作和发送消息动作构成的动作序列)进行抽象解释,用踪迹中出现的消息多集 抽象该踪迹,并用经典逻辑中的逻辑规则替换线性逻辑中的逻辑规则,Skolem化 逻辑规则中带存在量词的公式,最后通过程序变换删除逻辑规则中与保密性验证 无关的原子公式,得到了基于Horn逻辑的安全协议模型。与基于线性逻辑的安全 协议模型比较,基于Horn逻辑的安全协议模型可以采用推迟实例化、删除逻辑规 则前件中相同的原子公式、 被逻辑蕴涵的逻辑规则不参与消解计算等已有的计算 优化方法,验证保密性和认证性时具有更好的计算效率,正因为如此,Blanchet 基于Horn逻辑模型设计和实现的安全协议验证工具Proverif在安全协议源代码 级的程序验证中得到了广泛的应用。 4.2 基于抽象解释理论的程序安全性验证 基于Galois连接的抽象解释理论框架的程序验证工作主要是Cousot等人以 程序静态分析工具ASTREE为主要成果的一系列研究,研究以C程序编写的运算密 集型的嵌入式实时安全攸关软件系统作为研究对象,以检查软件系统中的运行时 错误作为主要研究内容。ASTREE首先对软件系统进行编译链接,得到对应的抽象 语法树,针对抽象语法树使用结构归纳法构造软件系统的不动点语义,不动点语 义计算过程中使用基于阈值(threshold)的Widening算子,使计算过程收敛或加 速其收敛。ASTREE 以存储抽象域和算术抽象域上的计算抽象程序运行过程中的 计算。算术抽象域包括区间抽象域、八边形抽象域等多种抽象域,在计算精度要 求较高时,八边形抽象域代替区间抽象域进行抽象计算,八边形抽象域通过迭代 计算可以得到程序变量之间形如?u?v≤c的线性不变式。ASTREE的抽象分析过程 使用了参数化方法,用于调整抽象计算的计算精度和计算效率之间的平衡关系。 例如,在选择区间抽象域、 八角型抽象域方面,ASTREE采用了对变量进行分组的方 法,同一组中的变量采用同一抽象域进行抽象计算。ASTREE基于软件系统的抽象 语法树以及存储抽象域和算术抽象域的迭代计算得到抽象的不变式形式的后向 不动点(post-fixpoint),以前向传播(forward propagation)的方式根据后 向不动点检查软件系统是否存在运行时错误。对于虚假反例,ASTREE基于数据依 赖和控制依赖的后向程序切片方法定位引起虚假反例的变量集合,对变量集合中 与验证性质相关并且缺少精确抽象计算结果的变量集合采用计算精度较高的八 角形抽象域的计算进行精化。2006年,Mine进一步提出了C程序中Union类型数据 结构和指针算术的抽象分析方法,扩大了ASTREE分析的语法对象范围,使得它能 够对许多嵌入式C程序检查运行时错误。ASTREE在应用领域专家进行参数设置后 自动运行,它的抽象分析过程遍历软件的每一个抽象状态,不会遗漏每一个运行 时错误,并且抽象分析过程总是终的;使得验证时间大大缩减。 4.3基于抽象解释理论的程序活性性质验证 4.3.1基于迁移谓词抽象的程序活性性质验证 基于迁移谓词抽象的程序活性性质验证 迁移谓词抽象也是程序抽象解释的特殊形式,迁移谓词抽象以给定的一组迁 移谓词上的计算抽象程序迁移关系域上的计算,基于迁移谓词抽象的抽象-精化 迭代验证也被应用于对大规模软件活性性质的自动验证中。典型的研究工作是 Podelski,Rybalchenko和Cook等人对大规模软件活性性质验证的一系列研究。 他 们首先提出了迁移不变式的概念,迁移不变式是程序迁移关系的超集,基于良基 (well-founded)迁移关系和程序停机性之间的关联,对于程序停机性性质验证 提出了基于析取良基迁移不变式的刻画定理,基于Vardi的自动机理论框架,对于 程序活性性质验证给出了基于析取良基迁移不变式的刻画定理。在此基础上,提 出了基于迁移谓词抽象的抽象-精化迭代验证框架,对大规模软件的活性性质进 行验证,并应用提出的验证方法对Windows操作系统的驱动程序进行了验证,发现 了之前未曾发现的不满足活性性质的软件bug。 4.3.2 规约为参数化数学最优化问题的活性性质验证 在Floyd、Naur、Hoare经典程序正确性验证方法的基础上,Cousot针对半代 数程序(semialgebraic program)提出了程序不变式和用于停机性验证的秩函 数(rank function)的自动构造方法。基于半代数程序多项式形式的计算语义, 根据程序不变式和秩函数设定的参数化抽象的表达式形式和程序的迁移关系以 及验证条件,给出程序不变式和秩函数参数化表达式中参数之间的数值约束关系, 参数之间的数值约束关系可以进一步使用拉格朗日松弛法进行松弛变换,消除参 数之间数值约束关系中的逻辑蕴涵; 然后基于求解半正定方程约束最优化问题的 求解算法,给出参数化表达式中参数的一组可行解,半正定方程约束求解能够消 除参数之间数值约束关系中的全称量词约束。 基于程序不变式和秩函数的自动构 造方法,Cousot给出了自动验证安全性以及活性性质的新思路。 综上所述,Cousot等人以ASTREE为主要成果的一系列研究建立在区间抽象 域、八边形抽象域等具有不同抽象层次的抽象域的基础上,用更精细的抽象域进 行抽象计算是ASTREE 采用的抽象精化方法,谓词抽象以一组谓词作为抽象域,在 原有谓词基础上增加新的谓词进行抽象计算,是谓词抽象采用的抽象精化方法, 两者都应用于对程序安全性性质进行验证,抽象分析方法本质上都是对程序状态 进行抽象;在对程序活性性质进行验证的研究中,抽象分析方法本质上都是对程 序迁移关系进行抽象,Cousot的研究更注重于应用参数化数学最优化问题的求解 算法及其计算工具软件包。 4.4基于抽象解释的其他应用 基于模型的软件调试MBSD(Model-Based Software Debugging)技术运用Reiter 基于模型的诊断MBD (Model-Based Diagnosis) 思想, 对程序中的错误进行定位, 为研究和开发自动化的程序调试方法和工具提供了可行的尝试。 基于抽象解释的 程序诊断框架,在系统建模过程中利用程序的抽象解释建立模型AIM(Abstract Interpretation-based Model)。AIM中使用Galois连接( α , γ )将程序从具体 语义抽象至区间语义,构造一个抽象程序图,在这个抽象图上重复进行前向-后 向分析去除不可能出现的初态和终态,直至达到一个不动点,从而实现对候选诊 断的有穷分析。 与其他基于MBD建立的模型或非MBD调试技术 (如程序切片) 相比, 基于AIM得到的诊断结果准确性有较大提高,且能应用于一些其他方法无法处理 的困难程序。但AIM 的计算耗费较大,需要进一步的优化使其能应用于大中型规 模的程序的诊断。此外,抽象解释还在程序的最差执行时间(WCET)分析、代码 迷惑算法分析及程序水印技术等方面得到了广泛应用。 5.总结: 总结: 抽象解释理论从对象域抽象、Widening算子、迁移关系抽象3个方面建立对程序 不动点语义上界抽象逼近的理论框架。 使得在较高抽象层次语义中对程序性质进 行可靠、高效的分析和验证成为可能,在程序分析与验证研究中得到广泛应用, 针对大规模软件和硬件系统的基于抽象解释理论的自动分析与验证工具也在不 断出现并得到了实际应用。本文讨论了基于抽象解释理论的程序变换、活性性质 验证两种典型的应用。 基于抽象解释理论的程序验证技术在取得巨大进展的同时, 该领域仍然面临着很多挑战,也有很多问题值得进一步研究,问题主要集中在以 下几个方面: (1)将基于抽象解释的形式化分析融入软件开发的整个过程,从最初的规范到 最终的实现,提高各开发阶段的工作效率,将有效缩短开发周期,降低软件开发 成本。 (2)如何建立一个通用的、具有较强表达能力且代价合理的抽象理论以处理不 同应用领域中的复杂结构及特性(如并行化中的数据依赖、嵌入式系统中的时间 限制及概率特性等)。 (3)对更高阶的结构化模块分析和涉及到复杂数据和控制概念(对象、并发线 程、分布式/移动程序设计等)的计算,需进一步加强现有工具,使之能自动组 合不同抽象方法,对抽象进行局部精化,并能与用户和其他形式化或非形式化工 具与方法实现交互。 参考文献 [1]Clarke E M, Grumberg J O, Peled D A. Model Checking.1999 [2]Cousot P, Halbwachs N. Automatic discovery of linear restraints among variables of a program. In: Proc. of the 5th POPL. Arizona:ACM Press, 1978. [3]Cousot P, Cousot R. Basic concepts of abstract interpretation. In: René J, ed. Building the Information Society. Toulouse: Kluwer Academic Publishers, 2004. [4]Cousot P. Proving program invariance and termination by parametric abstraction, lagrangian relaxation and semidefinite programming. In: Cousot R, ed. Proc. of the VMCAI 2005. LNCS 3385, Paris: Springer-Verlag, 2005.. [5]Henzinger TA, Jhala R, Majumdar R, McMillan KL. Abstractions from proofs. In: Jones ND, Leroy X, eds. Proc. of the 31st ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages. Venice: ACM Press, 2004.

http://acetechpng.com/zhichenyuyi/393.html
锟斤拷锟斤拷锟斤拷QQ微锟斤拷锟斤拷锟斤拷锟斤拷锟斤拷锟斤拷微锟斤拷
关于我们|联系我们|版权声明|网站地图|
Copyright © 2002-2019 现金彩票 版权所有