Modern vehicles are no longer merely mechanical systems but are monitored and controlled by various electronic systems. Safety-critical systems of connected vehicles become vulnerable to cyberattacks because of increasing interconnection. At present, the security risk analysis of connected vehicles is mainly based on qualitative methods, while these methods are usually subjective and lack consideration for functional safety. In order to solve this problem, we propose in this paper a security risk analysis framework for connected vehicles based on formal methods. Firstly, we introduce the electronic and electrical architecture of the connected vehicle and analyze the attack surfaces of the in-vehicle safety-critical systems from three levels of sensors, in-vehicle networks, and controllers. Secondly, we propose a method to model the target of evaluation (i.e., in-vehicle safety-critical system) as a Markov decision process and use probabilistic computation tree logic to formally describe its security properties. Then, a probabilistic model checker PRISM is used to analyze the security risk of target systems quantitatively according to security properties. Finally, we apply the proposed approach to analyze and compare the security risks of the collision warning system under a distributed and centralized electrical and electronic architecture. In addition, from a practical point of view, we propose a Markov model generation method based on a SysML activity diagram, which can simplify our modeling process. The evaluation results show that we can have a quantitative understanding of the security risks at the system level in the early stage of system design.
One-time Traversal Algorithm to Search Modules in a Fault Tree for the Risk Analysis of Safety-critical Systems