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.
|Title of host publication||Proceedings - 49th Annual IEEE/IFIP International Conference on Dependable Systems and Networks Workshop, DSN-W 2019|
|Number of pages||8|
|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
|Name||Proceedings - 49th Annual IEEE/IFIP International Conference on Dependable Systems and Networks Workshop, DSN-W 2019|
|Conference||49th Annual IEEE/IFIP International Conference on Dependable Systems and Networks Workshop, DSN-W 2019|
|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.
- 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