支持抽象解释的静态分析方法的形式化体系研究

在安全关键领域中,如何保证软件的安全性已经成为了一个广受关注的重要课题。静态程序分析是一类十分有效的程序自动化验证方法。基于抽象解释的静态分析技术在验证软件的非功能性安全属性上表现十分突出。可配置程序分析(Configurable Program Analysis,CPA)是一种通用静态分析方法形式化体系,旨在用一种形式化体系对静态分析的分析阶段进行建模。使用CPA对基于抽象解释的静态分析进行建模,给出如何使用CPA形式化体系描述基于抽象解释的静态分析,给出了从待分析程序到CPA形式化体系的转换规则;提供了一种在安全关键性领域中的软件正确性自动验证方法,为基于抽象解释的静态分析工具的实现提供了一种可行方案。     

基于抽象解释的迹划分技术研究

确保程序中没有运行时错误,对于软件安全性的保证十分重要。基于抽象解释的静态分析方法对程序语义进行抽象,是验证运行时错误最合适的形式化方法之一。然而抽象解释对于程序语义的抽象可能导致过近似问题,从而引发误报,降低了分析精度。因此提出了迹划分的技术,根据程序的迹对程序控制流图进行划分,对静态分析过程进行局部细化,减少了抽象解释过程中过近似引发的误报。迹划分技术以局部分析效率降低为代价换来了分析精度的提高。     

抽象解释及其应用研究进展

抽象解释是一种对用于形式描述复杂系统行为的数学结构进行抽象和近似并推导或验证其性质的理论. 抽象解释自20世纪70年代提出以来,在语义模型、程序分析验证、混成系统验证、程序转换、系统生物学模型分析等领域取得了广泛应用. 近年来,抽象解释在程序分析、神经网络验证、完备性推理、抽象域改进等方面取得较大进展. 基于此,系统综述了抽象解释及其应用的研究进展. 首先概述了抽象解释理论的基本概念,介绍了抽象解释理论、抽象域的研究进展;然后概述了基于抽象解释的程序分析方面的研究进展; 之后概述了基于抽象解释的神经网络模型验证、神经网络模型鲁棒训练、深度学习程序的分析等方面的研究进展;又对抽象解释在智能合约可信保证、信息安全保证、量子计算可信保证等方面的应用进展进行了介绍;最后指明了抽象解释未来可能的研究方向.

     

基于指向与数值抽象的带指针算术程序的分析方法

带指针算术的程序往往包含数组越界、缓冲区溢出等运行时错误。单纯的指针分析技术和数值分析技术都无法有效处理指针算术。为了将指针分析与数值分析相结合,首先提出一种新的指针内存模型,然后基于该模型设计了一个刻画指针指向关系和指针偏移量的抽象域。最后在抽象解释框架下,设计并实现了一个面向带指针算术C程序的静态分析工具原型PAA。实验结果表明,PAA能够有效地分析指针程序的指向关系和数值性质,并能够在效率和精度间取得合理的权衡。     

一种基于抽象解释的WCET自动分析工具

利用基于抽象解释的变量值范围传播技术,提出了一种自动分析高级语言程序流信息的方法;并在白盒测试工具NPCA的基础上,利用该方法实现了WCET分析工具NPCA-WCET。     

基于抽象解释的代码迷惑有效性比较框架

代码迷惑是一种以增加理解难度为目的的程序变换技术,用来保护软件免遭逆向剖析.代码迷惑是否有效是代码迷惑研究中首要解决的问题.目前对有效性证明的研究大都是基于非语义的方式.文章将语义与有效性证明联系起来,建立了基于语义的代码迷惑有效性比较框架,该框架能够为迷惑算法在静态分析这样的限定环境下提供有效性证明,而且也能严格比较迷惑算法之间的有效性,最后使用实例描述比较框架如何应用到证明代码迷惑的有效性.     

基于抽象解释的可执行代码值范围分析

阐述可执行代码抽象存储空间模型的概念并给出程序运行时刻环境抽象表示技术。通过抽象解释静态逼近程序不动点语义的理论保证二进制代码数据流分析的正确性以及可计算性。基于抽象解释和单调数据流框架提出一种自动分析可执行代码变量取值范围的方法及自动获取程序循环最大迭代次数和不可执行路径,并给出数据流分析实例。     

基于抽象解释理论的循环边界计算方法

在实时系统的应用中常常需要对系统的执行时间,尤其是最坏执行时间进行分析。而程序中的循环结构的迭代次数对程序执行时间的分析结果具有重要的影响。程序的循环边界分析目的在于给出较为接近程序真实运行情况下的循环结构迭代的上界和下界。提出了一种基于抽象解释理论的程序循环边界计算方法,该方法对原有的循环边界分析方法进行了改进。首先在程序切片阶段对原程序建立程序依赖图,并提出了对程序依赖图的约简方法。由约简后的依赖关系可以对变量的取值进行约束,得到更小的取值范围,因此基于该方法的循环边界分析结果更加接近程序的实际执行边界,对获取精确的程序执行时间具有重要意义。     

一种基于抽象解释和通用单调数据流框架的值范围分析方法

安全而又精确的值范围分析对编译器优化至关重要．系统地提出了一个基于抽象解释和通用单调数据流框架的值范围分析框架，包括精确的定叉、分析和完整的正确性证明．与一般的值范围分析方法不同，该框架不仅包括抽象解释，还包括与之对应的具体解释，以及相应的正确性证明．     

基于抽象解释理论的程序验证技术

抽象解释(abstract interpretation)理论是Cousot.P和Cousot.R于1977年提出的程序静态分析时构造和逼近(approxiamation)程序不动点语义的理论.描述了程序语义基于Galois连接的抽象解释理论框架,讨论了基于抽象解释理论的程序变换、程序安全性验证和活性性质验证这3种典型的应用,并指出了基于抽象解释理论的程序验证的主要研究方向.     

基于抽象解释自动导出针对WCET分析的程序流信息的方法

通过在通用单调数据流框架基础上使用基于抽象解释的变量值范围传播技术,本文提出了一种自动获取循环最大迭代次数和不可行路径的方法。该方法有利于精确计算实时程序最差情况下的执行时间（WCET）。     

基于抽象解释的C程序信息保密性研究

在分析程序具体语义的基础上,提出一种信息保密性检测方法。构造具体语义和抽象语义的对应关系,根据待测程序性质构建抽象语义,同时在抽象基础上,采用限界思想来优化检测的效率。通过该方法降低程序检测的复杂性,减少时间和空间的浪费,提高了检测的效率和准确度。     

基于抽象解释的服务间消息的数据约减

面向服务软件中服务间消息的变量值可能存在无穷域的情况,从而导致模型检测时产生状态空间爆炸问题。为了使终止性验证在实践上可行,需要约减模型状态空间的大小,使得计算时间和空间需求合理。为此,基于抽象解释的区间抽象理论扩展了经典区间抽象域方法,并在统一的区间抽象域方法上借助异常控制流图对变量进行区间分析,在此基础上逆向分析得到服务间消息的变量区间集。变量区间上任意值相对于终止性验证是等价性,因此从每一个变量区间集中选取一个代表值,可组成服务间消息变量的约减值,从而为异常处理的终止性验证提供了约减的初始配置,有效避免了状态空间爆炸。     

Algebraic Power Analysis by Abstract Interpretation

In this paper we design abstract domains for power analysis. These domains are conceived to discover properties of the following type: The variable X at a given program point is the power of c with the exponent having a given property , where c and are automatically determined. This construction is general and includes different algebraic entities, such as numerical and polynomial (with rational coefficients), as bases. Several families of domains are presented, some of these consider that the exponent can be any natural or integer value, the others also include the analysis of properties of the exponent set. Relevant lattice-theoretic properties of these domains are proved such as the absence of infinite ascending chain and the structure of their meet-irreducible elements. The numerical domains are applied in the analysis of integer powers of imperative programs and in the analysis of probabilistic concurrent programming, with probabilistic non-deterministic choice. Moreover we use the numerical power domains in order to analyze the factorization of integer variables, i.e., invariant properties of factors and of their exponents. In this way we are able to statically detect information hidden in prime factorization, which can be used in software watermarking.