Model Checking Resiliency and Sustainability of In-Vehicle Network for Real-Time Authenticity
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...
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
MDPI AG
2021-01-01
|
| Series: | Applied Sciences |
| Subjects: | |
| Online Access: | https://www.mdpi.com/2076-3417/11/3/1068 |
| _version_ | 1797407776063881216 |
|---|---|
| author | Jin Hyun Kim Hyo Jin Jo Insup Lee |
| author_facet | Jin Hyun Kim Hyo Jin Jo Insup Lee |
| author_sort | Jin Hyun Kim |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-03-09T03:46:33Z |
| format | Article |
| id | doaj.art-815d707aabd7410f9f3cc63cf3eb2c7e |
| institution | Directory Open Access Journal |
| issn | 2076-3417 |
| language | English |
| last_indexed | 2024-03-09T03:46:33Z |
| publishDate | 2021-01-01 |
| publisher | MDPI AG |
| record_format | Article |
| series | Applied Sciences |
| spelling | doaj.art-815d707aabd7410f9f3cc63cf3eb2c7e2023-12-03T14:33:45ZengMDPI AGApplied Sciences2076-34172021-01-01113106810.3390/app11031068Model Checking Resiliency and Sustainability of In-Vehicle Network for Real-Time AuthenticityJin Hyun Kim0Hyo Jin Jo1Insup Lee2Department of Information and Communication, Gyeongsang National University, Jinju 52828, KoreaSchool of Software, Soongsil University, Seoul 06978, KoreaDepartment of Computer and Information Science, University of Pennsylvania, Philadelphia, PA 19104, USAThe 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.https://www.mdpi.com/2076-3417/11/3/1068controller area network busauthenticationauthenticityresiliencysustainabilityformal verification |
| spellingShingle | Jin Hyun Kim Hyo Jin Jo Insup Lee Model Checking Resiliency and Sustainability of In-Vehicle Network for Real-Time Authenticity Applied Sciences controller area network bus authentication authenticity resiliency sustainability formal verification |
| title | Model Checking Resiliency and Sustainability of In-Vehicle Network for Real-Time Authenticity |
| title_full | Model Checking Resiliency and Sustainability of In-Vehicle Network for Real-Time Authenticity |
| title_fullStr | Model Checking Resiliency and Sustainability of In-Vehicle Network for Real-Time Authenticity |
| title_full_unstemmed | Model Checking Resiliency and Sustainability of In-Vehicle Network for Real-Time Authenticity |
| title_short | Model Checking Resiliency and Sustainability of In-Vehicle Network for Real-Time Authenticity |
| title_sort | model checking resiliency and sustainability of in vehicle network for real time authenticity |
| topic | controller area network bus authentication authenticity resiliency sustainability formal verification |
| url | https://www.mdpi.com/2076-3417/11/3/1068 |
| work_keys_str_mv | AT jinhyunkim modelcheckingresiliencyandsustainabilityofinvehiclenetworkforrealtimeauthenticity AT hyojinjo modelcheckingresiliencyandsustainabilityofinvehiclenetworkforrealtimeauthenticity AT insuplee modelcheckingresiliencyandsustainabilityofinvehiclenetworkforrealtimeauthenticity |