This project started with a literature study about the aviation industry and DLM.
From this most of terminology was settled in the rest of the project, and most of the case study was settled.
From previous work done in [NNL15] it was clear that DLM had some short-comings and needed to be extended with the conditional policies. Furthermore, I unsuccessful tried to map DLM work [ML00] to the new work in [NNL15]. The work done for this part was therefore discarded.
After the first third of the project period the draft paper [NNd] was presented to me, and the project took a turnover. The idea was now to verify the many of the facts, lemmas and proofs in [NNd] and to implement the type system also presented there.
The goal for the project was clear and a more regular day began. Thus, I used a much time understanding the type system and its correctness result. Furthermore, I wrote the case about the electronic flight bag with help from PhD student Ximeng Li
C.3 Auto-evaluation 117
from DTU Compute. This was good for the project to have another semi realistic case.
Along the way I took many notes, which have been really helpful in the end phase where all the smaller parts are merged together to form this thesis.
The overall project process has therefore been a mix of experimental and analytic approach.
Bibliography
[A81105] Airlines Electronic Engineering Committee.ARINC report 811: Commer-cial Aircraft Information Security Concepts of Operation and Process Framework. Aeronautical Radio, INC., 2005 (cited on pages 2, 3).
[Asta] Astrée. Astrée Run-Time Error Analyzer. url: http : / / www . absint . com/astree/index.htm(visited on January 27, 2015) (cited on page 6).
[Astb] Astrée Static Analyzer. The Astrée Static Analyzer. url: http://www.
astree.ens.fr/(visited on January 27, 2015) (cited on page 6).
[BH07] Lennart Beringer and Martin Hofmann. “Secure information flow and program logics”. In:Proceedings – IEEE Computer Security Foundations Symposium (2007), pages 233–245 (cited on page 39).
[Bou09] Ǵerard Boudol. Secure information flow as a safety property, In: For-mal Aspects in Security and Trust. Edited by Pierpaolo Degano, Joshua Guttman, and Fabio Martinelli. Volume 5491. Lecture Notes in Computer Science. Berlin, Heidelberg: Springer Berlin Heidelberg, 2009, pages 20–
34 (cited on page 39).
[But07] Henning Butz. “The Airbus Approach to Open Integrated Modular Avion-ics (IMA): Technology, Methods, Processes and Future Road Map”. In:
Workshop on Aircraft System Technologies(2007) (cited on pages 1, 2).
[CC12a] Common Criteria.Common Criteria for Information Technology Security Evaluation Part 1: Introduction and general model. 2012 (cited on page 2).
[CC12b] Common Criteria. Common Criteria for Information Technology Secu-rity Evaluation Part 2: SecuSecu-rity functional components. 2012 (cited on page 2).
[CC12c] Common Criteria.Common Criteria for Information Technology Security Evaluation Part 3: Security assurance components. 2012 (cited on page 2).
[DD12] Anthony Dessiatnikoff and Yves Deswarte. “Potential Attacks on On-board Aerospace Systems”. In: August (2012), pages 71–74 (cited on pages 1, 6).
[DD77] Dorothy E. Denning and Peter J. Denning. “Certification of programs for secure information flow”. In:Communications of the ACM 20 (1977), pages 504–513 (cited on page 9).
[DFP98] Rocco De Nicola, Gian Luigi Ferrari, and Rosario Pugliese. “Klaim: A kernel language for agents interaction and mobility”. In: IEEE Trans-actions on Software Engineering 24.5 (1998), pages 315–330 (cited on page 66).
[GAO15] United States Government Accountability Office. “Air Traffic Control:
FAA Needs a More Comprehensive Approach to Address Cybersecurity As Agency Transitions to NextGen”. In: April (2015) (cited on page 1).
[HNN09] Chris Hankin, Flemming Nielson, and Hanne R. Nielson. “Advice from belnap policies”. In:Proceedings - IEEE Computer Security Foundations Symposium(2009), pages 234–247 (cited on page 67).
[Hur15] Mark S. Hurley. “Search warrant for Chris Robberts’ electronics”. In:
(2015), pages 1–22.url:http://aptn.ca/news/wp-content/uploads/
sites/4/2015/05/warrant-for-Roberts-electronics.pdf(cited on page 1).
[Jif] Jif software.Jif: Java + information flow.url:http://www.cs.cornell.
edu/jif/(visited on July 7, 2015) (cited on page 68).
[Mil+97] Robin Milner et al. “The Definition of Standard ML, revised edition”. In:
MIT Press1.2 (1997), pages 2–3 (cited on page 54).
[ML00] Andrew C. Myers and Barbara Liskov. “Protecting privacy using the de-centralized label model”. In:ACM Transactions on Software Engineering and Methodology (TOSEM)9.4 (2000), pages 410–442 (cited on pages 3, 4, 68, 116).
[ML97] Andrew C. Myers and Barbara Liskov. “A Decentralized Model for In-formation Flow Control”. In: Proceedings of the 16th ACM Symposium on Operating Systems Principles (SOSP)(1997) (cited on pages 3, 68).
[Mül+12] Kevin Müller et al. “MILS-related information flow control in the avionic domain: A view on security-enhancing software architectures”. In: Pro-ceedings of the International Conference on Dependable Systems and Networks(2012) (cited on page 5).
[Mül+14] Kevin Müller et al. “Secure Information Flow Control in Safety-Critical Systems”. In: (2014) (cited on page 69).
[NN07] Hanne R. Nielson and Flemming Nielson. Semantics with Applications, An Appetizer (Undergraduate Topics in Computer Science). 2007 (cited on pages iii, 31, 35).
[NNd] Hanne R. Nielson and Flemming Nielson. “Content-Dependent Informa-tion Flow Control”. In:DTU Compute(2015). DRAFT (cited on pages 6, 10, 116).
[NNL15] Hanne R. Nielson, Flemming Nielson, and Ximeng Li. “Disjunctive In-formation Flow”. In: DTU Compute(2015) (cited on pages 5, 6, 10, 57, 116).
Bibliography 121
[SL15] The Security Ledger. GAO Warns of Cyber Risks In-Flight. 2015. url:
https : / / securityledger . com / 2015 / 04 / gao warns of cyber -risks-in-flight/(visited on June 29, 2015) (cited on page 1).
[SML/NJ] SML/NJ Fellowship.Standard ML of New Jersey (SML/NJ).url:http:
//www.smlnj.org/(visited on June 27, 2015) (cited on page 54).
[SYSGO] SYSGO. SYSGO – Embedding innocations. url: http : / / www . sysgo . com/ (visited on January 28, 2015) (cited on page 2).
[VSI09] Dennis Volpano, Geoffrey Smith, and Cynthia Irvine. “A Sound Type Sys-tem for Secure Flow Analysis”. In:Journal of Computer Security(2009), pages 1–20 (cited on page 4).
[WIR15] WIRED. Feds Say That Banned Researcher Commandeered a Plane.
2015. url: http : / / www . wired . com / 2015 / 05 / feds say banned -researcher-commandeered-plane/(visited on June 29, 2015) (cited on page 1).
[Yan] Jean Yang. Jeeves Programming Language. url: http : / / projects . csail.mit.edu/jeeves/(visited on July 7, 2015) (cited on page 69).
[YYS12] Jean Yang, Kuat Yessenov, and Armando Solar-Lezama. “A language for automatically enforcing privacy policies”. In:ACM SIGPLAN Notices47 (2012), page 85 (cited on page 69).
[Z3] Microsoft Research. Z3 – Efficient Theorem Prover. url: https : / / github.com/Z3Prover/z3(visited on June 27, 2015) (cited on page 54).