[RFC] Module language syntax

[RFC] Module language syntax

[Joshua Brindle]

Late last year we announced a prototype of the SELinux loadable policy
modules (previously called binary policy modules). That prototype
included several language changes to enable features like optional
policy blocks and modules dependency information. Only after starting to
write policy with these language extensions did it become apparent that
there were some shortcomings. For those who have never seen the module
language here is an example of the new syntax:

module foo 1.0;

require {
	type user_t, user_home_dir_t;
	class file { read write };
}
allow user_t user_home_dir_t : file { read write };

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


With this syntax macros can add their dependencies at the same time
they add the rules, and the same macros can be used in the global
scope as well as inside optionals.

The modules separate the development environment from the production
environment. Ideally the modules are compiled in a development
environment, tested and then sent to the production environment for
installation. The production environment then does not need a build
environment such as make, m4 and so on. The module tools will allow
these modules to be "linked in" to the current policy. It's at this link
time that both the modules dependencies and the optional dependencies
are determined and optionals with fulfilled dependencies are enabled.

All optionals are considered discrete entities with their own sets of
dependencies. The existence of these dependencies is checked at module
link time.

optionals my also have an else branch:

optional {
	require {
		type a, b, c;
	}
	allow {a c} b : file read;
} else {
	#no require for else
	allow foo bar : file read;
}

the else branch will not have a require block, and will use the modules
global scope.

The scoping rules are the same as the initial module work, the global
scope consists of symbols either declared outside of optionals and
symbols in require blocks outside of optionals. Each optional now has
it's own scope which is not shared with any other optional, this
consists of symbols declared inside that block and symbols in the
require blocks inside that optional.

For additional information on Loadable policy modules and the language
syntax please visit

http://sepolicy-server.sourceforge.net/index.php?page=modules
http://sepolicy-server.sourceforge.net/index.php?page=module-overview

More pages will be added shortly.

We believe this syntax is much more friendly to policy writers and would
like any comments or suggestions about the syntax. If this syntax seems
reasonable to everyone we should have a patch to implement it shortly.
Thank you


Joshua Brindle
Tresys Technology


--
This message was distributed to subscribers of the selinux mailing list.
If you no longer wish to subscribe, send mail to majordomo@tycho.nsa.gov with
the words "unsubscribe selinux" without quotes as the message.

Re: [RFC] Module language syntax

[Luke Kenneth Casson Leighton]

On Fri, May 27, 2005 at 02:17:33PM -0400, Joshua Brindle wrote:

> installation. The production environment then does not need a build
> environment such as make, m4 and so on. The module tools will allow
> these modules to be "linked in" to the current policy. It's at this link
> time that both the modules dependencies and the optional dependencies
> are determined and optionals with fulfilled dependencies are enabled.
 
 i take it that booleans are ... just... added / supported, too?

 such that they are declared in the binary module, used in the binary
 module, added to the config files and can be set at runtime, yes/

 l.


--
This message was distributed to subscribers of the selinux mailing list.
If you no longer wish to subscribe, send mail to majordomo@tycho.nsa.gov with
the words "unsubscribe selinux" without quotes as the message.

Re: [RFC] Module language syntax

[Joshua Brindle]

On Fri, 2005-05-27 at 19:53 +0100, Luke Kenneth Casson Leighton wrote:
> On Fri, May 27, 2005 at 02:17:33PM -0400, Joshua Brindle wrote:
> 
> > installation. The production environment then does not need a build
> > environment such as make, m4 and so on. The module tools will allow
> > these modules to be "linked in" to the current policy. It's at this link
> > time that both the modules dependencies and the optional dependencies
> > are determined and optionals with fulfilled dependencies are enabled.
>  
>  i take it that booleans are ... just... added / supported, too?
> 
>  such that they are declared in the binary module, used in the binary
>  module, added to the config files and can be set at runtime, yes/
> 
>  l.
> 

booleans and conditionals are runtime and are not at all affected by the
loadable modules. The optional dependencies added for modules are
totally separate from conditionals and are much closer to m4 ifdefs in
practice and could hopefully be used to replace many of them.

Joshua Brindle


--
This message was distributed to subscribers of the selinux mailing list.
If you no longer wish to subscribe, send mail to majordomo@tycho.nsa.gov with
the words "unsubscribe selinux" without quotes as the message.

Re: [RFC] Module language syntax

[Luke Kenneth Casson Leighton]

On Fri, May 27, 2005 at 02:54:26PM -0400, Joshua Brindle wrote:
> On Fri, 2005-05-27 at 19:53 +0100, Luke Kenneth Casson Leighton wrote:
> > On Fri, May 27, 2005 at 02:17:33PM -0400, Joshua Brindle wrote:
> > 
> > > installation. The production environment then does not need a build
> > > environment such as make, m4 and so on. The module tools will allow
> > > these modules to be "linked in" to the current policy. It's at this link
> > > time that both the modules dependencies and the optional dependencies
> > > are determined and optionals with fulfilled dependencies are enabled.
> >  
> >  i take it that booleans are ... just... added / supported, too?
> > 
> >  such that they are declared in the binary module, used in the binary
> >  module, added to the config files and can be set at runtime, yes/
> > 
> >  l.
> > 
> 
> booleans and conditionals are runtime and are not at all affected by the
> loadable modules. 


 great!  ... just checkin :)


--
This message was distributed to subscribers of the selinux mailing list.
If you no longer wish to subscribe, send mail to majordomo@tycho.nsa.gov with
the words "unsubscribe selinux" without quotes as the message.

Re: [RFC] Module language syntax

[Russell Coker]

On Saturday 28 May 2005 04:54, Joshua Brindle <jbrindle@tresys.com> wrote:
> booleans and conditionals are runtime and are not at all affected by the

So loading a module can define new booleans?

> loadable modules. The optional dependencies added for modules are
> totally separate from conditionals and are much closer to m4 ifdefs in
> practice and could hopefully be used to replace many of them.

The optional parts of modules will still take up disk space.  I presume that 
they will take up RAM as well - the program that loads the policy won't know 
which modules might be loaded.

Currently the strict policy is 10M in size and growing.  This is a problem 
that will become worse if we remove ifdefs.

Some ifdefs will need to be changed to optional dependencies for correct 
functionality, maybe many.  I don't see this as a benefit but rather as an 
unavoidable problem that is outweighed by the benefits of modules.

-- 
http://www.coker.com.au/selinux/   My NSA Security Enhanced Linux packages
http://www.coker.com.au/bonnie++/  Bonnie++ hard drive benchmark
http://www.coker.com.au/postal/    Postal SMTP/POP benchmark
http://www.coker.com.au/~russell/  My home page

--
This message was distributed to subscribers of the selinux mailing list.
If you no longer wish to subscribe, send mail to majordomo@tycho.nsa.gov with
the words "unsubscribe selinux" without quotes as the message.

Re: [RFC] Module language syntax

[Joshua Brindle]

Russell Coker wrote:

>On Saturday 28 May 2005 04:54, Joshua Brindle <jbrindle@tresys.com> wrote:
>  
>
>>booleans and conditionals are runtime and are not at all affected by the
>>    
>>
>
>So loading a module can define new booleans?
>
>  
>
Yes, just like loading a module can define new types, roles, users, etc. 
load_policy would continue to set the booleans as it does now I'd imagine

>>loadable modules. The optional dependencies added for modules are
>>totally separate from conditionals and are much closer to m4 ifdefs in
>>practice and could hopefully be used to replace many of them.
>>    
>>
>
>The optional parts of modules will still take up disk space. 
>
Yes

> I presume that 
>they will take up RAM as well - the program that loads the policy won't know 
>which modules might be loaded.
>  
>
They will only take up ram during module linking. Optional policy tha 
has been disabled will never make it to the kernel

>Currently the strict policy is 10M in size and growing.  This is a problem 
>that will become worse if we remove ifdefs.
>
>  
>
The disabled optionals will only be present in their modules. The 
advantage here is that the policy should never be 10 meg in kernel 
memory if the user has disabled unneeded policy modules.

>Some ifdefs will need to be changed to optional dependencies for correct 
>functionality, maybe many.  I don't see this as a benefit but rather as an 
>unavoidable problem that is outweighed by the benefits of modules.
>  
>
The benefits are fairly large. Instead of using an ifdef that depends on 
the existance of a filename to determine if a type is available (very 
weak dependancy mechanism) you use an optional that depends on that 
specific type actually being present. This stops policy breakage that 
occurs when you try disabling certain modules that are improperly 
ifdef'd. Further, it allows more freedom in policy development since 
modules (and optional blocks) will now depend on the existance of types, 
roles, etc instead of filenames. For example, if someone wanted to split 
up a policy they'd have to search for everywhere the types in those 
policies are used and rewrap the statements in ifdefs wheras with this 
nothing needs to be done, if the dependancies are met the module and 
optional block will become active.

One of the purposes of loadable policy modules was to fix the dependancy 
problem in policy. Each module has require block(s) that specify all the 
symbols that this particular module will need. The optional blocks are a 
way of specifying policy that should optionally be activated given the 
presense of certain symbols. The language changes we made make them use 
the exact same syntax for each so that, for example, a macro that 
declares it's depenencies will be able to do so whether it's in the 
global scope of a module or inside an optional without needing to know 
the difference.

Joshua Brindle

--
This message was distributed to subscribers of the selinux mailing list.
If you no longer wish to subscribe, send mail to majordomo@tycho.nsa.gov with
the words "unsubscribe selinux" without quotes as the message.