Please wait a minute...
 首页  期刊介绍 期刊订阅 联系我们
 
最新录用  |  预出版  |  当期目录  |  过刊浏览  |  阅读排行  |  下载排行  |  引用排行  |  百年期刊
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
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
Download: PDF(988 KB)  
Export: BibTeX | EndNote | Reference Manager | ProCite | RefWorks    
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.
Keywords abstraction interpretation      invariant verification      fixed point      program security verification     
ZTFLH:  TP311.5  
Issue Date: 15 July 2016
Service
E-mail this article
E-mail Alert
RSS
Articles by authors
ZHANG Yan
QIAN Junyan
LI Zhoujun
MA Dianfu
Cite this article:   
ZHANG Yan,QIAN Junyan,LI Zhoujun, et al. Program security verification based on abstract invariants[J]. Journal of Tsinghua University(Science and Technology), 2016, 56(7): 777-784.
URL:  
http://jst.tsinghuajournals.com/EN/10.16511/j.cnki.qhdxxb.2016.21.036     OR     http://jst.tsinghuajournals.com/EN/Y2016/V56/I7/777
  
  
  
  
  
  
[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.
[1] BAI Xiaoying, HUANG Jun. Case generation by constraints combinatorial testing[J]. Journal of Tsinghua University(Science and Technology), 2017, 57(3): 225-233.
[2] GAO Xiaolin, YAN Jian, LU Jianhua. Priority weighted rate control algorithm in aeronautical Ad hoc networks[J]. Journal of Tsinghua University(Science and Technology), 2017, 57(3): 293-298.
[3] GUO Jun, MA Anxiang, YAN Yongming, MENG Yu, ZHANG Bin. Cloud service performance bottleneck diagnosis based on the component service quality and performance[J]. Journal of Tsinghua University(Science and Technology), 2017, 57(2): 208-212.
[4] GUO Jun, YAN Yongming, MA Anxiang, ZHANG Bin. Eliminating hot-spots based on cold-spot virtual machine migration in the cloud[J]. Journal of Tsinghua University(Science and Technology), 2016, 56(11): 1232-1236.
[5] LI Xiu, OUYANG Xiaogang, TANG Youhua, HUANG Rongsheng, MA Hui. Cyberinfrastructure prototype for seafloor observations[J]. Journal of Tsinghua University(Science and Technology), 2016, 56(9): 949-955.
[6] LIN Peng, YAN Jian, FEI Ligang, KOU Baohua, LIU Huafeng, LU Jianhua. Multi-satellite and multi-antenna TDRSS dynamic scheduling method[J]. Journal of Tsinghua University(Science and Technology), 2015, 55(5): 491-496,502.
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed   
Copyright © Journal of Tsinghua University(Science and Technology), All Rights Reserved.
Powered by Beijing Magtech Co. Ltd