云系统中多域安全策略规范与验证方法

为了有效管理云系统间跨域互操作中安全策略的实施,提出一种适用于云计算环境的多域安全策略验证管理技术。首先,研究了安全互操作环境的访问控制规则和安全属性,通过角色层次关系区分域内管理和域间管理,形式化定义了基于多域的角色访问控制（domRBAC）模型和基于计算树逻辑（CTL）的安全属性规范;其次,给出了基于有向图的角色关联映射算法,以实现domRBAC角色层次推理,进而构造出了云安全策略验证算法。性能实验表明,多域互操作系统的属性验证时间开销会随着系统规模的扩大而增加。技术采用多进程并行检测方式可将属性验证时间减少70.1%～88.5%,其模型优化检测模式相比正常模式的时间折线波动更小,且在大规模系统中的时间开销要明显低于正常模式。该技术在规模较大的云系统安全互操作中具有稳定和高效率的属性验证性能。     

A verification approach to applied system security

We present a method for the security analysis of realistic models over off-the-shelf systems and their configuration by formal, machine-checked proofs. The presentation follows a large case study based on a formal security analysis of a CVS-Server architecture.The analysis is based on an abstract architecture (enforcing a role-based access control), which is refined to an implementation architecture (based on the usual discretionary access control provided by the POSIX environment). Both architectures serve as a skeleton to formulate access control and confidentiality properties.Both the abstract and the implementation architecture are specified in the language Z. Based on a logical embedding of Z into Isabelle/HOL, we provide formal, machine-checked proofs for consistency properties of the specification, for the correctness of the refinement, and for security properties.     

A formal model for knowledge-based systems verification

A logico-algebraic model for verification of Knowledge Based Systems, based on Abraham Robinson's meta-algebra, is presented in this article. the set of rules of Knowledge Based System is considered to be the set of axioms of a theory “T”. the model consists of: (i) the collection “P” of all well formed formulas of the language of T, (ii) a subset P₀ of P that has as its elements the axioms of a given logic (bivalued, intuitionistic, or other), plus all the theorems that can be deduced from this logic inside the language of T, (iii) some distinguished subsets of P, to be called m-ideals and m-filters, that depend on T and P₀. Important concepts that are involved in the verification of Knowledge Based Systems are considered, such as forward and backward reasoning consistencies. Appropriate characterizations are obtained by using properties of m-ideals and m-filters. © 1994 John Wiley & Sons, Inc.     

A baseline security policy for distributed healthcare information systems

In this paper, the need for identifying and analyzing the generic security characteristics of a healthcare information system is, first, demonstrated. The analysis of these characteristics is based upon a decision-support roadmap. The results from this profiling work are then analyzed in the light of the fact that more than 1000 accidental deaths happened due to computer system failures. As a result of this analysis, a set of recommendations is drawn up, leading to the development of a baseline security policy for healthcare institutions. Such a policy should be flexible enough to reflect the local needs, expectations and user requirements, as well as strict enough to comply with international recommendations. An example of such a baseline policy is then provided. The policy refers to a given security culture and has been based upon an abstract approach to the security needs of a healthcare institution.     

基于移动代理的网络安全审计策略*

针对普通审计策略在网格环境下实施的各种问题,以及网格环境下审计系统设计和实现的困难,提出了一种基于移动代理的网格安全审计策略,介绍了该策略的基本结构和实现过程,通过在实验平台下实施该策略并与普通审计策略进行比较,证明了基于移动代理的网格安全审计策略的可行性和高效性。     

Security policy verification for multi-domains in cloud systems

The cloud is a modern computing paradigm with the ability to support a business model by providing multi-tenancy, scalability, elasticity, pay as you go and self-provisioning of resources by using broad network access. Yet, cloud systems are mostly bounded to single domains, and collaboration among different cloud systems is an active area of research. Over time, such collaboration schemas are becoming of vital importance since they allow companies to diversify their services on multiple cloud systems to increase both uptime and usage of services. The existence of an efficient management process for the enforcement of security policies among the participating cloud systems would facilitate the adoption of multi-domain cloud systems. An important issue in collaborative environments is secure inter-operation. Stemmed from the absence of relevant work in the area of cloud computing, we define a model checking technique that can be used as a management service/tool for the verification of multi-domain cloud policies. Our proposal is based on NIST’s (National Institute of Standards and Technology) generic model checking technique and has been enriched with RBAC reasoning. Current approaches, in Grid systems, are capable of verifying and detect only conflicts and redundancies between two policies. However, the latter cannot overcome the risk of privileged user access in multi-domain cloud systems. In this paper, we provide the formal definition of the proposed technique and security properties that have to be verified in multi-domain cloud systems. Furthermore, an evaluation of the technique through a series of performance tests is provided.     

User requirements for security in wireless mobile systems

Security of wireless mobile systems continues to be a hot topic; now generating its own conferences and platforms, such as the recent 2nd IEE Secure Mobile Communications held by the IEE on 23 September 2004. The general discussion on security in wireless systems takes place in technical fora, and while this is a totally valid discussion, it sometimes seems to be taking place in isolation. From the user perspective the wireless system usually forms part of a larger, interconnected system. This paper raises the question, “What about the user?” and offers some views on the user requirements on this most important part of system design where people are one end of the chain which involves wireless and other systems.     

A cooperative agent-based model for active security systems

This paper presents a multi-agent model for implementing active security concepts. In this model, a group of agents can carry out their tasks cooperatively in order to achieve an ultimate security goal. Thus a low-level module of the proposed model reads the values of interesting data items of the relevant current network events and passes them to a relational database. Comparing these measurements against predefined values in an intruder signature database may point to a particular attack.The proposed model consists of two parts. (1) A multiagent Intrusion Detection System (MIDS) for detecting attacks. (2) An Active Security Mechanism (ASM) for taking active, network-wide, response against attackers. The proposed approach provides a customizable host environment built from various systems software components to allow an optimal match between the intrusion circumstances and the underlying security architecture. Thus, different frameworks can support alternative responses of existing security services. In addition, the ASM can take rapid response against attacks by making use of sensible sharing of attack intelligence. System agents communicate with each other on different hosts using an agent communication language through a message router.     

Parameterized model checking for security policy analysis

International Journal on Software Tools for Technology Transfer - We explain how a parameterized model checking technique can be exploited to mechanize the analysis of access control policies. The...     

Benchmarking reputation systems: A quantitative verification approach

Trust and reputation systems are classes of decision support tools which help detecting malicious behavior based on collecting ratings and opinions. Despite their advantages, these systems are vulnerable to some kinds of attacks in which the attacker can deceive the system using sequences of misleading behaviors. Robustness of reputation systems against these attacks are frequently investigated in the literature. However the existing works usually evaluate the robustness using a qualitative simulation method. Lack of a formal evaluation method and a quantitative measure of robustness make it hard to extend the results and to compare the systems precisely. This paper proposes a quantitative robustness measure for reputation systems based on a formal verification approach. Using the robustness measure and the verification method, a comprehensive benchmarking of a number of well-known reputation systems is presented which includes evaluation of the systems against basic and the worst case attacks. The results are used for ranking and classifying the systems. The studies show that robustness is not an absolute feature of a reputation model, but it also depends on the properties of the environment. The benchmarking results have been also used to indicate the proper environment for each class of systems/attacks.     

An approach to systems verification

The term systems verification refers to the specification and verification of the components of a computing system, including compilers, assemblers, operating systems and hardware. We outline our approach to systems verification, and summarize the application of this approach to several systems components. These components consist of a code generator for a simple high-level language, an assembler and linking loader, a simple operating system kernel, and a microprocessor design.     

A security approach for off-chip memory in embedded microprocessor systems

This paper describes a complete off-chip memory security solution for embedded systems. Our security core is based on a one-time pad (OTP) encryption circuit and a CRC-based integrity checking module. These modules safeguard external memory used by embedded processors against a series of well-known attacks, including replay attacks, spoofing attacks and relocation attacks. Our implementation limits on-chip memory space overhead to less than 33% versus memory used by a standard microprocessor and reduces memory latency achieved by previous approaches by at least half. The performance loss for software execution with our solution is only 10% compared with a non-protected implementation. An FPGA prototype of our security core has been completed to validate our findings.     

ACTEN: A conceptual model for security systems design

This paper describes ACTEN, a conceptual model for the design of security systems. Security information is represented by action-entity pairs and organized into a framework composed of graphs and tables. The rules permitting the building and management of this framework are introduced.The model describes both static and dynamic aspects of the security system; in fact, it shows the access modalities between objects in the system and the evolution of such modalities due to grant and revocation of rights within the security system.ACTEN also allows the identification of the authority and protection level of each component of the system. The tools for this analysis are introduced and an example is given.     

A UML-based static verification framework for security

Secure software engineering is a new research area that has been proposed to address security issues during the development of software systems. This new area of research advocates that security characteristics should be considered from the early stages of the software development life cycle and should not be added as another layer in the system on an ad-hoc basis after the system is built. In this paper, we describe a UML-based Static Verification Framework (USVF) to support the design and verification of secure software systems in early stages of the software development life-cycle taking into consideration security and general requirements of the software system. USVF performs static verification on UML models consisting of UML class and state machine diagrams extended by an action language. We present an operational semantics of UML models, define a property specification language designed to reason about temporal and general properties of UML state machines using the semantic domains of the former, and implement the model checking process by translating models and properties into Promela, the input language of the SPIN model checker. We show that the methodology can be applied to the verification of security properties by representing the main aspects of security, namely availability, integrity and confidentiality, in the USVF property specification language.     

Optimisation-based verification process of obstacle avoidance systems for unicycle-like mobile robots

This paper presents an optimisation-based verification process for obstacle avoidance systems of a unicycle-like mobile robot. It is a novel approach for the collision avoidance verification process. Local and global optimisation based verification processes are developed to find the worst-case parameters and the worst-case distance between the robot and an obstacle. The kinematic and dynamic model of the unicycle-like mobile robot is first introduced with force and torque as the inputs. The design of the control system is split into two parts. One is velocity and rotation using the robot dynamics, and the other is the incremental motion planning for robot kinematics. The artificial potential field method is chosen as a path planning and obstacle avoidance candidate technique for verification study as it is simple and widely used. Different optimisation algorithms are applied and compared for the purpose of verification. It is shown that even for a simple case study where only mass and inertia variations are considered, a local optimization based verification method may fail to identify the worst case. Two global optimisation methods have been investigated: genetic algorithms (GAs) and GLOBAL algorithms. Both of these methods successfully find the worst case. The verification process confirms that the obstacle avoidance algorithm functions correctly in the presence of all the possible parameter variations.     

安全协议验证模型的高效自动生成

为了能高效地利用模型检测技术对安全协议进行分析与验证,提高工作效率,提出了一种适用范围广,自动化程度及验证效率均较高的建模算法。开发了一个基于该建模算法“网络安全协议验证模型生成系统”,该系统可高效地对安全协议进行分析与验证,系统在对攻击者建模时采用偏序规约、语法重定序及类型检查等优化策略以提高验证效率,有效地缓解了模型检测过程中的状态爆炸问题。     

A logical approach to multilevel security of probabilistic systems

Summary. We set out a modal logic for reasoning about multilevel security of probabilistic systems. This logic contains expressions for time, probability, and knowledge. Making use of the Halpern-Tuttle framework for reasoning about knowledge and probability, we give a semantics for our logic and prove it is sound. We give two syntactic definitions of perfect multilevel security and show that their semantic interpretations are equivalent to earlier, independently motivated characterizations. We also discuss the relation between these characterizations of security and between their usefulness in security analysis.