Characterizing intransitive noninterference for 3-domain security policies with observability

This note introduces a new algorithmic approach to the problem of checking the property of intransitive noninterference (INI) using discrete-event systems (DESs) tools and concepts. INI property is widely used in formal verification of security problems in computer systems and protocols. The approach consists of two phases: First, a new property called iP-observability (observability based on a purge function) is introduced to capture INI. We prove that a system satisfies INI if and only if it is iP-observable. Second, a relation between iP-observability and P-observability (observability as used in DES) is established by transforming the automaton modeling a system/protocol into an automaton where P-observability (and, hence, iP-observability) can be determined. This allows us to check INI by checking P-observability, which can be done efficiently. Our approach can be used for all systems/protocols with three domains or levels, which is sufficient for most noninterference problems for cryptographic protocols and systems.     

Modeling and formal verification of embedded systems based on a Petri net representation

In this paper we concentrate on aspects related to modeling and formal verification of embedded systems. First, we define a formal model of computation for embedded systems based on Petri nets that can capture important features of such systems and allows their representation at different levels of granularity. Our modeling formalism has a well-defined semantics so that it supports a precise representation of the system, the use of formal methods to verify its correctness, and the automation of different tasks along the design process. Second, we propose an approach to the problem of formal verification of embedded systems represented in our modeling formalism. We make use of model checking to prove whether certain properties, expressed as temporal logic formulas, hold with respect to the system model. We introduce a systematic procedure to translate our model into timed automata so that it is possible to use available model checking tools. We propose two strategies for improving the verification efficiency, the first by applying correctness-preserving transformations and the second by exploring the degree of parallelism characteristic to the system. Some examples, including a realistic industrial case, demonstrate the efficiency of our approach on practical applications.     

基于模拟关系的精化检测方法

精化检测是一种重要的形式化验证方法,将系统实现和性质规约用相同形式化语言进行建模,如能证明两者间存在某种精化关系且该关系能够维持性质,可得出系统实现满足性质规约.为验证不同类型的系统性质, traces、stable failures和failures-divergence精化检测方法已被提出.精化检测算法依赖于子集构造,因而其面临状态空间爆炸问题.近年来,已有学者针对NFA语言包含问题提出了基于模拟关系的状态空间消减方法,大大提高了算法性能,且该方法能直接用于traces精化检测.在此基础上,本文提出了基于模拟关系的stable failures和failures-divergence精化检测方法.此外,本文还将精化检测扩展到了时间系统的验证中,提出了基于模拟关系的时间自动机traces精化检测方法.实验结果表明,基于模拟关系的算法效率有很大提高.     

Typing correspondence assertions for communication protocols

Woo and Lam propose correspondence assertions for specifying authenticity properties of security protocols. Prior work on checking correspondence assertions depends on model-checking and is limited to finite-state systems. We propose a dependent type and effect system for checking correspondence assertions. Since it is based on type-checking, our method is not limited to finite-state systems. This paper presents our system in the simple and general setting of the π-calculus. We show how to type-check correctness properties of example communication protocols based on secure channels. In a related paper, we extend our system to the more complex and specific setting of checking cryptographic protocols based on encrypted messages sent over insecure channels.     

State space analysis of Petri nets with relation-algebraic methods

A large variety of systems can be modelled by Petri nets. Their formal semantics are based on linear algebra which in particular allows the calculation of a Petri net’s state space. Since state space explosion is still a serious problem, efficiently calculating, representing, and analysing the state space is mandatory. We propose a formal semantics of Petri nets based on executable relation-algebraic specifications. Thereupon, we suggest how to calculate the markings reachable from a given one simultaneously. We provide an efficient representation of reachability graphs and show in a correct-by-construction approach how to efficiently analyse their properties. Therewith we cover two aspects: modelling and model checking systems by means of one and the same logic-based approach. On a practical side, we explore the power and limits of relation-algebraic concepts for concurrent system analysis.     

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

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

不确定环境下hCPS系统的形式化建模与动态验证

随着科技的进步,新型复杂系统例如人机物融合系统（Human Cyber-Physical Systems,HCPS）已经与人类社会生活越来越密不可分.软件系统所处的信息空间与人们日常生活所处的物理空间日渐融合.物理空间内环境的复杂多变、时空数据的爆发增长以及难以预料的人类行为等不确定因素威胁着系统安全.由于系统安全需求的增长,系统的规模和复杂度随之增加所带来的一系列问题亟待解决.因此,在不确定性环境下,构造智能、安全的人机物融合系统已经成为软件行业不可回避的挑战.环境不确定性使得人机物融合系统软件无法准确感知其所处的运行环境.感知的不确定性将导致系统的误判,从而影响系统的安全性.环境不确定性使得系统设计人员无法为人机物融合系统软件的运行环境提供准确的形式化规约.而对于安全要求较高的系统,准确的形式化规约是保证系统安全的首要条件.为了应对规约的不确定性,本文提出时空数据驱动与模型驱动相结合的建模方式,即通过使用机器学习算法,基于环境中时空数据对环境进行建模.根据安全软件的典型特征,采用动态验证的方式保证系统的安全,从而构建统一安全的理论框架.为了展示方案的可行性,本文以自动驾驶车辆与人驾驶的摩托车的交互场景为例说明了在不确定性环境下的人机物融合系统的建模与验证的具体应用.     

Web服务安全会话协议的SPIN建模与分析

Web Services Secure Conversation是基于XML的安全协议.本文对该协议进行了形式化的分析,并使用模型检验工具SPIN验证了协议的安全性,结果表明该协议存在认证性缺陷。为此,修改了协议的消息结构并对用户口令进行了数字签名。对改进后协议的安全性进行分析,结果表明改进后的协议不存在原协议的缺陷,协议满足认证性要求。     

Extracting trust information from security system of a service

The issue of trust is a research problem in emerging open environments, such as ubiquitous networks. Such environments are highly dynamic and they contain diverse number of services and autonomous entities. Entities in open environments have different security needs from services. Trust computations related to the security systems of services necessitate information that meets needs of each entity. Obtaining such information is a challenging issue for entities. In this paper, we propose a model for extracting trust information from the security system of a service based on the needs of an entity. We formally represent security policies and security systems to extract trust information according to needs of an entity. The formal representation ensures an entity to extract trust information about a security property of a service and trust information about whole security system of the service. The proposed model is applied to Dental Clinic Patient Service as a case study with two scenarios. The scenarios are analyzed experimentally with simulations. The experimental evaluation shows that the proposed model provides trust information related to the security system of a service based on the needs of an entity and it is applicable in emerging open environments.     

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

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

Model checking action system refinements

Action systems provide a formal approach to modelling parallel and reactive systems. They have a well established theory of refinement supported by simulation-based proof rules. This paper introduces an automatic approach for verifying action system refinements utilising standard CTL model checking. To do this, we encode each of the simulation conditions as a simulation machine, a Kripke structure on which the proof obligation can be discharged by checking that an associated CTL property holds. This procedure transforms each simulation condition into a model checking problem. Each simulation condition can then be model checked in isolation, or, if desired, together with the other simulation conditions by combining the simulation machines and the CTL properties.     

一种基于扩展不完全Kripke结构的三值逻辑模型检测方法

多值模型检测是解决形式化验证中状态爆炸问题的一种重要方法,三值模型检测是多值模型检测的基础,其中如何检验不确定状态的真值是一难点。针对不确定状态检验,提出了一种模型检测方法,首先对不完全Kripke结构PKS进行了扩展,然后在扩展后的模型上给出了检测不确定状态真值的方法,最后给出了基于扩展不完全Kripke结构的三值逻辑模型检测算法。与已有的三值逻辑模型检测算法相比,该算法降低了算法复杂度,完善了对于不确定或不一致信息的处理,从而增强了三值逻辑模型检测的实用性。     

Model checking probabilistic social commitments for intelligent agent communication

Interaction among autonomous agents in Multi-Agent Systems (MASs) is a key aspect for agents to coordinate with one another. Social approaches, as opposed to the mental approaches, have recently received a considerable attention in the area of agent communication. They exploit observable social commitments to develop a verifiable formal semantics through which communication protocols can be specified. Developing and implementing algorithmic model checking for social commitments have been recently addressed. However, model checking social commitments in the presence of uncertainty is yet to be investigated.In this paper, we propose a model checking technique for verifying social commitments in uncertain settings. Social commitments are specified in a modal logical language called Probabilistic Computation Tree Logic of Commitments (PCTLC). The modal logic PCTLC extends PCTL, the probabilistic extension of CTL, with modalities for commitments and their fulfillments. The proposed verification method is a reduction-based model checking technique to the model checking of PCTL. The technique is based upon a set of reduction rules that translate PCTLC formulae to PCTL formulae to take benefit of existing model checkers such as PRISM. Proofs that confirm the soundness of the reduction technique are presented. We also present rules that transform our new version of interpreted systems into models of Markov Decision Processes (MDPs) to be suitable for the PRISM tool. We implemented our approach on top of the PRISM model checker and verified some given properties for the Oblivious Transfer Protocol from the cryptography domain. Our simulation demonstrates the effectiveness of our approach in verifying and model checking social commitments in the presence of uncertainty. We believe that the proposed formal verification technique will advance the literature of social commitments in such a way that not only representing social commitments in uncertain settings is doable, but also verifying them in such settings becomes achievable.     

基于不可满足核的近似逼近可达性分析

近年来,形式化验证技术受到了越来越多的关注,它在保障安全关键领域系统的安全性和正确性方面发挥着重要的作用.模型检测作为形式化验证中自动化程度较高的分支,具有十分广阔的发展前景.本文中我们研究并提出了一种新的模型检测技术,可以有效地对迁移系统进行模型检测,包括不安全性检测和证明安全性.与现有的模型检测算法不同,我们提出的这种方法——基于不可满足核（unsatisfiable core,UC）的近似逼近可达性分析（UC-based approximate incremental reachability,UAIR）,主要利用不可满足核来求解一系列的候选安全不变式直至生成最终的不变式,以此来实现安全性证明和不安全性检测（漏洞查找）.在基于SAT求解器的符号模型检测中,我们使用由可满足性求解器得到的UC构造候选安全不变式,如果迁移系统本身是安全的,我们得到的初始不变式只是安全不变式的一个近似.然后,我们在检查安全性的同时,逐步改进候选安全不变式,直到找到一个真正的不变式,证明系统是安全的;如果系统是不安全的,我们的方法最终可以找到一个反例证明系统是不安全的.作为一种全新的方法,我们利用不可满足核进行安全性模型检测,取得了相当好的效果.众所周知,模型检测领域没有绝对最好的方法,尽管我们的方法在基准的可解数量上无法超越当前的成熟方法例如IC3、CAR等,但是我们的方法却可以解出3个其他方法都无法解出的案例,相信本方法可以作为模型检测工具集很有价值的补充.     

基于时态测试器的实时分支时态逻辑模型检测

基于自动机理论的模型检测技术在形式化验证领域处于核心地位, 然而传统自动机在时态算子上不具备可组合性, 导致各种时态逻辑的模型检测算法不能有机整合.本文为了实现集成限界时态算子的实时分支时态逻辑RTCTL*的高效模型检测, 提出一种RTCTL*正时态测试器构造方法, 以及相关符号化模型检测算法.证明了所提出的RTCTL*正时态测试器构造方法是完备的.也证明了该算法时间复杂度与被验证系统呈线性关系, 与公式长度呈指数关系.我们基于JavaBDD软件包成功开发了该算法的模型检测工具MCTK 2.0.0.我们完成了MCTK与著名的符号化模型检测工具nuXmv之间的实验对比分析工作, 结果表明MCTK虽然在内存消耗上要多于nuXmv, 但是MCTK的时间复杂度双指数级小于nuXmv, 使得利用MCTK验证大规模系统的实时时态性质成为可能.     

基于UML和模型检测的安全模型验证方法

安全策略的形式化分析与验证随着安全操作系统研究的不断深入已成为当前的研究热点之一.文中在总结前人工作的基础上,首次提出一种基于UML和模型检测器的安全模型验证方法.该方法采用UML将安全策略模型描述为状态机图和类图,然后利用转换工具将UML图转化为模型检测器的输入语言,最后由模型检测器来验证安全模型对于安全需求的满足性.作者使用该方法验证了DBLP和SLCF模型对机密性原则的违反.     

A game-theoretic approach for integrity assurance in resource-bounded systems

Assuring communication integrity is a central problem in security. However, overhead costs associated with cryptographic primitives used toward this end introduce significant practical implementation challenges for resource-bounded systems, such as cyber-physical systems. For example, many control systems are built on legacy components which are computationally limited, but have strict timing constraints. If integrity protection is a binary decision, it may simply be infeasible to introduce into such systems; without it, however, an adversary can forge malicious messages, which can cause significant physical or financial harm. To bridge the gap between such binary decisions, we propose a stochastic message authentication approach that can explicitly trade computational cost off for security. We introduce a formal game-theoretic framework for optimal stochastic message authentication, providing provable guarantees for resource-bounded systems based on an existing message authentication scheme. We use our framework to investigate attacker deterrence, as well as optimal stochastic message authentication when deterrence is impossible, in both short-term and long-term equilibria. Additionally, we propose two schemes for implementing stochastic message authentication in practice, one for saving computation only at the receiver and one for saving computation at both ends, and demonstrate the associated computational savings using an actual implementation.     

基于概念格因子分解的零件三维CAD模型检索

针对影响概念格应用的重要问题—即使是一个小规模数据集也会产生大量的形式概念,文中提出了可以满足关系覆盖的用对象（属性）概念分解形式背景对应的布尔矩阵的新方法.用这种方法原对象属性间的二元关系可以用数量在对象（属性）概念个数以内的概念表达出来,成为概念格因子.文中给出了概念格因子生成的基本原理及其算法.通过分析三维CAD零件模型功能表面间的关系构建零件工程图结构模型,并将其映射为形式背景,从而完成概念格因子到零件关键结构的应用.最后,实例演示了概念格因子在基于零件工程图结构模型的零件CAD模型检索中的运用.     

Vulnerability analysis of networks to detect multiphase attacks using the actor-based language Rebeca

Increasing use of networks and their complexity make the task of security analysis more and more complicated. Accordingly, automatic verification approaches have received more attention recently. In this paper, we investigate applying of an actor-based language based on reactive objects for analyzing a network environment communicating via Transport Protocol Layer (TCP). The formal foundation of the language and available tools for model checking provide us with formal verification support. Having the model of a typical network including client and server, we show how an attacker may combine simple attacks to construct a complex multiphase attack. We use Rebeca language to model the network of hosts and its model checker to find counter-examples as violations of security of the system. Some simple attacks have been modeled in previous works in this area, here we detect these simple attacks in our model and then verify the model to find more complex attacks which may include simpler attacks as their steps. We choose Rebeca because of its powerful yet simple actor-based paradigm in modeling concurrent and distributed systems. As the real network environment is asynchronous and event-based, Rebeca can be utilized to specify and verify the asynchronous systems, including network protocols.