Please wait a minute...
 首页  期刊介绍 期刊订阅 联系我们 横山亮次奖 百年刊庆
 
最新录用  |  预出版  |  当期目录  |  过刊浏览  |  阅读排行  |  下载排行  |  引用排行  |  横山亮次奖  |  百年刊庆
清华大学学报(自然科学版)  2016, Vol. 56 Issue (7): 777-784    DOI: 10.16511/j.cnki.qhdxxb.2016.21.036
  计算机科学与技术 本期目录 | 过刊浏览 | 高级检索 |
基于抽象不变式的程序安全性验证
张1,2, 钱俊彦3, 李舟军1, 马殿富1
1. 北京航空航天大学 计算机学院, 北京 100085;
2. 湖北大学 计算机与信息工程学院, 武汉 430062;
3. 桂林电子科技大学 计算机科学学院, 桂林 541004
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
全文: PDF(988 KB)  
输出: BibTeX | EndNote (RIS)      
摘要 程序安全性验证是软件系统安全领域的研究难点,构造程序不变式是程序安全性验证的主要方法之一。验证程序是否满足时态性质的问题可转化为不动点求解问题,然而直接构造不动点的求解算法是非常困难的。该文探讨了一类基于抽象解释框架的不变式求解构造方法。首先通过Tableau方法构造时态公式的谓词图,基于传统不变式构造规则,使用前向或逆向状态转换,改进不变式验证规则;然后采用抽象解释框架构造抽象状态转换系统,给出了抽象不变式验证规则;最后基于不动点抽象定理,通过前向或逆向转换求解近似的不动点,使用加宽近似和收窄近似操作进一步加速收敛,从而给出基于抽象不动点的不变式验证算法,最终完成了基于抽象不变式的程序安全性自动验证。
服务
把本文推荐给朋友
加入引用管理器
E-mail Alert
RSS
作者相关文章
张
钱俊彦
李舟军
马殿富
关键词 抽象解释不变式验证不动点程序安全性验证    
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 wordsabstraction interpretation    invariant verification    fixed point    program security verification
收稿日期: 2015-08-20      出版日期: 2016-07-22
ZTFLH:  TP311.5  
基金资助:国家“八六三”高技术项目(2015AA016004);国家自然科学基金面上项目(90718017,61562015)
通讯作者: 李舟军,教授,E-mail:lizj@buaa.edu.cn     E-mail: lizj@buaa.edu.cn
引用本文:   
张, 钱俊彦, 李舟军, 马殿富. 基于抽象不变式的程序安全性验证[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.
链接本文:  
http://jst.tsinghuajournals.com/CN/10.16511/j.cnki.qhdxxb.2016.21.036  或          http://jst.tsinghuajournals.com/CN/Y2016/V56/I7/777
  图1 规则INV
  图2 规则SAFE
  图3 规则StrongGSAFE
  图4 抽象规则SAFE
  图5 抽象规则StrongGSAFE
  图6 基于抽象不动点检查的验证不变式算法
[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] 林鹏, 晏坚, 费立刚, 寇保华, 刘华峰, 陆建华. 中继卫星系统的多星多天线动态调度方法[J]. 清华大学学报(自然科学版), 2015, 55(5): 491-496,502.
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed   
版权所有 © 《清华大学学报(自然科学版)》编辑部
本系统由北京玛格泰克科技发展有限公司设计开发 技术支持:support@magtech.com.cn