Formal Security Analysis in Industry, at the Example of Electronic Distribution of Aircraft Software (EDS)

Summary form only given. When developing products or solutions in industry and assessing their quality, formal methods provide the most rigorous tools for checking for safety and security flaws. In this talk we share our first-hand general experience in this area, and furthermore provide some details of a project specifying and modeling electronic distribution software (EDS). We comment on the motivation, practice, and impact of applying formal methods in industry, including the role of evaluation and certification according to the common criteria. Second, we give an overview of which modeling and verification techniques we have found useful so far, for which reasons. Third, we present some ongoing work on specifying and modeling EDS. The aim of EDS is to alleviate the burden of distributing initial and update versions of software in modern airplanes. By now this is done physically using disks, which is becoming unbearable with the amount of software steadily increasing. EDS is currently under standardization in the ARINC 666 committee, which includes the main players Boeing and Airbus, as well as their maintenance partners. Obviously, electronic shipment via cable-based and wireless connections faces severe security threats, such that one should better check with maximal scrutiny whether the mechanisms actually fulfill the security goals required, in particular integrity and authenticity.