Probabilistic model checking for the quantification of DoS security threats

Secure authentication features of communication and electronic commerce protocols involve computationally expensive and memory intensive cryptographic operations that have the potential to be turned into denial-of-service (DoS) exploits. Recent proposals attempt to improve DoS resistance by implementing a trade-off between the resources required for the potential victim(s) with the resources used by a prospective attacker. Such improvements have been proposed for the Internet Key Exchange (IKE), the Just Fast Keying (JFK) key agreement protocol and the Secure Sockets Layer (SSL/TLS) protocol. In present article, we introduce probabilistic model checking as an efficient tool-assisted approach for systematically quantifying DoS security threats. We model a security protocol with a fixed network topology using probabilistic specifications for the protocol participants. We attach into the protocol model, a probabilistic attacker model which performs DoS related actions with assigned cost values. The costs for the protocol participants and the attacker reflect the level of some resource expenditure (memory, processing capacity or communication bandwidth) for the associated actions. From the developed model we obtain a Discrete Time Markov Chain (DTMC) via property preserving discrete-time semantics. The DTMC model is verified using the PRISM model checker that produces probabilistic estimates for the analyzed DoS threat. In this way, it is possible to evaluate the level of resource expenditure for the attacker, beyond which the likelihood of widespread attack is reduced and subsequently to compare alternative design considerations for optimal resistance to the analyzed DoS threat. Our approach is validated through the analysis of the Host Identity Protocol (HIP). The HIP base-exchange is seen as a cryptographic key-exchange protocol with special features related to DoS protection. We analyze a serious DoS threat, for which we provide probabilistic estimates, as well as results for the associated attacker and participants' costs.     

Specification-based Testing for Gui-based Applications

The development of GUI-based applications has raised a lot of new issues, one of them being how to automate effective testing for applications with complicated graphical user interactions. In this paper, we discuss the architectural issues and the implementation concerns of our approach to an automated specification-based testing technique for GUI-based applications. This approach is carried out by enriching existing architecture for automated specification-based testing. An essential part of our work is a visual environment to obtain test specifications. This environment pre-runs the Application Under Test (AUT) under its own control, with two prominent characteristics: First, testers can edit test specifications within the true GUI environment of the AUT. Second, the recorded input and output contain the same references as those in the AUT, so that the test cases generated from the edited specification can be used directly by test oracles during the automated testing procedure.We present our running prototype of a visual specification editor that allows users to graphically manipulate test specifications when these specifications are given in term of Finite State Machines (FSM) and the implementations of the AUT are GUI-based Java applications.     

A lightweight secure mobile Payment protocol for vehicular ad-hoc networks (VANETs)

In the last few years, many value-added applications (such as Payment services) in Vehicular Ad hoc NETworks (VANETs) have emerged. Although these applications offer great business opportunities they also introduce new concerns regarding security and privacy. Moreover, the wide range of scenarios (with or without connectivity restrictions) arising from vehicle-to-vehicle and vehicle-to-roadside communications have opened up new security challenges which must be considered by Payment system designers to achieve the same security capabilities independent of the scenario where Payment occurs. We designed and implemented a lightweight (using symmetric-key operations which requires low computational power) secure Payment protocol for those scenarios in VANETs and other mobile environments where the Merchant cannot communicate directly with the Acquirer (the Merchant’s financial institution) to process the Payment Request. We also present practical performance results that can be achieved with the proposed Payment protocol.     

Typing the Behavior of Objects and Components using Session Types

This paper describes a proposal for typing the behavior of objects in component models. Most component models, CORBA in particular, do not offer any support for expressing behavioral properties of objects beyond the “Static” information provided by IDLs. We build on the works by Honda et al. [6] and Gay and Hole [5] to show how session types can be effectively used for describing protocols, extending the information currently provided by object interfaces. We show how session types not only allow high level specifications of complex object interactions, but also allow the definition of powerful interoperability tests at the protocol level, namely compatibility and substitutability of objects     

Subtyping for session types in the pi calculus

Extending the pi calculus with the session types proposed by Honda et al. allows high-level specifications of structured patterns of communication, such as client-server protocols, to be expressed as types and verified by static typechecking. We define a notion of subtyping for session types, which allows protocol specifications to be extended in order to describe richer behaviour; for example, an implemented server can be refined without invalidating type-correctness of an overall system. We formalize the syntax, operational semantics and typing rules of an extended pi calculus, prove that typability guarantees absence of run-time communication errors, and show that the typing rules can be transformed into a practical typechecking algorithm. Malcolm Hole died on 28th February 2004, a few weeks after the original submission of this paper.     

Specification and Verification of Agent Interaction using Social Integrity Constraints

In this paper we propose a logic-based social approach to the specification and verification of agent interaction. We firstly introduce integrity constraints about social acts (called Social Integrity Constraints) as a formalism to express interaction protocols and to give a social semantics to the behavior of agents, focusing on communicative acts. Then, we discuss several possible kinds of verification of agent interaction, and we show how social integrity constraints can be used to verify some properties in this respect. We focus our attention on static verification of compliance of agent specifications to interaction protocols, and on run-time verification, based on agents' observable behavior. We adopt as a running example the NetBill security transaction protocol for the selling and delivery of information goods.     

TinySOA: a service-oriented architecture for wireless sensor networks

Wireless sensor networks provide the means for gathering vast amounts of data from physical phenomena, and as such they are being used for applications such as precision agriculture, habitat monitoring, and others. However, there is a need to provide higher level abstractions for the development of applications, since accessing the data from wireless sensor networks currently implies dealing with very low-level constructs. We propose TinySOA, a service- oriented architecture that allows programmers to access wireless sensor networks from their applications by using a simple service-oriented API via the language of their choice. We show an implementation of TinySOA and the results of an experiment where programmers developed an application that exemplifies how easy Internet applications can integrate sensor networks.

Specification, decomposition and agent synthesis for situation-aware service-based systems

Service-based systems are distributed computing systems with the major advantage of enabling rapid composition of distributed applications, such as collaborative research and development, e-business, health care, military applications and homeland security, regardless of the programming languages and platforms used in developing and running various components of the applications. In dynamic service-oriented computing environment, situation awareness (SAW) is needed for system monitoring, adaptive service coordination and flexible security policy enforcement. To greatly reduce the development effort of SAW capability in service-based systems and effectively support runtime system adaptation, it is necessary to automate the development of reusable and autonomous software components, called SAW agents, for situation-aware service-based systems. In this paper, a logic-based approach to declaratively specifying SAW requirements, decomposing SAW specifications for efficient distributed situation analysis, and automated synthesis of SAW agents is presented. This approach is based on AS³ calculus and logic, and our declarative model for SAW. Evaluation results of our approach are also presented.     

A formal and sound transformation from Focal to UML: an application to airport security regulations

We propose an automatic transformation of Focal specifications to UML class diagrams. The main motivation for this work lies within the framework of the EDEMOI project, which aims to integrate and apply several requirements engineering and formal methods techniques to analyze airport security regulations. The idea is to provide a graphical documentation of formal models for developers, and in the long-term, for certification authorities. The transformation is formally described and an implementation has been designed. We also show how the soundness of our approach can be achieved.     

Single tag sharing scheme for multiple-object RFID applications

RFID systems have been widely adopted in various industrial as well as personal applications. However, traditional RFID systems are limited to address only one tag for each application object. This limitation hinders the usability of RFID applications because it is difficult, if not impossible, to distinguish many tags simultaneously with existing RFID systems. In this paper, we propose a new RFID tag structure to support multiple-objects that can be easily shared by many different RFID applications. That is, the proposed RFID tag structure supports that a tag maintains several different objects and allows those applications to access them simultaneously. We also propose an authentication protocol to support multiple-object RFID applications. Especially, we focus on the efficiency of the authentication protocol by considering different security levels in RFID applications. The proposed protocol includes two types of authentication procedures. In the proposed protocol, an object has its security level and goes through one of different authentication procedures suitable for its security level. We report the results of a simulation to test the performance of the proposed scheme. In our simulation, we considered the safety of our scheme against potential attacks and evaluated the efficiency of the proposed protocol.     

A Per Model of Secure Information Flow in Sequential Programs

This paper proposes an extensional semantics-based formal specification of secure information-flow properties in sequential programs based on representing degrees of security by partial equivalence relations (pers). The specification clarifies and unifies a number of specific correctness arguments in the literature and connections to other forms of program analysis. The approach is inspired by (and in the deterministic case equivalent to) the use of partial equivalence relations in specifying binding-time analysis, and is thus able to specify security properties of higher-order functions and partially confidential data. We also show how the per approach can handle nondeterminism for a first-order language, by using powerdomain semantics and show how probabilistic security properties can be formalised by using probabilistic powerdomain semantics. We illustrate the usefulness of the compositional nature of the security specifications by presenting a straightforward correctness proof for a simple type-based security analysis.     

Capability-Passing Processes

Capability-passing processes model global applications in a way that decouples the global agreement aspects of protocols from the details of how the communications are actually made. It relies on a restricted API or programming language and on the exchange of digital certificates representing capabilities to ensure that participants are faithful to a protocol and that outsiders cannot interfere. At the specification level, protocols are reasoned about independently of the underlying communication, using a process calculus with an abstraction of logs to isolate the remote state required for such protocols. At the implementation level, protocol steps no longer perform global communication; instead capabilities are used to transmit evidence of remote state, which in turn are used to authorize local log changes (corresponding to protocol steps). In this way, an API for global agreement protocols is defined independently of the underlying communication system.     

On the modeling and generation of service-oriented tool chains

Tool chains have grown from ad-hoc solutions to complex software systems, which often have a service-oriented architecture. With service-oriented tool integration, development tools are made available as services, which can be orchestrated to form tool chains. Due to the increasing sophistication and size of tool chains, there is a need for a systematic development approach for service-oriented tool chains. We propose a domain-specific modeling language (DSML) that allows us to describe the tool chain on an appropriate level of abstraction. We present how this language supports three activities when developing service-oriented tool chains: communication, design and realization. A generative approach supports the realization of the tool chain using the service component architecture. We present experiences from an industrial case study, which applies the DSML to support the creation of a service-oriented tool chain. We evaluate the approach both qualitatively and quantitatively by comparing it with a traditional development approach.     

Information based reasoning about security protocols

We propose a notion of information based abstraction for the logical study of security protocols and study how protocol actions update agents' information. We show that interesting security properties of Needham-Schroeder like protocols can be verified automatically.     

Reverse engineering relational databases to identify and specify basic Web services with respect to service oriented computing

Service-oriented computing (SOC) is the computing paradigm that utilizes services as a fundamental building block. Services are self-describing, open components intended to support composition of distributed applications. Currently, Web services provide a standard-based realization of SOC due to: (1) the machine-readable format (XML) of their functional and nonfunctional specifications, and (2) their messaging protocols built on top of the Internet. However, how to methodologically identify, specify, design, deploy and manage a sound and complete set of Web services to move to a service-oriented architecture (SOA) is still an issue. This paper describes a process for reverse engineering relational database applications architecture into SOA architecture, where SQL statements are insulated from the applications, factored, implemented, and registered as Web services to be discovered, selected, and reused in composing e-business solutions. The process is based on two types of design patterns: schema transformation pattern and CRUD operations pattern. First, the schema transformation pattern allows an identification of the services. Then the CRUD operations pattern allows a specification of the abstract part of the identified services, namely their port types. This process is implemented as a CASE tool, which assists analysts specifying services that implement common, reusable, basic business logic and data manipulation.

A declarative two-level framework to specify and verify workflow and authorization policies in service-oriented architectures

The specification of distributed service-oriented applications spans several levels of abstraction, e.g., the protocol for exchanging messages, the set of interface functionalities, the types of the manipulated data, the workflow, the access policy, etc. Many (even executable) specification languages are available to describe each level in separation. However, these levels may interact in subtle ways (for example, the control flow may depend on the values of some data variables) so that a precise abstraction of the application amounts to more than the sum of its per level components. This problem is even more acute in the design phase when automated analysis techniques may greatly help the difficult task of building “correct” applications faced by designers. To alleviate this kind of problems, this paper introduces a framework for the formal specification and automated analysis of distributed service-oriented applications in two levels: one for the workflow and one for the authorization policies. The former allows one to precisely describe the control and data parts of an application with their mutual dependencies. The latter focuses on the specification of the criteria for granting or denying third-party applications the possibility to access shared resources or to execute certain interface functionalities. These levels can be seen as abstractions of one or of several levels of specification mentioned above. The novelty of our proposal is the possibility to unambiguously specify the—often subtle—interplay between the workflow and policy levels uniformly in the same framework. Additionally, our framework allows us to define and investigate verification problems for service-oriented applications (such as executability and invariant checking) and give sufficient conditions for their decidability. These results are non-trivial because their scope of applicability goes well beyond the case of finite state spaces allowing for applications manipulating variables ranging over infinite domains. As proof of concept, we show the suitability and flexibility of our approach on two quite different examples inspired by industrial case studies.     

Formal methods for security in the Xenon hypervisor

This paper reports on the Xenon project’s use of formal methods. Xenon is a higher-assurance secure hypervisor based on re-engineering the Xen open-source hypervisor. The Xenon project used formal specifications both for assurance and as guides for security re-engineering. We formally modelled the fundamental definition of security, the hypercall interface behaviour, and the internal modular design. We used three formalisms: CSP, Z, and Circus for this work. Circus is a combination of Standard Z, CSP with its semantics given in Hoare and He’s unifying theories of programming. Circus is suited for both event-based and state-based modelling. Here, we report our experiences to date with using these formalisms for assurance.     

Hybrid

Combining higher-order abstract syntax and (co)-induction in a logical framework is well known to be problematic. We describe the theory and the practice of a tool called Hybrid, within Isabelle/HOL and Coq, which aims to address many of these difficulties. It allows object logics to be represented using higher-order abstract syntax, and reasoned about using tactical theorem proving and principles of (co)induction. Moreover, it is definitional, which guarantees consistency within a classical type theory. The idea is to have a de Bruijn representation of λ-terms providing a definitional layer that allows the user to represent object languages using higher-order abstract syntax, while offering tools for reasoning about them at the higher level. In this paper we describe how to use Hybrid in a multi-level reasoning fashion, similar in spirit to other systems such as Twelf and Abella. By explicitly referencing provability in a middle layer called a specification logic, we solve the problem of reasoning by (co)induction in the presence of non-stratifiable hypothetical judgments, which allow very elegant and succinct specifications of object logic inference rules. We first demonstrate the method on a simple example, formally proving type soundness (subject reduction) for a fragment of a pure functional language, using a minimal intuitionistic logic as the specification logic. We then prove an analogous result for a continuation-machine presentation of the operational semantics of the same language, encoded this time in an ordered linear logic that serves as the specification layer. This example demonstrates the ease with which we can incorporate new specification logics, and also illustrates a significantly more complex object logic whose encoding is elegantly expressed using features of the new specification logic.     

Specification in CTL+Past for Verification in CTL

We describe PCTL, a temporal logic extending CTL with connectives allowing to refer to the past of a current state. This incorporates the new N, “from now on,” combinator we recently introduced. PCTL has a branching future, but a determined, finite, and cumulative past. We argue this is the right choice for a semantical framework and show this through an extensive example. We investigate the feasibility of verification with PCTL and demonstrate how a translation-based approach allows model-checking specifications written in NCTL, a fragment of PCTL.     

A framework for early design and prototyping of service-oriented applications with design patterns

Service-oriented computing is playing an important role in several domains. Today the biggest shift in mainstream design and programming is toward service-oriented applications. However, the service paradigm raises a bundle of problems that did not exist in traditional component-based development where abstraction, encapsulation, and modularity were the only main concerns. Due to their distributed, dynamic, and heterogeneous nature, service-oriented software applications require us to discover, document, and share new design patterns at the service- and architecture-level. Moreover, service-oriented applications are hard to design and validate, and demand for new foundational theories, modeling notations and analysis techniques.In line to such a vision, this article presents a framework, called SCA-PatternBox, to design and prototype service-oriented applications with design patterns. The framework relies on the OASIS standard Service Component Architecture (SCA) and on SCA component implementation types, such as SCA-Java, for supporting an “implementation-oriented” approach to service-oriented architecture modeling and to the definition and instantiation of design patterns. Moreover, in order to provide formally verified design patterns, SCA-PatternBox allows the formal specification and analysis of the functional behavioral aspects of a design pattern using a formal service specification language called SCA-ASM (Service Component Architecture-Abstract State Machine). As major evaluation of the framework, two case studies and lessons learned are presented. A final comparison of existing design pattern languages is also reported.