%A 张, 钱俊彦, 李舟军, 马殿富 %T 基于抽象不变式的程序安全性验证 %0 Journal Article %D 2016 %J 清华大学学报(自然科学版) %R 10.16511/j.cnki.qhdxxb.2016.21.036 %P 777-784 %V 56 %N 7 %U {http://jst.tsinghuajournals.com/CN/abstract/article_149182.shtml} %8 2016-07-15 %X 程序安全性验证是软件系统安全领域的研究难点,构造程序不变式是程序安全性验证的主要方法之一。验证程序是否满足时态性质的问题可转化为不动点求解问题,然而直接构造不动点的求解算法是非常困难的。该文探讨了一类基于抽象解释框架的不变式求解构造方法。首先通过Tableau方法构造时态公式的谓词图,基于传统不变式构造规则,使用前向或逆向状态转换,改进不变式验证规则;然后采用抽象解释框架构造抽象状态转换系统,给出了抽象不变式验证规则;最后基于不动点抽象定理,通过前向或逆向转换求解近似的不动点,使用加宽近似和收窄近似操作进一步加速收敛,从而给出基于抽象不动点的不变式验证算法,最终完成了基于抽象不变式的程序安全性自动验证。