SE Linux Loadable Policy Modules

Syntax

As a result of additional needs for SELinux loadable policy modules some language extensions were made. These extensions do several things including identification of modules, versioning, adding explicit dependancy information to modules and optional policy blocks. This paper summarizes those changes and provides a reference for the syntax of loadable policy modules.

First each module has a name and version number

module syslogd 1.0;

This module name is used to list active modules and remove modules. The version should be used to identify what version a module is. Next each module must declare it's dependencies. This is done by way of require blocks.

require {
	type user_t, user_home_dir_t;
	role user_r;
	class file { read write };
}

These require blocks define the symbols a module uses. If the module use a symbols not required or declared within the module it will not compile. Further, if the required symbols are not available at link time the module cannot be inserted into the policy. This prevents an inconsistant policy.

Require blocks can also be used inside optional blocks to define optional policy rules that are contingent on the existance of these symbols.

optional {
	require {
		type user_home_sshd_t;
	}
	allow user_t user_home_sshd_t : file read;
}

This adds the rule allow user_t user_home_sshd_t : file read; only if the type user_home_sshd_t is available in the policy. The require header for optionals, stating those policy components necessary for this block to be active, must be present and have at least one declaration. There may be more than one require section, and they may appear in any location where an AV rule may exist. For convenience, if there are more than one then the compiler will concatenate their contents into a single one. The following optional block would be illegal as that it is empty:

optional {
	require {}
	allow a b: file { read };
}

This optional block is illegal because it has no require section at all:

optional {
	allow a b: file { read };
}

A module may both declare a symbol and then later require it, but only if the latter requirement occurs within the symbol's scope. Thus the first example below is legal but the second is not.

type type_in_scope_t;
optional {
	require { type type_in_scope_t; }
	allow a type_in_scope_t: file { read }
}

optional {
	type type_not_in_scope_t;
	allow a type_not_in_scope_t: file { read }
}
optional {
#	require { type type_not_in_scope_t; }  # this produces an error
#	allow a type_not_in_scope_t: file { read }
	# another error: this optional block has no requirements
}

However one may not require a symbol and then later declare it.

Optional blocks may also have else branches. No more than one else branch may be associated per optional block.. Be aware that the else branch may not have its own require section; all symbols within it must have been either required or declared by its parent's scope. Furthermore they may not declare any new symbols within. Here is an example:

optional {
	require {
		type a, b, c;
	}

allow a b: file {read};

} else {
# require block is forbidden within else branches
# require { type X; }

# no declarations are allowed in else branches either
# type Y;
allow d e: file {read};

}

Below is a reference grammar for module optional blocks. As that some programs and fonts do not correctly render the epsilon glyph it is explicitly written as {e}. Aspects of the policy that are not directly related to optionals have been omitted. Note that this grammar does not enforce all aspects of optionals, such as the necessity that there must exist at least one require block within an optional.

module := module_declaration ... avrules_block ...
avrules_block := avrule_decls users
avrule_decls := avrule_decl avrule_decls | avrule_decl
avrule_decl := rbac_decl | te_decl | cond_stmt_def |
               require_block | optional_block
require_block := REQUIRE '{' require_list '}'
require_list := require_decl require_list
              | require_decl
optional_block := OPTIONAL '{' avrules_block '}'
                  optional_else
optional_else := ELSE '{' avrules_block '}'
               | {e}
cond_stmt_def := IF cond_expr '{' cond_pol_list '}'
               | IF cond_expr '{' cond_pol_list '}'
                 ELSE '{' cond_pol_list '}'
               | ...
cond_pol_list := cond_rule_def cond_pol_list
               | optional_block cond_pol_list
               | {e}