Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userPHOENIX: Device-Centric Cellular Network Protocol Monitoring using Runtime Verification
78
0
0.0
(
0
)
Added by
Mitziu Echeverria
Publication date
2021
fields
Informatics Engineering
and research's language is
English
Ask ChatGPT about the research
No Arabic abstract
End-user-devices in the current cellular ecosystem are prone to many different vulnerabilities across different generations and protocol layers. Fixing these vulnerabilities retrospectively can be expensive, challenging, or just infeasible. A pragmatic approach for dealing with such a diverse set of vulnerabilities would be to identify attack attempts at runtime on the device side, and thwart them with mitigating and corrective actions. Towards this goal, in the paper we propose a general and extendable approach called Phoenix for identifying n-day cellular network control-plane vulnerabilities as well as dangerous practices of network operators from the device vantage point. Phoenix monitors the device-side cellular network traffic for performing signature-based unexpected behavior detection through lightweight runtime verification techniques. Signatures in Phoenix can be manually-crafted by a cellular network security expert or can be automatically synthesized using an optional component of Phoenix, which reduces the signature synthesis problem to the language learning from the informant problem. Based on the corrective actions that are available to Phoenix when an undesired behavior is detected, different instantiations of Phoenix are possible: a full-fledged defense when deployed inside a baseband processor; a user warning system when deployed as a mobile application; a probe for identifying attacks in the wild. One such instantiation of Phoenix was able to identify all 15 representative n-day vulnerabilities and unsafe practices of 4G LTE networks considered in our evaluation with a high packet processing speed (~68000 packets/second) while inducing only a moderate amount of energy overhead (~4mW).
rate research
Read More
Fault injections are increasingly used to attack/test secure applications. In this paper, we define formal models of runtime monitors that can detect fault injections that result in test inversion attacks and arbitrary jumps in the control flow. Runtime verification monitors offer several advantages. The code implementing a monitor is small compared to the entire application code. Monitors have a formal semantics; and we prove that they effectively detect attacks. Each monitor is a module dedicated to detecting an attack and can be deployed as needed to secure the application. A monitor can run separately from the application or it can be ``weaved inside the application. Our monitors have been validated by detecting simulated attacks on a program that verifies a user PIN.
In this paper, we develop a comprehensive analytical framework for cache enabled cellular networks overlaid with coordinated device-to-device (D2D) communication. We follow an approach similar to LTE Direct, where the base station (BS) is responsible for establishing D2D links. We consider that an arbitrary requesting user is offloaded to D2D mode to communicate with one of its k closest D2D helpers within the macrocell subject to content availability and helper selection scheme. We consider two different D2D helper selection schemes: 1) uniform selection (US), where the D2D helper is selected uniformly and 2) nearest selection (NS), where the nearest helper possessing the content is selected. Employing tools from stochastic geometry, we model the locations of BSs and D2D helpers using independent homogeneous Poisson point processes (HPPPs). We characterize the D2D mode probability of an arbitrary user for both the NS and US schemes. The distribution of the distance between an arbitrary user and its ith neighboring D2D helper within the macrocell is derived using disk approximation for the Voronoi cell, which is shown to be reasonably accurate. We fully characterize the overall coverage probability and the average ergodic rate of an arbitrary user requesting a particular content. We show that significant performance gains can be achieved compared to conventional cellular communication under both the NS and US schemes when popular contents are requested and NS scheme always outperforms the US scheme. Our analysis reveals an interesting trade off between the performance metrics and the number of candidate D2D helpers k. We conclude that enhancing D2D opportunities for the users does not always result in better performance and the network parameters have to be carefully tuned to harness maximum gains.
Continuous Authentication (CA) has been proposed as a potential solution to counter complex cybersecurity attacks that exploit conventional static authentication mechanisms that authenticate users only at an ingress point. However, widely researched human user characteristics-based CA mechanisms cannot be extended to continuously authenticate Internet of Things (IoT) devices. The challenges are exacerbated with increased adoption of device-to-device (d2d) communication in critical infrastructures. Existing d2d authentication protocols proposed in the literature are either prone to subversion or are computationally infeasible to be deployed on constrained IoT devices. In view of these challenges, we propose a novel, lightweight, and secure CA protocol that leverages communication channel properties and a tunable mathematical function to generate dynamically changing session keys. Our preliminary informal protocol analysis suggests that the proposed protocol is resistant to known attack vectors and thus has strong potential for deployment in securing critical and resource-constrained d2d communication.
We present MetaCP, a tool to aid the cryptographer throughout the process of designing and modelling a communication protocol suitable for formal verification. The crucial innovative aspect of the tool is its data-centric approach, where protocol specification is stored in a structured way rather than in natural languages to facilitate its interpretation to multiple target languages. Previous work shows a single exporting plugin (for Tamarin) which required aftermath modifications. By improving the expressiveness of the specification data structure we extend the tool to export to an additional formal language, i.e. ProVerif, as well as a C++ implementation. Starting with its modern graphical interface, MetaCP allows us to model the Diffie-Hellman key exchange, traditionally referred to as a case study, in just a few minutes. Ultimately, we use the formal tools to verify the executability and correctness of the automatically exported models. The design core of MetaCP is freely available in an online demo that provides two further sample protocols, Needham-Schroeder and Needham-Schroeder-Lowe, along with instructions to use the tool to begin modelling from scratch and to export the model to desired external languages.
In this paper, we propose a blockchain-based computing verification protocol, called EntrapNet, for distributed shared computing networks, an emerging underlying network for many internet of things (IoT) applications. EntrapNet borrows the idea from the practice of entrapment in criminal law to reduce the possibility of receiving incorrect computing results from trustless service providers who have offered the computing resources. Furthermore, we mathematically optimize EntrapNet to deal with the fundamental tradeoff of a network: security and efficiency. We present an asymptotic optimal solution to this optimization. It will be seen that EntrapNet can be performed as an independent and low-cost layer atop any trustless network that requires outsourced computing, thus making secure computing affordable and practical.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
