Search

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.

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 escaping. 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., Comment: 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

Food insecurity is associated with increased risk for several health conditions and with increased national burden of chronic disease. Key determinants for household food insecurity are income and food costs. Forecasts show household disposable income for 2020 expected to fall and for 2021 to rise only slightly. Prices are forecast to rise. Thus, future increased food prices would be a significant driver of greater food insecurity. Structured expert judgement elicitation, a well-established method for quantifying uncertainty, using experts. In July 2020, each expert estimated the median, 5th percentile and 95th percentile quantiles of changes in price to April 2022 for ten food categories under three end-2020 settlement Brexit scenarios: A: full WTO terms; B: a moderately disruptive trade agreement (better than WTO); C: a minimally disruptive trade agreement. When combined in proportions for calculate Consumer Prices Index food basket costs, the median food price change under full WTO terms is expected to be +17.9% [90% credible interval:+5.2%, +35.1%]; with moderately disruptive trade agreement: +13.2% [+2.6%, +26.4%] and with a minimally disruptive trade agreement +9.3% [+0.8%, +21.9%]. The number of households experiencing food insecurity and its severity are likely to increase because of expected sizeable increases in median food prices in the months after Brexit, whereas low income group spending on food is unlikely to increase, and may be further eroded by other factors not considered here (e.g. COVID-19). Higher increases are more likely than lower rises and towards the upper limits, these would entail severe impacts. Research showing a low food budget leads to increasingly poor diet suggests that demand for health services in both the short and longer term is likely to increase due to the effects of food insecurity on the incidence and management of diet-sensitive conditions., Comment: 6 pages one table

Persistence diagrams concisely represent the topology of a point cloud whilst having strong theoretical guarantees, but the question of how to best integrate this information into machine learning workflows remains open. In this paper we extend the ubiquitous Fuzzy c-Means (FCM) clustering algorithm to the space of persistence diagrams, enabling unsupervised learning that automatically captures the topological structure of data without the topological prior knowledge or additional processing of persistence diagrams that many other techniques require. We give theoretical convergence guarantees that correspond to the Euclidean case, and empirically demonstrate the capability of our algorithm to capture topological information via the fuzzy RAND index. We end with experiments on two datasets that utilise both the topological and fuzzy nature of our algorithm: pre-trained model selection in machine learning and lattices structures from materials science. As pre-trained models can perform well on multiple tasks, selecting the best model is a naturally fuzzy problem; we show that fuzzy clustering persistence diagrams allows for model selection using the topology of decision boundaries. In materials science, we classify transformed lattice structure datasets for the first time, whilst the probabilistic membership values let us rank candidate lattices in a scenario where further investigation requires expensive laboratory time and expertise., Comment: Version 4

Food insecurity is associated with increased risk for several health conditions and with poor chronic disease management. Key determinants for household food insecurity are income and food costs. Whereas short-term household incomes are likely to remain static, increased food prices would be a significant driver of food insecurity. To investigate food price drivers for household food security and its health consequences in the UK under scenarios of Deal and No deal for Brexit . To estimate the 5\% and 95\% quantiles of the projected price distributions. Structured expert judgement elicitation, a well-established method for quantifying uncertainty, using experts. In July 2018, each expert estimated the median, 5\% and 95\% quantiles of changes in price for ten food categories under Brexit Deal and No-deal to June 2020 assuming Brexit had taken place on 29th March 2019. These were aggregated based on the accuracy and informativeness of the experts on calibration questions. Ten specialists in food procurement, retail, agriculture, economics, statistics and household food security. Results: when combined in proportions used to calculate Consumer Prices Index food basket costs, median food price change for Brexit with a Deal is expected to be +6.1\% [90\% credible interval:-3\%, +17\%] and with No deal +22.5\% [+1\%, +52\%]. The number of households experiencing food insecurity and its severity are likely to increase because of expected sizeable increases in median food prices after Brexit. Higher increases are more likely than lower rises and towards the upper limits, these would entail severe impacts. Research showing a low food budget leads to increasingly poor diet suggests that demand for health services in both the short and longer term is likely to increase due to the effects of food insecurity on the incidence and management of diet-sensitive conditions.

In cryptography, secure Multi-Party Computation (MPC) protocols allow participants to compute a function jointly while keeping 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.

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.

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., Comment: 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

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., Comment: In Proceedings of the Third Workshop on Mobile Security Technologies (MoST) 2014 (http://arxiv.org/abs/1410.6674)

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.

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.