摘要
随着软件运行时验证技术的发展,出现了许多面向C语言的运行时内存安全验证工具。这些工具大多是基于源代码或者中间代码插桩技术来实现内存安全的运行时检测。但是,其中一些没有经过严格证明的验证工具往往存在两方面的问题,一是插桩程序的加入可能会改变源程序的行为及语义,二是插桩程序并不能有效保证内存安全。为了解决这些问题,文中提出了一种使用Coq定理证明器来判定内存安全验证工具算法是否正确的形式化方法,并使用该方法对C语言运行时验证工具Movec的动态检测算法的正确性进行了证明。对安全规范性质的证明结果表明了Movec的内存安全性动态检测算法是正确的。
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.
作者
孙小祥
陈哲
SUN Xiao-xiang;CHEN Zhe(College of Computer Science and Technology,Nanjing University of Aeronautics and Astronautics,Nanjing 211106,China;Key Laboratory of Safety-Critical Software,Ministry of Industry and Information Technology,Nanjing 211106,China;Collaborative Innovation Center of Novel Software Technology and Industrialization,Nanjing 211106,China)
出处
《计算机科学》
CSCD
北大核心
2021年第1期268-272,共5页
Computer Science
基金
国家自然科学基金委员会-中国民航局民航联合研究基金(U1533130)
中央高校基本科研业务费人工智能+专项(NZ2020019)。
关键词
运行时验证
源代码插桩
内存安全
定理证明
COQ
Runtime verification
Source code instrumentation
Memory safety
Theorem proof
Coq
