CRV: Automated Cyber-Resiliency Reasoning for System Design Models

Daniel Larraz; Robert Lorch; Moosa Yahyazadeh; M. Fareed Arif; Omar Chowdhury; Cesare Tinelli

doi:10.34727/2023/isbn.978-3-85448-060-0_29

CRV: Automated Cyber-Resiliency Reasoning for System Design Models

Daniel Larraz
, Robert Lorch
, Moosa Yahyazadeh
, M. Fareed Arif
, Omar Chowdhury
, Cesare Tinelli

Computer Science

University of Iowa
University of Oxford

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

Abstract

We present the design and implementation of an automated static analysis approach and corresponding diagnostic tool, called Cyber Resiliency Verifier (CRV), to check whether a system design satisfies its end-to-end guarantees when the integrity of one or more of its components cannot be guaranteed. CRV's key insight is to reason about effects of integrity attacks instead of concrete attacks, enabling it to reason also about the impact of future attacks having the same captured effects. We demonstrate CRV's effectiveness with a case study on a realistic design of an unmanned aerial delivery drone.

Original language	English
Title of host publication	Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design, FMCAD 2023
Editors	Alexander Nadel, Kristin Yvonne Rozier, Warren A. Hunt, Georg Weissenbacher
Publisher	Institute of Electrical and Electronics Engineers Inc.
Pages	209-220
Number of pages	12
ISBN (Electronic)	9783854480600
DOIs	https://doi.org/10.34727/2023/isbn.978-3-85448-060-0_29
State	Published - 2023
Event	23rd International Conference on Formal Methods in Computer-Aided Design, FMCAD 2023 - Ames, United States Duration: Oct 24 2023 → Oct 27 2023

Publication series

Name	Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design, FMCAD 2023

Conference

Conference	23rd International Conference on Formal Methods in Computer-Aided Design, FMCAD 2023
Country/Territory	United States
City	Ames
Period	10/24/23 → 10/27/23

Access to Document

10.34727/2023/isbn.978-3-85448-060-0_29

Cite this

Larraz, D., Lorch, R., Yahyazadeh, M., Arif, M. F., Chowdhury, O., & Tinelli, C. (2023). CRV: Automated Cyber-Resiliency Reasoning for System Design Models. In A. Nadel, K. Y. Rozier, W. A. Hunt, & G. Weissenbacher (Eds.), Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design, FMCAD 2023 (pp. 209-220). (Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design, FMCAD 2023). Institute of Electrical and Electronics Engineers Inc.. https://doi.org/10.34727/2023/isbn.978-3-85448-060-0_29

Larraz, Daniel ; Lorch, Robert ; Yahyazadeh, Moosa et al. / CRV : Automated Cyber-Resiliency Reasoning for System Design Models. Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design, FMCAD 2023. editor / Alexander Nadel ; Kristin Yvonne Rozier ; Warren A. Hunt ; Georg Weissenbacher. Institute of Electrical and Electronics Engineers Inc., 2023. pp. 209-220 (Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design, FMCAD 2023).

@inproceedings{eae112ec64e74c5f9558687aee5ef645,

title = "CRV: Automated Cyber-Resiliency Reasoning for System Design Models",

abstract = "We present the design and implementation of an automated static analysis approach and corresponding diagnostic tool, called Cyber Resiliency Verifier (CRV), to check whether a system design satisfies its end-to-end guarantees when the integrity of one or more of its components cannot be guaranteed. CRV's key insight is to reason about effects of integrity attacks instead of concrete attacks, enabling it to reason also about the impact of future attacks having the same captured effects. We demonstrate CRV's effectiveness with a case study on a realistic design of an unmanned aerial delivery drone.",

author = "Daniel Larraz and Robert Lorch and Moosa Yahyazadeh and Arif, \{M. Fareed\} and Omar Chowdhury and Cesare Tinelli",

note = "Publisher Copyright: {\textcopyright} 2023 FMCAD Association and individual authors.; 23rd International Conference on Formal Methods in Computer-Aided Design, FMCAD 2023 ; Conference date: 24-10-2023 Through 27-10-2023",

year = "2023",

doi = "10.34727/2023/isbn.978-3-85448-060-0\_29",

language = "English",

series = "Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design, FMCAD 2023",

publisher = "Institute of Electrical and Electronics Engineers Inc.",

pages = "209--220",

editor = "Alexander Nadel and Rozier, \{Kristin Yvonne\} and Hunt, \{Warren A.\} and Georg Weissenbacher",

booktitle = "Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design, FMCAD 2023",

}

Larraz, D, Lorch, R, Yahyazadeh, M, Arif, MF, Chowdhury, O & Tinelli, C 2023, CRV: Automated Cyber-Resiliency Reasoning for System Design Models. in A Nadel, KY Rozier, WA Hunt & G Weissenbacher (eds), Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design, FMCAD 2023. Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design, FMCAD 2023, Institute of Electrical and Electronics Engineers Inc., pp. 209-220, 23rd International Conference on Formal Methods in Computer-Aided Design, FMCAD 2023, Ames, United States, 10/24/23. https://doi.org/10.34727/2023/isbn.978-3-85448-060-0_29

CRV: Automated Cyber-Resiliency Reasoning for System Design Models. / Larraz, Daniel; Lorch, Robert; Yahyazadeh, Moosa et al.
Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design, FMCAD 2023. ed. / Alexander Nadel; Kristin Yvonne Rozier; Warren A. Hunt; Georg Weissenbacher. Institute of Electrical and Electronics Engineers Inc., 2023. p. 209-220 (Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design, FMCAD 2023).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - CRV

T2 - 23rd International Conference on Formal Methods in Computer-Aided Design, FMCAD 2023

AU - Larraz, Daniel

AU - Lorch, Robert

AU - Yahyazadeh, Moosa

AU - Arif, M. Fareed

AU - Chowdhury, Omar

AU - Tinelli, Cesare

PY - 2023

Y1 - 2023

N2 - We present the design and implementation of an automated static analysis approach and corresponding diagnostic tool, called Cyber Resiliency Verifier (CRV), to check whether a system design satisfies its end-to-end guarantees when the integrity of one or more of its components cannot be guaranteed. CRV's key insight is to reason about effects of integrity attacks instead of concrete attacks, enabling it to reason also about the impact of future attacks having the same captured effects. We demonstrate CRV's effectiveness with a case study on a realistic design of an unmanned aerial delivery drone.

AB - We present the design and implementation of an automated static analysis approach and corresponding diagnostic tool, called Cyber Resiliency Verifier (CRV), to check whether a system design satisfies its end-to-end guarantees when the integrity of one or more of its components cannot be guaranteed. CRV's key insight is to reason about effects of integrity attacks instead of concrete attacks, enabling it to reason also about the impact of future attacks having the same captured effects. We demonstrate CRV's effectiveness with a case study on a realistic design of an unmanned aerial delivery drone.

UR - https://www.scopus.com/pages/publications/85180366251

U2 - 10.34727/2023/isbn.978-3-85448-060-0_29

DO - 10.34727/2023/isbn.978-3-85448-060-0_29

M3 - Conference contribution

AN - SCOPUS:85180366251

T3 - Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design, FMCAD 2023

SP - 209

EP - 220

BT - Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design, FMCAD 2023

A2 - Nadel, Alexander

A2 - Rozier, Kristin Yvonne

A2 - Hunt, Warren A.

A2 - Weissenbacher, Georg

PB - Institute of Electrical and Electronics Engineers Inc.

Y2 - 24 October 2023 through 27 October 2023

ER -

Larraz D, Lorch R, Yahyazadeh M, Arif MF, Chowdhury O, Tinelli C. CRV: Automated Cyber-Resiliency Reasoning for System Design Models. In Nadel A, Rozier KY, Hunt WA, Weissenbacher G, editors, Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design, FMCAD 2023. Institute of Electrical and Electronics Engineers Inc. 2023. p. 209-220. (Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design, FMCAD 2023). doi: 10.34727/2023/isbn.978-3-85448-060-0_29

CRV: Automated Cyber-Resiliency Reasoning for System Design Models

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this