Let be the set of files on the system. In , we can find /sbin/init, /etc/modules.conf, /usr/bin/, etc.
Let be the set of rights that can be given to a program. In we can find «mount a partition» or «read /this/file» or «execute /that/program if uid=0». We will see more details on this set later.
Then we can consider two functions and from to (the set of parts of ), that map a sub-set of to each file on the system.
The set of rights mapped by to a file are the rights that will be given to a process exec'ed with this file. Those mapped with are those the process will be able to transmit to a child.
Let be the property to be executable. For , will mean that is executable. is defined by induction :
The files can't use by themselves the rights they are given. They must be executed to give their process their rights. A file that can't be executed and that have some rights won't be able to use them, but who cares ?
When a file is exec'ed, the new process inherits its rights from the rights mapped to the file but also from its parent process rights.
Note that for , there can exist so that we have and , i.e. can have the right to give as inheritage a right it doesn't own. That means that if its process obtain this right by inheritage, it can transmit it.
We can't consider a static set of processes. Let be the set of running processes at the time . is a discrete virtual time variable that is incremented when a process is forked, is exec'ed or dies.
Let be a function from to that maps a sub-set of to each running processes, which will be the rights of this process.
Let be a function from to that maps a sub-set of to each running processes, which will be the rights the process can give to its lineage by inheritage.
The initial state, , is a singleton and the unique element is the init process.
So, if is /sbin/init and then . Moreover, we define and . This is the initial state.
The transition rules are :
Let be the set of couple of functions that enable the computer to fulfill its work. Each element of is a complete set of access controls that can rule the behaviour of the machine. Let define the partial order over :
If and are two elements of and , we can affirm that is more secure than because give at the very least one unnecessary right to a file. As the order is partial1.9, there can be more than one minimal element1.10.
There is no rule to decide which of two minimal elements is the most secure, but I think there will generally be only one minimal element.