Standard
Using Threat Analysis Techniques to Guide Formal Verification: A Case Study of Cooperative Awareness Messages. / Farrell, Marie
; Bradbury, Matthew; Fisher, Michael et al.
Software Engineering and Formal Methods: 17th International Conference, SEFM 2019, Oslo, Norway, September 18–20, 2019, Proceedings. ed. / Peter Csaba Ölveczky; Gwen Salaün. Cham: Springer International Publishing, 2019. p. 471-490 (Lecture Notes in Computer Science ; Vol. 11724).
Research output: Contribution in Book/Report/Proceedings - With ISBN/ISSN › Conference contribution/Paper › peer-review
Harvard
Farrell, M
, Bradbury, M, Fisher, M, Dennis, LA, Dixon, C, Yuan, H & Maple, C 2019,
Using Threat Analysis Techniques to Guide Formal Verification: A Case Study of Cooperative Awareness Messages. in PC Ölveczky & G Salaün (eds),
Software Engineering and Formal Methods: 17th International Conference, SEFM 2019, Oslo, Norway, September 18–20, 2019, Proceedings. Lecture Notes in Computer Science , vol. 11724, Springer International Publishing, Cham, pp. 471-490.
https://doi.org/10.1007/978-3-030-30446-1_25APA
Farrell, M.
, Bradbury, M., Fisher, M., Dennis, L. A., Dixon, C., Yuan, H., & Maple, C. (2019).
Using Threat Analysis Techniques to Guide Formal Verification: A Case Study of Cooperative Awareness Messages. In P. C. Ölveczky, & G. Salaün (Eds.),
Software Engineering and Formal Methods: 17th International Conference, SEFM 2019, Oslo, Norway, September 18–20, 2019, Proceedings (pp. 471-490). (Lecture Notes in Computer Science ; Vol. 11724). Springer International Publishing.
https://doi.org/10.1007/978-3-030-30446-1_25Vancouver
Farrell M
, Bradbury M, Fisher M, Dennis LA, Dixon C, Yuan H et al.
Using Threat Analysis Techniques to Guide Formal Verification: A Case Study of Cooperative Awareness Messages. In Ölveczky PC, Salaün G, editors, Software Engineering and Formal Methods: 17th International Conference, SEFM 2019, Oslo, Norway, September 18–20, 2019, Proceedings. Cham: Springer International Publishing. 2019. p. 471-490. (Lecture Notes in Computer Science ). doi: 10.1007/978-3-030-30446-1_25
Author
Farrell, Marie
; Bradbury, Matthew ; Fisher, Michael et al. /
Using Threat Analysis Techniques to Guide Formal Verification : A Case Study of Cooperative Awareness Messages. Software Engineering and Formal Methods: 17th International Conference, SEFM 2019, Oslo, Norway, September 18–20, 2019, Proceedings. editor / Peter Csaba Ölveczky ; Gwen Salaün. Cham : Springer International Publishing, 2019. pp. 471-490 (Lecture Notes in Computer Science ).
Bibtex
@inproceedings{420155d58b2b4f04a85794ee2fb8e8bc,
title = "Using Threat Analysis Techniques to Guide Formal Verification: A Case Study of Cooperative Awareness Messages",
abstract = "Autonomous robotic systems such as Connected and Autonomous Vehicle (CAV) systems are both safety-and security-critical, since a breach in system security may impact safety. Generally, safety and security concerns for such systems are treated separately during the development process. In this paper, we consider an algorithm for sending Cooperative Awareness Messages (CAMs) between vehicles in a CAV system and the use of CAMs in preventing vehicle collisions. We employ threat analysis techniques that are commonly used in the cyber security domain to guide our formal verification. This allows us to focus our formal methods on those security properties that are particularly important and to consider both safety and security in tandem. Our analysis centres on identifying STRIDE security properties and we illustrate how these can be formalised, and subsequently verified, using a combination of formal tools for distinct aspects, namely Promela/SPIN and Dafny.",
author = "Marie Farrell and Matthew Bradbury and Michael Fisher and Dennis, {Louise A.} and Clare Dixon and Hu Yuan and Carsten Maple",
year = "2019",
month = sep,
day = "1",
doi = "10.1007/978-3-030-30446-1_25",
language = "English",
isbn = "9783030304454",
series = "Lecture Notes in Computer Science ",
publisher = "Springer International Publishing",
pages = "471--490",
editor = "{\"O}lveczky, {Peter Csaba} and Gwen Sala{\"u}n",
booktitle = "Software Engineering and Formal Methods",
}
RIS
TY - GEN
T1 - Using Threat Analysis Techniques to Guide Formal Verification
T2 - A Case Study of Cooperative Awareness Messages
AU - Farrell, Marie
AU - Bradbury, Matthew
AU - Fisher, Michael
AU - Dennis, Louise A.
AU - Dixon, Clare
AU - Yuan, Hu
AU - Maple, Carsten
PY - 2019/9/1
Y1 - 2019/9/1
N2 - Autonomous robotic systems such as Connected and Autonomous Vehicle (CAV) systems are both safety-and security-critical, since a breach in system security may impact safety. Generally, safety and security concerns for such systems are treated separately during the development process. In this paper, we consider an algorithm for sending Cooperative Awareness Messages (CAMs) between vehicles in a CAV system and the use of CAMs in preventing vehicle collisions. We employ threat analysis techniques that are commonly used in the cyber security domain to guide our formal verification. This allows us to focus our formal methods on those security properties that are particularly important and to consider both safety and security in tandem. Our analysis centres on identifying STRIDE security properties and we illustrate how these can be formalised, and subsequently verified, using a combination of formal tools for distinct aspects, namely Promela/SPIN and Dafny.
AB - Autonomous robotic systems such as Connected and Autonomous Vehicle (CAV) systems are both safety-and security-critical, since a breach in system security may impact safety. Generally, safety and security concerns for such systems are treated separately during the development process. In this paper, we consider an algorithm for sending Cooperative Awareness Messages (CAMs) between vehicles in a CAV system and the use of CAMs in preventing vehicle collisions. We employ threat analysis techniques that are commonly used in the cyber security domain to guide our formal verification. This allows us to focus our formal methods on those security properties that are particularly important and to consider both safety and security in tandem. Our analysis centres on identifying STRIDE security properties and we illustrate how these can be formalised, and subsequently verified, using a combination of formal tools for distinct aspects, namely Promela/SPIN and Dafny.
U2 - 10.1007/978-3-030-30446-1_25
DO - 10.1007/978-3-030-30446-1_25
M3 - Conference contribution/Paper
SN - 9783030304454
T3 - Lecture Notes in Computer Science
SP - 471
EP - 490
BT - Software Engineering and Formal Methods
A2 - Ölveczky, Peter Csaba
A2 - Salaün, Gwen
PB - Springer International Publishing
CY - Cham
ER -
