Automated verification of access control policies using a SAT solver

Managing access control policies in modern computer systems can be challenging and error-prone. Combining multiple disparate access policies can introduce unintended consequences. In this paper, we present a formal model for specifying access to resources, a model that encompasses the semantics of the xacml access control language. From this model we define several ordering relations on access control policies that can be used to automatically verify properties of the policies. We present a tool for automatically verifying these properties by translating these ordering relations to Boolean satisfiability problems and then applying a sat solver. Our experimental results demonstrate that automated verification of xacml policies is feasible using this approach. This work is supported by NSF grants CCF-0614002 and CCF-0716095.     

Optimized temporal monitors for SystemC

SystemC is a modeling language built as an extension of C++. Its growing popularity and the increasing complexity of designs have motivated research efforts aimed at the verification of SystemC models using assertion-based verification (ABV), where the designer asserts properties that capture the design intent in a formal language such as PSL or SVA. The model then can be verified against the properties using runtime or formal verification techniques. In this paper we focus on automated generation of runtime monitors from temporal properties. Our focus is on minimizing runtime overhead, rather than monitor size or monitor-generation time. We identify four issues in monitor generation: state minimization, alphabet representation, alphabet minimization, and monitor encoding. We conduct extensive experimentation and identify a combination of settings that offers the best performance in terms of runtime overhead.     

Security patterns modeling and formalization for pattern-based development of secure software systems

Pattern-based development of software systems has gained more attention recently by addressing new challenges such as security and dependability. However, there are still gaps in existing modeling languages and/or formalisms dedicated to modeling design patterns and the way how to reuse them in the automation of software development. The solution envisaged here is based on combining metamodeling techniques and formal methods to represent security patterns at two levels of abstraction to fostering reuse. The goal of the paper is to advance the state of the art in model and pattern-based security for software and systems engineering in three relevant areas: (1) develop a modeling language to support the definition of security patterns using metamodeling techniques; (2) provide a formal representation and its associated validation mechanisms for the verification of security properties; and (3) derive a set of guidelines for the modeling of security patterns within the integration of these two kinds of representations.     

Security analysis of GTRBAC and its variants using model checking

Security analysis is a formal verification technique to ascertain certain desirable guarantees on the access control policy specification. Given a set of access control policies, a general safety requirement in such a system is to determine whether a desirable property is satisfied in all the reachable states. Such an analysis calls for the use of formal verification techniques. While formal analysis on traditional Role Based Access Control (RBAC) has been done to some extent, recent extensions to RBAC lack such an analysis. In this paper, we consider the temporal RBAC extensions and propose a formal technique using timed automata to perform security analysis by analyzing both safety and liveness properties. Using safety properties one ensures that something bad never happens while liveness properties show that some good state is also achieved. GTRBAC is a well accepted generalized temporal RBAC model which can handle a wide range of temporal constraints while specifying different access control policies. Analysis of such a model involves a process of mapping a GTRBAC based system into a state transition system. Different reduction rules are proposed to simplify the modeling process depending upon the constraints supported by the system. The effect of different constraints on the modeling process is also studied.     

Cybersecurity policy verification with declarative programming

Cybersecurity is a growing concern in today’s society. Security policies have been developed to ensure that data and assets remain protected for legitimate users, but there must be a mechanism to verify that these policies can be enforced. This paper addresses the verification problem of security policies in role-based access control of enterprise software. Most existing approaches employ traditional logic or procedural programming that tends to involve complex expressions or search with backtrack. These can be time-consuming, and hard to understand, and update, especially for large-scale security verification problems. Declarative programming paradigms such as “Answer Set” programming have been widely used to alleviate these issues by ways of elegant and flexible modeling for complex search problems. However, solving problems using these paradigms can be challenging due to the nature and limitation of the declarative problem solver. This paper presents an approach to automated security policy verification using Answer Set programming. In particular, we investigate how the separation of duty security policy in role-based access control can be verified. Our contribution is a modeling approach that maps this verification problem into a graph-coloring problem to facilitate the use of generate-and-test in a declarative problem-solving paradigm. The paper describes a representation model and rules that drive the Answer Set Solver and illustrates the proposed approach to securing web application software to assist the hiring process in a company.     

Building Automated Trust Negotiation architecture in virtual computing environment

Automated Trust Negotiation (ATN) is an important method to establish trust relationship between two strangers by exchanging their access control policies and credentials. Unfortunately, ATN is not widely adopted because of the complexity and multiformity of negotiation policies, especially in virtual computing environment, where the situation becomes worse than in traditional computing environment, due to the fact that a host with multiple virtual machines needs to be deployed with multiple negotiation policies. Moreover, all of these policies for each virtual machine must be upgraded and checked. To ease the burden on the administrator when deploying ATN access control policies and credentials in virtual computing environment, we propose an automated trusted negotiation architecture called virtual automated trust negotiation (VATN) to centralize ATN policies and credentials for multiple virtual machines in a physical node into a privileged virtual machine. VATN puts policy compliance checker and credential verification control in each virtual machine to improve the execution efficiency of trust negotiation. We implement VATN in Xen virtualization platform. Finally, we discuss the correctness of policy consistency checking and make performance analysis of VATN implemented in Xen.     

可信执行环境访问控制建模与安全性分析

可信执行环境(TEE)的安全问题一直受到国内外学者的关注. 利用内存标签技术可以在可信执行环境中实现更细粒度的内存隔离和访问控制机制, 但已有方案往往依赖于测试或者经验分析表明其有效性, 缺乏严格的正确性和安全性保证. 针对内存标签实现的访问控制提出通用的形式化模型框架, 并提出一种基于模型检测的访问控制安全性分析方法. 首先, 利用形式化方法构建基于内存标签的可信执行环境访问控制通用模型框架, 给出访问控制实体的形式化定义, 定义的规则包括访问控制规则和标签更新规则; 然后利用形式化语言B以递增的方式设计并实现该框架的抽象机模型, 通过不变式约束形式化描述模型的基本性质; 再次以可信执行环境的一个具体实现TIMBER-V为应用实例, 通过实例化抽象机模型构建TIMBER-V访问控制模型, 添加安全性质规约并运用模型检测验证模型的功能正确性和安全性; 最后模拟具体攻击场景并实现攻击检测, 评估结果表明提出的安全性分析方法的有效性.     

A verification framework for spatio-temporal consistency language with CCSL as a specification language

The Spatio-Temporal Consistency Language(STeC)is a high-level modeling language that deals natively with spatio-temporal behaviour,i.e.,behaviour relating to certain locations and time.Such restriction by both locations and time is of first importance for some types of real-time systems.CCSL is a formal specification language based on logical clocks.It is used to describe some crucial safety properties for real-time systems,due to its powerful expressiveness of logical and chronometric time constraints.We consider a novel verification framework combining STeC and CCSL,with the advantages of addressing spatio-temporal consistency of system behaviour and easily expressing some crucial time constraints.We propose a theory combining these two languages and a method verifying CCSL properties in STeC models.We adopt UPPAAL as the model checking tool and give a simple example to illustrate how to carry out verification in our framework.     

Modeling and control of discrete event systems using finite state machines with variables and their applications in power grids

Control theories for discrete event systems modeled as finite state machines have been well developed to address various fundamental control issues. However, finite state machine model has long suffered from the problem of state explosion that renders it unsuitable for some practical applications. In an attempt to mitigate the state explosion problem, we propose an efficient representation that appends finite sets of variables to finite state machines in modeling discrete event systems. We also present the control synthesis techniques for such finite state machines with variables (FSMwV). We first present our notion and means of control under this representation. We next present our algorithms for both offline and online synthesis of safety control policies. We then apply these results to the control of electric power grids.     

A formal role-based access control model for security policies in multi-domain mobile networks

Mobile users present challenges for security in multi-domain mobile networks. The actions of mobile users moving across security domains need to be specified and checked against domain and inter-domain policies. We propose a new formal security policy model for multi-domain mobile networks, called FPM-RBAC, Formal Policy Model for Mobility with Role Based Access Control. FPM-RBAC supports the specification of mobility and location constraints, role hierarchy mapping, inter-domain services, inter-domain access rights and separation of duty. Associated with FPM-RBAC, we also present a formal security policy constraint specification language for domain and inter-domain security policies. Formal policy constraint specifications are based on ambient logic and predicate logic. We also use ambient calculus to specify the current state of a mobile network and actions within security policies for evaluation of access requests according to security policies. A novel aspect of the proposed policy model is the support for formal and automated analysis of security policies related to mobility within multiple security domains.     

A Rule-based System for Web site Verification

In this paper, we describe a system, written in Haskell, for the automated verification of Web sites which can be used to specify (partial) correctness and completeness properties of a given Web site, and then automatically check whether these properties are actually fulfilled. It provides a rule-based, formal specification language which allows us to define syntactic/semantic conditions for the Web site by means of a user-friendly graphical interface as well as a verification facility for recognizing forbidden/incorrect patterns and incomplete/missing Web pages.     

基于DTE策略的安全域隔离Z形式模型

基于DTE策略的安全域隔离技术是构造可信系统的基本技术之一.但现有DTE实现系统存在安全目标不明确、缺乏对系统及其安全性质的形式定义和分析的缺点,导致系统安全性难以得到保证.定义了一个基于DTE策略的安全域隔离模型,采用Z语言形式定义了系统状态、基于信息流分析的不变量和安全状态,并借助Z/EVES工具给出验证系统安全的形式分析方法.解决了DTE系统的形式化建模问题,为安全域隔离技术的实现和验证奠定了基础.     

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

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

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.     

IFS与L系统的统一描述语言及其分类

为了更高效地表示分形图形,依据形式语言的文法结构及正则表达式的文法规则,通过引入代数运算,提出了一个能够对L系统和迭代函数系统(IFS)统一描述的语言代数系统。根据语言代数系统产生式的文法规则,将此系统的产生式集划分为五类。结合分形理论,此语言代数系统着重将DOL系统、迭代函数系统(IFS)、带凝聚集迭代函数系统(凝聚IFS)、随机迭代函数系统(IFSP)和再归迭代函数系统(RIFS)等进行描述,同时用此系统的正则表达式方程解将分形吸引子进行代数表示,并给出一些实例。通过实例表明,分形图形可以用该语言代数系统简单、明了、高效地表示。     

Combining UML, ASTD and B for the formal specification of an access control filter

Combination of formal and semi-formal methods is more and more required to produce specifications that can be, on the one hand, understood and thus validated by both designers and users and, on the other hand, precise enough to be verified by formal methods. This motivates our aim to use these complementary paradigms in order to deal with security aspects of information systems. This paper presents a methodology to specify access control policies starting with a set of graphical diagrams: UML for the functional model, SecureUML for static access control and ASTD for dynamic access control. These diagrams are then translated into a set of B machines. Finally, we present the formal specification of an access control filter that coordinates the different kinds of access control rules and the specification of functional operations. The goal of such B specifications is to rigorously check the access control policy of an information system taking advantage of tools from the B method.     

Formal verification of algorithms for critical systems

The authors describe their experience with formal, machine-checked verification of algorithms for critical applications, concentrating on a Byzantine fault-tolerant algorithm for synchronizing the clocks in the replicated computers of a digital flight control system. The problems encountered in unsynchronized systems and the necessity, and criticality, of fault-tolerant synchronization are described. An overview of one such algorithm and of the arguments for its correctness are given. A verification of the algorithm performed using the authors' EHDM system for formal specification and verification is described. The errors found in the published analysis of the algorithm and benefits derived from the verification are indicated. Based on their experience, the authors derive some key requirements for a formal specification and verification system adequate to the task of verifying algorithms of the type considered. The conclusions regarding the benefits of formal verification in this domain and the capabilities required of verification systems in order to realize those benefits are summarized     

A Formal Virtual Enterprise Access Control Model

A virtual enterprise (VE) refers to a cooperative alliance of legally independent enterprises, institutions, or single persons that collaborate with each other by sharing business processes and resources across enterprises in order to raise enterprise competitiveness and reduce production costs. Successful VEs require complete information transparency and suitable resource sharing among coworkers across enterprises. Hence, this investigation proposes a formal flexible integration solution, named the formal VE access control (VEAC) model, based on the role-based AC model, to integrate and share distributed resources owned by VE members. The formal VEAC model comprises a fundamental VEAC model, a project AC policy (PACP) language model, and a model construction methodology. The fundamental VEAC model manages VE resources and the resources of participating enterprises, in which various project relationships are presented to facilitate different degrees of resource sharing across projects and enterprise boundaries, and cooperative modes among VE roles are presented to enable collaboration among coworkers in a VE. This PACP language model features object-subject-action-condition AC policies that jointly determine user access authorizations. In addition, the methodology supplies a systematic method to identify fundamental elements of the VEAC model and to establish assignments between elements and relations.     

基于本体的多域访问控制策略集成研究

本体是共享概念模型的形式化规范说明,是一种能在语义和知识层次上描述信息系统概念模型的建模工具,为解决多域环境中的安全互操作提供了一种新的方法.使用本体及其描述语言,对基于角色的访问控制策略进行了描述,形成一个概念和属性的公理集合（TBox）,并采用ALCN（含有个数限制和补算子的描述逻辑语言）对TBox进行形式化的描述.利用域间角色映射方法来解决多域访问控制策略的集成.使用基于规则的推理技术,定义多域访问控制中的一系列推理规则,实现访问控制领域的推理.基于前述方法实现了OntoAC系统,实验结果表明该方法是有效的.