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 proceedingpeer-review

    1 Citation (Scopus)
    34 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

    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

    Fingerprint Dive into the research topics of 'Enabling security checking of automotive ECUs with formal CSP models'. Together they form a unique fingerprint.

    Cite this