计算机科学 ›› 2017, Vol. 44 ›› Issue (12): 126-130.doi: 10.11896/j.issn.1002-137X.2017.12.025
张弛,黄志球,丁泽文
ZHANG Chi, HUANG Zhiqiu and DING Zewen
摘要： 在安全关键领域中,如何保证软件的安全性已经成为了一个广受关注的重要课题。静态程序分析是一类十分有效的程序自动化验证方法。基于抽象解释的静态分析技术在验证软件的非功能性安全属性上表现十分突出。可配置程序分析(Configurable Program Analysis,CPA)是一种通用静态分析方法形式化体系,旨在用一种形式化体系对静态分析的分析阶段进行建模。使用CPA对基于抽象解释的静态分析进行建模,给出如何使用CPA形式化体系描述基于抽象解释的静态分析,给出了从待分析程序到CPA形式化体系的转换规则；提供了一种在安全关键性领域中的软件正确性自动验证方法,为基于抽象解释的静态分析工具的实现提供了一种可行方案。
| [1] CHESS B,MCGRAW G.Static Analysis for Security[J].IEEE Security & Privacy Magazine,2004,2(2):76-79. [2] ZHANG J H,HUANG Z Q,CAO Z N.Counterexample Genera-tion for Probabilistic Timed Automata Model Checking [J].Journal of Computer Research and Development,2008,5(10):1638-1645.(in Chinese) 张君华,黄志球,曹子宁.模型检测基于概率时间自动机的反例产生研究[J].计算机研究与发展,2008,5(10):1638-1645. [3] JHALA R,MAJUMDAR R.Software model checking[J].ACM Computing Surveys (CSUR),2009,1(4):1-54. [4] COUSOT P,COUSOT R,MAUBORGNE L.Theories,solvers and static analysis by abstract interpretation[J].Journal of the ACM (JACM),2012,9(6):1-56. [5] COUSOT P,COUSOT R,FERET J,et al.The ASTRéE analyzer[C]∥European Symposium on Programming.Springer Berlin Heidelberg,2005:21-30. [6] BEYER D,HENZINGER T A,THODULOZ G.Configurable Software Verification:Concretizing the Convergence of Model Checking and Program Analysis[C]∥International Conference on Computer Aided Verification.2007:504-518. [7] CHEN L Q.Sound Floating-point and Non-convex Static Analysis Using Interval Linear Abstract Domains [D].Changsha:National University of Defense Technology,2010.(in Chinese) 陈立前.基于区间线性抽象域的可靠浮点及非凸静态分析[D].长沙:国防科学技术大学,2010. [8] LU C,HUANG Z Q,KAN S L,et al.Safety Analysis for Slats and Flaps Control Unit Based on Octagon Abstract Domain [J].Journal of Chinese Computer Systems,2016,7(5):902-907.(in Chinese) 陆陈,黄志球,阚双龙,等.基于八边形抽象域的襟缝翼控制系统安全性分析[J].小型微型计算机系统,2016,7(5):902-907. [9] COUSOT P,CCOUSOT R.Abstract Interpretation:A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints[C]∥ACM Sigact-Sigplan Symposium on Principles of Programming Languages.1977:238-252. [10] KSTNER D,FERDINAND C.Applying Abstract Interpreta-tion to Verify EN-50128 Software Safety Requirements[C]∥International Conference on Reliability,Safety and Security of Railway Systems.Springer International Publishing,2016:191-202. [11] BLANCHET B,COUSOT P,COUSOT R,et al.A static analyzer for large safety-critical software[C]∥Proceedings of the ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation 2003.San Diego,California,USA,2003:196-207. [12] CHEN L Q,WANG J,HOU S N.An Abstract Domain of One-Variable Interval Linear Inequalities [J].Chinese Journal of Computers,2010,3(3):427-439.(in Chinese) 陈立前,王戟,侯苏宁.单变量区间线性不等式抽象域[J].计算机学报,2010,3(3):427-439. [14] COUSOT P,COUSOT R.A galois connection calculus for abstract interpretation[C]∥ACM Sigplan-Sigact Symposium on Principles of Programming Languages.ACM,2014:3-4. [15] COUSOT P,COUSOT R.Abstract interpretation:past,present and future[M].ACM,2014. [16] BALL T,PODELSKI A,RAJAMANI S K.Boolean and Cartesian abstraction for model checking C programs[M]∥Tools and Algorithms for the Construction and Analysis of Systems.Springer Berlin Heidelberg,2001:268-283. [17] HENZINGER T A,JHALA R,MAJUMDAR R,et al.LazyAbstraction[C]∥POPL.2002:58-70. [18] FOSCHER J,JHALA R,MAJUMDAR R.Joining dataflow withpredicates[J].AcmSigsoft Software Engineering Notes,2005,30(5):227-236. [19] LALIRE G,ARGROUND M,JEANNET B.Interproc.http://pop-art.inrialpes.fr/people/bjeannet/bjeannet-forge/interproc. [20] MAUBORGNE L,RIVAL X.Trace Partitioning in Abstract Interpretation Based Static Analyzers[M]∥Programming Languages and Systems.Springer Berlin Heidelberg,2005:5-20. |
| No related articles found! |
|
||
首页