基于Coq的软件安全性验证

针对数组越界、空指针应用和缓冲区溢出三类威胁软件安全的不规范操作,提出了一种基于Coq验证上述三类操作的形式化方法。首先编写三类安全问题的程序实例,并采用形式化方法进行标注;其次运用Frama-C和Why工具对标注程序进行解析,生成需要证明的定理;最后基于Coq集成开发环境证明定理,实现安全问题的验证。结果表明,该方法有效验证了软件安全中的三类问题,为形式化方法在软件安全性验证方面的应用奠定了基础。     

出具证明编译器中线性整数命题证明的自动生成

近年来,出具证明编译器作为构建高可信软件的重要途径,逐渐成为编译器理论和形式化验证的研究热点.在其理论框架中,编译器需要借助自动定理证明技术,自动地证明验证条件并生成机器可检查的证明项,因此好的自动定理证明器对出具证明编译器至关重要.本文基于Simplex算法在出具证明编译器的框架内设计并实现了一个支持线性整数命题求解的自动定理证明器,并且提出一套证明项构造方法,将其应用于自动定理证明器中可生成Coq可检查的证明.     

汇编级顺序语句块的自动形式化规约及其验证

软件的形式化验证是保障软件可证明性、可靠性和安全性的重要手段,但传统形式化验证脚本的生成过程复杂且需要形式化验证专家的大量手工验证。为提高证明效率,构建一种自动证明模型,并在此基础上提出语义自动规约算法以及对所规约的语义自动生成证明脚本的算法。利用C++和Python并通过交互式定理证明器Isabelle 2017在基准数据中随机选择10个程序进行测试,结果表明,与完全人工操作相比,该算法具有较高的验证效率,可实现顺序语句块的自动化规约与验证。     

操作系统安全验证形式化分析框架

结合当前形式化验证方法的特点和操作系统安全模型情况,本文提出了这些方法在操作系统安全分析中的应用。结合传统定理证明方法的优势,将模型检验方法纳入形式化安全分析体系当中,并分别提出了在安全分析中的应用情况。将用定理证明用于从模型到规则的分析,模型检验从实现中抽取模型,用于从实现到规则的分析。     

同步数据流语言输入结构体的可信翻译

为最大程度地减少同步数据流语言编译过程中由编译器引入的错误,需要利用形式化方法自动生成代码,保证编译器产生的代码能够应用于核能仪控系统.本研究使用定理证明工具Coq,对同步数据流语言Lustre到Clight的主节点输入结构翻译阶段涉及的语法、语义及翻译算法进行了形式化定义,并完成翻译算法的形式化证明.研究表明这种经过形式化的编译器能够生成与源代码行为一致的可信目标代码,同时生成的目标代码能够很好满足核能仪控系统的执行规范.     

基于KeY的程序分析和验证

可信性是各安全攸关领域软件的基础要求,例如航空航天飞行器控制软件、核电站控制软件和交通控制管理软件等,基于形式化方法的程序验证和分析是确保软件正确,具有可信性的重要手段。相比软件测试,基于定理证明的程序验证具有语法和语义的严格性,和属性相关的完备性。本文对程序形式化Hoare语义规约和相关的程序逻辑推理规则系统进行了详细的讨论。基于形式化验证平台Ke Y,采用完全自动化和交互式两种方法,对具有一定规模的,含有循环结构,并且具有实际意义的程序进行验证。研究证明过程的具体证明策略和方法,尤其是关于循环不变式的规约方法;对Ke Y的证明效率,先进性和局限性进行评估。     

针对教学场景的ZFC集合论Coq形式化

离散数学是计算机类专业的基础课程之一,命题逻辑、一阶逻辑与公理集合论是其重要组成部分.教学实践表明,初学者准确理解语法、语义、推理系统等抽象概念是有一定难度的.近年来,已有一些学者开始在教学中引入交互式定理证明工具,以帮助学生构造形式化证明,更透彻地理解逻辑系统.然而,现有的定理证明器有较高上手门槛,直接使用会增加学生的学习负担.鉴于此,在Coq中开发了针对教学场景的ZFC公理集合论证明器.首先,形式化了一阶逻辑推理系统和ZFC公理集合论;之后,开发了数条自动化推理规则证明策略.学生可以在与教科书风格相同的简洁证明环境中使用自动化证明策略完成定理的形式化证明.该工具被用在了大一新生离散数学课程的教学中,没有定理证明经验的学生使用该工具可以快速完成数学归纳法和皮亚诺算术系统等定理的形式化证明,验证了该工具的实际效果.     

面向平面几何命题理解的融合算法研究

随着初等几何命题可视化机器证明的发展,如何让几何教学辅助软件能够直接理解几何命题的含义,自动生成对应的几何图形并进行推理证明,成为当前研究的一个新问题。现有的几何命题理解方法虽然在一定程度上实现了几何命题向形式化命令的转化,但是这些方法均没有考虑几何命题中分句间的逻辑关系,无法解决分句间形式化命令的冗余和冲突问题,导致后期自动作图和推理的准确率不高。针对这一问题,在前期工作的基础上提出了一个几何命题分句间形式化命令融合算法,并将该融合算法集成应用于已有的自然语言几何作图接口进行实验论证。结果显示,几何命题分句间形式化命令融合算法将自然语言几何作图的准确率从原来的84.17%提高到了91.67%,能够有效提高几何命题理解的准确性。     

具有冲突约束的RBAC模型的形式化规范与证明

在实际应用"基于角色的访问控制"(RBAC)模型时,经常遇到由于责任分离等策略而引起的冲突问题,如权限间的互斥等.访问控制操作应满足某些约束条件,以避免冲突的存在.但这些冲突关系相当复杂,如何检测出冲突问题是模型安全实施的重要保证.借助Z语言,提出了基于状态的RBAC形式化模型,对状态转换函数进行了形式化规范,描述了操作的具体内容和应满足的冲突约束条件.根据安全不变量给出了安全性定理,分别进行数学的和形式化的证明.最后,通过实例分析,说明在实际系统中,如何形式化规约和验证RBAC系统并检测出冲突问题,从而为今后使用RBAC模型开发具有高安全保证的系统提供了一种形式化规范和证明方法.     

GJK算法的一种特殊情形的形式化验证和应用

计算几何算法经常用于机器人避碰运动规划等安全攸关领域,对这些算法进行正确性证明非常重要.用形式化方法对算法进行验证是一种十分有效的手段,尤其是定理证明的方法用严格的数学公理和定理推理证明逻辑模型的性质,对所验证的性质而言是完备的.基于GJK算法设计了计算空间两条线段间距离的算法,用定理证明器HOL4对其相关的定义和定理进行形式化定义和证明,进而基于霍尔逻辑完成形式化表示和证明,对该算法的正确性实现了形式化验证.最后,给出了这一经过验证的算法在双臂机器人无碰撞运动规划中的应用.     

形式化方法概貌

形式化方法是基于严格数学基础,对计算机硬件和软件系统进行描述、开发和验证的技术.其数学基础建立在形式语言、语义和推理证明三位一体的形式逻辑系统之上.形式化方法已经以不同程度和不同方式愈来愈多地应用在计算系统生命周期的各个阶段.介绍了形式化方法的发展历程和基本方法体系;以形式规约和形式验证为主线,综述了形式化方法的理论、方法、工具和应用的现状,展示了形式化方法与软件学科其他领域的交叉和融合;分析了形式化方法的启示,并展望了其面临的发展机遇和未来趋势.形式化方法的发展和研究现状表明：其应用已经取得了长足的进步,在提高计算系统的可靠性和安全性方面发挥了重要作用.在当今软件日益成为社会基础设施的时代,形式化方法将与人工智能、网络空间安全、量子计算、生物计算等领域和方向交叉融合,得到更加广阔的应用.研究和建立这种交叉融合的理论和方法不仅重要,而且具有挑战性.     

基于代码审计技术的OpenSSL脆弱性分析

本文讨论应用代码审计技术,分析OpenSSL源代码,进行脆弱性分析,并作出针对性修补建议.在进行源码级分析时,主要采用数据流分析技术,动态污点分析技术,定理证明等.各类代码审计技术由于都主要采用形式化手段分析软件构架的安全需求,通常都对某种特定场景有较好效果,但实用性较差.在审计linux,xen等大型成熟软件项目时,存在效率低下,误报率高等缺陷,甚至可能根本无法挖掘出有效漏洞.为此通过采用搭配使用各种不同代码审计技术,同时使用一种新的安全属性定义手法,从底层角度定义安全属性,以提升其对软件安全需求描述的准确度,避免其审计缺陷.在保留代码审计技术自动化程度高的优点同时提升其审计效率以及降低误报率,深层次发掘代码脆弱性.     

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

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

Establishing flight software reliability: testing,model checking,constraint-solving,monitoring and learning

In this paper we discuss the application of a range of techniques to the verification of mission-critical flight software at NASA’s Jet Propulsion Laboratory. For this type of application we want to achieve a higher level of confidence than can be achieved through standard software testing. Unfortunately, given the current state of the art, especially when efforts are constrained by the tight deadlines and resource limitations of a flight project, it is not feasible to produce a rigorous formal proof of correctness of even a well-specified stand-alone module such as a file system (much less more tightly coupled or difficult-to-specify modules). This means that we must look for a practical alternative in the area between traditional testing and proof, as we attempt to optimize rigor and coverage. The approaches we describe here are based on testing, model checking, constraint-solving, monitoring, and finite-state machine learning, in addition to static code analysis. The results we have obtained in the domain of file systems are encouraging, and suggest that for more complex properties of programs with complex data structures, it is possibly more beneficial to use constraint solvers to guide and analyze execution (i.e., as in testing, even if performed by a model checking tool) than to translate the program and property into a set of constraints, as in abstraction-based and bounded model checkers. Our experience with non-file-system flight software modules shows that methods even further removed from traditional static formal methods can be assisted by formal approaches, yet readily adopted by test engineers and software developers, even as the key problem shifts from test generation and selection to test evaluation.     

一种新的安全协议形式化分析方法——证据逻辑

形式化分析技术对于安全协议的正确设计至关重要,考虑到现有信仰逻辑分析方法的不足,该文提出一种新的安全协议形式化分析方法——证据逻辑,即通过对协议主体证据的推理来实现安全协议的形式化分析。与现有的方法相比,该方法不仅能够用于认证协议、密钥协商(交换)协议的分析,也能用于电子商务协议的不可否认性和公平性的分析,因此具有更好的通用性和更强的协议分析能力。     

B方法规格说明的构造及应用

B方法是一种软件形式化方法,支持从规格说明到代码生成的整个软件开发周期.本文比较系统地分析了B方法规格说明的构造结构,并结合所设计的实例演示了用B方法编写规格说明的过程,简略地给出了其规格说明的证明义务,并对其规格说明进行了一次精化.     

Applying Formal Methods to a Certifiably Secure Software System

A major problem in verifying the security of code is that the code's large size makes it much too costly to verify in its entirety. This paper describes a novel and practical approach to verifying the security of code which substantially reduces the cost of verification. In this approach, a compact security model containing only information needed to reason about the security properties of interest is constructed and the security properties are represented formally in terms of the model. To reduce the cost of verification, the code to be verified is partitioned into three categories and only the first category, which is less than 10 percent of the code in our application, requires formal verification. The proof of the other two categories is relatively trivial. Our approach was developed to support a common criteria evaluation of the separation kernel of an embedded software system. This paper describes 1) our techniques and theory for verifying the kernel code and 2) the artifacts produced, that is, a top-level specification (TLS), a formal statement of the security property, a mechanized proof that the TLS satisfies the property, the partitioning of the code, and a demonstration that the code conforms to the TLS. This paper also presents the formal basis for the argument that the kernel code conforms to the TLS and consequently satisfies the security property.     

基于模型的开发方法在多应用智能卡中的应用

安全性、可靠性是嵌入式软件的重要性质。为了更好地保证开发的嵌入式软件是可靠和安全的,提出了一种基于模型的开发方法学,包括提炼需求、建立抽象模型及逐层精化三个步骤。首先从环境、功能、性质三个主要方面提取需求,同时明确层次化的精化策略;然后利用形式化方法建立抽象模型并对该模型进行形式化验证,在正确的抽象模型上逐层精化,并对每层模型进行验证;最后,基于满足需求的模型,进一步利用工具完成代码自动生成。该方法从抽象到具体,以逐层递增的方式明确被开发系统的需求及性质,进行形式化建模,通过反馈机制确保模型的正确性及可用性。为了证明该方法学的可行性,文章以多应用智能卡为开发实例,基于Event—B方法及Rodin平台给出了实际建模及证明的过程和结果。     

Building a Quantum Network: How to Optimize Security and Expenses

Quantum key distribution (QKD) is regarded as a key-technology for the upcoming decades. Its practicability has been demonstrated through various experimental implementations. Wide-area QKD networks are a natural next step and should inherit the selling point of provable security. However, most research in QKD focuses on point-to-point connections, leaving end-to-end security to the trustworthiness of intermediate repeater nodes, thus defeating any formal proof of security: why bother outwitting QKD, if the repeater node is an easy prey, and an equally valuable target? We discuss methods of designing QKD networks with provable end-to-end security at provably optimized efforts. We formulate two optimization problems, along with investigations of computational difficulty: First, what is the minimal cost for a desired security? Second, how much security is achievable under given (budget-)constraints? Both problems permit applications of commercial optimization software, so allow taking a step towards an economic implementation of a globally spanning QKD network.     

基于Object—Z的形式化验证方法

定理证明是一种形式化验证技术，也是形式化方法的重要组成部分，它能从形式规格说明中推理出应具备的性质与属性，从而可以对规格说明进行形式验证。Obiect-Z是形式规格说明语言Z的面向对象扩充，基于集合论与数理逻辑，具有严密的逻辑性，适合精确地描述大型软件系统，并且可以对其形式规格说明进行推理。本文首先给出了基于Object—Z规格说明的定理证明验证方法，接着用Object-Z描述了一个电梯操作系统的实例，在此基础上给出了其形式规格说明的定理证明方法来进行形式化验证。