BLP改进模型的形式化描述及自动化验证

在《信息安全技术操作系统安全技术要求》中,提出访问验证保护级安全操作系统的研发过程需要完全形式化的安全策略模型。针对该情况,对经典的数据机密性BLP模型进行相应改进,为系统中的主客体引入多级安全标签以及安全迁移规则,使其满足实际系统开发的需求。运用完全形式化的方法对改进模型的状态、不变量、迁移规则等进行描述,使用Isabelle定理证明器证明了迁移规则对模型的不变量保持性,从而实现对模型正确性的自动形式化验证,并保证了模型的可靠性。     

数据库管理系统强制访问控制形式化分析与明证

强制访问控制是保护数据库管理系统安全的有效机制.DMOSMAC是一个依赖于安全操作系统实现强制访问控制机制的数据库管理系统.在分析该系统实现的基础上,对该系统进行了形式化分析.给出了信息流的概念,将信息流集合作为被验证系统状态的一部分.信息流集合始终是一个递增的集合,利用信息集合流可防止删除等操作的证明被绕过的可能,保证验证过程的严密性.在信息流的基础上提出了一种对系统代码进行抽象、抽取的形式化分析方法.即抽象DMOSMAC系统状态,从源代码中提取操作规则,将BLP模型中的状态、访问规则分别与DMOSMAC系统的状态、操作规则建立映射关系,BLP模型中简单安全性和*-特性转换为面向信息流的状态不变式,继承BLP模型的相关安全公理和定理进行分析和证明;最后用定理证明器COQ进行安全性证明的方法.     

操作系统对象语义模型(OSOSM)及形式化验证

操作系统的复杂性使得其安全性问题日益突出.有不少的研究工作采用形式化的方式对现有的操作系统进行了正确性的验证,这些工作主要是采用程序形式逻辑验证代码级的功能实现性.从系统设计的角度,以高阶逻辑和类型论为基础,提出了操作系统对象语义模型(OSOSM).OSOSM采用分层结构,包括基本功效层、实现层和优化层.OSOSM将操作系统中的行为主体和资源抽象为操作系统对象,建立操作系统的论域,利用以操作系统对象变元集合为定义域到论域的映射表示操作系统的状态,描述操作系统系统调用等行为的语义,使用逻辑系统的谓词公式表达操作系统的安全属性,给出如何验证操作系统在运行过程中保持安全策略和属性的形式化描述方法.以实现并经过形式化验证的可信操作系统(VTOS)为例,阐述OSOSM的语义正确性.使用Isabelle定理证明工具验证设计和安全需求的一致性,以说明VTOS具有预期的安全属性.     

操作系统安全结构框架中应用类通信安全模型的研究

经典的BLP模型是解决保密性问题的理论基础,Biba模型是一种简明易实现的完整性模型．在应用系统中数据的共享和安全是一对矛盾．在将应用系统抽象为应用类的基础上,引入完整性规则集代表信息的可信度,结合BLP模型和Biba模型构造了一种应用类通信的安全模型,并给出了模型的形式化描述和正确性证明．应用类通信安全模型不仅解决了保密性问题,而且解决了完整性问题．以支持B／S文电传输应用系统的安全为例,给出了在操作系统中实现应用类通信安全模型的方法,分析了模型实现的有效性．     

Isabelle在分析安全操作系统状态机模型中的应用

为了解决已有的状态机模型的形式化框架在分析安全操作系统状态机模型时不够直观、简洁的问题,提出了一套使用Isabelle工具对安全操作系统模型状态中的类型、变量、常量、关系、映射、函数,以及模型中的安全不变量和状态迁移规则进行形式化描述的新方法.通过实际验证一种典型的安全操作系统状态机模型--可信进程模型,总结出了有效地使用Isabelle辅助形式化设计、分析、验证模型的策略.     

安全协议认证的形式化方法研究

安全协议认证是网络安全领域中重大课题之一。形式化方法多种多样。该文首先论述了模型检测技术及其在安全协议验证中的应用,然后介绍了各种定理证明方法和定理证明工具,接着讨论其它形式化验证方法,最后论述形式化方法的一些研究方向。     

操作系统形式化设计与安全需求的一致性验证研究

采用数学形式化方法对操作系统进行设计和验证可以保证系统的高度安全性.目前已有的操作系统形式化研究工作主要是验证系统的实现在代码级的程序正确性.提出一种操作系统形式化设计和验证的方法,采用操作系统对象语义模型(OSOSM)对系统的设计进行形式化建模,使用带有时序逻辑的高阶逻辑对操作系统的安全需求进行分析和定义.对象语义模型作为系统设计和形式化验证的联系.以实现和验证过的可信微内核操作系统VTOS为实例,阐述形式化设计和安全需求分析,并使用定理证明器Isabelle/HOL①对系统的设计和安全需求的一致性进行验证,表明VTOS达到预期的安全性.     

安全协议自动验证工具的状态空间剪枝

串空间模型是分析安全协议的一种实用、直观和严格的形式化方法。概述基于该模型结合使用定理证明和模型检测技术开发的安全协议验证工具AVSP的体系结构，提出一些剪枝规则对状态搜索空间进行剪枝。通过Needham-Schroeder安全协议的弱一致性认证属性验证过程来表明这些状态搜索空间剪枝规则可有效缩小状态搜索空间，防止状态空间爆炸。     

安全操作系统中制定安全策略的研究

本文在对Bell-LaPadula模型进行深入分析的基础上，提出了在某些Linux和UNIX安全操作系统设计中对Bell-LaPadula模型的一种错误理解，并结合实际生活中的安全操作对模型进行分析，并给出了模型的形式化操作规则和保密性证明，表明该模型完全符合保密性要求，从而纠正了安全策略的错误制订，避免造成系统的失泄密。     

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

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

电力智能单元传输规约安全性分析模型研究

电力智能单元传输规约的安全性是保障智能电网中智能通信实现高速、可靠、安全的基础。为了构建适用于电力智能单元传输规约的安全性分析模型,概述了主流的协议安全性分析理论与方法。基于符号模型的形式化方法包括逻辑推理、模型检验、定理证明;基于计算模型的计算方法包括RO模型、BCP模型、CK模型以及UC模型;基于计算可靠性理论的方法包括映射方法、模型方法、形式化方法的计算可靠性以及计算方法的直接形式化。提出了面向智能电网领域的电力智能单元传输规约安全性分析模型,为进一步的电力智能化单元传输规约的安全性分析奠定了基础。     

软件安全漏洞的静态检测技术

软件安全漏洞问题日益严重,静态漏洞检测提供从软件结构和代码中寻找漏洞的方法。该文研究软件漏洞静态检测的两个主要方面：静态分析和程序验证,重点分析词法分析、规则检查、类型推导、模型检测、定理证明和符号执行等方法,将常用的静态检测工具按方法归类,讨论、总结静态检测技术的优势、适用性和发展趋势。     

应用吴方法进行高层次定界模型检验

以吴方法为理论基础,提出一种针对高层次设计验证的定界模型检验方法.通过使用多项式等式建模高层次设计和待验证性质,将定界模型检验问题转化为定理证明问题,并用吴方法有效地解决该定理证明问题.实验结果表明,与基于布尔SAT、基于LP的RTL SAT以及基于非线性求解器的性质检验方法相比,该方法在时间消耗上具有相当大的优势.     

Verifying a signature architecture: a comparative case study

We report on a case study in applying different formal methods to model and verify an architecture for administrating digital signatures. The architecture comprises several concurrently executing systems that authenticate users and generate and store digital signatures by passing security relevant data through a tightly controlled interface. The architecture is interesting from a formal-methods perspective as it involves complex operations on data as well as process coordination and hence is a candidate for both data-oriented and process-oriented formal methods. We have built and verified two models of the signature architecture using two representative formal methods. In the first, we specify a data model of the architecture in Z that we extend to a trace model and interactively verify by theorem proving. In the second, we model the architecture as a system of communicating processes that we verify by finite-state model checking. We provide a detailed comparison of these two different approaches to formalization (infinite state with rich data types versus finite state) and verification (theorem proving versus model checking). Contrary to common belief, our case study suggests that Z is well suited for temporal reasoning about process models with complex operations on data. Moreover, our comparison highlights the advantages of proving theorems about such models and provides evidence that, in the hands of an experienced user, theorem proving may be neither substantially more time-consuming nor more complex than model checking.     

AVSP算法

AVSP(Automatic Verifier of Secrurity Protocols)是基于串空间模型(Strand Space Model),并结合使用定理证明和模型检测技术开发出来的密码安全协议自动验证工具。AVSP使用了理想的语义和逻辑来表达安全协议的保密性,同时采用了一些证明策略以控制和减少状态空间爆炸的规模,并加快发现协议中存在的漏洞。     

基于串空间的Athena分析技术研究

基于串空间模型的研究是当前安全协议领域的一个研究热点。Song对串空间模型进行了扩展,将模型检验和定理证明结合起来,提出了一种取名为Athena的安全协议分析方法,并基于该方法开发了自动证明工具APV,Song的工作被认为是串空间理论发展的一个重要事件。本文对Athena进行了系统的分析,介绍了Athena的假设条件,给出了Athena的语法和语义,分析了该逻辑的优点和局限性,在此基础上,分析了Athena的核心算法,讨论了Athena算法自动高效的原因,以及该算法如何避免状态空间爆炸的技术,指出了该算法的缺陷,形成原因以及解决的一般方法。最后对Athena方法的发展方向进行了讨论。     

Formal Verification of a Partial-Order Reduction Technique for Model Checking

Mechanical theorem proving and model checking are the two main methods of formal verification, each with its own strengths and weaknesses. While mechanical theorem proving is more general, it requires intensive human guidance. Model checking is automatic, but is applicable to a more restricted class of problems. It is appealing to combine these two methods in order to take advantage of their different strengths. Prior research in this direction has focused on how to decompose a verification problem into parts each of which is manageable by one of the two methods. In this paper we explore another possibility: we use mechanical theorem proving to formally verify a meta-theory of model checking. As a case study, we use the mechanical theorem prover HOL to verify the correctness of a partial-order reduction technique for cutting down the amount of state search performed by model checkers. We choose this example for two reasons. First, this reduction technique has been implemented in the protocol analysis tool SPIN to significantly speed up the analysis of many practical protocols; hence its correctness has important practical consequences. Second, the correctness arguments involve nontrivial mathematics, the formalization of which we hope will become the basis of a formal meta-theory of other model-checking algorithms and techniques. Interestingly, our formalization led to a nontrivial generalization of the original informal theory. We discuss the lessons, both encouraging and discouraging, learned from this exercise. In the appendix we highlight the important definitions and theorems from each of our HOL theories. The complete listing of our HOL proof is given in a separate document because of space limitations.     

State-rich model checking

In this paper we survey the area of formal verification techniques, with emphasis on model checking due to its wide acceptance by both academia and industry. The major approaches and their characteristics are presented, together with the main problems faced while trying to apply them. With the increased complexity of systems, as well as interest in software correctness, the demand for more powerful automatic techniques is pushing the theories and tools towards integration. We discuss the state of the art in combining formal methods tools, mainly model checking with theorem proving and abstract interpretation. In particular, we present our own recent contribution on an approach to integrate model checking and theorem proving to handle state-rich systems specified using a combination of Z and CSP.