IFCIL: An Information Flow Configuration Language for SELinux (Extended Version)

TL;DR

This paper introduces IFCIL, an extension of CIL for SELinux, enabling administrators to specify and verify fine-grained information flow policies to enhance security configurations.

Contribution

We propose IFCIL, a backward compatible language extension for CIL, with a static verification tool for information flow policies in SELinux configurations.

Findings

IFCIL allows expressing confidentiality, integrity, and non-interference policies.

The verification tool effectively checks compliance with specified information flow requirements.

IFCIL improves the security policy development process for SELinux.

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. But this 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. However, CIL lacks mechanisms for ensuring that the resulting configurations obey desired information flow policies. To remedy this, we propose IFCIL, a backward compatible extension of CIL for specifying fine-grained information flow requirements for CIL configurations. Using IFCIL, administrators can express, e.g., confidentiality, integrity, and non-interference properties. We also provide a tool to statically verify these requirements.