arXiv subjects

Masoud Ebrahimi

Publications and source records attributed to Masoud Ebrahimi.

9 recordsLinked to original sources

arXiv2023

A Systematic Approach to Automotive Security

We propose a holistic methodology for designing automotivesystems that consider security a central concern at every design stage.During the concept design, we model the system architecture and definethe security attributes of its components. We perform threat analysis onthe system model to identify structural security issues. From that analysis,we derive attack trees that define recipes describing steps to successfullyattack the system's assets and propose threat prevention measures.The attack tree allows us to derive a verification and validation (V&V)plan, which prioritizes the testing effort. In particular, we advocate usinglearning for testing approaches for the black-box components. It consistsof inferring a finite state model of the black-box component from its executiontraces. This model can then be used to generate new relevanttests, model check it against requirements, and compare two differentimplementations of the same protocol. We illustrate the methodologywith an automotive infotainment system example. Using the advocated approach, we could also document unexpected and potentially criticalbehavior in our example systems.

cs.CR↗

arXiv2022

Identification and Verification of Attack-Tree Threat Models in Connected Vehicles

As a result of the ever-increasing application of cyber-physical components in the automotive industry, cybersecurity has become an urgent topic. Adapting technologies and communication protocols like Ethernet and WiFi in connected vehicles yields many attack scenarios. Consequently, ISO/SAE 21434 and UN R155 (2021) define a standard and regulatory framework for automotive cybersecurity. Both documents follow a risk management-based approach and require a threat modeling methodology for risk analysis and identification. Such a threat modeling methodology must conform to the Threat Analysis and Risk Assessment (TARA) framework of ISO/SAE 21434. Conversely, existing threat modeling methods enumerate isolated threats disregarding the vehicle's design and connections. Consequently, they neglect the role of attack paths from a vehicle's interfaces to its assets. In other words, they are missing the TARA work products, e.g., attack paths compromising assets or feasibility and impact ratings. We propose a threat modeling methodology to construct attack paths by identifying, sequencing, and connecting vulnerabilities from a valid attack surface to an asset. Initially, we transform cybersecurity guidelines to attack trees, and then we use their formal interpretations to assess the vehicle's design. This workflow yields compositional construction of attack paths along with the required TARA work products (e.g., attack paths, feasibility, and impact). More importantly, we can apply the workflow iteratively in the context of connected vehicles to ensure design conformity, privacy, and cybersecurity. Finally, to show the complexity and the importance of preemptive threat identification and risk analysis in the automotive industry, we evaluate the presented model-based approach in a connected vehicle testing platform, SPIDER.

cs.CR↗

arXiv2022

Threat Repair with Optimization Modulo Theories

We propose a model-based procedure for automatically preventing security threats using formal models. We encode system models and potential threats as satisfiability modulo theory (SMT) formulas. This model allows us to ask security questions as satisfiability queries. We formulate threat prevention as an optimization problem over the same formulas. The outcome of our threat prevention procedure is a suggestion of model attribute repair that eliminates threats. Whenever threat prevention fails, we automatically explain why the threat happens. We implement our approach using the state-of-the-art Z3 SMT solver and interface it with the threat analysis tool THREATGET. We demonstrate the value of our procedure in two case studies from automotive and smart home domains, including an industrial-strength example.

cs.CR↗

arXiv2020

Safety Synthesis Sans Specification

We define the problem of learning a transducer ${S}$ from a target language $U$ containing possibly conflicting transducers, using membership queries and conjecture queries. The requirement is that the language of ${S}$ be a subset of $U$. We argue that this is a natural question in many situations in hardware and software verification. We devise a learning algorithm for this problem and show that its time and query complexity is polynomial with respect to the rank of the target language, its incompatibility measure, and the maximal length of a given counterexample. We report on experiments conducted with a prototype implementation.

cs.FL↗

arXiv2019

Learning a Behavior Model of Hybrid Systems Through Combining Model-Based Testing and Machine Learning (Full Version)

Models play an essential role in the design process of cyber-physical systems. They form the basis for simulation and analysis and help in identifying design problems as early as possible. However, the construction of models that comprise physical and digital behavior is challenging. Therefore, there is considerable interest in learning such hybrid behavior by means of machine learning which requires sufficient and representative training data covering the behavior of the physical system adequately. In this work, we exploit a combination of automata learning and model-based testing to generate sufficient training data fully automatically. Experimental results on a platooning scenario show that recurrent neural networks learned with this data achieved significantly better results compared to models learned from randomly generated data. In particular, the classification error for crash detection is reduced by a factor of five and a similar F1-score is obtained with up to three orders of magnitude fewer training samples.

cs.LG↗

arXiv2008

On the Throughput Maximization in Dencentralized Wireless Networks

A distributed single-hop wireless network with $K$ links is considered, where the links are partitioned into a fixed number ($M$) of clusters each operating in a subchannel with bandwidth $\frac{W}{M}$. The subchannels are assumed to be orthogonal to each other. A general shadow-fading model, described by parameters $(α,\varpi)$, is considered where $α$ denotes the probability of shadowing and $\varpi$ ($\varpi \leq 1$) represents the average cross-link gains. The main goal of this paper is to find the maximum network throughput in the asymptotic regime of $K \to \infty$, which is achieved by: i) proposing a distributed and non-iterative power allocation strategy, where the objective of each user is to maximize its best estimate (based on its local information, i.e., direct channel gain) of the average network throughput, and ii) choosing the optimum value for $M$. In the first part of the paper, the network hroughput is defined as the \textit{average sum-rate} of the network, which is shown to scale as $Θ(\log K)$. Moreover, it is proved that in the strong interference scenario, the optimum power allocation strategy for each user is a threshold-based on-off scheme. In the second part, the network throughput is defined as the \textit{guaranteed sum-rate}, when the outage probability approaches zero. In this scenario, it is demonstrated that the on-off power allocation scheme maximizes the throughput, which scales as $\frac{W}{α\varpi} \log K$. Moreover, the optimum spectrum sharing for maximizing the average sum-rate and the guaranteed sum-rate is achieved at M=1.

cs.IT↗

arXiv2007

Rate-Constrained Wireless Networks with Fading Channels: Interference-Limited and Noise-Limited Regimes

A network of $n$ wireless communication links is considered in a Rayleigh fading environment. It is assumed that each link can be active and transmit with a constant power $P$ or remain silent. The objective is to maximize the number of active links such that each active link can transmit with a constant rate $λ$. An upper bound is derived that shows the number of active links scales at most like $\frac{1}λ \log n$. To obtain a lower bound, a decentralized link activation strategy is described and analyzed. It is shown that for small values of $λ$, the number of supported links by this strategy meets the upper bound; however, as $λ$ grows, this number becomes far below the upper bound. To shrink the gap between the upper bound and the achievability result, a modified link activation strategy is proposed and analyzed based on some results from random graph theory. It is shown that this modified strategy performs very close to the optimum. Specifically, this strategy is \emph{asymptotically almost surely} optimum when $λ$ approaches $\infty$ or 0. It turns out the optimality results are obtained in an interference-limited regime. It is demonstrated that, by proper selection of the algorithm parameters, the proposed scheme also allows the network to operate in a noise-limited regime in which the transmission rates can be adjusted by the transmission powers. The price for this flexibility is a decrease in the throughput scaling law by a multiplicative factor of $\log \log n$.

cs.IT↗

arXiv2007

Throughput Scaling Laws for Wireless Networks with Fading Channels

A network of n communication links, operating over a shared wireless channel, is considered. Fading is assumed to be the dominant factor affecting the strength of the channels between transmitter and receiver terminals. It is assumed that each link can be active and transmit with a constant power P or remain silent. The objective is to maximize the throughput over the selection of active links. By deriving an upper bound and a lower bound, it is shown that in the case of Rayleigh fading (i) the maximum throughput scales like $\log n$ (ii) the maximum throughput is achievable in a distributed fashion. The upper bound is obtained using probabilistic methods, where the key point is to upper bound the throughput of any random set of active links by a chi-squared random variable. To obtain the lower bound, a decentralized link activation strategy is proposed and analyzed.

cs.IT↗

arXiv2007

Characterization of Rate Region in Interference Channels with Constrained Power

In this paper, an $n$-user Gaussian interference channel, where the power of the transmitters are subject to some upper-bounds is studied. We obtain a closed-form expression for the rate region of such a channel based on the Perron-Frobenius theorem. While the boundary of the rate region for the case of unconstrained power is a well-established result, this is the first result for the case of constrained power. We extend this result to the time-varying channels and obtain a closed-form solution for the rate region of such channels.

cs.IT↗