VODCA 2004

Developing security-critical systems is difficult and there are many well-known examples of security weaknesses exploited in practice. In particular, so far little research has been performed on the soundly based design of secure architectures, which would be urgently needed to develop secure systems reliably and efficiently. In this abstract, we sketch some research on a sound methodology supporting secure architecture design. We give an overview over an extension of UML, called UMLsec, that allows expressing security-relevant information within the diagrams in an architectural design specification. We define foundations for secure architectural design patterns. We present tool-support which has been developed for the UMLsec secure architecture approach.

Web services represent a challenge and an opportunity for organizations wishing to expose product and services offerings through the Internet. The Web service technology provides an environment in which service providers and consumers can discover each other and conduct business transactions through the exchange of XML-based documents. However, any organization using XML and Web Services must ensure that only the right users, sending the appropriate XML content, can access their Web Services. Access control policy specification for controlling access to Web services is then becoming an emergent research area due to the rapid development of Web services in modern economy. This paper is an effort to understand the basic concepts for securing Web services and the requirements for implementing secure Web services. We describe the design and implementation of a Web service architecture for enforcing access control policies, the overall rationale and some specific choices of our design are discussed.

We present a Model Driven Development (MDD) approach to the development of access control  policies for distributed systems. The models are expressed as Meta-Object Facility (MOF) models enriched by Unified Modeling Language (UML) profiles. The view-based access control model is used as an example, for which we present a platform independent meta-model and platform specific meta-models for the Java 2 Platform, Enterprise Edition (J2EE). A management application is used to build instance models for the platform independent and platform specific meta-models, respectively. We present in this paper how the platform independent models can be  used to generate the platform specific models, and how the meta-models can be used to generate the models for the specific application. Finally, the platform specific models are used to generate the security policy to be  deployed in the security infrastructure. We show how consistence requirements can be verified formally by using category-based graph transformations.

LUNCH BREAK

Currently, security appears to be one of the strongest sales arguments for software vendors all over the world. No other sector of the software industry has undergone a similar wave of mergers and acquisitions recently as the producers of security software. Market analyses from all leading business consultants predict heavy growth in the field, and the annual figures of the major players such as Checkpoint or Symantec back up these statements. However, the main mechanisms of the industry still apply: Innovations have to be created and presented where demand is predicted and the pressure to come up with new solutions is at an all time high. Consequently, the products are pushed out the door as quickly as possible---and all too often before quality control has been dedicated the amount of time and effort that would have been implied by due diligence. While any customer of security software expects the product to enhance the security of their environment, it might actual pose new risks. Blind faith in these solutions can further contribute to compromising the overall security of a network where a substantial advantage had been expected. The purpose of this article is to shed a little light on the situation as it really is.

The application of formal methods to security protocol analysis has been extensively researched during the last 25 years. Several formalisms and (semi-)automatic tools for the verification of security protocols have been developed. However, their applicability is limited to relatively small protocols that run in isolation. Many of the protocols that are in use today cannot be verified using these methods. One of the main reasons for this is that these protocols are composed of several sub- protocols. Such a composition of protocols is not addressed in the majority of formalisms. In this paper we identify a number of issues that are relevant to applying formal methods to the problem of security protocol composition. Additionally, we describe what research needs to be done to meet this challenge.

We use Team Automata in order to model a protocol by Cachin et al. for securing agents in a hostile environment. Our study focuses on privacy properties of the agents. We use the framework to prove a result from the work by Cachin et al. As a by-product, our analysis gives some initial insight on the limits of the protocol. From a different perspective, this study continues a line of research on the expressive power and modelling capabilities of Team Automata. To the best of our knowledge, this is the first attempt to use Team Automata for the analysis of privacy properties.

COFFEE BREAK

Spatiality is an important aspect of distributed systems because their computations depend both on the dynamic behaviour and on the structure of their components. Spatial logics have been proposed as the formal device for expressing spatial properties of systems. We define CCS ||, a CCS-like calculus whose semantics allows one to observe spatial aspects of systems on the top of which we define models of the spatial logic. Our alternative definition of models is proved equivalent to the standard one. Furthermore, logical equivalence is characterized in terms of the bisimilarity of CCS ||.

The way developers define architecture, execute architectural strategy, and record the results make a critical difference in the ability to deal  with information and knowledge. In this context, integrating databases is very important indeed, but the different semantics they possibly have  usually complicates administration. Therefore, recovering information through a common semantics becomes crucial in order to realise the full knowledge contained in the databases. In this paper, we describe and illustrate a proposal on the use of layered architectures to integrate knowledge from heterogeneous sources. We illustrate how the process might be facilitated by applying ontology-based comparisons as part of the components' behaviour.

We introduce a simple graph logic that supports specification of Quality of Service (QoS) properties of applications. The idea is that we are not only interested in representing whether two sites are connected, but we want to express the QoS level of the connection. The evaluation of a formula in the graph logic is a value of a suitable algebraic structure, a c-semiring, representing the QoS level of the formula and not just a boolean value expressing whether or not the formula holds. We present some examples and briefly discuss the expressiveness and complexity of our logic.