Publications

This paper presents an analysis of an asynchronous communication mechanism due to Simpson. The properties required of an abstract version of the mechanism are discussed. Simpson's mechanism is described in terms of a process algebraic model. We then use automated techniques to test this mechanism against the properties stated.

The software control systems that are embedded in many products are increasingly complex. There are many stages in the typical software design life cycle, and these include testing, and sometimes use formal methods.
This thesis aims to strengthen the design life cycle by demonstrating a pragmatic use of formal methods for an industrially-applicable design method.
We take a design method and notation called DORIS (which is used by British Aerospace), and give a formal syntax for the notation. This then forms the structure into which we place activities (the active processing parts of the system), and intercommunication data areas (IDAs, the `passive' parts of the system through which activities communicate).
We aim to give an industrially useful semantics for this notation, so we use several models of Timed CSP as the underlying semantic domain. This allows us to represent the many timed and liveness requirements in BAe's work using the well-understood theory for Timed CSP.
For a given system design, we can generate a Timed CSP representation of the system from its DORIS design. This representation is an abstraction of the behaviour of the system modelling the interactions between components in that system. This Timed CSP model can be analyzed and assertions tested against it. However, because of the size of these systems, tool support is necessary.
The final part of this thesis concerns the construction of such tool-supported proofs, using both a bespoke tool for generating Timed CSP from the DORIS design, and two industrial-strength tools, PVS and FDR. We illustrate this with two case studies, one of them a significant model based on a real system.
This work demonstrates that even when using current state-of-the-art tools, it is difficult to apply these methods in practice. We conclude that without significant advances in tool technology, it will continue to be difficult to prove non-trivial properties about large systems at the level of abstraction presented in this thesis.

Modeling languages, like programming languages, need to be designed if they are to be practical, usable, accepted, and of lasting value. We present principles for the design of modeling languages. To arrive at these principles, we consider the intended use of modeling languages. We conject that the principles are applicable to the development of new modeling languages, and for improving the design of existing modeling languages that have evolved, perhaps through a process of unification. The principles are illustrated and explained by several examples, drawing on object-oriented and mathematical modeling languages.

A graphical notation for representing Timed CSP (TCSP) specifications is presented. The notation, which integrates features from a number of existing specification languages, including Statecharts, is aimed at providing the means for more easily constructing and managing large TCSP specifications, with the intention of forming the basis for tools and a methodology for applying TCSP in the large. The graphical notation extends TCSP by allowing specifications to be both processes and arbitrary predicates, thus increasing the expressiveness and applicability of the notation. An extendible tool framework, designed for the graphical notation and to be integrated with other tools, is presented. We discuss the features of this framework, especially how it aims to support reasoning about TCSP specifications.

A method, based on BON [17], for building reliable object-oriented software systems was proposed in [14]. It combined use of modelling and Extreme Programming [1] (XP) practices, emphasizing the use of a limited set of views of a software system, with consistency rules and automatic generation tools defined between the views. This paper builds upon this framework and formally specifies the consistency constraints between the two BON views: the static view provided by class diagrams, and the dynamic view provided by collaboration diagrams. The constraints are specified as an extension of the BON metamodel from [12], and are implemented in PVS. They ensure that the sequence of messages appearing in the dynamic view are permitted, given the contracts appearing in the static view. A sketch of how the constraints might be implemented in a BON CASE tool is also provided.
A revised version of this paper was published in Proc.~Fourth Workshop on Rigorous Object-Oriented Methods (ROOM4), London, UK, Springer, March 2002.

We present a formal, mechanically checked specification of the consistency constraints between two views of object-oriented systems described in BON: the static view provided by class diagrams annotated with contracts, and the dynamic view provided by collaboration diagrams. The constraints are specified as an extension of the BON metamodel, and are implemented in PVS. They ensure that the sequence of messages appearing in the dynamic view is legal, given the pre- and postconditions of methods appearing in the static view. A sketch of how the constraints might be implemented in the BON CASE tool is also provided.

Hehner's theory of predicative programming is a general-purpose refinement calculus for producing correct sequential, concurrent, real-time, and communicating programs from specifications. However, only limited tool support exists for this theory. We give an overview of an ongoing project on how we are providing support for predicative programming via PVS, particularly for discharging the proof obligations that arise during algorithm refinement, and specifically, in the domain of real-time applications.

The academic literature concerning fault tree analysis relates almost entirely to the design and development of safety-critical systems. This paper illustrates how similar techniques can be applied to the design and analysis of security-critical systems. The application of this technique is illustrated in an example inspired by a current public-key cryptosystem.

A formal, mechanically checked specification of the consistency constraints between two views of object-oriented systems are presented. The views, described in the BON modelling language, capture the static architecture of systems via contract-annotated class diagrams, and the dynamic view provided by collaboration diagrams. The constraints are specified as an extension of the BON metamodel, and are implemented in PVS. They ensure that the sequence of messages appearing in the dynamic view is legal, given the pre- and postconditions of methods appearing in the static view. An example of how the PVS theorem prover might be used to verify view consistency is described.

An agile methodology that integrates selected XP practices, UML modeling and Enterprise Java Beans is described. A case study in the domain of web-based systems is outlined, which applies and assesses the utility of the methodology. The applicability of agile modeling to the domain of webbased e-commerce systems implemented using Enterprise Java Beans is discussed.

Ongoing work is described in which a theory of Eiffel reference and expanded (composite) types is formalised. The theory is expressed in the PVS specification language, thus enabling the use of the PVS theorem prover and model checker to semi-automatically prove properties about Eiffel structures and programs. The theory is being used as the basis for automated support for the Eiffel Refinement Calculus.

The problem of checking the consistency of different views of a system is presented, and a test-based approach which is being implemented in the context of an object-oriented CASE tool is described using the Eiffel language. The approach is novel in that: it supports design-by-contract mechanisms, including preconditions, postconditions, and class invariants, which may be embedded within views; it is compatible with agile development practices; and, it requires only a compiler and a CASE tool (for constructing models) in order to be applied. The agile development process in which the approach is intended to be used is outlined.

A significant limitation with object-oriented formal specification languages, such as Object-Z, is that they lack development and management processes, which can be used to guide the production of reliable, robust object-oriented systems. An integration of an object-oriented methodology, BON, and Object-Z is presented in order to add an industrially validated development process to Object-Z. An extensible CASE tool for BON is also described that supports the integration with an Object-Z code generation engine.

This paper outlines some important issues that relate to security attacks against mobile ad hoc networks from research carried out at Network Research Group, University of Plymouth, on designing intrusion detection system for mobile ad hoc network. In designing security mechanisms for mobile ad hoc networks, one must consider the attacks variations as well as the characteristics of the attacks that could be launched against the ad hoc networks. The discussions of these two aspects are summarized in this paper. This paper also classifies several common attacks against the ad hoc networks routing protocols based upon the techniques that could be used by attackers to exploit routing messages. Those techniques are modification, interception, fabrication, and interruption.

A broad range of interactive and distributed systems are essentially virtual worlds; these include examples such as multiplayer games, and even operating systems. They enable the formation and maintenance of virtual societies, which must be healthy in order to be prosperous and useful. We describe properties, inspired by writings on law and psychology, that we use to define the notion of fairness, which is an essential characteristic of a healthy society. By using multiplayer gaming as a running example, we discuss how a fair virtual society will interact with its real-world counterparts, and outline how one might choose to detect and deal with transgressors who violate rules designed to enable fair interaction and prohibit cheating. This is a conceptual paper, and raises a number of issues and problems that must be considered when designing virtual worlds. Our aim is to develop guidelines for the design of fair virtual societies.

Metamodels precisely define the constructs and underlying well-formedness rules for modelling languages. They are vital for tool vendors, who aim to provide support so that concrete models can be checked formally and automatically against a metamodel for conformance. This paper describes how an executable metamodel which supports fully automated conformance checking was developed using a model-driven extension of test-driven development. The advantages and disadvantages of this approach to building metamodels are discussed.

A metamodel defines the well-formedness rules for a modelling language such as UML. We outline how an executable metamodel was designed and implemented using an agile method based on test-driven development that aimed at achieving high reliability. The test-driven approach was augmented with design-by-contract techniques to increase the likelihood of obtaining a correct, robust implementation.

Providing a robust and reliable Intrusion Detection System (IDS) for Mobile Ad Hoc Network (MANET) is not as straightforward as in the wired networks because of the characteristics, threats and vulnerabilities, and security requirements related to such network. This paper discusses these issues along with a discussion of the existing research works that have been proposed to secure MANET. After considering these issues, a novel IDS framework (a two-tier IDS for MANET), is proposed to improve the performance of existing IDS in MANET environment.

We describe a contract-aware unit testing framework, E-Tester, for the Eiffel programming language. The framework differs from JUnit in its first-class support for lightweight formal methods, through test support for contracts and assertions. As well, it supports a form of negative test, called violation cases, which aim at validating contracts. It also differs based on its use of agents for expressing tests and test cases. We compare E-Tester with JUnit and suggest several advantages it offers, with the additional aim of making recommendations for improving JUnits support for testing software with contracts. We also explain how it can be applied within a test-driven process for building reliable systems.

Software development methods are software products, in the sense that they should be engineered by following a methodology to meet the behavioural and non-behavioural requirements of the intended users of the method. We argue that agile approaches are the most appropriate means for engineering new methods, and particularly for integrating formal methods. We show how agile principles and practices apply to engineering methods, and demonstrate their application by integrating parts of the Eiffel development method with CSP.

A secure system is one that is protected against specific undesired outcomes. Delivering a secure system, and particularly a secure web application, is not easy. Integrating general-purpose information systems development methods with security development activities could be a useful means to surmount these difficulties.
Agile processes, such as Extreme Programming, are of increasing interest in software development. Most significantly for web applications, agile processes encourage and embrace requirements change, which is a desirable characteristic for web application development.
In this paper, we present an agile process to deliver secure web applications. The contribution of the research is not the development of a new method or process that addresses security concerns. Rather, we investigate general-purpose information system development methods (e.g., Feature-Driven Development (FDD)) and mature security methods, namely risk analysis, and integrate them to address the development of secure web applications. The key features of our approach are (1) a process capable of dealing with the key challenges of web applications development, namely decreasing life-cycle times and frequently changing requirements; and (2) an iterative approach to risk analysis that integrates security design throughout the development process.

Purpose --- This paper presents the process of constructing a language tailored to describing insider threat incidents, for the purposes of mitigating threats originating from legitimate users in an IT infrastructure.
Design/methodology/approach --- Various information security surveys indicate that misuse by legitimate (insider) users has serious implications for the health of IT environments. A brief discussion of survey data and insider threat concepts is followed by an overviewof existing research efforts tomitigate this particular problem. None of the existing insider threat mitigation frameworks provide facilities for systematically describing the elements of misuse incidents, and thus all threat mitigation frameworks could benefit from the existence of a domain specific language for describing legitimate user actions.
Findings --- The paper presents a language development methodology which centres upon ways to abstract the insider threat domain and approaches to encode the abstracted information into language semantics. The language construction methodology is based upon observed information security survey trends and the study of existing insider threat and intrusion specification frameworks.
Originality/value --- This paper summarizes the picture of the insider threat in IT infrastructures and provides a useful reference for insider threat modeling researchers by indicating ways to abstract insider threats.
Keywords Data security, Information systems
Paper type Conceptual paper

Software product lines are sets of software systems that share common features. Product lines are built as if they were a family of products, identifying those features that change and those that can be reused. There is an evident incompatibility between the requirements of software product lines and agile practices. We report on experiments that used Feature-Driven Development to build software product lines, and describe the minor extensions that were useful for developing software product lines.

A new taxonomy is proposed in which the type of output and the data scale over which an intrusion system operates is used for classification. This taxonomy allows a graphical comparison of different intrusion systems to be undertaken in terms of their footprint on an intrusion matrix. It is proposed that quantitative comparison of systems can only be undertaken at points of overlap of their footprints and that overlap specific measures are needed for this comparison. New areas of application for intrusion systems are also discussed.

This book constitutes the refereed proceedings of the Third International Conference on Security in Pervasive Computing, SPC 2006, held in York, UK, in April 2006.
The 16 revised papers presented together with the extended abstract of 1 invited talk were carefully reviewed and selected from 56 submissions. The papers are organized in topical sections on protocols, mechanisms, integrity, privacy and security, information flow and access control, and authentication.

Existing Intrusion Detection Systems (IDS) in Mobile Ad Hoc Net-work (MANET) environments suffer from many problems because of the inherent characteristics of the network. Limited audit data, along with the problems faced in achieving global detection and response mechanisms, creates challenges for establishing reliable IDS for MANETs. In this paper, several scenarios are investigated where a friend concept has been applied to solve MANET problems. This same concept is applied to a new IDS framework, and discussion is presented into how it can help in minimizing the problems that are faced in existing IDS. The key advantages of this two-tier IDS framework are its ability to detect intrusion at an early stage of such behaviour in the network, and its capability to minimize the impact of colluding blackmail attackers in the systems.

Security is a critical part of systems development, particularly for web-based systems. There is little known about how to effectively integrate security into incremental development processes such as Extreme Programming. This paper presents the results of a project that used Extreme Programming practices and deferred consideration of security until system functionality was complete. The findings suggest that refactorings within incremental development processes are capable of delivering high quality security solutions, and provide insights into how security requirements can be incorporated in the planning game.

Simple Concurrent Object-Oriented Programming (SCOOP) is the leading proposed mechanism for introducing concurrency to Eiffel. We summarise our position on the status of SCOOP, and on the open issues and research questions that should be addressed.

Simple Concurrent Object-Oriented Programming (SCOOP) is the leading proposedmechanism for introducing concurrency to Eiffel. We outline a number of concerns, related to the semantics of SCOOP, and present an alternative concurrencymodel for Eiffel that alleviatesmany of these problems. Comparison with the SCOOP model is made, and ongoing work on evaluating the alternative model is discussed. A sketch of the model in CSP is given.

Preface This volume contains the papers presented at the First International Symposium on Concurrency, Real-Time, and Distribution in Eiffel-like Languages (CORDIE 2006), held 4-5 July, 2006, at the King's Manor, York, United Kingdom.
The symposium's focus was on evolving concurrency, real-time and distribution mechanisms in object-oriented languages that supported features like those appearing in Eiffel. In particular, we saw a substantial emphasis on the relationships between Eiffel-like contracts (i.e., routine pre- and postconditions, and class invariants), and mechanisms for concurrency such as synchronisation and locking. Topics of interest included contracts for concurrency, real-time extensions, formal models and semantics for concurrency in Eiffellike languages, tool support, distributed middleware, synchronisation, locking, asynchronous exception handling, and formal verification.
The programme committee accepted 9 full papers for presentation, some after a second round of review and revision. Each submission was reviewed by at least three members of the international programme committee. We are grateful to the programme committee members for their timely completion of the reviewing process, and for the quality and detail of their reviews and discussion.
Our thanks go to all members of the programme committee for their efforts; the authors, for submitting their papers; our invited speakers, Andy Wellings and Antónia Lopes; our closing speaker, Bertrand Meyer; our sponsors: the ARTIST Network of Excellence, the University of Teesside, the University of York, and the Chair of Software Engineering, ETH Zürich. We also thank Formal Methods Europe for their support in advertising the event.

There are some application domains to which it appears intrinsically challenging to introduce the services offered by formal engineering methods. This paper is an evidence-based presentation that lightweight formal methods are effective in building realistic networked multiplayer games. The evidence is produced via a pilot study that uses Design-by-Contract, under realistic game development conditions, and encompasses both qualitative and empirical results.

Modern online multiplayer games are complex heterogeneous distributed systems comprised of servers and untrusted clients, which are often engineered under considerable commercial pressures. Under these conditions, security breaches allowing clients to employ illegal behaviours have become common; current commercial approaches have limited capabilities for reacting rapidly to such threats. This paper presents an approach to the detection of a cheating player, and describes a proof-ofconcept system designed to detect cheating play (specifically wallhacking) through the analysis of player behaviour. This approach differs from current methods in that it does not rely on knowledge about specific vulnerabilities and their method of exploitation in order to protect the system, but instead monitors player behaviour for indications of cheating play. Statistical evidence is presented which shows that the proof-of-concept correctly distinguishes between most cheating and non-cheating players.

The success of authentication mechanisms, intrusion detection and response systems, and other security measures to protect MANET from attack are very much dependant on nodes' cooperation. Ensuring a node's cooperation is very challenging in a MANET environment because of the nature of such a network; consisting of a set of anonymous nodes that operate independently, without the existence of a central authority to enforce them to cooperate. One of the solutions for this problem is by creating a trust chain between nodes to create a trusted community. This paper discusses some of the existing studies that have been proposed to overcome this issue and proposes a novel trust framework based upon a friendship concept. Results from simulation experiments proved that the proposed trust framework is capable of creating a trusted community in MANET, whilst at the same time addressing limitations of existing trust frameworks.

Purpose To propose a new taxonomy for intrusion detection systems as a way of generating further research topics focussed on improving intrusion system performance.
Approach Intrusion systems are characterised by the type of output they are capable of producing, such as intrusion/non-intrusion declarations, through to intrusion plan determination. The output type is combined with the data scale used to undertake the intrusion determination, to produce a two-dimensional intrusion matrix.
Findings Different approaches to intrusion detection can produce different footprints on the intrusion matrix. Qualitative comparison of systems can be undertaken by examining the area covered within the footprint and the footprint overlap between systems. Quantitative comparison can be achieved in the areas of overlap.
Research Implications --- The comparison of systems based on their footprint on the intrusion matrix may allow a deeper understanding of the limits of performance to be developed. The separation of what was previously understood as detection into the three areas of Detection, Recognition and Identification may provide further impetus for the development of a theoretical framework for intrusion systems.
Practical Implications The intrusion matrix can be divided into areas in which the achievement of arbitrarily high performance is relatively easily achievable. Other areas within the matrix, such as the Prosecution and Enterprise regions, present significant practical difficulties and therefore are opportunities for further research.
Originality --- The use of a taxonomy based on the type of output produced by an intrusion system is new to this paper, as is the combination with data scale to produce an intrusion matrix. The recognition that the network data scale should also be split to differentiate trusted and untrusted networks is new and presents challenging opportunities for further research topics.

We have recently constructed a model, and carried out an analysis, of a concurrent extension to an object-oriented language at a level of abstraction above threads. The model was constructed in CSP.
We subsequently found that existing CSP tools were unsuitable for reasoning about and analysing this model, so it became necessary to create a new tool to handle CSP models: CSPsim.
We describe this tool, its capabilities and algorithms, and compare it with the related tools, FDR2 and ProBE. We illustrate CSPsim's usage with examples from the model. The tool's on-the-fly construction of successor states is important for exhaustive and non-exhaustive state exploration. Thus we found CSPsim to be particularly useful for parallel compositions of components with infinite states that reduce to finite-state systems.

Current practice suggests that security is considered through all stages of the software development life cycle, and that a risk-based and plan-driven approach is best suited to establish security criteria. Based on experience in applying security practices, this paper proposes two new security practices, security training and a fundamental security architecture, for applying Extreme Programming.

Model-driven development --- using languages such as UML and BON --- often makes use of multiple diagrams (e.g., class and sequence diagrams) when modelling systems. These diagrams, presenting different views of a system of interest, may be inconsistent. A metamodel provides a unifying framework in which to ensure and check consistency, while at the same time providing the means to distinguish between valid and invalid models, i.e., conformance. Two formal specifications of the metamodel for an object-oriented modelling language are presented, and it is shown how to use these specifications for model conformance and multi-view consistency checking. Comparisons are made in terms of completeness and the level of automation each provide for checking multi- view consistency and model conformance. The lessons learned from applying formal techniques to the problems of metamodelling, model conformance, and multi-view consistency checking are summarized.

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.

We describe the problem of asynchronous exceptions in Eiffel's Simple Concurrent Object-Oriented Programming (SCOOP). We discuss a range of possible solutions to further enable dependable computing in concurrent Eiffel. We propose a mechanism to handle asynchronous exceptions via a limited developer choice, including the notion of a failed or dead object, and necessarily introduce a small number of new exceptions. We additionally describe a number of mechanisms that were discarded as unsuitable.

Nowadays, a commonly used wireless network (i.e., Wi-Fi) operates with the aid of a fixed infrastructure (i.e., an access point) to facilitate communication between nodes. The need for such a fixed supporting infrastructure limits the adaptability and usability of the wireless network, especially in situations where the deployment of such an infrastructure is impractical. Recent advancements in computer network introduced a new wireless network, known as a mobile ad hoc network (MANET), to overcome the limitations. Often referred as a peer to peer network, the network does not have any fixed topology, and through its multi hop routing facility, each node can function as a router, thus communication between nodes becomes available without the need of a supporting fixed router or an access point. However, these useful facilities come with big challenges, particularly with respect to providing security. A comprehensive analysis of attacks and existing security measures suggested that MANET are not immune to a colluding blackmail because such a network comprises autonomous and anonymous nodes. This paper addresses MANET security issues by proposing a novel intrusion detection system based upon a friendship concept, which could be used to complement existing prevention mechanisms that have been proposed to secure MANETs. Results obtained from the experiments proved that the proposed concepts are capable of minimising the problem currently faced in MANET intrusion detection system (IDS). Through a friendship mechanism, the problems of false accusations and false alarms caused by blackmail attackers in intrusion detection and response mechanisms can be eliminated.

Distributed processing has a strong theoretical foundation, but many day-to-day practitioners make limited use of the advantages this theory can give them. The result includes unreliable systems with obscure and intermittent failures that can cost time, money and in extreme cases, lives. Reliable construction of distributed and concurrent systems must incorporate theory in practice.
This book provides a concise presentation of the theory closely linked to the practical realisation of these concepts. This easy-to-follow textbook focuses on practical issues of building working distributed systems and gives an overview of the basic theory, principles and techniques, whilst illustrating how these fit together, via the process of building interesting, non-trivial systems.

Critical systems must be shown to be acceptably safe and secure to deploy and use in their environment. But the size, scale, heterogeneity, and distributed nature of these increasingly complex systems makes them difficult to verify and analyse. Additionally, domain experts use a variety of languages to model and build their systems. We present an automated safety analysis technique, Fault Propagation and Transformation Analysis, and explain how it can be used for automatically calculating the failure behaviour of an entire system from the failure behaviours of its components. We outline an implementation of the technique in the Epsilon model management platform, thus allowing it to be used in combination with state-of-the-art model management languages and tools, and making it applicable to a variety of different domain-specific modelling languages.

We describe the results of a pilot study on the application of an agile process to building a high-integrity software system. The challenges in applying an agile process in this domain are outlined, and potential solutions for dealing with issues of communication, scalability, and system complexity are proposed. We report on the safety process, argumentation generated to support the process, and the technology and tools used to strengthen the agile process in terms of support for verification and validation.

We present a new concurrency model for the Eiffel programming language. The model is motivated by describing a number of semantic problems with the leading concurrency model for Eiffel, namely SCOOP. Our alternative model aims to preserve the existing behaviour of sequential programs and libraries wherever possible. Comparison with the SCOOP model is made. The concurrency aspects of the alternative model are presented in CSP along with a model of exceptions. The results show that while the new model provides increased parallelism, this comes with the price of increased overhead due to lock management.

In the autonomous environment of mobile ad hoc network (MANET) where nodes are free to move around and depend on each other to initiate communication, cooperation among nodes is an essential component of a successful data transmission process. Since there is no central controller such as router to determine the communication paths in MANET, each node in the ad hoc network has to rely on each other in order to forward packets, thus highly cooperative nodes are required to ensure that the initiated data transmission process does not fail. However, it is hard to encourage cooperativeness among nodes for each node owns limited resources that need to be preserved. These particular nodes which are also known as selfish nodes refuse to help other nodes in forwarding packets due to the anxiety of having resource degradation such as exhausted battery power and limited processor capability. This problem has aroused several issues in MANET: routing, security, Quality of Service (QoS), resource management and auto-configuration. Hence, there is a need to provide a mechanism that can encourage cooperation among nodes without jeopardizing their resources. In this paper, we provide evidence through simulation experiments on how a friendship concept could be used to minimize the number of false alarms raised in MANET Intrusion Detection System (IDS). In addition, we propose a security enhancement for the friendships mechanism by implementing trust features and show the effects of having such implementation in the existing friendships mechanism through simulation experiments. We also discuss on how the similar friendships concept could be used to address several challenges faced in MANET environment.

The use of digital document management and processing is increasing. Traditional workflows of paper forms are being replaced by electronic workflows of digital documents. These workflows often require multiple signatures to be added to the documents for authorisation and/or integrity.
We describe examples of digital workflows that illustrate problems with digital signatures: i.e., the use of digital signatures across entire documents results in signatures that can be unnecessarily invalidated by subsequent modification of the document. We propose the use of fragment signatures which reduce unnecessary invalidation of signatures and enable greater concurrency in workflows. Our approach is document-centric and does not use a centralised database.
We report on an implementation that allows fragment signatures over document fragments as well as the attachment (or embedding) of other documents. This allows collaborative or cooperative editing to occur on parts of a document without disturbing unrelated signatures. We describe the lessons learned from our deployments and offer further ways to embed such signatures into other document types.

Honey-pots and honey-nets are network-accessible decoy resources designed to attract unauthorized users, thereby deflecting their attention from security-critical systems. Combined with a process known as a LaBrea tar pit, honey-net and honey-pots can effectively entrap suspicious connection attempts and prevent the proliferation of further attacks via the host network. Use of these ‘sticky’ honey-pots and honey-nets is quite common within the network security community, and several ‘off the shelf’ solutions are available to individuals and commercial clients alike.
In this paper we describe a LaBrea tar-pit honey-net solution specifically designed for researchers interested in network security. Unlike the various honey net solutions mentioned above, this solution gives the user direct access to raw, packet-level data. Our reference implementation is built around a customized firewall distribution which acts as the honey-net bridge. This bridge uses an BSD-based firewall distribution known as PFSense in combination with a highly customizable network packet capturing facility called tcpdump.
The contribution of this work is twofold. Firstly, our reference implementation will enable researchers to quickly deploy a medium interaction honey-net network (with LaBrea Tar-pit functionality) that is more secure, more adaptable and more upgradeable than comparable systems. Secondly, our reference implementation will allow researchers to transparently gather raw, live-traffic data without the additional overhead of performing on-site traffic analysis. It is hoped that this will stimulate higher quality dataset collection throughout the network security field.

Typically, safety critical software systems are developed using plan-driven development processes. Agile processes have evolved to help reduce costs of software development and seek to minimise documentation overheads. For safety critical systems that must undergo certification, documentation is essential. The question this paper addresses is: can a process based on agile principles be used to deliver a safety critical software product, but also the evidence needed to satisfy assurance objectives? The paper makes three contributions. Firstly, it presents an analysis of agile processes and their applicability in this domain. It reviews positive indicators for their use, outlines challenges associated with their deployment and proposes strategies for addressing these challenges. Secondly, it makes a number of recommendations for adapting an agile process to the domain. Finally, the paper reports on an experiment to demonstrate the plausibility of using of an adapted agile process for building a safety critical software system.

Cheating is a key issue in multiplayer games as it causes unfairness which reduces legitimate users' satisfaction and is thus detrimental to game revenue. Many commercial solutions prevent cheats by reacting to specific implementations of cheats. As a result, they respond less efficiently to fast changing cheat techniques. This work proposes a framework which takes advantage of formal methods to discover the knowledge for categorising game players and then detecting cheats from server-visible game behaviours. We argue that this cheat detection is more resistant to changing cheat techniques.
Keywords: Cheat detection, multiplayer games, Event-B

Many security scenarios involve both network and cryptographic protocols and the interactions of different human participants in a real-world environment. Modelling these scenarios is complex, in part due to the imprecision and underspecification of the tasks and properties involved. We present work-in-progress on a domain-specific modelling approach for such scenarios; the approach is intended to support coarse-grained state exploration, and incorporates a classification of elements complementary to computer protocols, such as the creation, personalisation, modification and transport of identity tokens. We propose the construction of a domain-specific language for capturing these elements, which will in turn support domain-specific analyses related to the reliability and modifiability of said scenarios.

Complex systems exhibit emergent behaviour. The explanations for this explicit emergent behaviour are often difficult to identify, and usually require understanding of significant parts of system structure and component behaviour to interpret. We present ongoing work on a set of techniques, based on Model-Driven Engineering principles and practices, for helping to reveal explanations for system complexity. We outline the techniques abstractly, and then illustrate parts of them with three examples from the health care, system security and Through-Life Capability Management domains.

Cryptographic mechanisms are used in a wide range of applications, including email clients, web browsers, document and asset management systems, where typical users are not cryptography experts. A number of empirical studies have demonstrated that explicit, user-visible cryptographic mechanisms are not widely used by non-expert users, and as a result arguments have been made that cryptographic mechanisms need to be better hidden or embedded in end-user processes and tools. Other mechanisms, such as HTTPS, have cryptography built-in and only become visible to the user when a dialogue appears due to a (potential) problem. This paper surveys deployed and potential technologies in use, examines the social and legal context of broad classes of users, and from there, assesses the value and issues for those users.

As a system-level modelling language, SystemC possesses several novel features such as delayed notifications, notification cancelling, notification overriding and delta-cycle. It also has real-time and shared-variable features. Previously we have studied an operational semantics for SystemC Peng et al. (An operational semantics of an event-driven system-level simulator, pp 190–200, 2006) and bisimulation has been introduced based on some aspects of reasonable abstractions. The denotational method is another approach to studying the semantics of a programming language. It provides the mathematical meaning to programs and can predict the behaviour of programs. Due to the novel features of SystemC, it is challenging to study the denotational semantics for SystemC. In this paper, we apply Unifying Theories of Programming (abbreviated as UTP) Hoare and He (Unifying theories of programming, 1998) in exploring the denotational semantics. Two trace variables are introduced, one to record the state behaviours and another to record the event behaviours. The timed model is formalized in a threedimensional structure. A set of algebraic laws is explored, which can be proved via the presented denotational semantics. In this paper, we also consider the linking between denotational semantics and algebraic semantics. The linking is obtained by deriving the denotational semantics from algebraic semantics for SystemC. A complete set of parallel expansion laws is explored, where the location status of an instantaneous action is studied. The location status indicates an instantaneous action is due to which exact parallel component. We introduce the concept of head normal form for each program and every program is expressed in the form of guarded choice with location status. Based on this, the derivation strategy for deriving denotational semantics from algebraic semantics is provided.

I describe a secondment to the cybercrime area of Cleveland police. My normal employment is as a Reader in Computer Science at Teesside University’s School of Computing.
I applied for a secondment having worked full-time in academia for over a decade. My previous non-academic employment was in the Civil Service in a research and development role. As my academic interests have steadily shifted from formal methods to information security and the use of computers in crime, it seemed appropriate to apply for a formal secondment to a police or similar agency.
As I already had some engagement with Cleveland Police and knew that this was an area of significant interest to them, it was clear that this would be a valuable secondment to myself, the police and the university.
This report necessarily omits some details due to their sensitivity. To aid dissemination of the secondment results, I provide a protectively-marked annex to this report for police and other law enforcement agencies.

Investigation of cyber-dependent and cyber-enabled crimes requires the capture of evidence from Internet sources. Common examples include social media such as Facebook, Twitter and Youtube. The computers hosting this content are typically difficult to physically access, sometimes in a different country and may pose great inconvenience to innocent parties if seized. More generally, offences that traditionally had no computer element increasingly involve computers, mobile devices or the Internet to some degree. As a result, there is increasing demand for Internet evidence capture.
This presentation reports a recent secondment of an academic computer scientist to Cleveland Police's cybercrime area. It describes the typical process of capturing evidence from Internet sources. Lessons from this project are described, including problems of scalability of tools and the need for flexibility of approaches, for example, when dealing with a requirement to collect large numbers of files. A set of prototype tools to improve productivity in an era of limited resources is briefly presented before highlighting outstanding issues in the management of cybercrime.
This presentation argues that greater automation is required and that there are specific educational and experience requirements for investigators. This becomes particularly acute should the number of investigations increase. We reflect on the use of volunteers in this type of work. Finally, possible ways to develop this work are proposed.
The secondment was funded by the Royal Academy of Engineering and hosted by Cleveland Police.

Purpose: To evaluate the value of user-visible cryptographic mechanisms in typical email and web scenarios.
Design/methodology/approach: Review of existing literature, analysis of mechanisms available via user stories.
Findings: The scenarios identified suggest that background, opportunistic encryption has value, but more explicit, user-visible cryptographic mechanisms do not provide any further mitigation.
Research limitations/implications: Further work should be carried out on the trust issues with trusted third parties, as they are intrinsic to global, automated cryptographic mechanisms.
Practical implications: Deployed systems should rely on automation rather than explicit user dialogues.
Social implications: The user populations concerned rely significantly on the existing legal and social infrastructure to mitigate some risks, such as those associated with e-commerce.
Originality/value: This work uses user stories as a basis for a holistic review of the issues surrounding the use of cryptography.
Keywords: Security, cryptographic controls, email, web, legal aspects, regulation, risk management

We propose the use of modern proof assistants to specify, implement, and verify password quality checkers. We use the proof assistant Coq, focusing on Linux PAM, a widely-used implementation of pluggable authentication modules for Linux. We show how password quality policies can be expressed in Coq and how to use Coq’s code extraction features to automatically encode these policies as PAM modules that can readily be used by any Linux system.
We implemented the default password quality policy shared by two widely-used PAM modules: pam_cracklib and pam_pwquality. We then compared our implementation with the original modules by running them against a random sample of 100,000 leaked passwords obtained from a publicly available database. In doing this, we demonstrated a potentially serious bug in the original modules. The bug was reported to the maintainers of Linux PAM and is now fixed.

Examples of arguably unprofessional or unethical behaviour related to IT are fairly commonly reported events. For a number of years, BCS has been encouraging coverage of related issues within accredited higher education provision. Phil Brooke FBCS, Tom Prickett MBCS, Shelagh Keogh MBCS and David Bowers FBCS report on this issue.