责任政策形式化验证方法
形式化验证：从混成系统到CPS
卜 磊 南京大学 形式化验证：从混成系统到CPS 关键词：形式化验证 混成系统 CPS 混成系统是一种嵌入在物理环境下的实时系统，一般由离散组件和连续组件连接组成，组件之间的行为由计算模型控制。经典混成系统一般分为离散层和连续层，其构成体现了计算机科学和控制理论的交叉。在连续层，通过系统变量对时间的微分方程来描述系统的实际控制操作模型以及系统中参数的演变规律。而在离散层，则通过状态机、佩特里网等高抽象层次模型来描述系统的逻辑控制转换过程。在两层之间通过一定的接口和规则将连续层的信号与离散层的控制模式进行关联和转换。 大多数复杂实时控制系统，都包含连续变化的物理层与离散变化的决策控制层之间的交互过 程，因此混成系统在工业控制和国防等领域大量存在，特别是安全系统，如交通运输、航空航天、医疗卫生、工业控制等。随着在人们生活中的应用越来越广，重要性越来越高，人们对相应系统的质量特别是可信性的需求快速提升，系统失效所带来的灾难也越来越大。在交通运输方面，车 载导航系统的小小失误就可能造成交通事故，而飞机导航系统的失误则可能导致机毁人亡。在国防领域，对软件系统的错误已经进入零容忍度阶段。因此，如何对混成系统进行有效的可信性保 障成为一个亟待解决的问题。 一般而言，测试、仿真[2,3] 等技术是研究和保障软件质量的主要方法。这些方法主要以运行系统为发现问题的主要手段。由于人力无法穷尽地遍历系统所有可能的运行输入和场景，也就不足以保证检测的完备性，这可能会给系统后期运行留下安全隐患。因此，在对系统错误零容忍的安全攸关的系统领域，采用可 证明系统模型正确性的形式化验证理论和技术[4,5]来对系统模型进行安全性验证就显得极为重要，这也成为了相关领域近期的 主要关注点。 混成系统形式化验证 形式化方法 形式化方法(formal method) 混成系统 实时嵌入式系统，特别是复杂的实时控制系统，广泛存在着这样一类子系统：它们行为中的离散化逻辑控制与连续性的时间行为相互依赖，相互影响，彼此互为依存，息息相关。以列车控制系统为例，典型的列车控制系统一般存在多种不同的控制模式以应对当前的车况、路况以及各种突发事件，而系统中的重要参数如列车速度、当前位置、与前车距离等都会随着时间连续发生变化。列车在运行中为了满足特定的时间约束或者调整当前参数的取值而调整列车控制模式。在不同的列车控制模式下，列车中重要参数的变化规律完全不同，对各种事件的响应时间也会有所区别。在类似的这种系统中，逻辑控制与时间行为并不是孤立的两个部分，而是交错地有机结合在一起，构成了一种非常复杂的系统。这种复杂实时系统因其离散控制与实时连续行为混杂叠加的特性，一般被称为混成系统(hybrid system)[1]。
基于Hoare逻辑的密码软件形式化验证系统
基于Hoare 逻辑的密码软件形式化验证系统 郝耀辉郝耀辉，，郭渊博郭渊博，，罗 婷，燕菊维 (解放军信息工程大学电子技术学院，郑州 450004) 摘 要：在Hoare 逻辑理论和ACSL 语法规范的基础上，设计一种针对密码软件的形式化验证系统，由程序规范、验证推理规则、可靠性策略、验证推理等模块组成。以OpenSSL 中RC4算法的软件实现为例，对其功能正确性、保险性和信息流安全性进行验证，结果表明，该系统具有较高的自动化水平，可在一定程度上降低形式化验证方法的复杂度。 关键词关键词：：Hoare 逻辑；密码软件；形式化验证；程序规范；RC4算法 Formal Verification System of Cryptographic Software Based on Hoare Logic HAO Yao-hui, GUO Yuan-bo, LUO Ting, YAN Ju-wei (Institute of Electronic Technology, PLA Information Engineering University, Zhengzhou 450004, China) 【Abstract 】Based on Hoare logic and ANSI/ISO C Specification Language(ACSL) specification, this paper presents a formal verification system for cryptographic software, which is composed of program specification, inference rules, reliability strategy and verification module. It takes the software realization of RC4 algorithm in OpenSSL as an example, the functional correctness, safety properties and information flow security are tested and verified. Results show that this system can reduce the complexity of formal verification method and has a high level of automation. 【Key words 】Hoare logic; cryptographic software; formal verification; program specification; RC4 algorithm DOI: 10.3969/j.issn.1000-3428.2012.03.041 计 算 机 工 程 Computer Engineering 第38卷 第3期 V ol.38 No.3 2012年2月 February 2012 ·安全技术安全技术·· 文章编号文章编号：：1000—3428(2012)03—0121—03 文献标识码文献标识码：：A 中图分类号中图分类号：：TP319 1 概述 密码模块是保障安全系统中信息机密性与完整性的重要 部分，在许多安全系统中，密码模块主要是由密码算法的软 件实现构成，即密码软件部分。这就要求密码软件在向系统 提供安全服务的同时，其自身的安全性也应得到保证。 对此美国国家标准技术局(NIST)和加拿大通信安全局 (CSE)提出CMVP(Cryptographic Module Validation Program) 计划，规定了对安全软件的验证准则DTR [1](Derived Test Requirements)。但CMVP 计划主要依赖验证者的经验，完全 依靠手工完成，存在出错率较高、验证周期长、效率低等缺 点，其时效性和完备性已满足不了实际应用的需求。为此， 本文基于Hoare 逻辑理论，提出一种密码软件的形式化验证 系统。 2 相关知识 本文主要基于Hoare 逻辑原理，依据ACSL(ANSI/ISOC Specification Language)语法规范，对待验证的密码软件添加满足其需要验证的关键特性的前置、后置条件，再用所设计的验证系统对其进行验证。 2.1 Hoare 逻辑 Hoare 逻辑[2]是广泛应用的对命令式语言程序进行推理验证的逻辑系统，其基本思想是在代码段与调用者之间构建一种合同似的规格说明(contracts)，用于描述一段代码执行前后计算机状态的改变情况，由一个前置条件和一个后置条件构成，表示形式为：{Pre}P{Post}，称为Hoare 三元组或断言。其中，Pre 是前置条件，又称初始断言，描述代码段执行前程序状态必须满足的条件，即输入值必须具有的性质；Post 是后置条件，又称终结断言，描述在代码段正确运行后程序 状态所需要满足的条件，即输出值应该具有的性质。 2.2 ACSL 语言 ACSL [3]是一种以注释形式加在程序代码中，专门用于描述程序性质的形式化语言。该语言主要以函数合约(function contract)的形式存在，即要求对任一函数f ，需明确描述清楚函数f 开始时(输入)参数值的要求和结束时(输出)返回值应具有的性质。 其涵义是：若调用函数f 前，前置条件成立，则函数f 执行完后，后置条件也必须成立。其实质和Hoare 三元组表示的内容等同。 2.3 密码软件的关键特性 通过分析密码软件的特性，对保障密码软件安全的至关重要属性进行归纳总结，主要将其归为功能正确性、保险性、信息流安全性3类属性[4]，下面对其进行说明。 2.3.1 功能正确性 主要保证密码软件中程序的执行符合相应的设计规范， 简单的说就是保证程序执行的输入、输出行为和设计规范相 匹配。本系统将其用于验证密码软件输出值是否符合项目输 入值和输出值之间的关系。 2.3.2 保险性 主要指密码软件运行时不引起危险、灾难的能力，本文系统中主要将其用于验证密码软件在开发过程中是否存在缓 基金项目基金项目：：国家“863”计划基金资助项目“基于规范的容忍入侵中 间件关键技术与平台”(2007AA01Z405)；河南省科技创新杰出青年 计划基金资助项目(104100510025) 作者简介作者简介：：郝耀辉(1978－)，女，讲师、硕士，主研方向：信息安全， 密码学，数据库技术；郭渊博，副教授、博士；罗 婷，硕士研究 生；燕菊维，助教、硕士 收稿日期收稿日期：：2011-05-17 E-mail ：hao_yaohui@https://www.wendangku.net/doc/636084222.html,
形式化方法--程序的正确性验证-14
第十四讲形式化方法--程序的正确性验证 一、概述 计算机的程序是一种静态的对象，但它所描述的问题（问题的解）却是一个动态的对象。所谓的程序设计就是用程序设计语言中的语句改变程序中数据对象的状态，构造所描述问题的动态行为。这是不自然的，程序所描述的动态行为也无法直接用程序本身的静态结构进行正确性证明。 形式化规约（formal specification）是需求阶段的形式化说明，是用户需求的严格描述，其一般形式用Hoare逻辑描述[1]如下： ├{Φ}P{Ψ} <1> 其中Φ和Ψ分别表示初始和结束断言条件，其含义是：“假如初始状态d I满足条件Φ，那么程序结束并且终结状态d f必须满足Ψ”。 设D＝D1×……×D n为程序P的状态空间，其中，D j(j=1,……,n)表示程序中数据对象的值域。显然，由Φ和Ψ断言条件所确定的合法初始和结束状态的集合是D的一个子集。 执行函数E：Φ×P→Ψ定义如下： 无定义对合法的初始状态d i，程序P不结束 E（P,d I）= 终结状态d f对合法的初始状态d i，程序P结束 程序的正确性即为： ├{Φ}P{Ψ} iff <2> ?d i(├Φ(d i)→(├程序P结束 and ├Ψ(E(P,d i)))) 总地来讲，验证一个程序的正确与否有两种办法，一种是程序的测试，另一种是程序的正确性证明。 1．程序的测试与程序的验证 对给定的一个合法的初始状态d i，当程序执行结束时其终结状态为d f，那么，Φ(d i)和Ψ(d f)都应该被满足。这一点可用下式表示： {d i}P{d f} <3> 所谓程序的测试就是验证测试用例{d i}P{d f}，即验证程序对d i的执行结果是否为d f。由于合理的初始状态是无限的，因此，对程序验证来讲，测试不是一个完备的方法。测试被认为是一种尽量发现错误，但并不能保证程序中没有错误[2]的方法。对大数应用来讲，它是可满足的；但对有些应用来讲，测试是一种不能满足的验证方法，例如：航空、航天等领域的软件系统。 显然，对要求绝对正确的软件，测试是一种不能采用的方法。无论白盒测试还是黑盒测试都是在无限集合{(d i,d f)|?d i,?d f, d i和d f满足{d i}P{d f}中选择有限的一些(d i,d f)对进行验证，而各种测试方法只是选择(d i,d f)的策略不同而已。 因此，验证程序是否完全正确要寻求另外的解决途径。那就是程序的正确性验证。 2．形式语义与程序的正确性验证 程序的正确性验证应该具有严密的推量过程，以保证程序每步执行结果都是希望的结果，而与程序执行的某个初始状态无关。程序的正确性证明现有三种方式：操作语义、指称
软件需求的形式化转换模型
第３３卷砌厶３．拿第５期 Ｎｏ．５ 计算机工程 ＣｏｍｐｕｔｅｒＥｎｇｉｎｅｅｒｉｎｇ ２００７年３月 Ｍａｒｃｈ２∞７ ?软件技术与数据库?文章■号ｔ１０００—３４２８（２００７）０５－－－００７３－－０３文■标识码。Ａ中田分类号：］］］ｒ３１１软件需求的形式化转换模型 侯膏珍，蔡小娟，簟恒啊 （上海交通大学计算机科学与工程系，上海２００２４０） ■要：需求规范错误是软件设计错误的一大类。该文提出了一个软件需求的形式化转换模型，用来将软件需求分析直接、自动地转换为形式化描述，为需求验证提供帮助，避免软件在需求规范上可能产生的错误。 关ｔ嗣：软件需求；形式化转换；软件可靠性 Ｄｉｇｅｓｔｉｏｎ－ｂａｓｅｄＳｏｆｔｗａｒｅＦｏｒｍａｌＴｒａｎｓｆｏｒｍａｔｉｏｎ Ｍｏｄｅｌ ＨＯＵＬｉｚｈｅｎ，ＣＡＩＸｉａｏｊｕａｎ，ＺＯＵＨｅｎｇｍｉｎｇ （ＤｅｐａｒｔｍｅｎｔｏｆＣｏｍｐｕｔｅｒＳｃｉｅｎｃｅａｎｄＥｎｇｉｎｅｅｒｉｎｇ，ＳｈａｎｇｈａｉＪｉａｏｔｏｎｇＵｎｉｖｅｒｓｉｔｙ，Ｓｈａｎｇｈａｉ２００２４０） ［Ａｂｓｔｒａｃｔ］Ｒｅｑｕｉｒｅｍｅｎｔｓｐｅｃｉｆｉｃａｔｉｏｎｆａｕｌｔｉｓｏｎｅｋｉｎｄｏｆｓｏｆｔｗａｒｅｄｅｓｉｇｎｆａｕｌｔｓ．Ｔｈｉｓｐａｐｅｒｐｒｅｓｅｎｔｓａｄｉｇｅｓｔｉｏｎ—ｂａｓｅｄｓｏｆｔｗａｒｅｆｏｒｍａｌｔｒａｎｓｆｏｒｍａｔｉｏｎｍｏｄｅｌｔｈａｔｅｌｉｍｉｎａｔｅｓｔｈｅｗｅａｋｌｉｎｋｅｘｉｓｔｉｎｇｉｎｔｏｄａｙ’Ｓｓｏｆｔｗａｒｅｆｏｒｍａｌｍｅｔｈｏｄａｐｐｒｏａｃｈ，ａｎｄａｕｔｏｍａｔｉｃａｌｌｙｔｒａｎｓｆｏｒｍｎａｔｕｒａｌｌａｎｇｕａｇｅ—ｂａｓｅｄｒｅｑｕｉｒｅｍｅｎｔｉｎｔｏ ｆｏｒｍａｌｒｅｐｒｅｓｅｎｔａｔｉｏｎ． ［ＫｅｙｗｏｒｄｓｌＳｏｆｔｗａｒｅｒｅｑｕｉｒｅｍｅｎｔ；Ｆｏｒｍａｌｔｒａｎｓｆｏｒｍａｔｉｏｎ；Ｓｏｆｔｗａｒｅｒｅｌｉａｂｉｌｉｔｙ 在当今信息社会，软件故障造成的各种损失触目惊心。轻则丧财损物，重则直接对人的生命造成威胁。因此，构建可靠软件系统一直是国内外学术机构和信息工业界的一个非常突出和重要的研究课题。 目前高可靠软件系统的研究涵盖在软件工程的领域内，主要研究如何在软件的设计、开发、和实现过程中保持软件的可靠性以达到预先规定的可靠性标准¨’２ｊ。软件之所以存在着这样那样的不可靠性，根本原因是软件在很大程度上作为一门艺术而不是科学被学习和研究，即软件本身的设计因人不同而不同（即程序的构建方式、分拆和编码不同，而不是软件所要完成的功能不同）。 在具体表现上，软件设计的错误可以分为４个方面，即需求规范错误、运行环境错误、模块衔接错误和代码编写错误。本文针对上述４个方面中的一个进行研究，提出了一个软件需求的形式化转换¨。１模型，将软件需求分析直接、自动地转换为形式化描述，从而为需求验证提供帮助，消除软件在需求规范上可能产生的错误。 人们从自然界中食物消化过程中得到了一些启示。食物需要经过一系列步骤才能转化为被人体吸收的营养物质。类似地，软件需求需要经过一系列步骤转化为机器可识别的语言。通过研究和比较这两种过程（消化过程和需求转化过程），抽象出一种形式化转换模型。该模型不仅能提高软件需求转换的可靠性，同时能减轻系统设计人员的工作。 ｌ软件需求的形式化模墼 首先看一下食物消化的过程№Ｊ。食物转化为营养物质，包括以下几个步骤：首先，食物在口腔中被咀嚼，成为较小的食物颗粒。然后，这些较小的食物颗粒被送到胃器官并与胃中的胃酸发生化学反应成为更为细小的食物颗粒。这些小颗粒被送入肠道，由肠道中的微生物（在一系列反应规则下）将它们转化为营养物质。这就完成了一次消化过程。 软件需求的转化与之类似。由自然语言描述的软件需求要被转化为机器可识别的形式，类比于消化过程中胃和肠道，软件形式化转换模型也分为两部分：咀嚼编译器和消化编译器。咀嚼编译器将用自然语言表述的软件需求转化为需求颗粒（半形式化描述）；而消化编译器则进一步把需求颗粒转化为形式化表述。 这种两阶段方式使得整个转换过程容易控制。特别是，咀嚼编译器的工作是将软件需求划分为更小的颗粒，并且将发现的任何问题反馈给用户以便修改。咀嚼编译器产生的任何软件需求小颗粒由消化编译器转化为完全的形式化表述。任何没有正确转换的部分都被退回给用户以供修改。图１描述了这个模型。 圈１软件■求形式化转换过程模型 需求形式化转换过程划分为３个状态：用自然语言表述软件需求的非形式化状态；用伪规则表示的半形式化状态；用形式化语言表述软件需求的形式化状态。软件需求转换过程从初始的非形式化状态开始，以最后的形式化状态终结。显而易见整个转换过程可以用一个带有概率转移矩阵的有限作者骱：侯丽珍（１９８３－－），女，硕士生，主研方向：软件可靠性及数据恢复技术；蔡小娟，博士生；邹恒明，博士 收藕日期：２００６—０３—２８Ｅ－ｍａｉｌ：ｈｌｚ＠ｓｊｔｕ．ｅｄｕ．ｃａ —－７３— 万方数据
形式化验证笔记
形式化验证笔记 2.2 形式化方法简介 形式化方法是一类基于数学的用于精确化规范说明、开发和验证软件和硬件 系统的多种方法的总称[28]。对软件和硬件设计使用形式化方法是为了通过利用适当的数学分析方法，来保证设计的正确性、可靠性和健壮性。形式化方法一般可以分为形式化规范说明(Formal Specification)和形式化验证(Formal Verification)两大类。其中形式化验证又可分为定理证明(Theorem Proving)、模型检测(Model Checking)和自动测试用例生成(Automated Test Case Generation)三类。其中定理证明也称演绎验证(Deductive Verification)。本文中采用的形式化验证方法属于定理证明的范畴。 下面简要介绍一下这三种形式化验证技术: , 模型检测:模型检测是一种通过对目标系统建立一个有限的模型，并在模型发生改变时，检测某系统属性(如安全性和活性)在该模型中是否保持的技术。从本质上讲，模型检测技术就是穷尽地对状态空间搜索，并通过模型的有限性来保证该搜索过程一定会终止。最初模型检测应用在硬件和协议验证领域，大为成功，后来在软件系统的验证上也得到了广泛应用。 , 定理证明:定理证明是一种用某种数学逻辑公式来表达系统及其属性的技术，该数学逻辑公式被定义为一个形式化系统，包含一系列系统公理、已证明的定理及其推论，定理证明的本质就是基于该形式化系统，找到某属性的一个证明的过程。定理证明通常被应用于对软硬件系统重要属性的机械化验证。与模型检测的不同是，定理证明一般是需要人辅助来交互地完成证明的，而模型检测可以达到完全的自动化。由于使用了结构归纳(Structural Induction)等技术，定理
概率论的形式化验证
简介： 软硬件系统通常存在一些随机或不可预测的因素。由于这些随机组件,建立在任何情况下系统的正确性通常特别昂贵，工程的方法是使用概率分析来分析这些带有随机性和不确定性但又不可避免的元件的系统。 传统上，计算机仿真技术被用来执行概率分析。然而,他们给不出精确的结果,并且由于其巨大的计算机处理时间要求而不能处理大规模问题。为克服仿真技术的精度问题，一种解决方案是用高阶逻辑定理验证进行概率分析。 高阶逻辑是一个用精确语义进行推理的系统，它具有足够的表达力以至于能够规范几乎所有经典的数学理论。 对于要形式化的随机变量和任何类型的系统属性（包括概率属性和统计属性）,只要他们能在一个封闭的数学形式中表达，就可以利用高阶逻辑对其行为进行精确建模。 进行基于定理证明的概率分析最重要的标准是能够形式化基础数学理论——测度理论、概率论和勒贝格积分。 最近几年，三个基本理论大部分已在高阶逻辑中形式化。但是前人的工作均有局限性，例如,已形式化的主要测度理论不允许定义在任意拓扑空间中的随机变量的操作；概率论主要不允许我们使用随机变量之和作为随机变量本身。 本文提出一种广义的测度理论、概率理论和勒贝格积分的形式化,以利用他们的全部潜力去形式化概率分析系统。用布莱尔代数的广义形式化扩展测度理论。 证明可测的实值函数的重要性质，使用它们来定义实值随机变量并证明其属性。我们也形式化了独立随机变量的概念并验证了独立随机变量的关键属性。此外,我们证明了勒贝格积分的重要属性用它来定义随机变量的统计特性（期望和方差等）。这些都是目前不存在的。 概率论形式化一些可能应用包括验证安全协议和通信系统 Nedzusiak and Bialas在HOL中形式化了一些测度和概率理论，奠定了概率论分析在HOL中的早期基础。 Hurd构造了概率空间的定义和函数，发展了测度理论在HOL中的形式化。甚至连期望方差的基本概念都没有。 基于Hurd 的工作，Richter在Isabelle/HOL中形式化了测度理论。Richter定义的Borel集是间隔产生的，本文提出的Borel 代数是在开集上产生的，更具广泛性，能被应用到任意度量空间（复数，Rn）(不只是实数空间)。 Coble推广了Hurd的测度理论的形式化，基于此形式化了Lebesgue积分理论。但是他只证明了对于简单正函数的Lebesgue积分性质。 Hasan在上述前人的工作上来验证一些常用的离散或连续随机变量的概率属性和统计属性。展示了概率分析的形式化的实用性继承了缺陷 Lester在PVS中形式化了测度理论和积分理论，但是没有证明Lebesgue积分的性质和收敛定理。
软件形式化方法-模拟题-3
学习中心_________ 姓名_____________ 学号 西安电子科技大学网络教育学院 模拟试题三 《软件形式化方法》期末考试试题 （120分钟） 题号一二三四五六七总分 题分 得分 一、填空题。（20分） 1. 软件危机是指在计算机软件的过程中所遇到的一系列严重的问题，应对软件危机的方式分为两种方法：和。对于软件开发组织和管理的规范化方法中，主要研究、和三个要素。 2. 形式化方法研究如何把（具有清晰数学基础的）（描述形式、技术和过程等）融入软件开发的各个阶段；包括、形式化验证和程序精化三种活动。形式化验证主要技术包含和；程序精化是将与相结合，研究从抽象的推演出具体的面向计算机的。 3. 模式是Z语言规格中一个重要的元素，模式是由、和 组成。 4. Larch方法是软件系统规格的一种；Larch方法的程序规格包括和与目标语言相关的两个部分。 二、利用有限状态机描述“AB协议”。（15分） AB协议包含发送端和接收端两个实体。发送端协议实体从发送方用户获取一个报文，将序号寄存器值赋给报文，然后向接收端协议实体发出报文，发送方发出报文之后启动超时时钟，等待认可报文。如果在给定的时间内未收到认可报文，则重发报文；如果收到认可报文，其序号与发出报文序号相同，则发送端实体从发送方用户获取下个报文。接收端协议实体在收到报文之后，如果报文无错误，则想发送端实体发送认可报文，然后将报文递交给接收方用户；如果接收的报文有错误或者序号不正确，则丢失报文。假定所用通道不会中断；报文重复n次后最终能够被接收；认可报文只要发出就能正确收到；报文不会损坏；序号寄存器初始化为0 。 三、构造下图所示Petri网的覆盖树。（10分） 四、利用CSP对“生产者-消费者”系统进行规格。（10分） 五、逻辑演算证明。（15分） （1）?(Q∨R) ∧(P?Q)├?P （2）(P?(Q?S)) ∧ (?R∨P) ∧Q├ R→S （3）($x)P(x)?("x)(P(x)úQ(x)?R(x)), ($x)P(x), ($x)Q(x)├ R(a)ùR(c) 六、如图中所示的Kripke结构，利用标号算法对公式进行模型检验。（15） （1）E((p ∧r) ?p) （2）A(p?q) = ?E(?(p?q))
计算机系统形式化验证中的模型检测方法综述论文.doc
面临的挑战和未来发展方向等问题。 2 模型检测及相关技术 模型检测方法最初由Clarke，Emerson等人于1981年提出，因其自动化高效等特点，在过去的几十年里被广泛用于实时系统、概率系统和量子等多个领域。模型检测基本要素有系统模型和系统需满足的属性，其中属性被描述成时态逻辑公式Φ。检测系统模型是否满足时态逻辑公式Φ，如果满足则返回“是”，不满足则返回“否”及其错误路径或反例。时态逻辑主要有线性时态逻辑LTL(Linear TemporalLogic)和计算树逻辑CTL(Computation Tree Logic)。 2.1 线性时态逻辑 对一个系统进行检测，重要的是对系统状态正确性要求的形式化，其中一个基本维度是时间，同时需要知道检验结果与时间维度的关系。使用线性时态逻辑(LTL)来描述系统，可以使得系统更容易被理解，证明过程更加直截了当。LTL公式是一种线性时态逻辑。它在表示授权约束时，定义了无限的未来和过去，这样扩展了常用语义，并且保证了证明中判定的结果在各个时间点中都是成立的。LTL公式用逻辑连接符和时态算子表达系统运行时状态之间的关系。LTL的逻辑连接符包括：∧(与)，∨(或)，—|(非)，→(逻辑包含)，←→(逻辑对等)。时态算子包括：G(Globally)，U(Until)，F(Future)，X(neXt-time)。LTL模型检测验证系统状态转换模型是否满足属性，使用可满足性判定，即为检测系统模型M 中是否存在从某个状态出发的并满足LTL公式—|Φ的路径，如果所有路径都满足LTL公式Φ则不存在有路
径满足—|Φ。使用LTL公式也有一定的局限性，LTL公式只能包括全称量词，对于混用了全称和存在量词的性质，一般无法用这种方法进行模型检测。 2.2 计算树逻辑 计算树即为通过将迁移系统M 某一状态作为根，将M 用树形结构展开表示出来，CTL使用路径量词(包括：A(All)，E(Exist))和时态算子(包括F，G，X，U)对计算树属性进行形式化的描述，表示出系统的状态变化以及状态的分枝情况。LTL的时间定义是与路径相关的，每个时刻只有唯一的一个后继状态。LTL可用于有重点的选择感兴趣的路径分析，并且LTL可以表达公平概念而CTL不能。但是对于一些复杂属性，如每个计算总是可能返回到初始状态，LTL将无法描述，但是CTL可以。CTL的时间定义是与状态相关的，每个状态都有多个可能的后继状态，从一个给定的状态量化分离出路径，能够断言行为的存在。CTL可以用路径量词E，而LTL不可以;CTL公式使用路径量词A时与LTL公式表达内容可以相同。LTL和CTL各有优势，Emerson等人提出扩展的时间逻辑CTL，提供了一种统一的框架，包含了LTL和CTL，但是可满足性判定代价较高。 2.3 模型检测工具 模型检测因其自动化、高效等特点得到广泛应用，各类模型检测工具也层出不穷。以下是几类典型的模型检测工具。SPIN 是1980年美国贝尔实验室开发的模型检测工具，主要关心系统进程间的交互问题。它以promela为建模语言，以LTL为系统属性的逻辑描述语言，支持on-the-fly技术，可以根据用户的需要
四川大学软件系统形式化验证(双语)Software System Model Checking教学大纲
College of Software Engineering Undergraduate Course Syllabus Course ID 311031020 Course Name Software System Model Checking Course Attribute □Compulsory ■Selective Course Language ■English □Chinese Credit Hour 2 Period 32 Semester □First Fall □First Spring □Second Fall □Second Spring ■Third Fall □Third Spring □Fourth Fall □Fourth Spring Instructors Song Xiaoyu Description Today, software systems are widely used in applications where failure is unacceptable. Because of the success of the Internet and embedded systems in automobiles, airplanes, and other safety critical systems, we are likely to become even more dependent on the proper functioning of computing devices in the future. Due to this rapid growth in technology, it will become more important to develop methods that increase our confidence in the correctness of such systems. Traditional verification techniques use simulators with handcrafted or random test vectors to validate the design. Unfortunately, generating test vectors is very labor-intensive. The overall complexity of the designed systems implies that simulation cannot remain the sole means of design verification, and one must look at alternative methods to complement simulation. Recent years have brought about the development of powerful formal verification tools for verifying of software systems. By now, the information technology industry has realized the impact and importance of such tools in their own design and implementation processes. The objective of the course is to introduce the participants to the practical formal verification techniques for hardware/software systems that are beginning to penetrate industrial applications. Topics to be covered include: system modeling, formal logics for system verification (Boolean & first-order logic, higher-order logic, temporal logic), formal specifications, CTL model checking, BDDs, applications of theorem proving systems, and SA T solvers. Exercises are provided in the class. Prerequisites Software and Hardware Systems, Discrete Mathematics. Any senior or graduate student in ECE and CS is welcome to take this course. T extbook E. Clark, O. Grumberg, D. Peled, "Model Checking", MIT Press, 2000. Resource Lecture notes. Grading Assignments, attendance rate (40%) and final exam (60%) T opics Introduction to verification technology. Understand the basic notions of correctness Introduction to formal logics. Understand the basic notions for logics, proofs, specifications. System modeling. Understand the importance of system modeling and specification. Temporal logics. Understand the basic notions of temporal logics. Temporal Logic and Modeling Checking. Understand the extension of CTL, CTL*, etc. Modeling Checking with fixpoint computation. Boolean representations. Find a canonical Boolean representation, etc. Symbolic verification based on BDD and SA T. Symbolic Simulation, BMC Theorem proving systems. L TL model checking, Buchi automata, Omega- automata, etc.
形式化验证操作系统
形式化验证seL4操作系统 王俊超 摘要：完全的形式化验证是确保系统不会出现编程和设计错误的唯一方法。本文假设编译器，汇编代码和硬件层都是正确的，在此基础之上介绍了对seL4内核从抽象规约层到C语言实现层的形式化机器验证。目前为止，seL4是第一个经过形式化验证并证明功能正确性的完整的通用的操作系统内核。这里所指的功能性是说实现总是严格的满足上一抽象层内核行为的规约。本文证明了seL4操作系统在任何情况下都不会崩溃以及执行不安全的操作，更重要的是，可以精确的推断出seL4在所有情况下的行为。 关键词：seL4；形式化验证；操作系统 1.引言 操作系统的可靠性和安全性几乎与计算机系统等价，因为内核可以在处理器的最高权限上工作，可以随意的访问硬件。因此，操作系统内核实现出现的任何一个微小的错误都会导致整个计算机系统的崩溃。 为了保证操作系统的安全性，传统的一些做法有减少高权限的代码的数量，从而避免bug出现在较高的权限层内。那么，如果代码的数量较少，便可以通过形式化的机器验证方法来证明内核的实现满足规约，并且在实现时不会有程序员由于编码引入的实现漏洞。 本文通过机器检验的形式化证明验证了seL4的功能正确性，目前，seL4所能达到的功能如下： 能够在现实生活中使用，并且其性能与当前性能最好的微内核相当；其行为在抽象层进行了精确的规约；其形式化设计用来证明一些需要的属性比如中断等的安全性；其实现满足规约；访问控制机制能够保证高强度的安全性。 目前，seL4是第一个被完全形式化验证其功能正确性的操作系统内核，所以，它是一个前所未有的具有高度安全性和可靠性的底层系统级平台。 在本文所描述的功能正确性要比模型检验、静态分析以及采用类型安全编程语言实现的内核要强的多。本文不仅对内核的规约层面进行了分析，同时也对于内核的精细的行为进行了规约和验证。 此外，本文还创立了一套融合了传统操作系统研发技术和形式化方法技术，用来快速实现内核设计与实现的方法学，经过实践证明，利用这套方法学开发出的操作系统不仅在安全性上有着充分的保障，在性能上也不会受到影响。 2.研究现状 UCLA Secure Unix和Provably Secure Operating System (PSOS)在十九世纪七十年代末第一次尝试着来验证操作系统内核。本文借鉴了UCLA的功能正确性的验证思路。UCLA项目完成了90%的规约和20%的验证，最终得出了不变式的推理占据了证明的大部分时间，在本文的项目中这一点也得到了证实。 PSOS主要关注于内核设计的形式化验证，然而，却从来没有完成过大量的实现证明。他们的设计方法学被Ford Aerospace的Kernelized Secure Operating System (KSOS) 、Secure Ada Target(SAT)以及Logical Coprocessor Kernel (LOCK)所采用。 第一个实际的完整的证明是由KIT实现的。然而，其实现针对的对象是一个高度理想化的操作系统内核，并不能在实际的机器上运行。 Bevier和Smith随后将Mach的内核进行了形式化，但是并没有提供其实现的证明。其他的一些关于操作系统内核的形式化建模和证明都没有在实现层进行验证，包括EROS内核，基于FLASK的SELinux内核等。
形式化分析方法
安全协议的形式化分析方法 安全协议是采用密码技术来保障通信各方之间安全交换信息的一个规则序列。其目的是在通信各方之间提供认证或为新的会话分配会话密钥。尽管现有的安全协议是安全专家精心设计和详细审核过的但仍然可能存在一些不易发现的安全缺陷有些甚至数年后才被发现。长期以来，形式化方法被公认为分析安全协议的有力武器。 目前分析安全协议的形式化方法主要有： （1）推理构造法，该方法基于知识和信念推理的模态逻辑，如K3P逻辑等，但K3P逻辑只能分析协议的认证性质而不能分析协议的保密性质； （2）攻击构造法，该方法从协议的初始状态开始，对合法主体和一个攻击者所有可能的执行路径进行穷尽搜索，以期找到协议可能存在的错误。这种方法主要有基于模型检测技术的模型检测器QRS( 验证语言、代数简化理论模型以及特定专家系统（如特殊目的NRL分析器和Interrogator），但这种方法无法解决状态空间爆炸问题； （3）证明构造法，该方法集成了以上两类方法的思想及多种技术，主要有Bolignano证明方法和Paulson方法等。以上形式化分析方法的主要缺点是无法解决状态空间爆炸问题在很大程度上被限制在规模很小的协议分析中这显然不适应网络通信规模日益增大等发展的需要。 安全协议是建造网络安全环境的重要基石，是保证网络安全的核心技术。设计和证明安全协议自身的正确性和安全性，成为网络安全的基础。形式化分析方法已被证明是用于分析、设计和验证安全协议的重要方法，对安全协议的形式化分析、设计和验证已经成为当今形式化分析研究领域的一个热点问题。 虽然人们使用形式化分析方法已成功发现了许多现存安全协议存在的缺陷和针对她们的攻击，但是这些分析方法还存在许多缺陷。有些形式化分析方法自身不太完善，存在一定的局限性，不能分析和验证某些类型安全协议的安全性；有些只能分析安全协议的不安全性，不能给出协议安全性的精确证明。 在总结安全协议现存各种缺陷的基础上，根据缺陷产生各种原因将缺陷分为：过小保护缺陷、消息可重放缺陷、消息不可达性缺陷、并行会话缺陷和其他类型缺陷等五类。同时把针对安全协议的各种攻击方法可分为：重放消息型攻击、猜
计算机系统形式化验证中的模型检测方法综述
计算机系统形式化验证中的模型检测方法 综述 1 形式化方法概述 形式化方法是用数学和逻辑的方法来描述和验证系统设计是否满足需求。它将系统属性和系统行为定义在抽象层次上，以形式化的规范语言去描述系统。形式化的描述语言有多种，如一阶逻辑，Z语言，时序逻辑等。采用形式化方法可以有效提高系统的安全性、一致性和正确性，帮助分析复杂系统并且及早发现错误。形式化验证是保证系统正确性的重要方法，主要包括以数学、逻辑推理为基础的演绎验证(deductive verification)和以穷举状态为基础的模型检测(model checking)。演绎验证是基于人工数学来证明系统模型的正确性。它利用逻辑公式来描述系统，通过定理或证明规则来证明系统的某些性质。演绎验证既可以处理有限状态系统，又可以解决无限状态问题。但是演绎验证的过程一般为定理证明器辅助，人工参与，无法做到完全自动化，推导过程复杂，工作量大，效率低，不能适用于大型的复杂系统，因而适用范围较窄。常见的演绎验证工具有HOL，ACL2，PVS 和TLV等。模型检测主要应用于验证并发的状态转换系统，通过遍历系统的状态空间，对有限状态系统进行全自动验证，快速高效地验证出系统是否满足其设计期望。下面将主要介绍模型检测方法的发展历史和研究现状，以及当前面临的挑战和未来发展方向等问题。 2 模型检测及相关技术
模型检测方法最初由Clarke，Emerson等人于1981年提出，因其自动化高效等特点，在过去的几十年里被广泛用于实时系统、概率系统和量子等多个领域。模型检测基本要素有系统模型和系统需满足的属性，其中属性被描述成时态逻辑公式。检测系统模型是否满足时态逻辑公式，如果满足则返回是，不满足则返回否及其错误路径或反例。时态逻辑主要有线性时态逻辑LTL(Linear TemporalLogic)和计算树逻辑CTL(Computation Tree Logic)。 2.1 线性时态逻辑 对一个系统进行检测，重要的是对系统状态正确性要求的形式化，其中一个基本维度是时间，同时需要知道检验结果与时间维度的关系。使用线性时态逻辑(LTL)来描述系统，可以使得系统更容易被理解，证明过程更加直截了当。LTL公式是一种线性时态逻辑。它在表示授权约束时，定义了无限的未来和过去，这样扩展了常用语义，并且保证了证明中判定的结果在各个时间点中都是成立的。LTL公式用逻辑连接符和时态算子表达系统运行时状态之间的关系。LTL的逻辑连接符包括：(与)， (或)，|(非)，(逻辑包含)，(逻辑对等)。时态算子包括：G(Globally)，U(Until)，F(Future)，X(neXt-time)。LTL模型检测验证系统状态转换模型是否满足属性，使用可满足性判定，即为检测系统模型M 中是否存在从某个状态出发的并满足LTL公式| 的路径，如果所有路径都满足LTL公式则不存在有路径满足|。使用LTL公式也有一定的局限性，LTL公式只能包括全称量词，对于混用了全称和存在量词的性质，一般无法用这种方法进行模型检测。
关于形式化方法与软件可靠性
形式化方法与软件可靠性 作者：郭洋 摘要：形式化方法是一种基于数学的表示方法。它能帮助发现其它方法不容易发现的系统描述的不一致，不明确或不完整，有助于增加软件开发人员对系统的理解，因此形式化表示方法是提高软件系统，特别是提高安全苛刻系统的安全性与可靠性的重要手段。软件测试作为提高软件可靠性的一种形式化方法，在不同层次不同阶段可采取不同的方式方法。测试覆盖准则是判断测试充分性的重要手段。 关键词：形式化方法；软件；可靠性；软件测试；测试覆盖 形式化表示方法的出发点是数学逻辑方法。其目的是开发可靠的软件产品。以目前常用软件开发方法为出发点，主要研究怎样将这些方法形式化，使软件系统的描述更精确化，以减少可能的误解所带来的问题；或以目前常用的软件开发过程为出发点，研究怎样在软件开发过程中增加一些形式化方法的应用，以提高软件的可靠性。 1 什么是形式化方法 形式化方法是描述系统性质的基于数学的技术。这样的形式化方法提供了一个框架，人们可以在框架中以系统的而不是特别的方式刻划、开发和验证系统。如果一个方法有良好的数学基础，那么它是形式化的，典型地以形式化规约语言给出的。这个基础提供一系列精确定义的概念，如一致性和完整性，以及更进一
步，定义规约、实现和正确性。 形式化方法的一个重要研究内容是形式规约，它是对程序“做什么”的数学描述，是用具有精确语义的形式语言书写的程序功能描述，它是设计和编制程序的出发点，也是验证程序是否正确的依据。对形式规约通常要讨论其一致性和完备性等性质。形式规约的方法主要可分为两类：一类是面向模型的方法也称为系统建模，该方法通过构造系统的计算模型来刻画系统的不同行为特征；另一类是面向性质的方法也称为性质描述，该方法通过定义系统必须满足的一些性质来描述一个系统。不同的形式规约方法要求不同的形式规约语言，即用于书写形式规约的语言，如代数语言One/Two等；进程代数语言；时序逻辑语言等；这些规约语言由于基于不同的数学理论及规约方法，因而也千差万别，但它们有一个共同的特点，即每种规约语言均由基本成分和构造成分两部分构成。前者用来描述基本规约，后者把基本部分组合成大规约。构造成分是形式规约研究和设计的重点，也是衡量规约语言优劣的主要依据。 形式化方法的分类：（1）根据说明目标软件系统的方式，形式化方法可以分为面向模型的形式化方法和面向属性的形式化方法。（2）根据表达能力，形式化方法可以划分为基于模型的方法、基于逻辑的方法、代数方法、过程代数方法、基于网络的方法。 2 软件可靠性的定义 软件可靠性是软件系统固有特性之一，它表明了一个软件系统按照用户的要求和设计的目标，执行其功能的正确程度。软件可靠性与软件缺陷有关，也与系统输入和系统使用有关。理论上说，可靠的软件系统应该是正确、完整、一致和健壮的。但是实际上任何软件都不可能达到百分之百的正确，而且也无法精确度