To achieve the highest levels of assurance, MILS architectures need to be formally analysed. A key challenge is to reason about the interaction between the software applications running on top of MILS core components, such as the separation kernel. In this paper, we extend Rushby's model of noninterference with explicit information units and domain programs. These extensions enable the reasoning at an abstract level about systems built on top of noninterference. As an illustration of our approach, we formally model and analyse an example inspired by the GWV Firewall.
|Titel||International Workshop on MILS: Architecture and Assurance for Secure Systems, Prague, 19 January 2016|
|Status||Gepubliceerd - 19 jan 2016|
|Evenement||International Workshop on MILS: Architecture and Assurance for Secure Systems - Prague, Tsjechië|
Duur: 19 jan 2016 → 19 jan 2016
|Workshop||International Workshop on MILS: Architecture and Assurance for Secure Systems|
|Periode||19/01/16 → 19/01/16|
Koolen, R. P. J., & Schmaltz, J. (2016). Modelling information routing with noninterference. In International Workshop on MILS: Architecture and Assurance for Secure Systems, Prague, 19 January 2016 https://doi.org/10.5281/zenodo.47980