Security Enhanced Linux (SELinux) is a security architecture for Linux implementing Mandatory Access Control. It has been used in numerous security-critical contexts ranging from servers to mobile devices. However, its application is challenging as SELinux security policies are difficult to write, understand, and maintain. Recently, the intermediate language CIL was introduced to foster the development of high-level policy languages and to write structured configurations. Despite CIL's high level features, CIL configurations are hard to understand as different constructs interact in non-trivial ways. Moreover, there is no mechanism to ensure that a given configuration obeys desired information flow policies. To remedy this, we enrich CIL with a formal semantics, and we propose IFCIL, a backward compatible extension of CIL for specifying fine-grained information flow requirements. Using IFCIL, administrators can express confidentiality, integrity, and non-interference properties. We also provide a tool to statically verify these requirements and we experimentally assess it on ten real-world policies.

Specifying and Verifying Information Flow Control in SELinux Configurations

Ceragioli L.;Galletta L.;
2024-01-01

Abstract

Security Enhanced Linux (SELinux) is a security architecture for Linux implementing Mandatory Access Control. It has been used in numerous security-critical contexts ranging from servers to mobile devices. However, its application is challenging as SELinux security policies are difficult to write, understand, and maintain. Recently, the intermediate language CIL was introduced to foster the development of high-level policy languages and to write structured configurations. Despite CIL's high level features, CIL configurations are hard to understand as different constructs interact in non-trivial ways. Moreover, there is no mechanism to ensure that a given configuration obeys desired information flow policies. To remedy this, we enrich CIL with a formal semantics, and we propose IFCIL, a backward compatible extension of CIL for specifying fine-grained information flow requirements. Using IFCIL, administrators can express confidentiality, integrity, and non-interference properties. We also provide a tool to statically verify these requirements and we experimentally assess it on ten real-world policies.
2024
Access control
information flow control
File in questo prodotto:
File Dimensione Formato  
acmtops.pdf

non disponibili

Tipologia: Versione Editoriale (PDF)
Licenza: Copyright dell'editore
Dimensione 466.61 kB
Formato Adobe PDF
466.61 kB Adobe PDF   Visualizza/Apri   Richiedi una copia

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/20.500.11771/31818
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 0
social impact