Synthetically generated benchmark datasets are vitally important for machine learning and network intrusion research. When producing intrusion datasets for research, providers make complex, subtle and sometimes unwary decisions that can affect data utility. Unfortunately, examining network data is difficult, so these decisions are rarely audited. We perform an in-depth manual analysis of seven highly-cited benchmark datasets, discovering six suspect design patterns, which we term ‘data design smells’. We formulate six heuristics to measure the prevalence of these issues. These design choices, if not properly accounted for, can introduce severe experimental bias, which we demonstrate with four concrete examples. We then conduct a systematic impact analysis of the wider literature that relies on these datasets. Our results suggest that bad design smells correlate with poor data diversity, murky labelling and poorly-defined generalisation criteria. Worryingly, we find that improper usage of these datasets can weaken their utility as benchmarks which, in turn, biases downstream intrusion detection research. We conclude with some recommendations for using and creating NIDS datasets to help alleviate these issues.

Adversarial machine learning, a technique which seeks to deceive machine learning (ML) models, threatens the utility and reliability of ML systems. This is particularly relevant in critical ML implementations such as those found in Network Intrusion Detection Systems (NIDS). This paper considers the impact of adversarial influence on NIDS and proposes ways to improve ML based systems. Specifically, we consider five feature robustness metrics to determine which features in a model are most vulnerable, and four defense methods. These methods are tested on six ML models with four adversarial sample generation techniques. Our results show that across different models and adversarial generation techniques, there is limited consistency in vulnerable features or in effectiveness of defense method.

In the wake of the COVID-19 pandemic, contact tracing apps have been developed based on digital contact tracing frameworks. These allow developers to build privacy-conscious apps that detect whether an infected individual is in close-proximity with others. Given the urgency of the problem, these apps have been developed at an accelerated rate with a brief testing period. Such quick development may have led to mistakes in the apps’ implementations, resulting in problems with their functionality, privacy and security. To mitigate these concerns, we develop and apply a methodology for evaluating the functionality, privacy and security of Android apps using the Google/Apple Exposure Notification API. This is a three-pronged approach consisting of a manual analysis, general static analysis and a bespoke static analysis, using a tool we’ve developed, dubbed MonSTER. As a result, we have found that, although most apps met the basic standards outlined by Google/Apple, there are issues with th e functionality of some of these apps that could impact user safety.

Machine-checked proofs of security are important to increase the rigour of provable security. In this work we present a formalised theory of two fundamental two party cryptographic primitives: Σ-protocols and Commitment Schemes. Σ-protocols allow a prover to convince a verifier that they possess some knowledge without leaking information about the knowledge. Commitment schemes allow a committer to commit to a message and keep it secret until revealing it at a later time. We use CryptHOL (Lochbihler in Archive of formal proofs, 2017) to formalise both primitives and prove secure multiple examples namely; the Schnorr, Chaum-Pedersen and Okamoto Σ-protocols as well as a construction that allows for compound (AND and OR) Σ-protocols and the Pedersen and Rivest commitment schemes. A highlight of the work is a formalisation of the construction of commitment schemes from Σ-protocols (Damgard in Lecture notes, 2002). We formalise this proof at an abstract level using the modularity available in Isabelle/HOL and CryptHOL. This way, the proofs of the instantiations come for free.

Multi-Party Computation (MPC) allows multiple parties to compute a function together while keeping their inputs private. Large scale implementations of MPC protocols are becoming practical thus it is important to have strong guarantees for the whole development process, from the underlying cryptography to the implementation. Computer aided proofs are a way to provide such guarantees.

eHealth devices such as smart scales and wearable fitness trackers are a key part of many health technology solutions. However, these eHealth devices can be vulnerable to privacy and security related attacks. In this poster, we propose a security analysis framework for eHealth devices, called mH-PriSe, that will yield useful information for security analysts, vendors, health care providers, and consumers. We demonstrate our framework by analysing scales from 6 vendors. Our results show that while vendors strive to address security and privacy issues correctly, challenges remain in many cases. Only 5 out of 8 solutions can be recommended with some caveats whereas the remaining 3 solutions expose severe vulnerabilities.

Automatic malware classifiers often perform badly on the detection of new malware, i.e., their robustness is poor. We study the machine-learning-based mobile malware classifiers and reveal one reason: the input features used by these classifiers can't capture general behavioural patterns of malware instances. We extract the best-performing syntax-based features like permissions and API calls, and some semantics-based features like happen-befores and unwanted behaviours, and train classifiers using popular supervised and semi-supervised learning methods. By comparing their classification performance on industrial datasets collected across several years, we demonstrate that using semantics-based features can dramatically improve robustness of malware classifiers.

Modern mobile devices come with an array of sensors that support many interesting applications. However, sensors have different sampling costs (e.g., battery drain) and benefits (e.g., accuracy) under different circumstances. In this work we investigate the trade-off between the cost of using a sensor and the benefit gained from its use, with application to data-driven authentication on mobile devices. Current authentication practice, where user behaviour is first learned from the sensor data and then used to detect anomalies, typically assumes a fixed sampling rate and does not consider the battery consumption and usefulness of sensors. In this work we study how battery consumption and sensor effectiveness (e.g., for detecting attacks) vary when using different sensors and different sensor sampling rates. We use data from both controlled lab studies, as well as field trials, for our experiments. We also propose an adaptive sampling technique that adjusts the sampling rate based on an expected device vigilance level. Our results show that it is possible to reduce the battery consumption tenfold without significantly impacting the detection of attacks.

Challenge questions are an increasingly important part of mainstream authentication solutions, yet there are few published studies concerning their usability or security. This paper reports on an experimental investigation into user-chosen questions. We collected questions from a large cohort of students, in a way that encouraged participants to give realistic data. The questions allow us to consider possible modes of attack and to judge the relative effort needed to crack a question, according to an innovative model of the knowledge of the attacker. Using this model, we found that many participants were likely to have chosen questions with low entropy answers, yet they believed that their challenge questions would resist attacks from a stranger. Though by asking multiple questions, we are able to show a marked improvement in security for most users. In a second stage of our experiment, we applied existing metrics to measure the usability of the questions and answers. Despite having youthful memories and choosing their own questions, users made errors more frequently than desirable.

Abstract Linear typing schemes can be used to guarantee non-interference and so the soundness of in-place update with respect to a functional semantics. But linear schemes are restrictive in practice, and more restrictive than necessary to guarantee soundness of in-place update. This limitation has prompted research into static analysis and more sophisticated typing disciplines to determine when in-place update may be safely used, or to combine linear and non-linear schemes. Here we contribute to this direction by defining a new typing scheme that better approximates the semantic property of soundness of in-place update for a functional semantics. We begin from the observation that some data are used only in a “read-only” context, after which it may be safely re-used before being destroyed. Formalising the in-place update interpretation in a machine model semantics allows us to refine this observation, motivating three usage aspects apparent from the semantics that are used to annotate function argument types. The aspects are (1) used destructively, (2), used read-only but shared with result, and (3) used read-only and not shared with the result. The main novelty is aspect (2), which allows a linear value to be safely read and even aliased with a result of a function without being consumed. This novelty makes our type system more expressive than previous systems for functional languages in the literature. The system remains simple and intuitive, but it enjoys a strong soundness property whose proof is non-trivial. Moreover, our analysis features principal types and feasible type reconstruction, as shown in M. Konečn'y (In TYPES 2002 workshop, Nijmegen, Proceedings , Springer-Verlag, 2003).

The need for subtyping in type-systems with dependent types has been realized for some years. But it is hard to prove that systems combining the two features have fundamental properties such as subject reduction. Here we investigate a subtyping extension of the system /spl lambda/P, which is an abstract version of the type system of the Edinburgh Logical Framework LF. By using an equivalent formulation, we establish some important properties of the new system /spl lambda/P/sub /spl les//, including subject reduction. Our analysis culminates in a complete and terminating algorithm which establishes the decidability of type-checking.