We apply formal methods to lay and streamline theoretical foundations to reason about Cyber-Physical Systems (CPSs) and physics-based attacks, i.e., attacks targeting physical devices. We focus on a formal treatment of both integrity and denial of service attacks to sensors and actuators of CPSs, and on the timing aspects of these attacks. Our contributions are fourfold. (1) We define a hybrid process calculus to model both CPSs and physics-based attacks. (2) We formalise a threat model that specifies MITM attacks that can manipulate sensor readings or control commands in order to drive a CPS into an undesired state, and we provide the means to assess attack tolerance/vulnerability with respect to a given attack. (3) We formalise how to estimate the impact of a successful attack on a CPS and investigate possible quantifications of the success chances of an attack. (4) We illustrate our definitions and results by formalising a non-trivial running example in Uppaal SMC, the statistical extension of the Uppaal model checker; we use Uppaal SMC as an automatic tool for carrying out a static security analysis of our running example in isolation and when exposed to three different physics-based attacks with different impacts.
Oblivious Random Access Machine (ORAM) allows a client to hide the access pattern when accessing sensitive data on a remote server. It is known that there exists a logarithmic communication lower bound on any passive ORAM construction, where the server only acts as the storage service. This overhead was shown too costly for some applications. Several active ORAM schemes with server computation have been proposed to overcome this limitation. However, they mostly rely on costly homomorphic encryptions, whose performance is worse than passive ORAM. In this article, we propose S3ORAM, a new multi-server ORAM framework, which features O(1) client bandwidth blowup and low client storage without relying on costly cryptographic primitives. Our key idea is to harness Shamir Secret Sharing and a multi-party multiplication protocol on applicable binary tree-ORAM paradigms. This strategy allows the client to instruct the server(s) to perform secure and efficient computation on his/her behalf with a low intervention thereby, achieving a constant client bandwidth blowup and low server computational overhead. Our framework can also work atop a general ?-ary tree ORAM structure (??2). We fully implemented our framework, and strictly evaluated its performance on commodity cloud architecture (Amazon EC2). Our comprehensive experiments confirmed the efficiency of S3ORAM framework, where it is approximately 10× faster than the most efficient passive ORAM (i.e., Path-ORAM) for a moderate network bandwidth, while being three orders of magnitude faster than active ORAM with O(1) bandwidth blowup (i.e., Onion-ORAM). We have outsourced the implementation of our framework for public testing and adaptation
Location-based services (LBSs) typically crowdsource geo-tagged data from mobile users. However, while more data will generally improve the data utility for LBS providers, it also imposes higher risk to users? mobility privacy. Although this tension between data utility and mobility privacy has been recognized, there lacks of a solution that determines ?how much? data?in terms of both spatial and temporal distributions?is the ?best? for both the mobile users and the service providers. This paper proposes a strategy toward making the optimal trade-off, where a user submits data only if his/her mobility privacy will not be compromised and the data utility of the LBS provider will be improved by at least a given threshold. To this end, we first define and quantify a concept called privacy exposure, which incorporates both the spatial distribution and the temporal transition of a user?s activity points. Second, we define and quantify data utility based on an economics principle, in such a way that spatial repetitions at the same activity point and temporal elapsed time from the last submission are both taken into account. Then, we propose a privacy-preserving crowdsourcing algorithm to determine whether it is of the best interest to submit a piece of crowdsourced data based on the quantified privacy-utility trade-off. Simulations indicate that our proposed approach guarantees a non-increasing privacy exposure while improving the data utility for LBS.
Keystroke behaviour-based authentication employs the unique typing behaviour of users to authenticate them. Recent such proposals for virtual keyboards on smartphones employ diverse temporal, contact, and spatial features to achieve over 95% accuracy. Consequently, they have been suggested as a second line of defense with text-based password authentication. We show that a state-of-the-art keystroke behaviour-based authentication scheme is highly vulnerable against mimicry attacks. While previous research used training interfaces to attack physical keyboards, we show that this approach has limited effectiveness against virtual keyboards. This is mainly due to the large number of diverse features that the attacker needs to mimic for virtual keyboards. We address this challenge by developing an augmented reality-based app that resides on the attacker's smartphone and leverages computer vision and keystroke data to provide real-time guidance during password entry on the victim's phone. In addition, we propose an audiovisual attack in which the attacker overlays transparent film printed with spatial pointers on the victim's device, and uses audio cues to match the temporal behaviour of the victim. Both attacks require neither tampering or installing software on the victim's device nor specialized hardware. We conduct experiments with 30 users to mount over 400 mimicry attacks. We show that our methods enable an attacker to mimic keystroke behaviour on virtual keyboards with little effort. Furthermore, since our augmented reality-based method provides the attacker with real-time guidance on how to submit touch input on smartphones, it can be extended to attack other touch input behaviour-based systems for smartphones.