Using Threat Analysis Techniques to Guide Formal Verification: A Case Study of Cooperative Awareness Messages

Using Threat Analysis Techniques to Guide Formal Verification: A Case Study of Cooperative Awareness Messages. Farrell, M., Bradbury, M., Fisher, M., Dennis, L. A., Dixon, C., Yuan, H., & Maple, C. In Ölveczky, P. C. & Salaün, G., editors, Software Engineering and Formal Methods, pages 471–490, Cham, 2019. Springer International Publishing. [FAIR-SPACE]
abstract bibtex

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.

@InProceedings{Farrell2019,
author="Farrell, Marie
and Bradbury, Matthew
and Fisher, Michael
and Dennis, Louise A.
and Dixon, Clare
and Yuan, Hu
and Maple, Carsten",
editor="{\"O}lveczky, Peter Csaba
and Sala{\"u}n, Gwen",
title="Using Threat Analysis Techniques to Guide Formal Verification: A Case Study of Cooperative Awareness Messages",
booktitle="Software Engineering and Formal Methods",
year="2019",
publisher="Springer International Publishing",
address="Cham",
pages="471--490",
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.",
isbn="978-3-030-30446-1",
note = {[<span class="fs">FAIR-SPACE</span>]}
}

Downloads: 0

{"_id":"JWQEZqu3wjP85Ss9N","bibbaseid":"farrell-bradbury-fisher-dennis-dixon-yuan-maple-usingthreatanalysistechniquestoguideformalverificationacasestudyofcooperativeawarenessmessages-2019","authorIDs":[],"author_short":["Farrell, M.","Bradbury, M.","Fisher, M.","Dennis, L. A.","Dixon, C.","Yuan, H.","Maple, C."],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","author":[{"propositions":[],"lastnames":["Farrell"],"firstnames":["Marie"],"suffixes":[]},{"propositions":[],"lastnames":["Bradbury"],"firstnames":["Matthew"],"suffixes":[]},{"propositions":[],"lastnames":["Fisher"],"firstnames":["Michael"],"suffixes":[]},{"propositions":[],"lastnames":["Dennis"],"firstnames":["Louise","A."],"suffixes":[]},{"propositions":[],"lastnames":["Dixon"],"firstnames":["Clare"],"suffixes":[]},{"propositions":[],"lastnames":["Yuan"],"firstnames":["Hu"],"suffixes":[]},{"propositions":[],"lastnames":["Maple"],"firstnames":["Carsten"],"suffixes":[]}],"editor":[{"propositions":[],"lastnames":["Ölveczky"],"firstnames":["Peter","Csaba"],"suffixes":[]},{"propositions":[],"lastnames":["Salaün"],"firstnames":["Gwen"],"suffixes":[]}],"title":"Using Threat Analysis Techniques to Guide Formal Verification: A Case Study of Cooperative Awareness Messages","booktitle":"Software Engineering and Formal Methods","year":"2019","publisher":"Springer International Publishing","address":"Cham","pages":"471–490","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.","isbn":"978-3-030-30446-1","note":"[<span class=\"fs\">FAIR-SPACE</span>]","bibtex":"@InProceedings{Farrell2019,\nauthor=\"Farrell, Marie\nand Bradbury, Matthew\nand Fisher, Michael\nand Dennis, Louise A.\nand Dixon, Clare\nand Yuan, Hu\nand Maple, Carsten\",\neditor=\"{\\\"O}lveczky, Peter Csaba\nand Sala{\\\"u}n, Gwen\",\ntitle=\"Using Threat Analysis Techniques to Guide Formal Verification: A Case Study of Cooperative Awareness Messages\",\nbooktitle=\"Software Engineering and Formal Methods\",\nyear=\"2019\",\npublisher=\"Springer International Publishing\",\naddress=\"Cham\",\npages=\"471--490\",\nabstract=\"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.\",\nisbn=\"978-3-030-30446-1\",\nnote = {[<span class=\"fs\">FAIR-SPACE</span>]}\n}\n\n","author_short":["Farrell, M.","Bradbury, M.","Fisher, M.","Dennis, L. A.","Dixon, C.","Yuan, H.","Maple, C."],"editor_short":["Ölveczky, P. C.","Salaün, G."],"key":"Farrell2019","id":"Farrell2019","bibbaseid":"farrell-bradbury-fisher-dennis-dixon-yuan-maple-usingthreatanalysistechniquestoguideformalverificationacasestudyofcooperativeawarenessmessages-2019","role":"author","urls":{},"metadata":{"authorlinks":{}},"downloads":0},"bibtype":"inproceedings","biburl":"https://raw.githubusercontent.com/autonomy-and-verification/autonomy-and-verification.github.io/master/pubs.bib","creationDate":"2019-10-01T18:21:25.693Z","downloads":0,"keywords":[],"search_terms":["using","threat","analysis","techniques","guide","formal","verification","case","study","cooperative","awareness","messages","farrell","bradbury","fisher","dennis","dixon","yuan","maple"],"title":"Using Threat Analysis Techniques to Guide Formal Verification: A Case Study of Cooperative Awareness Messages","year":2019,"dataSources":["77JvGFZQteoFsRiyX","sf65xF3tXwz6TBuoQ","iqRbmbCgpDeaBjend"]}