Digital Twin (DT) is a revolutionary technology changing how a smart manufacturing industry carries out its day-to-day activities. DT can provide numerous advantages such as real-time synchronised functioning, monitoring and data analysis. However, security and privacy issues in DT have not been thoroughly investigated. This article proposes a user-empowerment-based privacy-preserving authentication protocol for a cloud-based Digital Twin using a Decentralised Identifier (DID) and Verifiable Credential (VC). Here, user empowerment provides full control to users over their identities, and with the help of VC, users can prove their authenticity and preserve their privacy. Although DID has emerged as a promising technology for introducing user empowerment, it suffers from some fundamental problems such as usability and auditability. Here we address all these issues and propose a user-revocation-enabled security solution for the DT. A security analysis of the proposed scheme shows that it is secured against significant security threats. With the help of performance analysis, we prove that the proposed work effectively ensures security and privacy in DT.

Underwater Acoustic Sensor Networks (UW-ASNs) are predominantly used for underwater environments and find applications in many areas. However, a lack of security considerations, the unstable and challenging nature of the underwater environment, and the resource-constrained nature of the sensor nodes used for UW-ASNs (which makes them incapable of adopting security primitives) make the UW-ASN prone to vulnerabilities. This paper proposes an Adaptive decentralised Intrusion Detection and Prevention System called AIDPS for UW-ASNs. The proposed AIDPS can improve the security of the UW-ASNs so that they can efficiently detect underwater-related attacks (e.g., blackhole, grayhole and flooding attacks). To determine the most effective configuration of the proposed construction, we conduct a number of experiments using several state-of-the-art machine learning algorithms (e.g., Adaptive Random Forest (ARF), light gradient-boosting machine, and K-nearest neighbours) and concept drift detection algorithms (e.g., ADWIN, kdqTree, and Page-Hinkley). Our experimental results show that incremental ARF using ADWIN provides optimal performance when implemented with One-class support vector machine (SVM) anomaly-based detectors. Furthermore, our extensive evaluation results also show that the proposed scheme outperforms state-of-the-art bench-marking methods while providing a wider range of desirable features such as scalability and complexity.

IPv6 over Low-powered Wireless Personal Area Networks (6LoWPAN) has grown in importance in recent years, with the Routing Protocol for Low Power and Lossy Networks (RPL) emerging as a major enabler. However, RPL can be subject to attack, with severe consequences. Most proposed IDSs have been limited to specific RPL attacks and typically assume a stationary environment. In this article, we propose the first adaptive hybrid IDS to efficiently detect and identify a wide range of RPL attacks (including DIO Suppression, Increase Rank, and Worst Parent attacks, which have been overlooked in the literature) in evolving data environments. We apply our framework to networks under various levels of node mobility and maliciousness. We experiment with several incremental machine learning (ML) approaches and various ‘concept-drift detection’ mechanisms (e.g. ADWIN, DDM, and EDDM) to determine the best underlying settings for the proposed scheme.

Low-power and Lossy Networks (LLNs) comprise nodes characterised by constrained computational power, memory, and energy resources. The LLN nodes empower ubiquitous connections amongst numerous devices (e.g. temperature, humidity, and turbidity sensors, together with motors, valves and other actuators) to sense, control and store properties of their environments. They are often deployed in hostile, unattended, and unfavourable conditions. Securing them often becomes very challenging. The extent of interconnected LLN devices poses a series of routing threats (e.g. wormhole, grayhole, DIO suppression, and increase rank attacks). Consequently, an efficient and effective intrusion detection system (IDS) is of utmost importance in identifying anomalous activities in the IPv6 over Low-powered Wireless Personal Area Networks (6LoWPAN). This article proposes a robust Adversarial Reinforcement Learning (ARL) framework to generate efficient IDSs for evolving data environments. The integration of ARL and incremental machine-learning facilitates the generation of resource-efficient and robust IDS detectors. We demonstrate in particular how such an approach, leveraging notions of ’concept drift’ detection and adaptation, can handle inevitable changes in the environment, giving the IDS best chances of detecting attacks in the current profile. The range of routing attacks considered is the most comprehensive to date. For the first time, Black-box and Grey-box ML-based adversaries aiming to destabilise the 6LoWPAN are distinguished and addressed.

Human-robot collaboration is on the increase and having a major impact on areas such as manufacturing, where the abilities of the human worker, augmented by those of the robot, bring increased flexibility and performance. However, close collaboration, including physical interaction, brings with it complex safety and security issues that were previously mitigated by human-robot segregation and isolated control networks. Exoskeletons pose a particularly interesting case whereby physical coupling of the user and robot is required throughout operation. We envisage the use of continuous authentication to exoskeletons, i.e. to ensure a user is who they claim to be, and that they have sufficient authority to operate the device for the duration of its use. In this paper we demonstrate such an approach to behavioural biometrics using data acquired through wearable sensors (hand manipulations recorded by a sensorised glove) while the user performs a selection of industrial tasks, including handling loads and inserting screws. The results show that the approach can discriminate between users with a low Equal Error Rate (EER; <3% in the worst case analysed). We believe that such an approach will also benefit other applications where wearables are used in robot control, such as in tele-operation.

The Internet of Things (IoT) is revolutionising nearly every aspect of modern life, playing an ever greater role in both industrial and domestic sectors. The increasing frequency of cyber-incidents is a consequence of the pervasiveness of IoT. Threats are becoming more sophisticated, with attackers using new attacks or modifying existing ones. Security teams must deal with a diverse and complex threat landscape that is constantly evolving. Traditional security solutions cannot protect such systems adequately and so researchers have begun to use Machine Learning algorithms to discover effective defence systems. In this paper, we investigate how one approach from the domain of evolutionary computation - grammatical evolution - can be used to identify cyberattacks in IoT environments. The experiments were conducted on up-to-date datasets and compared with state-of-the-art algorithms. The potential application of evolutionary computation-based approaches to detect unknown attacks is also examined and discussed.

The Routing Protocol for low power Lossy networks (RPL) is a critical operational component of low power wireless personal area networks using IPv6 (6LoWPANs). In this paper we propose a Reinforcement Learning (RL) based IDS to detect various attacks on RPL in 6LoWPANs, including several un-addressed by current research. The proposed scheme can also detect previously unseen attacks and the presence of mobile intruders. The scheme is well suited to the resource constrained environments of our target networks.

One of the most promising applications of near-term quantum computing is the simulation of quantum systems, a classically intractable task. Quantum simulation requires computationally expensive matrix exponentiation; Trotter-Suzuki decomposition of this exponentiation enables efficient simulation to a desired accuracy on a quantum computer. We apply the Covariance Matrix Adaptation Evolutionary Strategy (CMA-ES) algorithm to optimise the Trotter-Suzuki decompositions of a canonical quantum system, the Heisenberg Chain; we reduce simulation error by around 60%. We introduce this problem to the computational search community, show that an evolutionary optimisation approach is robust across runs and problem instances, and find that optimisation results generalise to the simulation of larger systems.

Source code analysis techniques used for automated software testing are insufficient to find security flaws in programs. Therefore, security researchers have been employing also fuzzing techniques for finding bugs and vulnerabilities in target programs. With the proliferation of mobile devices, researchers have started to explore the use of fuzz tests on mobile platforms. While most of these studies are GUI-based and implemented at the application level, the detection of vulnerabilities in lower levels is very critical due to affecting a broader range of Android users. Therefore, in this study, a new approach is proposed to fuzz testing for Android application installation process. The use of a search heuristic namely genetic algorithms is investigated for efficient fuzz testing on DEX (Dalvik EXecutable) files. The proposed black box fuzzing tool called GFuzz is shown to be able to produce more unique crashes in Android in a shorter time than recently proposed similar approaches and to detect new and existing bugs.

For software quality assurance, many safety-critical industries appeal to the use of dynamic testing and structural coverage criteria. However, there are reasons to doubt the adequacy of such practices. Mutation testing has been suggested as an alternative or complementary approach but its cost has traditionally hindered its adoption by industry, and there are limited studies applying it to real safety-critical code. This paper evaluates the effectiveness of state-of-the-art mutation testing on safety-critical code from within the U.K. nuclear industry, in terms of revealing flaws in test suites that already meet the structural coverage criteria recommended by relevant safety standards. It also assesses the practical feasibility of implementing such mutation testing in a real setting. We applied a conventional selective mutation approach to a C codebase supplied by a nuclear industry partner and measured the mutation score achieved by the existing test suite. We repeated the experiment using trivial compiler equivalence (TCE) to assess the benefit that it might provide. Using a conventional approach, it first appeared that the existing test suite only killed 82% of the mutants, but applying TCE revealed that it killed 92%. The difference was due to equivalent or duplicate mutants that TCE eliminated. We then added new tests to kill all the surviving mutants, increasing the test suite size by 18% in the process. In conclusion, mutation testing can potentially improve fault detection compared to structural-coverage-guided testing, and may be affordable in a nuclear industry context. The industry feedback on our results was positive, although further evidence is needed from application of mutation testing to software with known real faults.

Test selection techniques are used to reduce the human effort involved in software testing. Most research focusses on selecting efficient sets of test cases according to various coverage criteria for directed testing. We introduce a new technique to select efficient sets of sub domains from which new test cases can be sampled at random to achieve a high mutation score. We first present a technique for evolving multiple sub domains, each of which target a different group of mutants. The evolved sub domains are shown to achieve an average 160% improvement in mutation score compared to random testing with six real world Java programs. We then present a technique for selecting sets of the evolved sub domains to reduce the human effort involved in evaluating sampled test cases without reducing their fault finding effectiveness. This technique significantly reduces the number of sub domains for four of the six programs with a negligible difference in mutation score.

The effectiveness of probabilistic structural testing depends on the characteristics of the probability distribution from which test inputs are sampled at random. Metaheuristic search has been shown to be a practical method of optimising the characteristics of such distributions. However, the applicability of the existing search-based algorithm is limited by the requirement that the software's inputs must be a fixed number of numeric values.

Search Based Software Engineering (SBSE) has proved to be a very effective way of optimising software engineering problems. Nevertheless, its full potential as a means of dynamic adaptivity remains under explored. This paper sets out the agenda for Dynamic Adaptive SBSE, in which the optimisation is embedded into deployed software to create self-optimising adaptive systems. Dynamic Adaptive SBSE will move the research agenda forward to encompass both software development processes and the software products they produce, addressing the long-standing, and as yet largely unsolved, grand challenge of self-adaptive systems.

Mutation testing is effective at measuring the adequacy of a test suite, but it can be computationally expensive to apply all the test cases to each mutant. Previous research has investigated the effect of reducing the number of mutants by selecting certain operators, sampling mutants at random, or combining them to form new higher-order mutants. In this paper, we propose a new approach to the mutant reduction problem using static analysis. Symbolic representations are generated for the output along the paths through each mutant and these are compared with the original program. By calculating the range of their output expressions, it is possible to determine the effect of each mutation on the program output. Mutants with little effect on the output are harder to kill. We confirm this using random testing and an established test suite. Competent programmers are likely to only make small mistakes in their programming code. We argue therefore that test suites should be evaluated against those mutants that are harder to kill without being equivalent to the original program.

Optimising programs for non-functional properties such as speed, size, throughput, power consumption and bandwidth can be demanding; pity the poor programmer who is asked to cater for them all at once! We set out an alternate vision for a new kind of software development environment inspired by recent results from Search Based Software Engineering (SBSE). Given an input program that satisfies the functional requirements, the proposed programming environment will automatically generate a set of candidate program implementations, all of which share functionality, but each of which differ in their non-functional trade offs. The software designer navigates this diverse Pareto surface of candidate implementations, gaining insight into the trade offs and selecting solutions for different platforms and environments, thereby stretching beyond the reach of current compiler technologies. Rather than having to focus on the details required to manage complex, inter-related and conflicting, non-functional trade offs, the designer is thus freed to explore, to understand, to control and to decide rather than to construct.

This paper reports findings from a multi-method set of four studies that investigate why we continue to fall for phish. Current security advice suggests poor spelling and grammar in emails can be signs of phish. But a content analysis of a phishing archive indicates that many such emails contain no obvious spelling or grammar mistakes and often use convincing logos and letterheads. An online survey of 224 people finds that although phish are detected approximately 80% of the time, those with logos are significantly harder to detect. A qualitative interview study was undertaken to better understand the strategies used to identify phish. Blind users were selected because it was thought they may be more vulnerable to phishing attacks, however they demonstrated robust strategies for identifying phish based on careful reading of emails. Finally an analysis was undertaken of phish as a literary form. This identifies the main literary device employed as pastiche and draws on critical theory to consider why security based pastiche may be currently very persuasive.

Invariants are concise and useful descriptions of a program's behaviour. As most programs are not annotated with invariants, previous research has attempted to automatically generate them from source code. In this paper, we propose a new approach to invariant generation using search. We reuse the trace generation front-end of existing tool Daikon and integrate it with genetic programming and a mutation testing tool. We demonstrate that our system can find the same invariants through search that Daikon produces via template instantiation, and we also find useful invariants that Daikon does not. We then present a method of ranking invariants such that we can identify those that are most interesting, through a novel application of program mutation.

Model checking is an automatic technique that exhaustively checks the state space of a system/program to prove if a specification is satisfied. If an error is detected, the precise circumstances of the issue are returned to the user in the form of a counterexample. Exhaustively checking the state space of a large system, a system with many concurrent components for example, is often intractable. In this scenario, heuristic mechanisms can be employed with the task of detecting errors rather than proving the system is correct. Recently, a metaheuristic EDA-based approach to detecting deadlock in multithreaded Java software has shown great promise in this area. In this paper, we extend that work to search Promela models for counterexamples. We show that the EDA-based technique can find errors where algorithms such as A* search fail. We also show the ability of the EDA to find shorter errors than those discovered by traditional heuristic methods.

The grapheme codebook is a high-performing technique for offline writer identification. This paper considers whether the de facto standards for initial grapheme extraction are optimal for both modern and historical datasets. We examine the construction and representation of the graphemes that comprise the codebook, testing three segmentation methods and two grapheme size normalisation methods on two datasets: a 93-writer IAM dataset, and a 43-writer medieval English dataset. The standard minima-split segmentation is compared to a complementary segmentation method that preserves ligature shapes, as well as the union of both these methods. Classification performance for each method is compared on a range of codebook sizes. We demonstrate that grapheme aspect-ratio is not always a writer-specific feature, and that preserving the character body shape in segmentation is more informative than preserving cursive text ligatures.

Most applications of genetic programming (GP) involve the creation of an entirely new function, program or expression to solve a specific problem. In this paper, we propose a new approach that applies GP to improve existing software by optimizing its non-functional properties such as execution time, memory usage, or power consumption. In general, satisfying non-functional requirements is a difficult task and often achieved in part by optimizing compilers. However, modern compilers are in general not always able to produce semantically equivalent alternatives that optimize non-functional properties, even if such alternatives are known to exist: this is usually due to the limited local nature of such optimizations. In this paper, we discuss how best to combine and extend the existing evolutionary methods of GP, multiobjective optimization, and coevolution in order to improve existing software. Given as input the implementation of a function, we attempt to evolve a semantically equivalent version, in this case optimized to reduce execution time subject to a given probability distribution of inputs. We demonstrate that our framework is able to produce non-obvious optimizations that compilers are not yet able to generate on eight example functions. We employ a coevolved population of test cases to encourage the preservation of the function's semantics. We exploit the original program both through seeding of the population in order to focus the search, and as an oracle for testing purposes. As well as discussing the issues that arise when attempting to improve software, we employ rigorous experimental method to provide interesting and practical insights to suggest how to address these issues.

In large network environments multiple intrusion detection sensors are needed to adequately monitor network traffic. However, deploying and managing additional sensors on a large network can be a demanding task, and organizations have to balance their desire for detecting intrusions throughout their network with financial and staffing limitations. This paper investigates how intrusion detection system (IDS) sensors should best be placed on a network when there are several competing evaluation criteria. This is a computationally difficult problem and we show how Multi-Objective Genetic Algorithms provide an excellent means of searching for optimal placements.

In this paper we present work on automated scribe identification on a new Middle-English manuscript dataset from around the 14th - 15th century. We discuss the image and textual problems encountered in processing historical documents, and demonstrate the effect of accounting for manuscript style on the writer identification rate. The grapheme codebook method is used to achieve a Top-1 classification accuracy of up to 77% with a modification to the distance measure. The performance of the Sparse Multinomial Logistic Regression classifier is compared against five k-nn classifiers. We also consider classification against the principal components and propose a method for visualising the principal component vectors in terms of the original grapheme features.

In a masquerade attack, an adversary who has stolen a legitimate user's credentials attempts to impersonate him to carry out malicious actions. Automatic detection of such attacks is often undertaken constructing models of normal behaviour of each user and then measuring significant departures from them. One potential vulnerability of this approach is that anomaly detection algorithms are generally susceptible of being deceived. In this paper, we first investigate how a resourceful masquerader can successfully evade detection while still accomplishing his goals. We then propose an algorithm based on the Kullback-Leibler divergence which attempts to identify if a sufficiently anomalous attack is present within an apparently normal request. Our experimental results indicate that the proposed scheme achieves considerably better detection quality than adversarial-unaware approaches.

Statistical testing has been shown to be more efficient at detecting faults in software than other methods of dynamic testing such as random and structural testing. Test data are generated by sampling from a probability distribution chosen so that each element of the software's structure is exercised with a high probability. However, deriving a suitable distribution is difficult for all but the simplest of programs. This paper demonstrates that automated search is a practical method of finding near-optimal probability distributions for real-world programs, and that test sets generated from these distributions continue to show superior efficiency in detecting faults in the software.

Search based software engineering (SBSE) is an evolving field where meta-heuristic techniques are applied to solve many software engineering problems. One area of SBSE, where considerable research is underway, is software testing. We see much application of meta-heuristics search techniques for generating input test data. But most of the work in this area is concentrated on test data generation from source code. We see very little application of such techniques to testing from other sources such as requirement and design models. Zhan and Clark applied such techniques to generate test data for Simulink models. This paper extends the work of Zhan and Clark by investigating the application of genetic algorithms (GAs) to Simulink models and then statistically compares the results to the existing work, which is mainly based on simulated annealing (SA).

The critical functionality of many software applications relies on code that performs mathematically complex computations. However, such code is often difficult to test owing to the compound datatypes used and complicated mathematical operations performed. This paper proposes the use of automated search as an efficient means of generating test data for this type of software. Taking Matlab as an example of widely-used mathematical software, a technical framework is described that extends previous work on search-based test data generation in order to handle matrix datatypes and associated relational operators. An empirical evaluation demonstrates the feasibility of this approach.

Recently search based software engineering (SBSE) has evolved as a major research field in the software engineering community. SBSE has been applied successfully to many software engineering activities ranging from requirement engineering to software maintenance and quality assessment. One area where SBSE has seen much application is test data generation. Search based test data generation techniques have been applied to automatically generate data for testing functional and non-functional properties of softwares. For structural testing, most of the time, the criterion used, is branch coverage. However, this is not enough. For the wider acceptance of search based test data generation techniques, much stronger criteria are needed. In this paper we have proposed an automatic framework that extend search based testing techniques to more stronger criteria such as multiple condition and MCDC coverage.

We present a metaheuristic-based attack against the traceability of an ultra-lightweight authentication protocol for RFID environments called SLMAP, and analyse its implications. The main interest of our approach is that it is a complete black-box technique that doesn't make any assumptions on the components of the underlying protocol and can thus be easily generalised to analyse many other proposals.

In recent years mobile ad hoc networks (MANETs) have become a very popular research topic. By providing communication in the absence of a fixed infrastructure they are very attractive for many applications such as tactical and disaster recovery operations and virtual conferences. On the other hand, this flexibility introduces new security risks. Moreover, different characteristics of MANETs make conventional security systems ineffective and inefficient for this new environment. Intrusion detection, which is an indispensable part of a security system, presents also a particular challenge due to the dynamic nature of MANETs, the lack of central points, and their highly constrained nodes. In this paper, we propose to investigate the use of an artificial intelligence based learning technique to explore this difficult design space. The grammatical evolution technique inspired by natural evolution is explored to detect known attacks on MANETs such as DoS attacks and route disruption attacks. Intrusion detection programs are evolved for each attack and distributed to each node on the network. The performance of these programs is evaluated on different types of networks with different mobility and traffic patterns to show their effects on intrusion detection ability.

In the early days a policy was a set of simple rules with a clear intuitive motivation that could be formalised to good effect. However the world is now much more complex. Subtle risk decisions may often need to be made and people are not always adept at expressing rationale for what they do. Previous research has demonstrated that Genetic Programming can be used to infer statements of policies from examples of decisions made [1]. This allows a policy that may not formally have been documented to be discovered automatically, or an underlying set of requirements to be extracted by interpreting user decisions to posed ldquowhat ifrdquo scenarios. This study compares the performance of three different approaches in using genetic programming to infer security policies from decision examples made, namely symbolic regression, IF-THEN rules inference and fuzzy membership functions inference. The fuzzy membership functions inference approach is found to have the best performance in terms of accuracy. Also, the fuzzification and de-fuzzification methods are found to be strongly correlated; incompatibility between them can have strong negative impact to the performance.

In the early days a policy was a set of simple rules with a clear intuitive motivation that could be formalised to good effect. However the world is becoming much more complex. Subtle risk decisions may often need to be made and people are not always adept at expressing rationale for what they do. In this paper we investigate how policies can be inferred automatically using Genetic Programming (GP) from examples of decisions made. This allows us to discover a policy that may not formally have been documented, or else extract an underlying set of requirements by interpreting user decisions to posed "what if" scenarios. Three proof of concept experiments on MLS Bell-LaPadula, Budgetised MLS and Fuzzy MLS policies have been carried out. The results show this approach is promising.

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.

In this work, we show that heuristic techniques (particularly Simulated Annealing) can be successfully applied in the search of good non-linear approximations of cryptographic primitives. We also provide some experimental results, including two excellent non-linear approximations for the output of the Salsa20 stream cipher with 2 and 4 rounds. From these two approximations, very efficient distinguishers for Salsa20 could easily be obtained, leading to a much more practical attack that any other published so far against this cipher.

Recent years have seen the application of evolutionary and other nature-inspired search approaches to achieve human-competitive results in cryptography and cryptanalysis. We have also seen the emergence of quantum computation as a tremendously exciting computational paradigm with significant potential applications in these areas. To date there seems to have been no synergistic application of these techniques in these fields. All applications are geared to the effective exploitation of one computational paradigm or another. Nature-inspired search and quantum computing can, however, be combined to achieve results neither is capable of individually. All that is needed is that classical search get 'close enough' for quantum search to take over and solve the residual problem. This observation has significant implications for the security of crypto-systems and our understanding of the power and usefulness of nature-inspired and quantum search.

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

Search based test-data generation has proved successful for code-level testing. In this paper we investigate the application of such approaches at the higher levels of abstraction offered by Matlab-Simulink models. The presence of persistent state has been shown to be problematic at the code level and such difficulties remain when Matlab-Simulink models are to be tested. In such cases, sequences of inputs that can put the model under test into particular states are needed to enable the underlying test goals to be achieved. Simple search guidance appears to be insufficient and results in a 'flat' cost function landscape. To address this problem, we introduce a technique called tracing and deducing, which helps provide better guidance to the search, allowing our developed tools to home in on the targeted test-data.

We show how Genetic Programming (GP) can be used to evolve useful quantum computing artefacts of increasing sophistication and usefulness: firstly specific quantum circuits, then quantum programs, and finally system-independent quantum algorithms. We conclude the paper by presenting a human-competitive Quantum Fourier Transform (QFT) algorithm evolved by GP.

In this paper, we show how genetic programming (GP) can be used to evolve system-size-independent quantum algorithms, and present a human-competitive Quantum Fourier Transform (QFT) algorithm evolved by GP.

The efficient and effective generation of test-data from high-level models is of crucial importance in advanced modern software engineering. Empirical studies have shown that mutation testing is highly effective. This paper describes how search-based automatic test-data generation methods can be used to find mutation adequate test-sets for Matlab/Simulink models.

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.

Methods and Testing

When formal modelling is done we must validate both the model and the assumptions. Formal techniques tend to concentrate on the former. We examine how fault injection (specification mutation) and model checking can help address the latter, in particular, the effects of failure. We find that, in contrast with software testing, where they are a problem, "equivalent mutants" are valuable for specification validation.

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.

Cryptography is an indispensable component of much modern-day system security. It has also been an attractive application domain for researchers in non-standard computation. In this paper, the author identifies what the author believes to be important themes and pieces of work and explain why they matter. The author does not provide a full survey, the principal aim is to interest the us in the subject.

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.

Multiple anagramming is a general method for the cryptanalysis of transposition ciphers, and has a graph theoretic representation. Inspired by a partially mechanised approach used in World War II, we consider the possibility of a fully automated attack. Two heuristics based on measures of natural language are used - one to recognise plaintext, and another to guide construction of the secret key. This is shown to be unworkable for cryptograms of a certain difficulty due to random variation in the constructive heuristic. A solver based on an ant colony optimisation (AGO) algorithm is then introduced, increasing the range of cryptograms that can be treated; the pheromone feedback provides a mechanism for the recognition heuristic to correct the noisy constructive heuristic.

Formal methods have traditionally been used for specification and development of software. However there are potential benefits for the testing stage as well. The panel session associated with this paper explores the usefulness or otherwise of formal methods in various contexts for improving software testing. A number of different possibilities for the use of formal methods are explored and questions raised. The contributors are all members of the UK FORTEST Network on formal methods and testing. Although the authors generally believe that formal methods are useful in aiding the testing process, this paper is intended to provoke discussion. Dissenters are encouraged to put their views to the panel or individually to the authors.

Abstract The mutation method assesses test quality by examining the ability of a test set to distinguish syntactic deviations representing specific types of faults from the program under test. This paper describes an empirical study performed to evaluate the effectiveness of object‐oriented (OO) test strategies using the mutation method. The test sets for the experimental system are generated according to three selected OO test strategies and their effectiveness is compared by determining how well the developed test sets kill injected mutants derived from an established mutation system Mothra and the authors' own OO‐specific mutation technique which is termed Class Mutation. Copyright © 2001 John Wiley & Sons, Ltd.

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".

This paper presents a technique for automatically generating test-data to test exceptions. The approach is based on the application of a dynamic global optimization based search for the required test-data. The authors' work has focused on test-data generation for safety-critical systems. Such systems must be free from anomalous and uncontrolled behaviour. Typically, it is easier to prove the absence of any exceptions than proving that the exception handling is safe. A process for integrating automated testing with exception freeness proofs is presented as a way forward for tackling the special needs of safety critical systems. The results of a number of simple case-studies are presented and show the technique to be effective. The major result shows the application of the technique to a commercial aircraft engine controller system as part of a proof of exception freeness. This illustrates how automated testing can be effectively integrated into a formal safety-critical process to reduce costs and add value. Copyright © 2000 John Wiley & Sons, Ltd.

We discuss issues in the development of formal methods for use in aerospace applications, reflecting our experience in working with both Rolls-Royce and British Aerospace. We discuss some of the key factors which we believe govern the application of discrete mathematics to aerospace applications, drawing comparisons with applied engineering mathematics in other domains. We give an overview of three projects (the three "small steps"): the development of a domain-specific language for aircraft engine control system specification; the development of a formal semantics and tool support for state transition systems to facilitate analysis of specifications produced by systems engineers; the use of formalism in support of test automation. We then discuss the "gap" we see between the needs of industry and the current focus of the formal methods research community by pointing out important facets of industrial applicable formal methods which are not receiving adequate attention. We refer to this as a "giant leap" due to the need for a cultural shift in the research community and the need for a coherent approach to the identified research issues rather than piecemeal studies of the issues. Our conclusions are to be optimistic for the future use of formal methods in industry albeit with concern that their potential will not be realised unless there is a shift in emphasis within the research community?.

One of the major costs in a software project is the construction of test-data. This paper outlines a generalised test-case data generation framework based on optimisation techniques. The framework can incorporate a number of testing criteria, for both functional and non-functional properties. Application of the optimisation framework to testing specification failures and exception conditions is illustrated. The results of a number of small case studies are presented and show the efficiency and effectiveness of this dynamic optimisation-base approach to generating test-data.

Structural testing criteria are mandated in many software development standards and guidelines. The process of generating test data to achieve 100% coverage of a given structural coverage metric is labour-intensive and expensive. This paper presents an approach to automate the generation of such test data. The test-data generation is based on the application of a dynamic optimisation-based search for the required test data. The same approach can be generalised to solve other test-data generation problems. Three such applications are discussed-boundary value analysis, assertion/run-time exception testing, and component re-use testing. A prototype tool-set has been developed to facilitate the automatic generation of test data for these structural testing problems. The results of preliminary experiments using this technique and the prototype tool-set are presented and show the efficiency and effectiveness of this approach.