-
An Analysis of Home IoT Network Traffic and Behaviour
Authors:
Yousef Amar,
Hamed Haddadi,
Richard Mortier,
Anthony Brown,
James Colley,
Andy Crabtree
Abstract:
Internet-connected devices are increasingly present in our homes, and privacy breaches, data thefts, and security threats are becoming commonplace. In order to avoid these, we must first understand the behaviour of these devices.
In this work, we analyse network traces from a testbed of common IoT devices, and describe general methods for fingerprinting their behavior. We then use the informatio…
▽ More
Internet-connected devices are increasingly present in our homes, and privacy breaches, data thefts, and security threats are becoming commonplace. In order to avoid these, we must first understand the behaviour of these devices.
In this work, we analyse network traces from a testbed of common IoT devices, and describe general methods for fingerprinting their behavior. We then use the information and insights derived from this data to assess where privacy and security risks manifest themselves, as well as how device behavior affects bandwidth. We demonstrate simple measures that circumvent attempts at securing devices and protecting privacy.
△ Less
Submitted 14 March, 2018;
originally announced March 2018.
-
Formal Modelling, Testing and Verification of HSA Memory Models using Event-B
Authors:
Ashish Darbari,
Iain Singleton,
Michael Butler,
John Colley
Abstract:
The HSA Foundation has produced the HSA Platform System Architecture Specification that goes a long way towards addressing the need for a clear and consistent method for specifying weakly consistent memory. HSA is specified in a natural language which makes it open to multiple ambiguous interpretations and could render bugs in implementations of it in hardware and software. In this paper we presen…
▽ More
The HSA Foundation has produced the HSA Platform System Architecture Specification that goes a long way towards addressing the need for a clear and consistent method for specifying weakly consistent memory. HSA is specified in a natural language which makes it open to multiple ambiguous interpretations and could render bugs in implementations of it in hardware and software. In this paper we present a formal model of HSA which can be used in the development and verification of both concurrent software applications as well as in the development and verification of the HSA-compliant platform itself. We use the Event-B language to build a provably correct hierarchy of models from the most abstract to a detailed refinement of HSA close to implementation level. Our memory models are general in that they represent an arbitrary number of masters, programs and instruction interleavings. We reason about such general models using refinements. Using Rodin tool we are able to model and verify an entire hierarchy of models using proofs to establish that each refinement is correct. We define an automated validation method that allows us to test baseline compliance of the model against a suite of published HSA litmus tests. Once we complete model validation we develop a coverage driven method to extract a richer set of tests from the Event-B model and a user specified coverage model. These tests are used for extensive regression testing of hardware and software systems. Our method of refinement based formal modelling, baseline compliance testing of the model and coverage driven test extraction using the single language of Event-B is a new way to address a key challenge facing the design and verification of multi-core systems.
△ Less
Submitted 16 May, 2016;
originally announced May 2016.
-
Modelling and Refinement in CODA
Authors:
Michael Butler,
John Colley,
Andrew Edmunds,
Colin Snook,
Neil Evans,
Neil Grant,
Helen Marshall
Abstract:
This paper provides an overview of the CODA framework for modelling and refinement of component-based embedded systems. CODA is an extension of Event-B and UML-B and is supported by a plug-in for the Rodin toolset. CODA augments Event-B with constructs for component-based modelling including components, communications ports, port connectors, timed communications and timing triggers. Component beha…
▽ More
This paper provides an overview of the CODA framework for modelling and refinement of component-based embedded systems. CODA is an extension of Event-B and UML-B and is supported by a plug-in for the Rodin toolset. CODA augments Event-B with constructs for component-based modelling including components, communications ports, port connectors, timed communications and timing triggers. Component behaviour is specified through a combination of UML-B state machines and Event-B. CODA communications and timing are given an Event-B semantics through translation rules. Refinement is based on Event-B refinement and allows layered construction of CODA models in a consistent way.
△ Less
Submitted 27 May, 2013;
originally announced May 2013.
-
Building on the DEPLOY Legacy: Code Generation and Simulation
Authors:
Andrew Edmunds,
Michael Butler,
John Colley
Abstract:
The RODIN, and DEPLOY projects laid solid foundations for further theoretical, and practical (methodological and tooling) advances with Event-B. Our current interest is the co-simulation of cyber-physical systems using Event-B. Using this approach we aim to simulate various features of the environment separately, in order to exercise deployable code. This paper has two contributions, the first is…
▽ More
The RODIN, and DEPLOY projects laid solid foundations for further theoretical, and practical (methodological and tooling) advances with Event-B. Our current interest is the co-simulation of cyber-physical systems using Event-B. Using this approach we aim to simulate various features of the environment separately, in order to exercise deployable code. This paper has two contributions, the first is the extension of the code generation work of DEPLOY, where we add the ability to generate code from Event-B state-machine diagrams. The second describes how we may use code, generated from state-machines, to simulate the environment, and simulate concurrently executing state-machines, in a single task. We show how we can instrument the code to guide the simulation, by controlling the relative rate that non-deterministic transitions are traversed in the simulation.
△ Less
Submitted 25 October, 2012;
originally announced October 2012.
