Publication

Security Architecture and Formal Analysis of an Airplane Software Distribution System

The 26th Congress of the International Council of the Aeronautical Sciences (ICAS 2008)

Author(s): David von Oheimb, Monika Maidl, Richard Robinson
Year: 2008
Publisher: AIAA (on CD-ROM)
Editors:
Keywords: Loadable Software, Information Assurance, Safety, System Architecture, Formal Methods
Abstract: In order to make airplane maintenance procedures more efficient and thus save time and costs, the distribution of airplane embedded software will increasingly be performed electronically over networks. Since such software often implements vital functionality while on the other hand communication networks are inherently unreliable and insecure, protecting the software distribution process is critical, both from the safety and the security perspective. Therefore an airplane software distribution system must provide protection guarantees which need to be verified at a high assurance level. In this paper, we introduce a software distribution system architecture with a generic core component, such that the overall software transport from the supplier to the airplane is an interaction of several instances of this core component communicating over insecure networks. The main advantage of this architecture is reduction of development and certification costs. Further, we outline the security evaluation of the proposed system according to the Common Criteria (CC) methodology and describe in detail our formal model and verification of its main functionality using the AVISPA tool. This mix of formal and systematic informal methods is a key factor in achieving high confidence in the security of the software distribution system at moderate cost.

BibTeX entry:

@inproceedings{ICAS08-Siemens-Boeing, author = {Oheimb, David von and Monika Maidl and Richard Robinson}, title = {Security Architecture and Formal Analysis of an Airplane Software Distribution System}, booktitle = {26th Congress of the International Council of the Aeronautical Sciences (ICAS)}, publisher = {Proceedings on CD-ROM available from \url{secr.exec@icas.org}}, editor = {AIAA}, pages = {1--12}, year = 2008, note = {\url{http://ddvo.net/papers/ICAS08.html}}, abstract = { In order to make airplane maintenance procedures more efficient and thus save time and costs, the distribution of airplane embedded software will increasingly be performed electronically over networks. Since such software often implements vital functionality while on the other hand communication networks are inherently unreliable and insecure, protecting the software distribution process is critical, both from the safety and the security perspective. Therefore an airplane software distribution system must provide protection guarantees which need to be verified at a high assurance level. In this paper, we introduce a software distribution system architecture with a generic core component, such that the overall software transport from the supplier to the airplane is an interaction of several instances of this core component communicating over insecure networks. The main advantage of this architecture is reduction of development and certification costs. Further, we outline the security evaluation of the proposed system according to the Common Criteria (CC) methodology and describe in detail our formal model and verification of its main functionality using the AVISPA tool. This mix of formal and systematic informal methods is a key factor in achieving high confidence in the security of the software distribution system at moderate cost. } }