Modelling information routing with noninterference

R.P.J. Koolen, J. Schmaltz

Onderzoeksoutput: Hoofdstuk in Boek/Rapport/CongresprocedureConferentiebijdrageAcademicpeer review

11 Downloads (Pure)

Samenvatting

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.

Originele taal-2Engels
TitelInternational Workshop on MILS: Architecture and Assurance for Secure Systems, Prague, 19 January 2016
Aantal pagina's7
DOI's
StatusGepubliceerd - 19 jan 2016
EvenementInternational Workshop on MILS: Architecture and Assurance for Secure Systems - Prague, Tsjechië
Duur: 19 jan 201619 jan 2016

Workshop

WorkshopInternational Workshop on MILS: Architecture and Assurance for Secure Systems
LandTsjechië
StadPrague
Periode19/01/1619/01/16

Vingerafdruk Duik in de onderzoeksthema's van 'Modelling information routing with noninterference'. Samen vormen ze een unieke vingerafdruk.

  • Citeer dit

    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