进入21世纪以来,整个社会的信息化程度越来越高,网络信息爆炸,越来越多的信息技术走进每个人的生活。物联网技术的愈发多样,伴随而来的计算机系统软硬件的安全性与可靠性挑战比起以往都更加巨大,所以实现信息时代的信息安全成为当前的主流研究方向之一,构建高可信系统己成为世界范围的重要课题。为了保障软件开发安全,消除程序潜在隐患,我们通常使用逻辑推理系统来完成形式化验证的工作,实现信息安全,一个重要方向就是在软件开发过程中实现形式化验证。利用交互式定理数学证明,模块化的证明编写方式一直研究人员的一大关注点。在国防、金融、交通等对安全性要求极高的领域中,形式化验证已经在被广泛的研究应用当中。本文首先介绍了C语言在程序开发过程中存在的安全隐患以及国内外在程序验证方面的最新进展,然后对形式化验证的基础工具Coq、Comp Cert、VST、霍尔逻辑以及分离逻辑进行介绍和分析。在此基础上以C标准规定有符号整数运算是否越界为例进行深入研究,基于Coq和VST工具,在对一段C程序进行形式化验证时,假定对这段程序需要按照不同的编译要求进行验证,针对不同的编译要求,设定不同的验证规范。本文以验证整形溢出是否为未定义行为作引,研究确定三个不同的验证标准,同时以Coq语言函数式编程的方式抽象定义。就交互式程序验证工具VST而言,对不同的验证规范,修改基础架构Verifiable C程序逻辑,将涉及的各类证明定理进行拆分解耦和重新证明,以此保证整个VST工具程序逻辑的可靠性。最后详细论证在VST中,基于Verifiable C程序逻辑,通过交互式定理证明器Coq,验证一段C程序s是否符合Ps Q的可靠性,其中P为前条件,Q为后条件,深度解构VST中关于定义C表达式语义的形式化框架。通过比较高阶逻辑方式与模块/模块类方式这两种形式化编写方式的优劣,分析本文采用模块/模块类方式改造VST的益处。本文对VST结构的主要改进,采用Module/Module Type类方法,专注于C表达式求值的语义进行形式化验证,对已有大规模交互式定理证明进行解耦,通过VST的模块化改造实现基于分离逻辑的形式化定义与形式化证明;通过一些关键函数的抽象定义,使得其能根据所需场景对C表达式求值的语义验证规范执行不同的实例化,实现动态属性配置以及一些验证选项的参数化设定;保证VST在验证以功能正确性为代表的一系列高阶性质时,所编译C程序不出现运行错误。实验结果表明本项目以整形溢出为例,对VST验证逻辑框架进行模块化重构改造,当需要执行不同的验证标准时,仅需要将各Verifiable C变种逻辑相关的Coq证明调用不同的AC模块类实例,就可以保证在验证有关整形溢出问题的C程序时,实现C程序在不同编译标准下的端到端可靠性。同时本文对VST模块化改造方法也很容易将该改造方案推广到VST可靠性证明的其他部分中去,实现VST验证规范的动态配置,以使在进行可靠性验证时可以根据不同需求进行实例化证明,从而保证整个VST程序逻辑的完整性与可靠性。