基于定理证明的内存安全性动态检测算法的正确性研究

随着软件运行时验证技术的发展,出现了许多面向C语言的运行时内存安全验证工具。这些工具大多是基于源代码或者中间代码插桩技术来实现内存安全的运行时检测。但是,其中一些没有经过严格证明的验证工具往往存在两方面的问题,一是插桩程序的加入可能会改变源程序的行为及语义,二是插桩程序并不能有效保证内存安全。为了解决这些问题,文中提出了一种使用Coq定理证明器来判定内存安全验证工具算法是否正确的形式化方法,并使用该方法对C语言运行时验证工具Movec的动态检测算法的正确性进行了证明。对安全规范性质的证明结果表明了Movec的内存安全性动态检测算法是正确的。

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

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.