publication . Conference object . 2015

Formal Methods for MILS: Formalisations of the GWV Firewall

Koolen, Ruud; Schmaltz, Julien;
Open Access
  • Published: 20 Jan 2015
Abstract
To achieve security certification according to the highest levels of assurance, formal models and proofs of security properties are required. In the MILS context, this includes formalisation of key components - such as separation kernels - and the formalisation of applications built on top of these verified components. In this paper, we use the Isabelle/HOL proof assistant to formalise the Firewall application built on top of a verified separation kernel according to the model of Greve, Wilding, and Vanfleet (GWV). This Firewall application has been formalised twice after the original effort by GWV. These different efforts have been compared and discussed on pap...
Persistent Identifiers
Subjects
ACM Computing Classification System: TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMSTheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES
free text keywords: MILS, MILS
Download from
Open Access
Zenodo
Conference object . 2015
Provider: Datacite
Open Access
ZENODO
Conference object . 2015
Provider: ZENODO
Any information missing or wrong?Report an Issue