计算机软件系统已经在国防、金融、通信、医疗等安全关键领域中得到大规模应用。这些领域中的许多软件是采用 C 语言开发，在享受 C 语言高效的运行效率的同时，还需要承担 C语言指针操作带来的内存安全风险。为了构建高可信的软件系统。许多面向C语言的内存安全检测工具被广泛使用，这些工具使用代码插桩来实现内存安全错误的运行时检测。但是，这些内存安全检测工具及其算法都没有经过严格的正确性证明，这带来了两个问题。第一，插桩过的程序有可能会改变原有程序的行为及语义，导致改变原有程序的执行结果。第二，我们不能确保检测算法能检测出它所针对的所有内存安全性错误。因此，如何证明内存安全检测工具及其算法本身的可靠性和有效性就成为至关重要的问题。
　　针对以上两个问题，本文提出了一种基于定理证明的内存安全性动态检测算法的正确性证明方法，并使用该方法完成了对C语言内存安全性动态检测工具Movec的算法的正确性证明，具体而言，本文的工作主要包括以下三个部分：
　　首先，我们形式化地定义了C语言核心子集的语法和语义、Movec内存安全性检测算法的插桩语义。我们通过Coq内置的函数式编程语言实现了对C语言类型、操作语法语义的形式化表示。基于这些形式化定义，我们可以证明检测算法的两个正确性属性：行为不变性和内存安全性。
　　第二，我们证明了Movec算法的行为不变性，即所有的插桩行为不会改变原有程序的行为及语义，主要是通过对 Movec 包装函数的形式化规约来推导出 C 语言原有函数的方法来证明Movec算法的行为不变性。
　　第三，我们证明了Movec算法的内存安全性，即该算法能够在运行时检测出典型的时间和空间内存安全错误。首先我们定义了满足内存安全规范的良构环境，再结合Movec插桩操作的性质、相关公理来证明内存操作及操作语义保持的内存安全性。
　　最后，我们使用著名的Coq交互式定理证明器实现了以上所有的形式化定义，并自动化地证明了以上两个正确性属性，验证了本文方法的有效性。