Program security verification based on abstract invariants
ZHANG Yan1,2, QIAN Junyan3, LI Zhoujun1, MA Dianfu1
1. School of Computer Science and Engineering, BeiHang University, Beijing 100085, China;
2. School of Computer Science and Information Engineering, Hubei University, Wuhan 430062, China;
3. Department of Computer science and Engineering, Guilin University of Electronic Technology, Guilin 541004, China
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.
张, 钱俊彦, 李舟军, 马殿富. 基于抽象不变式的程序安全性验证[J]. 清华大学学报（自然科学版）, 2016, 56(7): 777-784.
ZHANG Yan, QIAN Junyan, LI Zhoujun, MA Dianfu. Program security verification based on abstract invariants. Journal of Tsinghua University(Science and Technology), 2016, 56(7): 777-784.
[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.
2016, Vol. 56 
