程序安全性验证是软件系统安全领域的研究难点，构造程序不变式是程序安全性验证的主要方法之一。验证程序是否满足时态性质的问题可转化为不动点求解问题，然而直接构造不动点的求解算法是非常困难的。该文探讨了一类基于抽象解释框架的不变式求解构造方法。首先通过Tableau方法构造时态公式的谓词图，基于传统不变式构造规则，使用前向或逆向状态转换，改进不变式验证规则；然后采用抽象解释框架构造抽象状态转换系统，给出了抽象不变式验证规则；最后基于不动点抽象定理，通过前向或逆向转换求解近似的不动点，使用加宽近似和收窄近似操作进一步加速收敛，从而给出基于抽象不动点的不变式验证算法，最终完成了基于抽象不变式的程序安全性自动验证。
Abstract
Program security verification is a difficult issue with program invariants used for program security verification. Verification of whether a program has the correct temporal nature is converted into a problem solved at a fixed point. However, directly constructing an algorithm to solve the fixed point problem is very difficult. This paper presents a class of invariant construction methods based on an abstract interpretation framework to solve the structure method. Firstly, the Tableau method is used to construct the figure of the temporal formula based on the traditional invariant structure rules, with forward or backward state transitions to improve the invariant validation rules. Secondly, this paper presents an abstract state transition system based on an abstract interpretation framework and gives the abstract invariants validation rules. Finally, the fixed point theorem of abstract invariants is used with the forward or reverse transformations to solve the approximate fixed point in an automatic validation method based on abstract invariants of the program. Approximate widening and narrowing operations based on the abstract fixed point invariant verification algorithm accelerate the convergence.
关键词
抽象解释 /
不变式验证 /
不动点 /
程序安全性验证
Key words
abstraction interpretation /
invariant verification /
fixed point /
program security verification
{{custom_sec.title}}
{{custom_sec.title}}
{{custom_sec.content}}
参考文献
[1] Podelski A, Rybalchenko A. Transition invariants and transition predicate abstraction for program termination[C]//International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Saarbrücken, Germany:Springer Verlag, 2011:3-10.
[2] Bensalem S, Bozga M, Legay A, et al. Incremental component-based construction and Verification using invariants[C]//Proceedings of the IEEE/ACM Conference on Formal Methods in Computer-Aided Design. Lugano, Switzerland:IEEE Computer Society, 2010:257-266.
[3] Chockler H, Ivrii A, Matsliah A, et al. Incremental formal verification of hardware[C]//Proceedings of the IEEE/ACM Conference on Formal Methods in Computer-Aided Design. Austin, Texas, USA:IEEE Computer Society, 2011:135-143.
[4] Bensalem S, Legay A, Nguyen T. H, et al. Incremental invariant generation for compositional design[C]//Proceedings of The 4th Theoretical Aspects of Software Engineering Conference. Taipei, Taiwan, China:IEEE Computer Society, 2010:157-167.
[5] I Dillig, T Dillig, B Li, et al. Inductive invariant generation via abductive inference[J]. Acm Sigplan Notices, 2013, 48(48):443-456.
[6] Lakhnech Y, Bensalem S, Berezin S. Incremental verification by abstraction[C]//Proceeding of the Tools and Algorithms for the Construction and Analysis of Systems. Genova, Italy:Springer Verlag, 2001:98-112.
[7] Bj?rner N, Browne A, Manna Z. Automatic generation of invariants and intermediate assertions[J]. Theoretical Computer Science, 1997, 173(1):49-87.
[8] Bensalem S. Automatic generation of invariants[J]. Formal Methods in System Design, 1999, 15(1):75-92.
[9] Loiseaux C, Graf S, Sifakis J, et al. Property preserving abstractions for the verification of concurrent systems[J]. Formal methods in System Design, 1995, 13(6):1-35.
[10] Cousot P. Formal verification by abstract interpretation[C]//Proceedings of the 4th NASA Formal Methods Symposium. Norfolk, VA, USA:Springer Verlag, 2012:3-7.
[11] Cousot P, Ganty P, Raskin F. Fixpoint-guided abstraction refinements[C]//Proceedings of the Fourteenth International Symposium on Static Analysis. Kongens Lyngby, Denmark:Springer Verlag, 2007:333-348.
[12] Ranzato F, Rossi Doria, Tapparo F. A forward-backward abstraction refinement algorithm[C]//Proceedings of the 9th International Conference on Verification, Model Checking and Abstract Interpretation. San Francisco, CA, USA:Springer Verlag, 2008:248-262.
[13] Gantya P, Maquetb N, Raskinb F. Fixed point guided abstraction refinement for alternating automata[J]. Theoretical Computer Science, 2010, 411(38-39):3444-3459.
[14] Malkis A, Podelski A, Rybalchenko A. Thread-Modular Counterexample-Guided Abstraction Refinement[J]. Lecture Notes in Computer Science, 2011, 6337:356-372.
[15] Meng W, He F, Wang B. Y, Liu Q. Thread-modular model checking with iterative refinement[C]//Proceedings of the NASA Formal Method. Berlin, Heidelberg:Springer-Verlag, 2012:237-251.
[16] Bensalem S, Graf S, Lakhnech Y. Abstraction as the key for invariant verification[J]. Lecture Notes in Computer Science, 2003, 2772:67-99.
[17] Gulwani S, Srivastava S, Venkatesan R. Constraint-based invariant inference over predicate abstraction[J]. Lecture Notes in Computer Science, 2009, 5403:120-135.
[18] Patrick C, Radhia C. Parsing as abstract interpretation of grammar semantics[J]. Theoretical Computer Science, 2003, 290:531-544.
基金
国家“八六三”高技术项目（2015AA016004）；国家自然科学基金面上项目（90718017，61562015）
PDF(988 KB)
