计算机科学 ›› 2021, Vol. 48 ›› Issue (1): 268-272.doi: 10.11896/jsjkx.200100097
孙小祥1, 陈哲1,2,3
SUN Xiao-xiang1, CHEN Zhe1,2,3
摘要： 随着软件运行时验证技术的发展,出现了许多面向C语言的运行时内存安全验证工具。这些工具大多是基于源代码或者中间代码插桩技术来实现内存安全的运行时检测。但是,其中一些没有经过严格证明的验证工具往往存在两方面的问题,一是插桩程序的加入可能会改变源程序的行为及语义,二是插桩程序并不能有效保证内存安全。为了解决这些问题,文中提出了一种使用Coq定理证明器来判定内存安全验证工具算法是否正确的形式化方法,并使用该方法对C语言运行时验证工具Movec的动态检测算法的正确性进行了证明。对安全规范性质的证明结果表明了Movec的内存安全性动态检测算法是正确的。
中图分类号:
| [1] BERTOT Y,CASTÉRAN P.Interactive theorem proving andprogram development:Coq'Art:the calculus of inductive constructions[M].Springer Science & Business Media,2013:12-25. [2] CORBINEAU P.A declarative language for the coq proof as- sistant[C]//International Workshop on Types for Proofs and Programs.Berlin:Springer,2007:69-84. [3] CHEN Z,MOTET G.Nevertrace claims for model checking[C]//International SPIN Workshop on Model Checking of Software.Berlin:Springer,2010:162-179. [4] CHEN Z,WANG Z,ZHU Y,et al.Parametric Runtime Verification of C Programs[C]//International Conference on Tools and Algorithms for the Construction and Analysis of Systems.Berlin:Springer,2016:299-315. [5] NAGARAKATTE S,ZHAO J,MARTIN M M K,et al.Soft-Bound:Highly Compatible and Complete Spatial Memory Safety for C[J].ACM SIGPLAN Notices,2009,44(6):245. [6] NECULA G C,CONDIT J,HARREN M,et al.CCured:type-safe retrofitting of legacy software[J].ACM Transactions on Programming Languages and Systems(TOPLAS),2005,27(3):477-526. [7] NAGARAKATTE S,ZHAO J,MARTIN M M,et al.CETS:compiler enforced temporal safety for C[J].ACM Sigplan Notices,2010,45(8):31-40. [8] MARONEZE A,PERRELLE V,KIRCHNER F.Advances inUsability of Formal Methods for Code Verification with Frama-C[J].Electronic Communications of the EASST,2019,77. [9] FULARA J,JAKUBCZYK K.Practically applicable formalmethods[C]//International Conference on Current Trends in Theory and Practice of Computer Science.Berlin:Springer,2010:407-418. [10] SEREBRYANY K,POTAPENKO A,ISKHODZHANOV T,et al.Dynamic race detection with LLVM compiler[C]//International Conference on Runtime Verification.Berlin:Springer,2011:110-114. [11] YANG L,GURUMANI S,CHEN D,et al.AutoSLIDE:Automatic source-level instrumentation and debugging for HLS[C]//2016 IEEE 24th Annual International Symposium on Field-Programmable Custom Computing Machines(FCCM).IEEE,2016:127-130. [12] CHEN Z.Parametric runtime verification is NP-complete andcoNP-complete[J].Information Processing Letters,2017,123:14-20. [13] CHEN Z,GU Y,Huang Z,et al.Model checking aircraft controller software:a case study[J].Software:Practice and Expe-rience,2015,45(7):989-1017. [14] CHEN Z,YAN J,KAN S,et al.Detecting memory errors at runtime with source-level instrumentation[C]//Proceedings of the 28th ACM SIGSOFT International Symposium on Software Testing and Analysis.2019:341-351. [15] CHEN Z,TAO C,ZHANG Z,et al.Poster:Beyond Spatial and Temporal Memory Safety[C]//2018 IEEE/ACM 40th International Conference on Software Engineering:Companion(ICSE-Companion).IEEE,2018:189-190. [16] CHEN Z,YAN J,LI W,et al.Poster:Runtime Verification of Memory Safety via Source Transformation[C]//2018 IEEE/ACM 40th International Conference on Software Engineering:Companion(ICSE-Companion).IEEE,2018:264-265. |
| [1] | 李凌, 李璜华, 王生原. 在可信编译器设计中实践CompCert编译器的语法分析器形式化验证过程 Experiment on Formal Verification Process of Parser of CompCert Compiler in Trusted Compiler Design 计算机科学, 2020, 47(6): 8-15. https://doi.org/10.11896/jsjkx.191000173 |
| [2] | 范永乾, 陈钢, 崔敏. 基于COQ的有限域GF(2n)的形式化研究 Formalization of Finite Field GF(2n) Based on COQ 计算机科学, 2020, 47(12): 311-318. https://doi.org/10.11896/jsjkx.190900197 |
| [3] | 马振威,陈钢. 基于Coq记录的矩阵形式化方法 Matrix Formalization Based on Coq Record 计算机科学, 2019, 46(7): 139-145. https://doi.org/10.11896/j.issn.1002-137X.2019.07.022 |
| [4] | 祝现威,朱智强,孙磊. Xen混合多策略模型的设计与形式化验证 Design and Formal Verification of Xen Hybrid Multi-police Model 计算机科学, 2017, 44(10): 134-141. https://doi.org/10.11896/j.issn.1002-137X.2017.10.026 |
| [5] | 叶俊民,张坤,叶竹君,陈盼,陈曙. 一种基于活性顺序图的运行时验证研究 Research of Runtime Verification Based on Live Sequence Chart 计算机科学, 2016, 43(8): 137-141. https://doi.org/10.11896/j.issn.1002-137X.2016.08.029 |
| [6] | 徐胜,叶俊民,陈曙,金聪,陈盼. 运行时验证中的减少监控开销方法研究 On Reducing Monitoring Overhead in Runtime Verification 计算机科学, 2016, 43(5): 162-168. https://doi.org/10.11896/j.issn.1002-137X.2016.05.030 |
| [7] | 李姗姗,赵春娜,关永,施智平,王瑞,李晓娟,叶世伟. 分数阶微积分定义的一致性在HOL4中的验证 Formalization of Consistency of Fractional Calculus in HOL4 计算机科学, 2016, 43(3): 23-26. https://doi.org/10.11896/j.issn.1002-137X.2016.03.004 |
| [8] | 杨秀梅,关永,施智平,吴爱轩,张倩颖,张杰. 函数矩阵及其微积分的高阶逻辑形式化 Higher-order Logic Formalization of Function Matrix and its Calculus 计算机科学, 2016, 43(11): 24-29. https://doi.org/10.11896/j.issn.1002-137X.2016.11.005 |
| [9] | 吕兴利,施智平,李晓娟,关 永,叶世伟,张 杰. 连续傅里叶变换基础理论的高阶逻辑形式化 Higher-order Logic Formalization of Basic Theory of Continuous Fourier Transform 计算机科学, 2015, 42(4): 31-36. https://doi.org/10.11896/j.issn.1002-137X.2015.04.004 |
| [10] | 张硕,贺飞. 运行时验证技术的研究进展 Research Advances in Runtime Verification 计算机科学, 2014, 41(Z11): 359-363. |
| [11] | 余俊,张鹏程,周宇鹏,刘宗磊. PSC2GS:一个基于属性序列图的监控器生成工具 PSC2GS:A Tool for Generating Monitors Based on Property Sequence Charts 计算机科学, 2014, 41(9): 84-87. https://doi.org/10.11896/j.issn.1002-137X.2014.09.015 |
| [12] | 师丽坤,赵春娜,关永,施智平,李晓娟,叶世伟. 实数二项式系数在HOL4中的形式化 Formalization of Real Binomial Coefficient in HOL4 计算机科学, 2014, 41(2): 15-18. |
| [13] | 张亚红,张琳琳,赵楷,陈佳丽,冯在文. 一种基于运行时验证的Web服务选择方法 Web Service Selection Method Based on Runtime Verification 计算机科学, 2014, 41(1): 246-249. |
| [14] | 张亚红,张琳琳,赵楷,陈佳丽,冯在文. 基于UML2．0序列图的Web服务运行时验证方法 Runtime Verification Method for Web Service Based on UML2．0Sequence Diagrams 计算机科学, 2013, 40(7): 138-138. |
| [15] | 谷伟卿，施智平，关永,张杰,赵春娜，叶世伟. Gauge积分在HOL4中的形式化 Formalization of Gauge Integration Theory in HOL4 计算机科学, 2013, 40(2): 191-194.228. |
|
||
首页