A Formal Modeling and Verification Scheme with an RNN-Based Attacker for CAN Communication System Authenticity
To enhance the attack resistance of the Controller Area Network (CAN) system and optimize the communication software design, a comprehensive model that combines a variable attacker with the CAN bus (VACB) is proposed to evaluate the bus communication risk. The VACB model consists of a variable attac...
| Main Authors: | , , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
MDPI AG
2022-06-01
|
| Series: | Electronics |
| Subjects: | |
| Online Access: | https://www.mdpi.com/2079-9292/11/11/1773 |
| _version_ | 1797493643313938432 |
|---|---|
| author | Yihua Wang Qing Zhou Yu Zhang Xian Zhang Jiahao Du |
| author_facet | Yihua Wang Qing Zhou Yu Zhang Xian Zhang Jiahao Du |
| author_sort | Yihua Wang |
| collection | DOAJ |
| description | To enhance the attack resistance of the Controller Area Network (CAN) system and optimize the communication software design, a comprehensive model that combines a variable attacker with the CAN bus (VACB) is proposed to evaluate the bus communication risk. The VACB model consists of a variable attacker and the CAN bus model. A variable attacker is a visualized generation of the attack traffic based on a recurrent neural network (RNN), which is used to evaluate the anti-attack performance of the CAN bus; the CAN bus model combines the data link layer and the application layer to analyze the anomalies in CAN bus data transmission after the attack message. The simulation results indicate that the transmission accuracy and successful response rate decreased by 1.8% and 4.3% under the constructed variable attacker. The CAN bus’s authenticity was promoted after the developers adopted this model to analyze and optimize the software design. The transmission accuracy and the successful response rate were improved by 2.5% and 5.1%, respectively. Moreover, the model can quantify the risk of potential attacks on the CAN bus, prompting developers to avoid it in early development to reduce the loss caused by system crashes. The comprehensive model can provide theoretical guidance for the timing design of embedded software. |
| first_indexed | 2024-03-10T01:22:58Z |
| format | Article |
| id | doaj.art-75401af5789745c5a4624fe87dbdc85b |
| institution | Directory Open Access Journal |
| issn | 2079-9292 |
| language | English |
| last_indexed | 2024-03-10T01:22:58Z |
| publishDate | 2022-06-01 |
| publisher | MDPI AG |
| record_format | Article |
| series | Electronics |
| spelling | doaj.art-75401af5789745c5a4624fe87dbdc85b2023-11-23T13:55:39ZengMDPI AGElectronics2079-92922022-06-011111177310.3390/electronics11111773A Formal Modeling and Verification Scheme with an RNN-Based Attacker for CAN Communication System AuthenticityYihua Wang0Qing Zhou1Yu Zhang2Xian Zhang3Jiahao Du4Key Laboratory of Electronics and Information Technology for Space System, National Space Science Center, Chinese Academy of Sciences, Beijing 100190, ChinaKey Laboratory of Electronics and Information Technology for Space System, National Space Science Center, Chinese Academy of Sciences, Beijing 100190, ChinaBeijing Jinghang Research Institute of Computing and Communication, Beijing 100074, ChinaBeijing Jinghang Research Institute of Computing and Communication, Beijing 100074, ChinaKey Laboratory of Electronics and Information Technology for Space System, National Space Science Center, Chinese Academy of Sciences, Beijing 100190, ChinaTo enhance the attack resistance of the Controller Area Network (CAN) system and optimize the communication software design, a comprehensive model that combines a variable attacker with the CAN bus (VACB) is proposed to evaluate the bus communication risk. The VACB model consists of a variable attacker and the CAN bus model. A variable attacker is a visualized generation of the attack traffic based on a recurrent neural network (RNN), which is used to evaluate the anti-attack performance of the CAN bus; the CAN bus model combines the data link layer and the application layer to analyze the anomalies in CAN bus data transmission after the attack message. The simulation results indicate that the transmission accuracy and successful response rate decreased by 1.8% and 4.3% under the constructed variable attacker. The CAN bus’s authenticity was promoted after the developers adopted this model to analyze and optimize the software design. The transmission accuracy and the successful response rate were improved by 2.5% and 5.1%, respectively. Moreover, the model can quantify the risk of potential attacks on the CAN bus, prompting developers to avoid it in early development to reduce the loss caused by system crashes. The comprehensive model can provide theoretical guidance for the timing design of embedded software.https://www.mdpi.com/2079-9292/11/11/1773controller area network busanti-attackattack traffic generationrecurrent neural networkmodel checkingUPPAAL |
| spellingShingle | Yihua Wang Qing Zhou Yu Zhang Xian Zhang Jiahao Du A Formal Modeling and Verification Scheme with an RNN-Based Attacker for CAN Communication System Authenticity Electronics controller area network bus anti-attack attack traffic generation recurrent neural network model checking UPPAAL |
| title | A Formal Modeling and Verification Scheme with an RNN-Based Attacker for CAN Communication System Authenticity |
| title_full | A Formal Modeling and Verification Scheme with an RNN-Based Attacker for CAN Communication System Authenticity |
| title_fullStr | A Formal Modeling and Verification Scheme with an RNN-Based Attacker for CAN Communication System Authenticity |
| title_full_unstemmed | A Formal Modeling and Verification Scheme with an RNN-Based Attacker for CAN Communication System Authenticity |
| title_short | A Formal Modeling and Verification Scheme with an RNN-Based Attacker for CAN Communication System Authenticity |
| title_sort | formal modeling and verification scheme with an rnn based attacker for can communication system authenticity |
| topic | controller area network bus anti-attack attack traffic generation recurrent neural network model checking UPPAAL |
| url | https://www.mdpi.com/2079-9292/11/11/1773 |
| work_keys_str_mv | AT yihuawang aformalmodelingandverificationschemewithanrnnbasedattackerforcancommunicationsystemauthenticity AT qingzhou aformalmodelingandverificationschemewithanrnnbasedattackerforcancommunicationsystemauthenticity AT yuzhang aformalmodelingandverificationschemewithanrnnbasedattackerforcancommunicationsystemauthenticity AT xianzhang aformalmodelingandverificationschemewithanrnnbasedattackerforcancommunicationsystemauthenticity AT jiahaodu aformalmodelingandverificationschemewithanrnnbasedattackerforcancommunicationsystemauthenticity AT yihuawang formalmodelingandverificationschemewithanrnnbasedattackerforcancommunicationsystemauthenticity AT qingzhou formalmodelingandverificationschemewithanrnnbasedattackerforcancommunicationsystemauthenticity AT yuzhang formalmodelingandverificationschemewithanrnnbasedattackerforcancommunicationsystemauthenticity AT xianzhang formalmodelingandverificationschemewithanrnnbasedattackerforcancommunicationsystemauthenticity AT jiahaodu formalmodelingandverificationschemewithanrnnbasedattackerforcancommunicationsystemauthenticity |