A type system for checking information flows in distributed systems | Kasper Laursen
| | Abstract | As the aviation industry integrates an expanding number of software components in airplanes, it is becoming increasingly difficult to reason about the security of the software. This thesis addresses aspects of this issue in the context of an abstract model of avionics systems as a distributed system using synchronous communication channels. The security of a system can then be related to the information flows and whether these are allowed by a set of policies, thus, using well-established theory from decentralised label model (DLM).
The security properties are verified using a combined type system and Hoare logic, which certifies that the defined policies are not violated by the execution of the distributed system as a whole.
In addition, the thesis describes a concrete implementation of parts of the type system, including tests on a use case from the avionics industry. The testing reveals a false positive, in which a secure system is erroneously declared non-secure. Therefore, the type system needs further adjustments. | | Type | Master's thesis [Academic thesis] | | Year | 2015 | | Publisher | Technical University of Denmark, Department of Applied Mathematics and Computer Science | | Address | Richard Petersens Plads, Building 324, DK-2800 Kgs. Lyngby, Denmark, compute@compute.dtu.dk | | Series | DTU Compute M.Sc.-2015 | | Note | DTU supervisor: Hanne Riis Nielson, hrni@dtu.dk, DTU Compute | | Electronic version(s) | [pdf] | | Publication link | http://www.compute.dtu.dk/English.aspx | | BibTeX data | [bibtex] | | IMM Group(s) | Computer Science & Engineering |
|