Program security verification based on abstract invariants

ZHANG Yan; QIAN Junyan; LI Zhoujun; MA Dianfu

doi:10.16511/j.cnki.qhdxxb.2016.21.036

PDF(988 KB)

Journal of Tsinghua University(Science and Technology) ›› 2016, Vol. 56 ›› Issue (7) : 777-784. DOI: 10.16511/j.cnki.qhdxxb.2016.21.036

COMPUTER SCIENCE AND TECHNOLOGY

Program security verification based on abstract invariants

{{article.zuoZhe_EN}}

Author information +

History +

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

Cite this article

EndNote

Ris (Procite)

Bibtex

Download Citations

ZHANG Yan, QIAN Junyan, LI Zhoujun, MA Dianfu. Program security verification based on abstract invariants[J]. Journal of Tsinghua University(Science and Technology). 2016, 56(7): 777-784 https://doi.org/10.16511/j.cnki.qhdxxb.2016.21.036

References

[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.