Analysis of Security Protocols in Embedded Systems

Publication: ResearchPh.D. thesis – Annual report year: 2016

Standard

Analysis of Security Protocols in Embedded Systems. / Bruni, Alessandro; Nielson, Flemming (Supervisor); Nielson, Hanne Riis (Supervisor).

Kgs. Lyngby : Technical University of Denmark (DTU), 2016. 155 p. (DTU Compute PHD-2016; No. 389).

Publication: ResearchPh.D. thesis – Annual report year: 2016

Harvard

Bruni, A, Nielson, F & Nielson, HR 2016, Analysis of Security Protocols in Embedded Systems. Ph.D. thesis, Technical University of Denmark (DTU), Kgs. Lyngby. DTU Compute PHD-2016, no. 389

APA

Bruni, A., Nielson, F., & Nielson, H. R. (2016). Analysis of Security Protocols in Embedded Systems. Kgs. Lyngby: Technical University of Denmark (DTU). (DTU Compute PHD-2016; No. 389).

CBE

Bruni A, Nielson F, Nielson HR 2016. Analysis of Security Protocols in Embedded Systems. Kgs. Lyngby: Technical University of Denmark (DTU). 155 p. (DTU Compute PHD-2016; No. 389).

MLA

Bruni, Alessandro, Flemming Nielson, and Hanne Riis Nielson Analysis of Security Protocols in Embedded Systems Kgs. Lyngby: Technical University of Denmark (DTU). 2016. (DTU Compute PHD-2016; Journal number 389).

Vancouver

Bruni A, Nielson F, Nielson HR. Analysis of Security Protocols in Embedded Systems. Kgs. Lyngby: Technical University of Denmark (DTU), 2016. 155 p. (DTU Compute PHD-2016; No. 389).

Author

Bruni, Alessandro; Nielson, Flemming (Supervisor); Nielson, Hanne Riis (Supervisor) / Analysis of Security Protocols in Embedded Systems.

Kgs. Lyngby : Technical University of Denmark (DTU), 2016. 155 p. (DTU Compute PHD-2016; No. 389).

Publication: ResearchPh.D. thesis – Annual report year: 2016

Bibtex

@phdthesis{d926bd84831042e0a23305cd8283f8b5,
title = "Analysis of Security Protocols in Embedded Systems",
abstract = "Embedded real-time systems have been adopted in a wide range of safety-critical applications—including automotive, avionics, and train control systems—where the focus has long been on safety (i.e., protecting the external world from the potential damage caused by the system) rather than security (i.e., protecting the system from the external world). With increased connectivity of these systems to external networks the attack surface has grown, and consequently there is a need for securing the system from external attacks. Introducing security protocols in safety critical systems requires careful considerations on the available resources, especially in meeting real-time and resource constraints, as well as cost and reliability requirements. For this reason many proposed security protocols in this domain have peculiar features, not present in traditional security literature.In this thesis we tackle the problem of analysing security protocols in safety critical embedded systems from multiple perspectives, extending current state-of-the-art analysis techniques where the combination of safety and security hinders our efforts. Examples of protocols in automotive control systems will follow throughout the thesis. We initially take a combined perspective of the safety and security features, by giving a security analysis and a schedulability analysis of the embedded protocols, with intertwined considerations. Then we approach the problem of the expressiveness of the tools used in the analysis, extending saturation-based techniques for formal protocol verification in the symbolic model. Such techniques gain much of their efficiency by coalescing all reachable states into a single set of facts. However, distinguishing different states is a requirement for modelling the protocols that we consider. Our effort in this direction is to extend saturation-based techniques so that enough state information can be modelled and analysed. Finally, we present a methodology for proving the same security properties in the computational model, by means of typing protocol implementations.",
author = "Alessandro Bruni and Flemming Nielson and Nielson, {Hanne Riis}",
year = "2016",
publisher = "Technical University of Denmark (DTU)",

}

RIS

TY - BOOK

T1 - Analysis of Security Protocols in Embedded Systems

AU - Bruni,Alessandro

A2 - Nielson,Flemming

A2 - Nielson,Hanne Riis

PY - 2016

Y1 - 2016

N2 - Embedded real-time systems have been adopted in a wide range of safety-critical applications—including automotive, avionics, and train control systems—where the focus has long been on safety (i.e., protecting the external world from the potential damage caused by the system) rather than security (i.e., protecting the system from the external world). With increased connectivity of these systems to external networks the attack surface has grown, and consequently there is a need for securing the system from external attacks. Introducing security protocols in safety critical systems requires careful considerations on the available resources, especially in meeting real-time and resource constraints, as well as cost and reliability requirements. For this reason many proposed security protocols in this domain have peculiar features, not present in traditional security literature.In this thesis we tackle the problem of analysing security protocols in safety critical embedded systems from multiple perspectives, extending current state-of-the-art analysis techniques where the combination of safety and security hinders our efforts. Examples of protocols in automotive control systems will follow throughout the thesis. We initially take a combined perspective of the safety and security features, by giving a security analysis and a schedulability analysis of the embedded protocols, with intertwined considerations. Then we approach the problem of the expressiveness of the tools used in the analysis, extending saturation-based techniques for formal protocol verification in the symbolic model. Such techniques gain much of their efficiency by coalescing all reachable states into a single set of facts. However, distinguishing different states is a requirement for modelling the protocols that we consider. Our effort in this direction is to extend saturation-based techniques so that enough state information can be modelled and analysed. Finally, we present a methodology for proving the same security properties in the computational model, by means of typing protocol implementations.

AB - Embedded real-time systems have been adopted in a wide range of safety-critical applications—including automotive, avionics, and train control systems—where the focus has long been on safety (i.e., protecting the external world from the potential damage caused by the system) rather than security (i.e., protecting the system from the external world). With increased connectivity of these systems to external networks the attack surface has grown, and consequently there is a need for securing the system from external attacks. Introducing security protocols in safety critical systems requires careful considerations on the available resources, especially in meeting real-time and resource constraints, as well as cost and reliability requirements. For this reason many proposed security protocols in this domain have peculiar features, not present in traditional security literature.In this thesis we tackle the problem of analysing security protocols in safety critical embedded systems from multiple perspectives, extending current state-of-the-art analysis techniques where the combination of safety and security hinders our efforts. Examples of protocols in automotive control systems will follow throughout the thesis. We initially take a combined perspective of the safety and security features, by giving a security analysis and a schedulability analysis of the embedded protocols, with intertwined considerations. Then we approach the problem of the expressiveness of the tools used in the analysis, extending saturation-based techniques for formal protocol verification in the symbolic model. Such techniques gain much of their efficiency by coalescing all reachable states into a single set of facts. However, distinguishing different states is a requirement for modelling the protocols that we consider. Our effort in this direction is to extend saturation-based techniques so that enough state information can be modelled and analysed. Finally, we present a methodology for proving the same security properties in the computational model, by means of typing protocol implementations.

M3 - Ph.D. thesis

BT - Analysis of Security Protocols in Embedded Systems

PB - Technical University of Denmark (DTU)

ER -