The increase in the use of cloud computing has put an increasing strain on resources, with huge amounts of data being produced and moved around the world. The need to verify this data after it has moved has meant even more work being done on the data before redirection. In this paper we propose an alternative way of moving this data, by creating an interface for data transfer one way from virtual machines to hypervisors. Our position is that the ability to transfer data directly in this way can provide a number of benefits to cloud users and providers, namely in the areas of security (confidentiality, integrity, and through decreased overhead), reduced energy consumption, and better use of hardware resources.

Abstract This paper proposes a formal method, based on Circus , for developing software systems that respect a joint specification of functionality and confidentiality attributes. We extend the semantics of Circus to capture the information that users can infer about a system’s behaviour, enabling confidentiality and functionality attributes of a system to be specified together. We represent inconsistencies between functionality and confidentiality properties as miracles, rendering insecure functionality infeasible. We present techniques for verifying that a system design’s functionality and confidentiality attributes are mutually consistent, and for ensuring that consistency is maintained by refinement steps.

Non-functional properties of software, such as power consumption and memory usage, are important factors in designing software for resource-constrained platforms. This is an area where Search-Based Software Engineering has yet to be applied, and this paper investigates the potential of using Genetic Programming and Multi-Objective Optimisation as key tools in satisfying non-functional requirements. We outline the benefits of such an approach and give an example application of evolving pseudorandom number generators and performing power-functionality trade-offs.

Abstract. Ten years ago the Mondex electronic purse was certified to ITSEC Level E6, the highest level of assurance for secure systems. This involved building formal models in the Z notation, linking them with refinement, and proving that they correctly implement the required security properties. The work has been revived recently as a pilot project for the international Grand Challenge in Verified Software. This paper records the history of the original project and gives an overview of the formal models and proofs used.

Abstract The current informal semantics of the simple concurrent object-oriented programming (SCOOP) mechanism for Eiffel is described. We construct and discuss a model using the process algebra CSP. This model gives a more formal semantics for SCOOP than existed previously. We implement the model mechanically via a new tool called CSPsim. We examine two semantic variations of SCOOP: when and how far to pass locks, and when to wait for child calls to complete. We provide evidence that waiting for child calls to complete both unnecessarily reduces parallelism without any increase in safety and increases deadlocks involving callbacks. Through the creation and analysis of the model, we identify a number of ambiguities relating to reservations and the underlying run-time system and propose means to resolve them.

This poster paper outlines a method for a search based approach to the development of provably correct protocols.

Boolean function design is at the heart of cryptography, and is the subject of a great deal of theoretical research. We have use a simulated annealing approach to find functions with particular desirable cryptographic properties; for functions of a small number of variables, results with properties as good as (and sometimes better than) the best so far have been achieved. The success of this approach is very sensitive to the cost function chosen; here we investigate this property, and describe a meta-search approach to finding the most effective cost function for this class of problems.

Substitution boxes are important components in many modern day block and stream ciphers. Their study has attracted a great deal of attention over many years. The development of a variety of cryptosystem attacks has lead to the development of criteria for resilience to such attacks. Some general criteria such as high nonlinearity and low autocorrelation have been proposed (providing some protection against attacks such as linear cryptanalysis and differential cryptanalysis). There has been little application of evolutionary search to the development of s-boxes. In This work we show how a cost function that has found excellent single-output Boolean functions can be generalised to provide improved results for small s-boxes.

Security protocols play an important role in modern communications. However, security protocol development is a delicate task, and experience shows that computer security protocols are notoriously difficult to get right. Recently, Clark and Jacob provided a framework for automatic protocol generation based on combinatorial optimization techniques and the symmetric key part of BAN logic. This paper shows how such an approach can be further developed to encompass the full BAN logic without the loss of efficiency and thereby synthesize public key protocols and hybrid protocols.

The design of Boolean functions with properties of cryptographic significance is a hard task. In this paper, we adopt an unorthodox approach to the design of such functions. Our search space is the set of functions that possess the required properties. It is “Boolean‐ness” that is evolved.

Security protocols play an important role in modern communications. However, security protocol development is a delicate task, and experience shows that computer security protocols are notoriously difficult to get right. Recently, Clark and Jacob (2001) provided a framework for automatic protocol generation based on combinatorial optimization techniques and the symmetric key part of BAN logic. This paper shows how such an approach can be further developed to encompass the full BAN logic without loss of efficiency and thereby synthesize public key protocols and hybrid protocols.

The design of Boolean functions with properties of cryptographic significance is a hard task. In this paper, we adopt an unorthodox approach to the design of such functions. Our search space is the set of functions that possess the required properties. It is 'Booleanness' that is evolved.

Research in the area of role-based access control has made fast progress over the last few years. However, little has been done to identify and describe existing role-based access control systems within large organisations. This paper describes the access control system of a major European Bank. An overview of the systems structure, its administration and existing control principles constraining the administration is given. In addition, we provide an answer to a key question - the ratio of the number of roles to the system user population - which was raised in the recent RBAC2000 Workshop. Having described certain weaknesses of the Banks system, the case study is extended to a comparison between the system and the RBAC96 models. In particular the issues of inheritance and grouping are addressed.

Tradeoffs are an important part of engineering security. Protocol security is important. So are efficiency and cost. The paper provides an early framework for handling such aspects in a uniform way based on combinatorial optimisation techniques. BAN logic is viewed as both a specification and proof system and as a "protocol programming language". The paper shows how evolutionary search in the form of genetic algorithms can be utilised to "grow" correct and efficient BAN protocols and shows how goals and assumptions can co-evolve, effectively engaging in "specification synthesis".

CSCW systems provide computer support to facilitate cooperation between users. In this paper we propose an approach for the formal specification of functionality requirements and confidentiality security requirements of a CSCW application. These requirements give rise to safety and confidentiality properties that a CSCW system, supporting the application, should uphold. The specification technique is illustrated with a case study.

CSCW systems provide computer support to facilitate cooperation between users. This paper proposes an approach to the formal specification of security requirements for CSCW applications, where a CSCW application is viewed as a collection of activitie

We build a mathematical structure in which we can ask questions about the methods for achieving security properties, such as confidentiality and integrity, and functionality properties, such as safety and liveness. The structure allows us to consider

A mathematical structure is built to represent integrity, where the word is used in the sense of preventing unauthorised modification of data. The author proves an important theorem relating functionality and integrity; the theorem tells one about the methods one may use to develop systems that satisfy integrity properties.>

Security (in the sense of confidentiality) properties are properties of shared systems. A suitable model of shared systems, in which one can formally define the term security property and then proceed to catalog several security properties, is presented. The purpose is to present various information-flow properties in a manner that exposes their differences and similarities. Abstraction is the main tool, and everything that is not central to the purpose is discarded. The presentation is generic in the model of computation. The abstraction lays bare a regular structure into which many interesting information-flow properties fall. A shared system is represented by a relation. How this model lets one reason about information flow is discussed and the term information flow property is formally defined. Various information-flow properties are described. Composability and probabilistic security properties are addressed.>

Noninterference (see J.A. Goguen and J. Meseguer, 1982) is given an abstract definition in category-theoretic terms. Unwinding theorems are investigated from this starting point. The theorems assume that commands form a monoid. Thus the results do not apply to systems where some sequences of commands are syntactically invalid. The extension to categories would generalize the results to languages where not every string is a syntactically valid program. It is concluded that category theory is a powerful tool for reasoning about noninterference.>

The author discusses the problems in deriving a system from its specification when that specification includes simple trace-based information-flow security properties as well as safety properties. He presents two fundamental theorems of information-flow security which describe the inherent difficulties of deriving secure implementations and considers the implications of these results. It is concluded that it is dangerous to extrapolate from success in the case of two to the case of many. Results proved about systems with just low- and high-access users may not extend easily to full lattices.>

A security and specification-oriented semantics for systems is given. The semantic model is derived from that for the trace model of C.A.R. Hoare's (1980) communicating sequential processes and is used to define various security concepts, such as multilevel secure systems, trusted users and integrity. It is indicated how implementations of secure systems can be derived from their specifications.>