Showing 1–8 of 8 results for author: Aspinall, D

Towards Interdependent Safety Security Assessments using Bowties

Authors: Luca Arnaboldi, David Aspinall

Abstract: We present a way to combine security and safety assessments using Bowtie Diagrams. Bowties model both the causes leading up to a central failure event and consequences which arise from that event, as well as barriers which impede events. Bowties have previously been used separately for security and safety assessments, but we suggest that a unified treatment in a single model can elegantly capture… ▽ More We present a way to combine security and safety assessments using Bowtie Diagrams. Bowties model both the causes leading up to a central failure event and consequences which arise from that event, as well as barriers which impede events. Bowties have previously been used separately for security and safety assessments, but we suggest that a unified treatment in a single model can elegantly capture safety-security interdependencies of several kinds. We showcase our approach with the example of the October 2021 Facebook DNS shutdown, examining the chains of events and the interplay between the security and safety barriers which caused the outage. △ Less

Submitted 6 August, 2022; originally announced August 2022.

Traffic Generation using Containerization for Machine Learning

Authors: Henry Clausen, Robert Flood, David Aspinall

Abstract: The design and evaluation of data-driven network intrusion detection methods are currently held back by a lack of adequate data, both in terms of benign and attack traffic. Existing datasets are mostly gathered in isolated lab environments containing virtual machines, to both offer more control over the computer interactions and prevent any malicious code from esca**. This procedure however lead… ▽ More The design and evaluation of data-driven network intrusion detection methods are currently held back by a lack of adequate data, both in terms of benign and attack traffic. Existing datasets are mostly gathered in isolated lab environments containing virtual machines, to both offer more control over the computer interactions and prevent any malicious code from esca**. This procedure however leads to datasets that lack four core properties: heterogeneity, ground truth traffic labels, large data size, and contemporary content. Here, we present a novel data generation framework based on Docker containers that addresses these problems systematically. For this, we arrange suitable containers into relevant traffic communication scenarios and subscenarios, which are subject to appropriate input randomization as well as WAN emulation. By relying on process isolation through containerization, we can match traffic events with individual processes, and achieve scalability and modularity of individual traffic scenarios. We perform two experiments to assess the reproducability and traffic properties of our framework, and demonstrate the usefulness of our framework on a traffic classification example. △ Less

Submitted 12 November, 2020; originally announced November 2020.

Comments: This work was presented at the ACSAC DYNAMICS '19: DYnamic and Novel Advances in Machine Learning and Intelligent Cyber Security Workshop in December 09-10, 2019, San Juan, PR, and will be published in the corresponding workshop proceedings. This document version is specifically for publication on arXiv. 12 pages, 7 figures

How to Simulate It in Isabelle: Towards Formal Proof for Secure Multi-Party Computation

Authors: David Butler, David Aspinall, Adria Gascon

Abstract: In cryptography, secure Multi-Party Computation (MPC) protocols allow participants to compute a function jointly while kee** their inputs private. Recent breakthroughs are bringing MPC into practice, solving fundamental challenges for secure distributed computation. Just as with classic protocols for encryption and key exchange, precise guarantees are needed for MPC designs and implementations;… ▽ More In cryptography, secure Multi-Party Computation (MPC) protocols allow participants to compute a function jointly while kee** their inputs private. Recent breakthroughs are bringing MPC into practice, solving fundamental challenges for secure distributed computation. Just as with classic protocols for encryption and key exchange, precise guarantees are needed for MPC designs and implementations; any flaw will give attackers a chance to break privacy or correctness. In this paper we present the first (as far as we know) formalisation of some MPC security proofs. These proofs provide probabilistic guarantees in the computational model of security, but have a different character to machine proofs and proof tools implemented so far --- MPC proofs use a \emph{simulation} approach, in which security is established by showing indistinguishability between execution traces in the actual protocol execution and an ideal world where security is guaranteed by definition. We show that existing machinery for reasoning about probabilistic programs adapted to this setting, paving the way to precisely check a new class of cryptography arguments. We implement our proofs using the CryptHOL framework inside Isabelle/HOL. △ Less

Submitted 31 May, 2018; originally announced May 2018.

DroidGen: Constraint-based and Data-Driven Policy Generation for Android

Authors: Mohamed Nassim Seghir, David Aspinall

Abstract: We present DroidGen a tool for automatic anti-malware policy inference. DroidGen employs a data-driven approach: it uses a training set of malware and benign applications and makes call to a constraint solver to generate a policy under which a maximum of malware is excluded and a maximum of benign applications is allowed. Preliminary results are encouraging. We are able to automatically generate a… ▽ More We present DroidGen a tool for automatic anti-malware policy inference. DroidGen employs a data-driven approach: it uses a training set of malware and benign applications and makes call to a constraint solver to generate a policy under which a maximum of malware is excluded and a maximum of benign applications is allowed. Preliminary results are encouraging. We are able to automatically generate a policy which filters out 91% of the tested Android malware. Moreover, compared to black-box machine learning classifiers, our method has the advantage of generating policies in a declarative readable format. We illustrate our approach, describe its implementation and report on the preliminary results. △ Less

Submitted 22 December, 2016; originally announced December 2016.

Accessible Banking: Experiences and Future Directions

Authors: Bela Gor, David Aspinall

Abstract: This is a short position paper drawing on experience working with the UK banking industry and their disabled and ageing customers in the Business Disability Forum, a UK non-profit member organisation funded by a large body of UK private and public sector businesses. We describe some commonly reported problems of disabled customers who use modern banking technologies, relating them to UK law and be… ▽ More This is a short position paper drawing on experience working with the UK banking industry and their disabled and ageing customers in the Business Disability Forum, a UK non-profit member organisation funded by a large body of UK private and public sector businesses. We describe some commonly reported problems of disabled customers who use modern banking technologies, relating them to UK law and best practice. We describe some of the recent banking industry innovations and the hope they may offer for improved inclusive and accessible multi-channel banking. △ Less

Submitted 16 July, 2015; originally announced July 2015.

Comments: 3 pages, presented at Workshop on Inclusive Privacy and Security (WIPS): Privacy and Security for Everyone, Anytime, Anywhere, held as part of Symposium on Usable Privacy and Security (SOUPS) 2015, July 22-24, 2015, Ottawa, Canada

ACM Class: H.1.2; K.4.2

Data Driven Authentication: On the Effectiveness of User Behaviour Modelling with Mobile Device Sensors

Authors: Hilmi Gunes Kayacik, Mike Just, Lynne Baillie, David Aspinall, Nicholas Micallef

Abstract: We propose a lightweight, and temporally and spatially aware user behaviour modelling technique for sensor-based authentication. Operating in the background, our data driven technique compares current behaviour with a user profile. If the behaviour deviates sufficiently from the established norm, actions such as explicit authentication can be triggered. To support a quick and lightweight deploymen… ▽ More We propose a lightweight, and temporally and spatially aware user behaviour modelling technique for sensor-based authentication. Operating in the background, our data driven technique compares current behaviour with a user profile. If the behaviour deviates sufficiently from the established norm, actions such as explicit authentication can be triggered. To support a quick and lightweight deployment, our solution automatically switches from training mode to deployment mode when the user's behaviour is sufficiently learned. Furthermore, it allows the device to automatically determine a suitable detection threshold. We use our model to investigate practical aspects of sensor-based authentication by applying it to three publicly available data sets, computing expected times for training duration and behaviour drift. We also test our model with scenarios involving an attacker with varying knowledge and capabilities. △ Less

Submitted 28 October, 2014; originally announced October 2014.

Comments: In Proceedings of the Third Workshop on Mobile Security Technologies (MoST) 2014 (http://arxiv.longhoe.net/abs/1410.6674)

Report number: MoST/2014/01

ProofPeer: Collaborative Theorem Proving

Authors: Steven Obua, Jacques Fleuriot, Phil Scott, David Aspinall

Abstract: We define the concept of collaborative theorem proving and outline our plan to make it a reality. We believe that a successful implementation of collaborative theorem proving is a necessary prerequisite for the formal verification of large systems. We define the concept of collaborative theorem proving and outline our plan to make it a reality. We believe that a successful implementation of collaborative theorem proving is a necessary prerequisite for the formal verification of large systems. △ Less

Submitted 24 April, 2014; originally announced April 2014.

Capturing Hiproofs in HOL Light

Authors: Steven Obua, Mark Adams, David Aspinall

Abstract: Hierarchical proof trees (hiproofs for short) add structure to ordinary proof trees, by allowing portions of trees to be hierarchically nested. The additional structure can be used to abstract away from details, or to label particular portions to explain their purpose. In this paper we present two complementary methods for capturing hiproofs in HOL Light, along with a tool to produce web-based vis… ▽ More Hierarchical proof trees (hiproofs for short) add structure to ordinary proof trees, by allowing portions of trees to be hierarchically nested. The additional structure can be used to abstract away from details, or to label particular portions to explain their purpose. In this paper we present two complementary methods for capturing hiproofs in HOL Light, along with a tool to produce web-based visualisations. The first method uses tactic recording, by modifying tactics to record their arguments and construct a hierarchical tree; this allows a tactic proof script to be modified. The second method uses proof recording, which extends the HOL Light kernel to record hierachical proof trees alongside theorems. This method is less invasive, but requires care to manage the size of the recorded objects. We have implemented both methods, resulting in two systems: Tactician and HipCam. △ Less

Submitted 10 July, 2013; originally announced July 2013.