基于动态分析的软件不变量综合技术
作者:
作者简介:

王博(1989-),男,河北邯郸人,博士生,CCF学生会员,主要研究领域为软件测试,缺陷自动修复;卢思睿(1998-),男,学士,CCF学生会员,主要研究领域为软件工程;姜佳君(1992-),男,博士生,CCF学生会员,主要研究领域为软件工程,缺陷修复,程序变换;熊英飞(1982-),男,博士,研究员,博士生导师,CCF专业会员,主要研究领域为软件工程,程序设计语言.

通讯作者:

熊英飞,E-mail:xiongyf@pku.edu.cn

基金项目:

国家自然科学基金(61922003,61672045)


Survey of Dynamic Analysis Based Program Invariant Synthesis Techniques
Author:
  • WANG Bo

    WANG Bo

    Software Engineering Institute, Department of Computer Science and Technology, School of Electronics Engineering and Computer Science, Peking University, Beijing 100871, China;Key Laboratory of High Confidence Software Technologies of Ministry of Education (Peking University), Beijing 100871, China
    在期刊界中查找
    在百度中查找
    在本站中查找
  • LU Si-Rui

    LU Si-Rui

    Software Engineering Institute, Department of Computer Science and Technology, School of Electronics Engineering and Computer Science, Peking University, Beijing 100871, China;Key Laboratory of High Confidence Software Technologies of Ministry of Education (Peking University), Beijing 100871, China
    在期刊界中查找
    在百度中查找
    在本站中查找
  • JIANG Jia-Jun

    JIANG Jia-Jun

    Software Engineering Institute, Department of Computer Science and Technology, School of Electronics Engineering and Computer Science, Peking University, Beijing 100871, China;Key Laboratory of High Confidence Software Technologies of Ministry of Education (Peking University), Beijing 100871, China
    在期刊界中查找
    在百度中查找
    在本站中查找
  • XIONG Ying-Fei

    XIONG Ying-Fei

    Software Engineering Institute, Department of Computer Science and Technology, School of Electronics Engineering and Computer Science, Peking University, Beijing 100871, China;Key Laboratory of High Confidence Software Technologies of Ministry of Education (Peking University), Beijing 100871, China
    在期刊界中查找
    在百度中查找
    在本站中查找
Fund Project:

National Natural Science Foundation of China (61922003, 61672045)

  • 摘要
  • | |
  • 访问统计
  • |
  • 参考文献 [93]
  • |
  • 相似文献 [20]
  • | | |
  • 文章评论
    摘要:

    软件不变量是软件的重要属性,在软件验证、软件调试和软件测试等领域有重要作用.自20世纪末以来,基于动态分析的不变量综合技术成为相关领域的一个研究热点,并且取得了一定的进展.收集了90篇相关论文对该领域进行系统总结.基于动态分析的不变量综合技术是该领域的核心问题,提出了“学习者-预言”框架统一描述相关方法,并且在此框架内根据学习者的归纳方法将综合技术大致分为4类,分别是基于模板穷举的方法、基于数值计算的方法、基于统计学习的方法以及基于符号执行的方法.其次,讨论了基于动态分析综合的不变量在软件验证和软件工程等领域的重要应用.随后,总结不变量生成技术中常用的实验对象程序和开源的不变量综合工具.最后,总结该领域并展望未来的研究方向.

    Abstract:

    Program invariants are important properties of software, which play important roles in many software research fields, such as verification, debugging, and testing. Since the end of 20th century, research on dynamic analysis based program invariant synthesis has become a hot topic in related research areas and made remarkable progress. This paper collects 90 related papers to survey researches within this topic. To dynamically synthesize invariants is the key problem of this field. An abstract framework, “learner-oracle”, is proposed to model and subsume synthesis approaches. In general, the synthesis approaches can be classified into four types, i.e. pattern enumeration based approaches, numerical calculation based approaches, statistical learning based approaches, and symbolic execution based approaches. Furthermore, important applications are discussed of dynamic invariants in software engineering and software verification. Then, important subject programs and synthesis tools are briefly summarized. Finally, the remaining opportunities are presented and a conclusion is reached.

    参考文献
    [1] Cousot P, Cousot R. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proc. of the 4th ACM SIGACT-SIGPLAN Symp. on Principles of Programming Languages. ACM, 1977. 238-252.
    [2] Cousot P, Halbwachs N. Automatic discovery of linear restraints among variables of a program. In: Proc. of the 5th ACM SIGACT-SIGPLAN Symp. on Principles of Programming Languages. ACM, 1978. 84-96.
    [3] Ernst MD, Griswold WG, Kataoka Y, et al. Dynamically discovering pointer-based program invariants. In: Proc. of the Int'l Conf. on Software Engineering. 1999. 373.
    [4] Mesbah A, Van Deursen A. Invariant-Based automatic testing of AJAX user interfaces. In: Proc. of the 2009 IEEE 31st Int'l Conf. on Software Engineering. IEEE, 2009. 210-220.
    [5] Nguyen TV, Kapur D, Weimer W, et al. Using dynamic analysis to discover polynomial and array invariants. In: Proc. of the 34th Int'l Conf. on Software Engineering. IEEE, 2012. 683-693.
    [6] Zhu H, Magill S, Jagannathan S. A data-driven CHC solver. ACM SIGPLAN Notices, 2018,53(4):707-721.
    [7] Zhu H, Xiong Z, Magill S, et al. An inductive synthesis framework for verifiable reinforcement learning. In: Proc. of the 40th ACM SIGPLAN Conf. on Programming Language Design and Implementation. ACM, 2019. 686-701.
    [8] Furia CA, Meyer B, Velder S. Loop invariants: Analysis, classification, and examples. ACM Computing Surveys (CSUR), 2014, 46(3):34.
    [9] Baldoni R, Coppa E, D'elia DC, et al. A survey of symbolic execution techniques. ACM Computing Surveys (CSUR), 2018,51(3): 50.
    [10] Jhala R, Majumdar R. Software model checking. ACM Computing Surveys (CSUR), 2009,41(4):21.
    [11] Chen Y, Poskitt CM, Sun J. Towards learning and verifying invariants of cyber-physical systems by code mutation. In: Proc. of the Int'l Symp. on Formal Methods. Cham: Springer-Verlag, 2016. 155-163.
    [12] Chen Y, Poskitt CM, Sun J. Learning from mutants: Using code mutation to learn and monitor invariants of a cyber-physical system. In: Proc. of the 2018 IEEE Symp. on Security and Privacy (SP). IEEE, 2018. 648-660.
    [13] Gopinath D, Converse H, Pasareanu CS, Taly A. Property inference for deep neural networks. In: Proc. of the 34th ACM/IEEE Int'l Conf. on Automated Software Engineering. ACM, 2019. 797-809.
    [14] Jha S, Seshia SA. A theory of formal synthesis via inductive learning. Acta Informatica, 2017,54(7):693-726.
    [15] Ernst MD, Cockrell J, Griswold WG, et al. Dynamically discovering likely program invariants to support program evolution. IEEE Trans. on Software Engineering, 2001,27(2):99-123.
    [16] Ernst MD, Perkins JH, Guo PJ, et al. The Daikon system for dynamic detection of likely invariants. Science of Computer Programming, 2007,69(1-3):35-45.
    [17] Hangal S, Lam MS. Tracking down software bugs using automatic anomaly detection. In: Proc. of the 24th Int'l Conf. on Software Engineering (ICSE 2002). IEEE, 2002. 291-301.
    [18] Nguyen T, Kapur D, Weimer W, et al. DIG: A dynamic invariant generator for polynomial and array invariants. ACM Trans. on Software Engineering and Methodology (TOSEM), 2014,23(4):30.
    [19] Nguyen TV, Antonopoulos T, Ruef A, et al. Counterexample-Guided approach to finding numerical invariants. In: Proc. of the 2017 11th Joint Meeting on Foundations of Software Engineering. ACM, 2017. 605-615.
    [20] Le TC, Zheng G, Nguyen TV. SLING: Using dynamic analysis to infer program invariants in separation logic. In: Proc. of the 40th ACM SIGPLAN Conf. on Programming Language Design and Implementation. ACM, 2019. 788-801.
    [21] Garg P, Löding C, Madhusudan P, et al. ICE: A robust framework for learning invariants. In: Proc. of the Int'l Conf. on Computer Aided Verification. Cham: Springer-Verlag, 2014. 69-87.
    [22] Padhi S, Sharma R, Millstein T. Data-Driven precondition inference with learned features. ACM SIGPLAN Notices, 2016,51(6): 42-56.
    [23] Zhu H, Petri G, Jagannathan S. Automatically learning shape specifications. ACM SIGPLAN Notices, 2016,51(6):491-507.
    [24] Csallner C, Tillmann N, Smaragdakis Y. DySy: Dynamic symbolic execution for invariant inference. In: Proc. of the 30th Int'l Conf. on Software Engineering. ACM, 2008. 281-290.
    [25] Kannan Y, Sen K. Universal symbolic execution and its application to likely data structure invariant generation. In: Proc. of the 2008 Int'l Symp. on Software Testing and Analysis. ACM, 2008. 283-294.
    [26] Vaziri M, Holzmann G. Automatic detection of invariants in Spin. In: Proc. of the SPIN. 1998. 129-138.
    [27] Perkins JH, Ernst MD. Efficient incremental algorithms for dynamic detection of likely invariants. ACM SIGSOFT Software Engineering Notes, 2004,29(6):23-32.
    [28] Zhang L, Yang G, Rungta N, et al. Feedback-Driven dynamic invariant discovery. In: Proc. of the 2014 Int'l Symp. on Software Testing and Analysis. ACM, 2014. 362-372.
    [29] Malik MZ, Pervaiz A, Khurshid S. Generating representation invariants of structurally complex data. In: Proc. of the Int'l Conf. on Tools and Algorithms for the Construction and Analysis of Systems. Springer, Berlin, Heidelberg, 2007. 34-49.
    [30] Fei L, Midkiff SP. Artemis: Practical runtime monitoring of applications for execution anomalies. ACM SIGPLAN Notices, 2006, 41(6):84-95.
    [31] Hangal S, Narayanan S, Chandra N, et al. IODINE: A tool to automatically infer dynamic invariants for hardware designs. In: Proc. of the 42nd Design Automation Conf. 2005. IEEE, 2005. 775-778.
    [32] Boshernitsan M, Doong R, Savoia A. From daikon to agitator: Lessons and challenges in building a commercial tool for developer testing. In: Proc. of the 2006 Int'l Symp. on Software Testing and Analysis. ACM, 2006. 169-180.
    [33] Li K, Reichenbach C, Smaragdakis Y, et al. Second-Order constraints in dynamic invariant inference. In: Proc. of the 2013 9th Joint Meeting on Foundations of Software Engineering. ACM, 2013. 103-113.
    [34] Beschastnikh I, Brun Y, Schneider S, et al. Leveraging existing instrumentation to automatically infer invariant-constrained models. In: Proc. of the 19th ACM SIGSOFT Symp. and the 13th European Conf. on Foundations of Software Engineering. ACM, 2011. 267-277.
    [35] Beschastnikh I, Abrahamson J, Brun Y, et al. Synoptic: Studying logged behavior with inferred models. In: Proc. of the 19th ACM SIGSOFT Symp. and the 13th European Conf. on Foundations of Software Engineering. ACM, 2011. 448-451.
    [36] Beschastnikh I, Brun Y, Abrahamson J, et al. Unifying FSM-inference algorithms through declarative specification. In: Proc. of the 2013 Int'l Conf. on Software Engineering. IEEE, 2013. 252-261.
    [37] Ohmann T, Herzberg M, Fiss S, et al. Behavioral resource-aware model inference. In: Proc. of the 29th ACM/IEEE Int'l Conf. on Automated Software Engineering. ACM, 2014. 19-30.
    [38] Ohmann T, Thai K, Beschastnikh I, et al. Mining precise performance-aware behavioral models from existing instrumentation. In: Proc. of the 36th Int'l Conf. on Software Engineering. ACM, 2014. 484-487.
    [39] Beschastnikh I, Brun Y, Ernst M D, et al. Inferring models of concurrent systems from logs of their behavior with CSight. In: Proc. of the 36th Int'l Conf. on Software Engineering. ACM, 2014. 468-479.
    [40] Lemieux C, Park D, Beschastnikh I. General LTL specification mining (T). In: Proc. of the 2015 30th IEEE/ACM Int'l Conf. on Automated Software Engineering (ASE). IEEE, 2015. 81-92.
    [41] Nguyen TV, Kapur D, Weimer W, et al. Using dynamic analysis to generate disjunctive invariants. In: Proc. of the 36th Int'l Conf. on Software Engineering. ACM, 2014. 608-619.
    [42] Sharma R, Gupta S, Hariharan B, et al. A data driven approach for algebraic loop invariants. In: Proc. of the European Symp. on Programming. Berlin, Heidelberg: Springer-Verlag, 2013. 574-592.
    [43] Nguyen TV, Dwyer MB, Visser W. SymInfer: Inferring program invariants using symbolic states. In: Proc. of the 32nd IEEE/ACM Int'l Conf. on Automated Software Engineering. IEEE, 2017. 804-814.
    [44] Reynolds JC. Separation logic: A logic for shared mutable data structures. In: Proc. of the 17th Annual IEEE Symp. on Logic in Computer Science. IEEE, 2002. 55-74.
    [45] Sankaranarayanan S, Chaudhuri S, Ivančić F, et al. Dynamic inference of likely data preconditions over predicates by tree learning. In: Proc. of the 2008 Int'l Symp. on Software Testing and Analysis. ACM, 2008. 295-306.
    [46] Garg P, Neider D, Madhusudan P, et al. Learning invariants using decision trees and implication counterexamples. ACM SIGPLAN Notices, 2016,51(1):499-512.
    [47] Ezudheen P, Neider D, D'Souza D, et al. Horn-ICE learning for synthesizing invariants and contracts. Proc. of the ACM on Programming Languages, 2018,2(OOPSLA):131.
    [48] Neider D, Saha S, Garg P, et al. Sorcar: Property-driven algorithms for learning conjunctive invariants. In: Proc. of the Int'l Static Analysis Symp. Cham: Springer-verlag, 2019. 323-346.
    [49] Gehr T, Dimitrov D, Vechev M. Learning commutativity specifications. In: Proc. of the Int'l Conf. on Computer Aided Verification. Cham: Springer, 2015. 307-323.
    [50] Brockschmidt M, Chen Y, Kohli P, et al. Learning shape analysis. In: Proc. of the Int'l Static Analysis Symp. Cham: Springer, 2017. 66-87.
    [51] Serebryany K, Bruening D, Potapenko A, et al. AddressSanitizer: A fast address sanity checker. In: Proc. of the Presented as part of the 2012 USENIX Annual Technical Conf. 2012. 309-318.
    [52] Duck GJ, Yap RHC. Heap bounds protection with low fat pointers. In: Proc. of the 25th Int'l Conf. on Compiler Construction. ACM, 2016. 132-142.
    [53] Duck GJ, Yap RHC, Cavallaro L. Stack bounds protection with low fat pointers. In: Proc. of the NDSS. 2017.
    [54] Duck GJ, Yap RHC. EffectiveSan: Type and memory error detection using dynamically typed C/C++. ACM SIGPLAN Notices, 2018,53(4):181-195.
    [55] Wang R, Ding Z, Gui N, et al. Detecting bugs of concurrent programs with program invariants. IEEE Trans. on Reliability, 2017, 66(2):425-439.
    [56] Baliga A, Ganapathy V, Iftode L. Automatic inference and enforcement of kernel data structure invariants. In: Proc. of the 2008 Annual Computer Security Applications Conf. (ACSAC). IEEE, 2008. 77-86.
    [57] Baliga A, Ganapathy V, Iftode L. Detecting kernel-level rootkits using data structure invariants. IEEE Trans. on Dependable and Secure Computing, 2010,8(5):670-684.
    [58] Ma JC, Wang Y. Approach for detecting soft error by using program invariant. Ruan Jian Xue Bao/Journal of Software, 2016,27(2): 219-230(in Chinese with English abstract). http://www.jos.org.cn/1000-9825/4915.htm [doi: 10.13328/j.cnki.jos.004915]
    [59] Lorenzoli D, Mariani L, Pezze M. Towards self-protecting enterprise applications. In: Proc. of the 18th IEEE Int'l Symp. on Software Reliability (ISSRE 2007). IEEE, 2007. 39-48.
    [60] Raz O, Koopman P, Shaw M. Semantic anomaly detection in online data sources. In: Proc. of the 24th Int'l Conf. on Software Engineering. ACM, 2002. 302-312.
    [61] Liu C, Fei L, Yan X, et al. Statistical debugging: A hypothesis testing-based approach. IEEE Trans. on Software Engineering, 2006, 32(10):831-848.
    [62] Jiang J, Wang R, Xiong Y, et al. Combining Spectrum-Based Fault Localization and Statistical Debugging: An Empirical Study. In: Proc. of the 34th ACM/IEEE Int'l Conf. on Automated Software Engineering. ACM, 2019. 502-514.
    [63] Xie T, Notkin D. Checking inside the black box: Regression testing based on value spectra differences. In: Proc. of the 20th IEEE Int'l Conf. on Software Maintenance. IEEE, 2004. 28-37.
    [64] Liblit B, Aiken A, Zheng AX, et al. Bug isolation via remote program sampling. ACM SIGPLAN Notices, 2003,38(5):141-154.
    [65] Brun Y, Ernst MD. Finding latent code errors via machine learning over program executions. In: Proc. of the 26th Int'l Conf. on Software Engineering. IEEE, 2004. 480-490.
    [66] Groce A, Visser W. What went wrong: Explaining counterexamples. In: Proc. of the Int'l SPIN Workshop on Model Checking of Software. Berlin, Heidelberg: Springer-Verlag, 2003. 121-136.
    [67] Nimmer JW, Ernst MD. Automatic generation of program specifications. ACM SIGSOFT Software Engineering Notes, 2002,27(4): 229-239.
    [68] Nimmer JW, Ernst MD. Invariant inference for static checking: An empirical evaluation. ACM SIGSOFT Software Engineering Notes, 2002,27(6):11-20.
    [69] Polikarpova N, Ciupa I, Meyer B. A comparative study of programmer-written and automatically inferred contracts. In: Proc. of the 18th Int'l Symp. on Software Testing and Analysis. ACM, 2009. 93-104.
    [70] Schiller TW, Donohue K, Coward F, et al. Case studies and tools for contract specifications. In: Proc. of the 36th Int'l Conf. on Software Engineering. ACM, 2014. 596-607.
    [71] Schiller TW, Ernst MD. Reducing the barriers to writing verified specifications. ACM SIGPLAN Notices, 2012,47(10):95-112.
    [72] Lorenzoli D, Mariani L, Pezzè M. Automatic generation of software behavioral models. In: Proc. of the 30th Int'l Conf. on Software Engineering. ACM, 2008. 501-510.
    [73] Harder M, Mellen J, Ernst MD. Improving test suites via operational abstraction. In: Proc. of the 25th Int'l Conf. on Software Engineering. IEEE Computer Society, 2003. 60-71.
    [74] Xie T, Notkin D. Tool-Assisted unit test selection based on operational violations. In: Proc. of the 18th IEEE Int'l Conf. on Automated Software Engineering. IEEE, 2003. 40-48.
    [75] Pacheco C, Ernst MD. Eclat: Automatic generation and classification of test inputs. In: Proc. of the European Conf. on Object- Oriented Programming. Berlin, Heidelberg: Springer-Verlag, 2005. 504-527.
    [76] Elbaum S, Diep M. Profiling deployed software: Assessing strategies and testing opportunities. IEEE Trans. on Software Engineering, 2005,31(4):312-327.
    [77] Gupta N, Heidepriem ZV. A new structural coverage criterion for dynamic detection of program invariants. In: Proc. of the 18th IEEE Int'l Conf. on Automated Software Engineering. IEEE, 2003. 49-58.
    [78] Yuan H, Xie T. Substra: A framework for automatic generation of integration tests. In: Proc. of the 2006 Int'l Workshop on Automation of Software Test. ACM, 2006. 64-70.
    [79] Xie T, Notkin D. Tool-Assisted unit-test generation and selection based on operational abstractions. Automated Software Engineering, 2006,13(3):345-371.
    [80] d'Amorim M, Pacheco C, Xie T, et al. An empirical comparison of automated generation and classification techniques for object-oriented unit testing. In: Proc. of the 21st IEEE/ACM Int'l Conf. on Automated Software Engineering (ASE 2006). IEEE, 2006. 59-68.
    [81] Csallner C, Smaragdakis Y, Xie T. DSD-Crasher: A hybrid analysis tool for bug finding. ACM Trans. on Software Engineering and Methodology (TOSEM), 2008,17(2):8.
    [82] Schuler D, Dallmeier V, Zeller A. Efficient mutation testing by checking invariant violations. In: Proc. of the 18th Int'l Symp. on Software Testing and Analysis. ACM, 2009. 69-80.
    [83] Ernst MD, Notkin D. Dynamically Discovering Likely Program Invariants. University of Washington, 2000.
    [84] McCamant S, Ernst MD. Predicting problems caused by component upgrades. In: Proc. of the 9th European Software Engineering Conf. and the 11th ACM SIGSOFT Symp. on the Foundations of Software Engineering. ACM, 2013. 287-296.
    [85] Perkins JH, Kim S, Larsen S, et al. Automatically patching errors in deployed software. In: Proc. of the ACM SIGOPS 22nd Symp. on Operating Systems Principles. ACM, 2009. 87-102.
    [86] Ding Z, Chen MH, Li X. Online reliability computing of composite services based on program invariants. Information Sciences, 2014,264:340-348.
    [87] Zhou Y, Ding ZH. Computing software reliability based on program invariants. Ruan Jian Xue Bao/Journal of Software, 2015, 26(12):3075-3087(in Chinese with English abstract). http://www.jos.org.cn/1000-9825/4803.htm [doi: 10.13328/j.cnki.jos. 004803]
    [88] Wei Y, Pei Y, Furia CA, et al. Automated fixing of programs with contracts. In: Proc. of the 19th Int'l Symp. on Software Testing and Analysis. ACM, 2010. 61-72.
    [89] Pei Y, Furia CA, Nordio M, et al. Automated fixing of programs with contracts. IEEE Trans. on Software Engineering, 2014,40(5): 427-449.
    [90] Nguyen TV. Automating program verification and repair using invariant analysis and test input generation. 2010.
    附中文参考文献:
    [58] 马骏驰,汪芸.一种基于不变量的软错误检测方法.软件学报,2016,27(2):219-230. http://www.jos.org.cn/1000-9825/4915.htm [doi: 10.13328/j.cnki.jos.004915]
    [87] 周远,丁佐华.基于程序不变量计算软件可靠性.软件学报,2015,26(12):3075-3087. http://www.jos.org.cn/1000-9825/4803.htm [doi: 10.13328/j.cnki.jos.004803]
    引证文献
    网友评论
    网友评论
    分享到微博
    发 布
引用本文

王博,卢思睿,姜佳君,熊英飞.基于动态分析的软件不变量综合技术.软件学报,2020,31(6):1681-1702

复制
分享
文章指标
  • 点击次数:4324
  • 下载次数: 8226
  • HTML阅读次数: 4080
  • 引用次数: 0
历史
  • 收稿日期:2019-11-25
  • 最后修改日期:2019-12-19
  • 在线发布日期: 2020-04-21
  • 出版日期: 2020-06-06
文章二维码
您是第19613736位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京市海淀区中关村南四街4号,邮政编码:100190
电话:010-62562563 传真:010-62562533 Email:jos@iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号