基于Coq构造携带证明的安全程序

对可靠程序的需求随着高可信软件在信息社会中的作用日益重要而增加。基于形式化证明工具构造携带证明的安全程序,给出严格的程序规范及其证明是提高软件可靠性的重要途径。论文介绍使用形式化证明工具Coq构造安全程序的过程和经验。     

基于Coq的Paxos形式化建模与验证

Paxos是一个在不可靠的分布式处理器网络中解决共识问题的算法族.共识问题是指分布式系统中一组参与者就一个结果达成一致的过程.随着Paxos在大型分布式系统中的广泛运用,比如区块链系统以及谷歌文件系统等,其安全性证明越来越重要.在定理证明工具Coq中,形式化描述和定义了Lamport的BasicPaxos算法,并且证明了其满足共识性.     

基于Coq的杨忠道定理形式化证明

实现拓扑学定理的机器证明,是吴文俊院士生前的宿愿.杨忠道定理涉及一般拓扑学中的诸多基本概念,对深刻理解拓扑空间的本质有重要意义.该定理表明,拓扑空间中每一个子集的导集为闭集当且仅当此空间中的每一个单点集的导集为闭集,是一般拓扑学中的一个重要定理.基于定理证明辅助工具Coq,从公理化集合论机器证明系统出发,对一般拓扑学中的开集、闭集、邻域、凝聚点和导集等拓扑基本概念进行形式化描述,给出这些概念基本性质的形式化验证,建立了拓扑空间的形式化框架.在此基础上,实现基于Coq的杨忠道定理形式化证明.全部引理、定理和推论均完整给出Coq的形式化描述和机器证明代码,并在计算机上运行通过,体现了基于Coq的数学定理机器证明具有可读性、交互性和智能性的特点,其证明过程规范、严谨、可靠.杨忠道定理的形式化证明是一般拓扑学形式化内容的一个深刻体现.     

基于Coq的矩阵代码生成技术

矩阵程序在智能系统中扮演着越来越重要的角色.随着矩阵应用的复杂性日益增加,生成正确矩阵代码的难度也在不断变大.并行硬件能够极大地提高矩阵运算的速度,然而,使用并行硬件进行编程以实现并行运算,需要编程人员在程序中描述功能以及如何利用硬件资源来交付结果.这些程序通常是命令式语言,难以推理并且重构,以尝试不同的并行化策略.在Coq中实现了由高级矩阵算子到C代码的矩阵表达式代码生成技术,其能够将带有执行策略的函数式矩阵代码转换为高效低级命令式代码.未来,将把矩阵的形式化同矩阵代码自动生成融合在一起,对矩阵代码转换的过程进行形式化验证,以保障生成的矩阵代码的可靠性,为实现基于矩阵形式化方法的高可靠性深度学习编译器的研制打下基础.     

μC/OS-Ⅲ任务调度器在Coq中的验证

以μC/OS-Ⅲ内核中的任务调度器为研究对象,选取调度相关的核心代码,验证调度器代码满足优先调度最高优先级任务的性质。基于分离逻辑与SCAP验证理论,利用Coq辅助证明工具,通过定义机器模型、操作语义、逻辑断言以及推导规则构建验证框架。在验证框架中,定义内核数据结构和内核相关性质的逻辑描述,模块化地对内核代码进行推理。验证结果表明,μC/OS-Ⅲ任务调度器满足可靠性要求,并且可以通过机器的自动检查。     

基于Coq的RVWMO加载值公理形式化描述与推论证明

RISC-V内存一致性模型（RVWMO）规定了RISC-V多核系统的访存序约束,是RISC-V软硬件设计者共同遵守的重要规范,旨在为硬件设计提供灵活性的同时保证软件的易开发性。RISC-V指令集规范使用全局访存序、保留程序序以及三条公理（加载值公理、原子公理与进度保证公理）描述RVWMO。通过运用RVWMO的规则,可对多线程程序的访存序合法性进行判定,进而指导芯片设计、验证与软件开发。其中,加载值公理是最为复杂和难以运用的规则之一,是多个典型案例合法性判定的重要基础。然而,规范对于该公理的描述及案例讲解主要基于自然语言,缺乏清晰严格的形式化描述和推理过程,不利于读者理解和运用该公理。本文基于交互式定理辅助证明工具Coq,给出了RVWMO加载值公理的形式化描述以及相关引理、定理和推论的证明,对于理解运用RVWMO加载值公理和判定访存序的合法性具有重要意义。     

基于Coq的分块矩阵运算的形式化

矩阵是工程领域中常用的一种数据结构,在深度学习领域,矩阵乘法是神经网络训练中的核心技术之一.面对大型矩阵的运算问题,分块矩阵技术可将大矩阵运算转换为小矩阵运算以实现并行运算,并且能够大幅度减少矩阵运算步骤并且提高矩阵运算速度.首先对目前学术界的矩阵形式化工作进行了系统总结,并且分析了矩阵形式化的主要几种方法;其次介绍并...     

基于高阶逻辑的定理证明方法及其对策的应用

定理证明是形式化验证的主要方法之一,其中定理证明器的使用是难点。为了提高证明效率,论述HOL4系统中主要的三种证明方法:支持高级证明步骤。自动推理和化简器,为定理的证明提供了一个完整而通用的理论框架。详细说明了以上三种证明方法的相关对策的功能和应用环境,并为应用中可能出现的问题提出解决方案。给出的对策应用实例不仅体现了三种方法中相关对策的实用性,还进一步表明了提出解决方案的有效性。     

基于函数式语义的循环和递归程序结构通用证明技术

各类安全攸关系统的可靠运行离不开软件程序的正确执行.程序的演绎验证技术为程序执行的正确性提供高度保障.程序语言种类繁多,且用途覆盖高可靠性场景的新式语言不断涌现,难以为每种语言设计支撑其程序验证任务的整套逻辑规则,并证明其相对于形式语义的可靠性和完备性.语言无关的程序验证技术提供以程序语言的语义为参数的验证过程及其可靠性结果.对每种程序语言,提供其形式语义后可直接获得面向该语言的程序验证过程.提出一种面向大步操作语义的语言无关演绎验证技术,其核心是对不同语言中循环、递归等可导致无界行为的语法结构进行可靠推理的通用方法.特别地,借助大步操作语义的一种函数式形式化提供表达程序中子结构所执行计算的能力,从而允许借助辅助信息对子结构进行推理.证明所提出验证技术的可靠性和相对完备性,通过命令式、函数式语言中的程序验证实例初步评估了该技术的有效性,并在Coq辅助证明工具中形式化了所有理论结果和验证实例,为基于辅助证明工具实现面向大步语义的语言无关程序验证工具提供了基础.     

Formal Verification of a C-like Memory Model and Its Uses for Verifying Program Transformations

This article presents the formal verification, using the Coq proof assistant, of a memory model for low-level imperative languages such as C and compiler intermediate languages. Beyond giving semantics to pointer-based programs, this model supports reasoning over transformations of such programs. We show how the properties of the memory model are used to prove semantic preservation for three passes of the Compcert verified compiler.     

Mothers of Pipelines

We present a method for pipeline verification using SMT solvers. It is based on a non-deterministic “mother pipeline” machine (MOP) that abstracts the instruction set architecture (ISA). The MOP vs. ISA correctness theorem splits naturally into a large number of simple subgoals. This theorem reduces proving the correctness of a given pipelined implementation of the ISA to verifying that each of its transitions can be modeled as a sequence of MOP state transitions.     

基于Coq的操作系统任务管理需求层建模及验证

为确保星上操作系统中任务管理设计的可靠性,利用定理证明工具Coq对操作系统任务管理模块进行需求层建模及形式化验证.从用户角度,基于星上操作系统任务管理的基本机制,提出一种基于任务状态列表集合的验证框架.在需求层将基本机制进行形式化建模,并在Coq中实现.针对建立的需求层模型,提出6条与实际星上操作系统任务管理一致的性质并进行验证.给出其中一条性质在Coq中的验证过程,结果表明,模型满足该条性质.     

面向形式化证明的命令生成技术

随着软件规模的不断增大,软件安全问题日益严重.作为软件系统安全检测的有效手段,形式化证明旨在利用数学方法完成对软件属性的严格验证.常用的形式化证明方法利用模式匹配来进行定理证明,但存在策略生成不完备等缺陷.本文提出一种基于注意力机制的命令预测框架,将LSTM与Coq结合,预测定理证明过程中的策略和参数.实验结果表明本文...     

实时操作系统中有限优先级反转的验证

实时操作系统常常运用优先级调度方案来进行抢占式调度.如果在这些操作系统中使用基于阻塞的同步原语则很容易产生无限优先级反转问题.历史上已经引入了多种不同的协议来避免产生这个问题.然而,这些协议往往非常复杂并且容易滋生错误.本文给出了一套系统的方案来定义这些协议并验证其能够保证有限优先级反转.本文首先给出有限优先级反转的形式化定义.然后介绍了验证框架,它可以用于验证不同的协议保证该性质.该框架可以支持协议抽象层面与具体实现层面的验证.本文已经成功的将该框架应用于验证POSIX标准中提供的优先级继承协议与优先级保护协议.并且,本文的所有工作都已在证明助手Coq中完成.     

Tilting at Windmills with Coq: Formal Verification of a Compilation Algorithm for Parallel Moves

This article describes the formal verification of a compilation algorithm that transforms parallel moves (parallel assignments between variables) into a semantically-equivalent sequence of elementary moves. Two different specifications of the algorithm are given: an inductive specification and a functional one, each with its correctness proofs. A functional program can then be extracted and integrated in the Compcert verified compiler.