Enabling security checking of automotive ECUs with formal CSP models

John Heneghan; Siraj Ahmed Shaikh; Jeremy Bryans; Madeline Cheah; Paul Wooderson

doi:10.1109/DSN-W.2019.00025

Enabling security checking of automotive ECUs with formal CSP models

John Heneghan, Siraj Ahmed Shaikh, Jeremy Bryans, Madeline Cheah, Paul Wooderson

HORIBA MIRA Ltd.

Research output: Chapter in Book/Report/Conference proceeding › Conference proceeding › peer-review

10 Citations (Scopus)

158 Downloads (Pure)

Abstract

This paper presents an approach, using the process-algebra CSP, that aims to support systematic security testing of ECU components. An example use case regarding Over-The-Air software updates demonstrates the potential of our approach. Initial results confirm application code implemented in a typical automotive development environment can be translated into machine-readable format for the FDR refinement checker to formally verify security functions and identify any existing security flaws. Although still early stage work, the potential contribution towards automatically model-checking ECU components and, by composing several CSP models, larger systems is encouraging.

Original language	English
Title of host publication	Proceedings - 49th Annual IEEE/IFIP International Conference on Dependable Systems and Networks Workshop, DSN-W 2019
Publisher	IEEE
Pages	90-97
Number of pages	8
ISBN (Electronic)	9781728130309
DOIs	https://doi.org/10.1109/DSN-W.2019.00025
Publication status	Published - 22 Aug 2019
Event	49th Annual IEEE/IFIP International Conference on Dependable Systems and Networks Workshop, DSN-W 2019 - Portland, United States Duration: 24 Jun 2019 → 27 Jun 2019

Publication series

Name	Proceedings - 49th Annual IEEE/IFIP International Conference on Dependable Systems and Networks Workshop, DSN-W 2019

Conference

Conference	49th Annual IEEE/IFIP International Conference on Dependable Systems and Networks Workshop, DSN-W 2019
Country/Territory	United States
City	Portland
Period	24/06/19 → 27/06/19

Bibliographical note

© 2019 IEEE. Personal use of this material is permitted. Permission from IEEE must be obtained for all other uses, in any current or future media, including reprinting/republishing this material for advertising or promotional purposes, creating new collective works, for resale or redistribution to servers or lists, or reuse of any copyrighted component of this work in other works.

Copyright © and Moral Rights are retained by the author(s) and/ or other copyright owners. A copy can be downloaded for personal non-commercial research or study, without prior permission or charge. This item cannot be reproduced or quoted extensively from without first obtaining permission in writing from the copyright holder(s). The content must not be changed in any way or sold commercially in any format or medium without the formal permission of the copyright holders.

Keywords

Automotive
concurrent computing
cyber security
embedded software
formal verification
model checking
Software engineering
system verification

ASJC Scopus subject areas

Artificial Intelligence
Information Systems
Safety, Risk, Reliability and Quality

Access to Document

10.1109/DSN-W.2019.00025

Post-PrintAccepted author manuscript, 644 KBLicence: Unspecified

Cite this

Heneghan, J., Shaikh, S. A., Bryans, J., Cheah, M., & Wooderson, P. (2019). Enabling security checking of automotive ECUs with formal CSP models. In Proceedings - 49th Annual IEEE/IFIP International Conference on Dependable Systems and Networks Workshop, DSN-W 2019 (pp. 90-97). Article 8805994 (Proceedings - 49th Annual IEEE/IFIP International Conference on Dependable Systems and Networks Workshop, DSN-W 2019). IEEE. https://doi.org/10.1109/DSN-W.2019.00025

Enabling security checking of automotive ECUs with formal CSP models. / Heneghan, John; Shaikh, Siraj Ahmed; Bryans, Jeremy et al.
Proceedings - 49th Annual IEEE/IFIP International Conference on Dependable Systems and Networks Workshop, DSN-W 2019. IEEE, 2019. p. 90-97 8805994 (Proceedings - 49th Annual IEEE/IFIP International Conference on Dependable Systems and Networks Workshop, DSN-W 2019).

Research output: Chapter in Book/Report/Conference proceeding › Conference proceeding › peer-review

Heneghan, J, Shaikh, SA, Bryans, J, Cheah, M & Wooderson, P 2019, Enabling security checking of automotive ECUs with formal CSP models. in Proceedings - 49th Annual IEEE/IFIP International Conference on Dependable Systems and Networks Workshop, DSN-W 2019., 8805994, Proceedings - 49th Annual IEEE/IFIP International Conference on Dependable Systems and Networks Workshop, DSN-W 2019, IEEE, pp. 90-97, 49th Annual IEEE/IFIP International Conference on Dependable Systems and Networks Workshop, DSN-W 2019, Portland, United States, 24/06/19. https://doi.org/10.1109/DSN-W.2019.00025

Heneghan J, Shaikh SA, Bryans J, Cheah M, Wooderson P. Enabling security checking of automotive ECUs with formal CSP models. In Proceedings - 49th Annual IEEE/IFIP International Conference on Dependable Systems and Networks Workshop, DSN-W 2019. IEEE. 2019. p. 90-97. 8805994. (Proceedings - 49th Annual IEEE/IFIP International Conference on Dependable Systems and Networks Workshop, DSN-W 2019). doi: 10.1109/DSN-W.2019.00025

Heneghan, John ; Shaikh, Siraj Ahmed ; Bryans, Jeremy et al. / Enabling security checking of automotive ECUs with formal CSP models. Proceedings - 49th Annual IEEE/IFIP International Conference on Dependable Systems and Networks Workshop, DSN-W 2019. IEEE, 2019. pp. 90-97 (Proceedings - 49th Annual IEEE/IFIP International Conference on Dependable Systems and Networks Workshop, DSN-W 2019).

@inproceedings{60fe0085dcd34c90897bd76c1363325a,

title = "Enabling security checking of automotive ECUs with formal CSP models",

abstract = "This paper presents an approach, using the process-algebra CSP, that aims to support systematic security testing of ECU components. An example use case regarding Over-The-Air software updates demonstrates the potential of our approach. Initial results confirm application code implemented in a typical automotive development environment can be translated into machine-readable format for the FDR refinement checker to formally verify security functions and identify any existing security flaws. Although still early stage work, the potential contribution towards automatically model-checking ECU components and, by composing several CSP models, larger systems is encouraging.",

keywords = "Automotive, concurrent computing, cyber security, embedded software, formal verification, model checking, Software engineering, system verification",

author = "John Heneghan and Shaikh, {Siraj Ahmed} and Jeremy Bryans and Madeline Cheah and Paul Wooderson",

note = "{\textcopyright} 2019 IEEE. Personal use of this material is permitted. Permission from IEEE must be obtained for all other uses, in any current or future media, including reprinting/republishing this material for advertising or promotional purposes, creating new collective works, for resale or redistribution to servers or lists, or reuse of any copyrighted component of this work in other works. Copyright {\textcopyright} and Moral Rights are retained by the author(s) and/ or other copyright owners. A copy can be downloaded for personal non-commercial research or study, without prior permission or charge. This item cannot be reproduced or quoted extensively from without first obtaining permission in writing from the copyright holder(s). The content must not be changed in any way or sold commercially in any format or medium without the formal permission of the copyright holders. ; 49th Annual IEEE/IFIP International Conference on Dependable Systems and Networks Workshop, DSN-W 2019 ; Conference date: 24-06-2019 Through 27-06-2019",

year = "2019",

month = aug,

day = "22",

doi = "10.1109/DSN-W.2019.00025",

language = "English",

series = "Proceedings - 49th Annual IEEE/IFIP International Conference on Dependable Systems and Networks Workshop, DSN-W 2019",

publisher = "IEEE",

pages = "90--97",

booktitle = "Proceedings - 49th Annual IEEE/IFIP International Conference on Dependable Systems and Networks Workshop, DSN-W 2019",

address = "United States",

}

TY - GEN

T1 - Enabling security checking of automotive ECUs with formal CSP models

AU - Heneghan, John

AU - Shaikh, Siraj Ahmed

AU - Bryans, Jeremy

AU - Cheah, Madeline

AU - Wooderson, Paul

N1 - © 2019 IEEE. Personal use of this material is permitted. Permission from IEEE must be obtained for all other uses, in any current or future media, including reprinting/republishing this material for advertising or promotional purposes, creating new collective works, for resale or redistribution to servers or lists, or reuse of any copyrighted component of this work in other works. Copyright © and Moral Rights are retained by the author(s) and/ or other copyright owners. A copy can be downloaded for personal non-commercial research or study, without prior permission or charge. This item cannot be reproduced or quoted extensively from without first obtaining permission in writing from the copyright holder(s). The content must not be changed in any way or sold commercially in any format or medium without the formal permission of the copyright holders.

PY - 2019/8/22

Y1 - 2019/8/22

N2 - This paper presents an approach, using the process-algebra CSP, that aims to support systematic security testing of ECU components. An example use case regarding Over-The-Air software updates demonstrates the potential of our approach. Initial results confirm application code implemented in a typical automotive development environment can be translated into machine-readable format for the FDR refinement checker to formally verify security functions and identify any existing security flaws. Although still early stage work, the potential contribution towards automatically model-checking ECU components and, by composing several CSP models, larger systems is encouraging.

AB - This paper presents an approach, using the process-algebra CSP, that aims to support systematic security testing of ECU components. An example use case regarding Over-The-Air software updates demonstrates the potential of our approach. Initial results confirm application code implemented in a typical automotive development environment can be translated into machine-readable format for the FDR refinement checker to formally verify security functions and identify any existing security flaws. Although still early stage work, the potential contribution towards automatically model-checking ECU components and, by composing several CSP models, larger systems is encouraging.

KW - Automotive

KW - concurrent computing

KW - cyber security

KW - embedded software

KW - formal verification

KW - model checking

KW - Software engineering

KW - system verification

UR - http://www.scopus.com/inward/record.url?scp=85072041866&partnerID=8YFLogxK

U2 - 10.1109/DSN-W.2019.00025

DO - 10.1109/DSN-W.2019.00025

M3 - Conference proceeding

T3 - Proceedings - 49th Annual IEEE/IFIP International Conference on Dependable Systems and Networks Workshop, DSN-W 2019

SP - 90

EP - 97

BT - Proceedings - 49th Annual IEEE/IFIP International Conference on Dependable Systems and Networks Workshop, DSN-W 2019

PB - IEEE

T2 - 49th Annual IEEE/IFIP International Conference on Dependable Systems and Networks Workshop, DSN-W 2019

Y2 - 24 June 2019 through 27 June 2019

ER -

Enabling security checking of automotive ECUs with formal CSP models

Abstract

Publication series

Conference

Bibliographical note

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this