scholarly journals Model Checking Resiliency and Sustainability of In-Vehicle Network for Real-Time Authenticity

2021 ◽  
Vol 11 (3) ◽  
pp. 1068 ◽  
Author(s):  
Jin Hyun Kim ◽  
Hyo Jin Jo ◽  
Insup Lee
Keyword(s):  
Model Checking ◽  
Timed Automata ◽  
Formal Analysis ◽  
Sufficient Conditions ◽  
Third Party ◽  
Area Network ◽  
Message Authentication ◽  
Network Systems ◽  
Authentication Mechanism ◽  
Vehicle Network

The Controller Area Network (CAN) is the most common network system in automotive systems. However, the standardized design of a CAN protocol does not consider security issues, so it is vulnerable to various security attacks from internal and external electronic devices. Recently, in-vehicle network is often connected to external network systems, including the Internet, and can result in an unwarranted third-party application becoming an attack point. Message Authentication CAN (MAuth-CAN) is a new centralized authentication for CAN system, where two dual-CAN controllers are utilized to process message authentication. MAuth-CAN is designed to provide an authentication mechanism as well as provide resilience to a message flooding attack and sustainably protect against a bus-off attack. This paper presents formal techniques to guarantee critical timing properties of MAuth-CAN, based on model checking, which can be also used for safety certificates of vehicle components, such as ISO 26262. Using model checking, we prove sufficient conditions that MAuth-CAN is resilient and sustainable against message flooding and bus-off attacks and provide two formal models of MAuth-CAN in timed automata that are applicable for formal analysis of other applications running on CAN bus. In addition, we discuss that the results of model checking of those properties are consistent with the experiment results of MAuth-CAN implementation.

scholarly journals A Model-Checking-Based Framework for Analyzing Ambient Assisted Living Solutions

Sensors ◽  
2019 ◽  
Vol 19 (22) ◽  
pp. 5057 ◽  
Author(s):  
Ashalatha Kunnappilly ◽  
Raluca Marinescu ◽  
Cristina Seceleanu
Keyword(s):  
Model Checking ◽  
Assisted Living ◽  
Timed Automata ◽  
Formal Analysis ◽  
Ambient Assisted Living ◽  
Living System ◽  
Design Stage ◽  
Generic Model ◽  
Modeling And Analysis ◽  
Analysis And Design

Since modern ambient assisted living solutions integrate a multitude of assisted-living functionalities, out of which some are safety critical, it is desirable that these systems are analyzed at their design stage to detect possible errors. To achieve this, one needs suitable architectures that support the seamless design of the integrated assisted-living functions, as well as capabilities for the formal modeling and analysis of the architecture. In this paper, we attempt to address this need, by proposing a generic integrated ambient assisted living system architecture, consisting of sensors, data collection, local and cloud processing schemes, and an intelligent decision support system, which can be easily extended to suit specific architecture categories. Our solution is customizable, therefore, we show three instantiations of the generic model, as simple, intermediate, and complex configurations, respectively, and show how to analyze the first and third categories by model checking. Our approach starts by specifying the architecture, using an architecture description language, in our case, the Architecture Analysis and Design Language, which can also account for the probabilistic behavior of such systems, and captures the possibility of component failure. To enable formal analysis, we describe the semantics of the simple and complex architectures within the framework of timed automata. We show that the simple architecture is amenable to exhaustive model checking by employing the UPPAAL tool, whereas for the complex architecture we resort to statistical model checking for scalability reasons. In this case, we apply the statistical extension of UPPAAL, namely UPPAAL SMC. Our work paves the way for the development of formally assured future ambient assisted living solutions.

scholarly journals ANOMALY-BASED INTRUSION DETECTION FOR A VEHICLE CAN BUS: A CASE FOR HYUNDAI AVANTE CN7

2021 ◽  
Vol 56 (5) ◽  
pp. 144-156
Author(s):  
Kennedy Okokpujie ◽  
Grace Chinyere Kennedy ◽  
Vingi Patrick Nzanzu ◽  
Mbasa Joaquim Molo ◽  
Emmanuel Adetiba ◽  
...  
Keyword(s):  
Support Vector Machine ◽  
Intrusion Detection ◽  
Research Work ◽  
Support Vector ◽  
Area Network ◽  
Network Systems ◽  
Detection Techniques ◽  
Detection Systems ◽  
Attack And Defense ◽  
Vehicle Network

Flooding, spoofing, replay, and fuzzing are common in various types of attacks faced by enterprises and various network systems. In-vehicle network systems are not immune to attacks and threats. Intrusion detection systems using different algorithms are proposed to enhance the security of the in-vehicle network. We use a dataset provided and collected in "Car Hacking: Attack and Defense Challenge" during 2020. This dataset has been realized by the organizers of the challenge for security researchers. With the aid of this dataset, the work aimed to develop attack and detection techniques of Controller Area Network (CAN) using different algorithms such as support vector machine and Feedforward Neural Network. This research work also provides a comparison of the rendering of these algorithms. Based on experimental results, this work will help future researchers to benchmark their results for the given dataset. The results obtained in this work show that the model selection does not depend only on the model's accuracy that is explained by the accuracy paradox. Therefore, for the overall result accuracy of 62.65%, they show that the support vector machine presents the most satisfying output in terms of precision and recall. The Radial basis kernel gives 65% and 67% precision for fuzzing and flooding and the recall of 64% and 100% for replay and spoofing, respectively.

Schedulability Analysis for Timed Automata With Tasks

2021 ◽  
Vol 20 (5s) ◽  
pp. 1-26
Author(s):  
Jinghao Sun ◽  
Nan Guan ◽  
Rongxiao Shi ◽  
Guozhen Tan ◽  
Wang Yi
Keyword(s):  
Model Checking ◽  
State Space ◽  
Real Time ◽  
Timed Automata ◽  
Schedulability Analysis ◽  
Scheduling Theory ◽  
Real Time Scheduling ◽  
Analysis Techniques ◽  
Model Complex ◽  
Time Scheduling

Research on modeling and analysis of real-time computing systems has been done in two areas, model checking and real-time scheduling theory. In model checking, an expressive modeling formalism such as timed automata (TA) is used to model complex systems, but the analysis is typically very expensive due to state-space explosion. In real-time scheduling theory, the analysis techniques are highly efficient, but the models are often restrictive. In this paper, we aim to exploit the possibility of applying efficient analysis techniques rooted in real-time scheduling theory to analysis of real-time task systems modeled by timed automata with tasks (TAT). More specifically, we develop efficient techniques to analyze the feasibility of TAT-based task models (i.e., whether all tasks can meet their deadlines on single-processor) using demand bound functions (DBF), a widely used workload abstraction in real-time scheduling theory. Our proposed analysis method has a pseudo-polynomial time complexity if the number of clocks used to model each task is bounded by a constant, which is much lower than the exponential complexity of the traditional model-checking based analysis approach (also assuming the number of clocks is bounded by a constant). We apply dynamic programming techniques to implement the DBF-based analysis framework, and propose state space pruning techniques to accelerate the analysis process. Experimental results show that our DBF-based method can analyze a TAT system with 50 tasks within a few minutes, which significantly outperforms the state-of-the-art TAT-based schedulability analysis tool TIMES.

Proving properties of autonomous car manoeuvres in urban traffic

2021 ◽  
Vol 0 (0) ◽  
Author(s):  
Maike Schwammberger
Keyword(s):  
Model Checking ◽  
Functional Properties ◽  
Timed Automata ◽  
Urban Traffic ◽  
Abstract Model ◽  
Automated Driving ◽  
Spatial Logic

Abstract As automated driving techniques are increasingly capturing the market, it is particularly important to consider vital functional properties of these systems. We present an overview of an approach that uses an abstract model to logically reason about properties of autonomous manoeuvres at intersections in urban traffic. The approach introduces automotive-controlling timed automata crossing controllers that use the traffic logic UMLSL (Urban Multi-lane Spatial Logic) to reason about traffic situations. Safety in the context of collision freedom is mathematically proven. Liveness (something good finally happens) and fairness (no queue-jumping) are examined and verified using a model-checking tool for timed automata, UPPAAL.

Sign in / Sign up

Export Citation Format

Share Document