Enabling security checking of automotive ECUs with formal CSP models

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

Research output: Chapter in Book/Report/Conference proceedingConference proceeding

1 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 languageEnglish
Title of host publicationProceedings - 49th Annual IEEE/IFIP International Conference on Dependable Systems and Networks Workshop, DSN-W 2019
PublisherIEEE
Pages90-97
Number of pages8
ISBN (Electronic)9781728130309
DOIs
Publication statusPublished - 22 Aug 2019
Event49th Annual IEEE/IFIP International Conference on Dependable Systems and Networks Workshop, DSN-W 2019 - Portland, United States
Duration: 24 Jun 201927 Jun 2019

Publication series

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

Conference

Conference49th Annual IEEE/IFIP International Conference on Dependable Systems and Networks Workshop, DSN-W 2019
CountryUnited States
CityPortland
Period24/06/1927/06/19

    Fingerprint

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

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). [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