Computer Science

Computer Science ›› 2021, Vol. 48 ›› Issue (1): 268-272.doi: 10.11896/jsjkx.200100097

• Information Security • Previous Articles     Next Articles

Study on Correctness of Memory Security Dynamic Detection Algorithm Based on Theorem Proving

SUN Xiao-xiang1, CHEN Zhe1,2,3   

  1. 1 College of Computer Science and Technology,Nanjing University of Aeronautics and Astronautics,Nanjing 211106,China
    2 Key Laboratory of Safety-Critical Software,Ministry of Industry and Information Technology,Nanjing 211106,China
    3 Collaborative Innovation Center of Novel Software Technology and Industrialization,Nanjing 211106,China
  • Received:2020-01-15 Revised:2020-04-08 Online:2021-01-15 Published:2021-01-15
  • About author:SUN Xiao-xiang,born in 1994,postgra-duate.His main research interests include software verification and so on.
    CHEN Zhe,born in 1981,Ph.D,professor,Ph.D supervisor,is a member of China Computer Federation.His main research interests include software verification and so on.
  • Supported by:
    Joint Research Funds of National Natural Science Foundation and Civil Aviation Administration of China(U1533130) and Fundamental Research Funds for AI(NZ2020019).

PDF (PC)

710

Abstract: With the development and improvement of software runtime verification technology,many C-oriented runtime memory security verification tools have appeared.Most of these tools are based on source code or intermediate code instrumentation technology to achieve memory-safe runtime detection.However,some of these verification tools that have not been rigorously proven often have two problems.One is that the addition of instrumentation programs may change the behavior and semantics of the source program,and the other is that instrumentation programs cannot effectively guarantee memory safety.In order to solve these two problems,this paper proposes a formal method that uses the Coq theorem prover to determine whether the memory security verification tool algorithm is correct,and uses this method to check the correctness of the dynamic runtime algorithm of the C language verification tool Movec Proven.The proof of the nature of the security specification shows that Movec's dynamic detection algorithm for memory security is correct.

Key words: Coq, Memory safety, Runtime verification, Source code instrumentation, Theorem proof

CLC Number: 

  • TP309
[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] LI Ling, LI Huang-hua, WANG Sheng-yuan. Experiment on Formal Verification Process of Parser of CompCert Compiler in Trusted Compiler Design [J]. Computer Science, 2020, 47(6): 8-15.
[2] FAN Yong-qian, CHEN Gang, CUI Min. Formalization of Finite Field GF(2n) Based on COQ [J]. Computer Science, 2020, 47(12): 311-318.
[3] MA Zhen-wei,CHEN Gang. Matrix Formalization Based on Coq Record [J]. Computer Science, 2019, 46(7): 139-145.
[4] YE Jun-min, ZHANG Kun, YE Zhu-jun, CHEN Pan and CHEN Shu. Research of Runtime Verification Based on Live Sequence Chart [J]. Computer Science, 2016, 43(8): 137-141.
[5] XU Sheng, YE Jun-min, CHEN Shu, JIN Cong and CHEN Pan. On Reducing Monitoring Overhead in Runtime Verification [J]. Computer Science, 2016, 43(5): 162-168.
[6] ZHANG Shuo and HE Fei. Research Advances in Runtime Verification [J]. Computer Science, 2014, 41(Z11): 359-363.
[7] SHI Li-kun,ZHAO Chun-na,GUAN Yong,SHI Zhi-ping,LI Xiao-juan and YE Shi-wei. Formalization of Real Binomial Coefficient in HOL4 [J]. Computer Science, 2014, 41(2): 15-18.
[8] ZHANG Ya-hong,ZHANG Lin-lin,ZHAO Kai,CHEN Jia-li and FENG Zai-wen. Web Service Selection Method Based on Runtime Verification [J]. Computer Science, 2014, 41(1): 246-249.
[9] ZHANG Ya-hong,ZHANG Lin-lin,ZHAO Kai,CHEN Jia-li and FENG Zai-wen. Runtime Verification Method for Web Service Based on UML2．0Sequence Diagrams [J]. Computer Science, 2013, 40(7): 138-138.
[10] . Field-sensitive Memory Model for Memory Safety of Heap-manipulating Programs [J]. Computer Science, 2012, 39(9): 109-114.
[11] SHI Kai-Yuan, PANG Jian-Min, ZHAO Rong-Cai, DAI Chao （Institute of Information Engineering, Information Engineering University, Zhengzhou 450002）. [J]. Computer Science, 2007, 34(5): 269-272.
[12] . [J]. Computer Science, 2007, 34(12): 273-277.
Viewed
Full text


Abstract

Cited
  Shared   
  Discussed   
No Suggested Reading articles found!
渝ICP备16013121号-4
Add:18# Honghu West Rd., Yubei ,Chongqing,China    Post Code: 401121
Tel: 023-63500828/023-67039612/023-67039623
E-mail: jsjkx12@163.com
Powered by Beijing Magtech Co., Ltd.