Elsewhere we have briefly described the mechanisms available for confining objects to ensure that there is no leakage of information from them, and to ensure their integrity. Here we consider how these can be used in practice.

As we shall frequently use the term file we first define its meaning. A file is an example of a module designed according to the standard uniform information-hiding module structure which applies to all major software modules in the SPEEDOS system. The data of a file is held in its own separate address space of persistent data segments.

The interface routines associated with a module are for the purposes of this discussion separated into three groups: enquiries (i.e. entry points which return information about the state of a module without changing this state), operations (i.e. entry points which may change the state of a module) and constructors, which construct new modules of the type. This terminology is taken over from the L1 Project.

Securing the Integrity of a File

To secure the integrity of file data involves ensuring that the persistent data segments of the file module are not modified in an unauthorised way.

A user of a file F, e.g. the owner O, might pass to another user U a capability with restricted access rights intended to provide only read access to information in the file. He does this normally by creating a copy capability for F which allows only (a subset of) the enquiry interface routines to be invoked. In an ideal world (e.g. in which a proof exists that the code of the module performs exactly according to its specification) this would be sufficient, but in reality such an ideal situation does not usually exist. There are two potential problems.

First, the owner O may misunderstand the specification and consequently make a mistake in reducing the access rights, leaving a valid access right for an operation set in the capability. However, O can easily avoid this mistake by also unsetting the confinement permission permit_op in the copy capability before passing it to U. The effect is that whenever a routine of F is invoked by U the corresponding primary permission in Process Security Word (PSecW) is unset and the Kernel ensures that the module's code routines can only access persistent data segments in read only mode.

Second, the owner O may not trust the code of the module F, suspecting that it contains a bomb which will modify the state of F even in an enquiry which he as the owner makes. In this case he cannot necessarily simply unset the confinement permission permit_op in a copy capability which he makes for his own use, especially if he wants to use a combination of enquiries and operations. The best he can do here using the basic mechanisms is to attempt to ensure that enquiries do not modify F. (To ensure that enquiries return only the information defined in a specification requires a correctness proof, which is beyond the scope of the basic mechanisms.)

To make this situation more interesting let us assume that he also wants to ensure that operations do not return information about the state of F.

All of this can be achieved by bracketing F with an attribute module which ensures that interface routines defined in the specification as enquiries operate with permit_op unset while operations have permit_enq unset. For this purpose we define an attribute type "Untrusted", as follows:

fileattr untrusted

constr create (in rt_count: int; in rt_list: list of bool)

 except invalid_parameters

rout

op reconfine (in rt_list: list of bool)

 except invalid_parameters

enq routine_count: int

enq routine_list: list of bool

end untrusted

This attribute can be used by the owner of a file who does not trust its implementation. When the attribute is created a parameter defines how many interface routines there are supposed to be (to avoid the implementation containing hidden interfaces) and a second parameter defined as a list of boolean values which of the routines are enquiries and which are operations. (An operation is indicated if the corresponding boolean in the list is true, otherwise it is an enquiry.)

This attribute type has been made more generally useful in that it also allows a count of interface routines to be provided, and so can check that hidden routines ar not implemented. We now see an implementation of the visible features of the type "untrusted".

impl untr1 for untrusted

file rout_count: int

 rout_list: list of bool

constr create (in rt_count: int; in rt_list: list of bool)

begin

 if #rt_list != rt_count then

 raise (invalid_parameters)

 else

 rout_count:= rt_count

 rout_list:= rt_list

 endif

end create

rout

opreconfine (in rt_list: list of bool)

begin

 if #rt_list != rout_count then

 raise (invalid_parameters)

 else

 rout_list:= rt_list

 endif

end reconfine

enq routine_count: int

begin

 routine_count:= rout_count

end routine_count

enq routine_list: list of bool

begin

 routine_list:= rout_list

end routine_list

end untr1

The attribute has its own persistent data, used to note the number of valid routines and the list of which routines are enquiries and which are operations. When these variables are initialised (in the constructor "create") or modified (in the operation "reconfine") the number of routines which the file owner assumes to be available (rt_count), typically based on the specification, is checked against the number of routines in the list of enquiries and operations (rt_list).

In the bracket routines it is possible to carry out further checks. In the following example a permission is unset to ensure that no calls are made from the module.

impl untr_no_calls for untrusted

reuses untr1

bracket *** -- applies to all routines of the module

var call_num: int

begin

 call_num:= kernel.if_routine

 if call_num > rout_count then

 raise (hidden_routine_call)

 endif

 if rout_list (call_num) then -- test whether the op bit is true

 kernel.unset_permit_enq (primary)

 else

 kernel.unset_permit_op (primary)

 endif

 kernel.unset_permit_calls (all)

 body

end bracket ***

end untr_no_calls

This implementation of "untrusted" reuses the implementation of the visible interfaces from the previous diagram. When an enquiry is called permit_op is unset, when an operation is called permit_enq is unset. permit_calls is always unset. The attribute also checks against its own file information whether the routine number called is higher than the number defined by the owner of the file, thus preventing the calling of hidden routines not known to the owner. Alternative implementations are possible which adopt a dfferent confinement policy with regard to the calling of secondary modules.

Notice the difference between the unsetting of permissions in capabilities and in bracket routines in this example. By unsetting permit_op in a capability passed to another user, the owner O of F guards against his own mistakes, while the use of bracketing tests that the code of F operates according to specifications (with respect to the modifying of its state or returning information about it).

Securing the Confidentiality of a File

A simple - but relatively unusual - example of the need to secure the confidentiality of a file arises when the owner of a log file distributes capabilities for this to various users with the intention that they should write journalising messages to it, recording particular events (e.g. details of incoming transactions). Assuming that the code of the log file is correct such users can be prevented from reading the file simply by providing them with capabilities which in the access rights allow only the semantic write operations which they need. But if the owner of the file wants to guard against his own mistakes he can distribute capabilities with the confinement permission permit_enq unset. He can also prevent untrusted code from returning information via enquiries by bracketing the code with the attribute untrusted described above.

Confining a Service Routine

Sometimes standard software, such as an editor or a spooler, must be provided with access to a file in order to carry out its function, but then the question arises how such a service routine can be prevented from leaking the information in the file to a third party. We take a file editor as an example.

The Editor in our example needs access to an interactive terminal, in order to receive its editing instructions from a user. For this purpose it needs access to a device, which is viewed in SPEEDOS as an instance of a device driver. Device drivers in SPEEDOS are modules like any other, and are accessed in the usual way via inter-module calls protected with module capabilities. Consequently the Editor needs to receive as a parameter a module capability for the appropriate terminal. Read and write operations to a device are considered as equivalent to read and write operations to a file and device drivers can be confined accordingly.

There are two reasonable ways of implementing an editor in an information-hiding system such as SPEEDOS, either as a separate (program) module or as an integrated routine of the file's implementation code. We consider these in turn.

A. Confining the Editor as a Separate Program

The following diagram illustrates the basic confinement problem involved in this case.

The first issue is that the Editor will probably be called by a standard Command Language Interpreter (CLI). To prevent collusion between the code of these two modules the editor must be prevented from passing information which it obtains from the file back to the CLI. This can be achieved by the user providing the CLI with a capability for the Editor in which the primary confinement permit_enq is unset.

The capability used to call the Editor must also ensure that information from the file is not passed to a hidden module such that it can then be stored in persistent data segments. To do this by forbidding calls might be too restrictive, as the Editor may for example legitimately need to access a spelling dictionary. Hence non-parameter calls should be permitted, but confined in the secondary permissions by unsetting permit_op, thus ensuring that all files (at all levels) not passed as parameters are accessible only in read-only mode.

Precautions must also be taken to ensure that the Editor module itself does not have secret file data into which information can be stored. Thus one of the primary confinements permit_op or permit_file should be unset.

It remains to be considered how the parameters (module capabilities for the file and the terminal) are to be confined. The primary permission permit_calls for parameters must be set. The secondary parameter permissions (in the capability for calling the Editor) defining permit_file, permit_op and permit_enq must all be set. Potentially permit_calls must also be set at the secondary level, as the file module and/or the terminal device driver might need access to other modules not known to the user. But this appears to create a problem: if calls are permitted from these modules and the same permissions are carried over, these modules could apparently pass information to other secret modules which could later be accessed by a third party.

But in reality this is not a problem. There are at least two ways of introducing confinements. First, the module capabilities passed as parameters can themselves contain confinement restrictions. For example the file passed to the Editor might be restricted by the capability in its primary rights by unsetting permit_op and the terminal modules by unsetting permit_calls (of both kinds). Alternatively - or in addition - they might both be bracketed by some implementation of the attribute type untrusted.

B. Confining the Editor as an Integrated Routine of the File Module

We now consider how a similar level of confinement might be achieved for an Editor implemented as an integrated routine of the file module which it is editing. In this case the basic confinement problem is illustrated in the following diagram.

As in the first case, collusion between the code of the Editor/File Module and the CLI must be prevented. This can be achieved by the user providing the CLI with a capability for the file module in which the primary confinement permit_enq is unset.

Again, forbidding general calls from the editor/file module might be too restrictive. Hence non-parameter calls should be permitted, but confined in the secondary permissions by unsetting permit_op, thus ensuring that all files (at all levels) not passed as parameters are accessible only in read-only mode.

In this scenario the editor/file module would not need a secret file data into which information can be stored, as it has direct access to the file data. In contrast with the first case, the primary confinements permit_op and permit_file must not be unset, as it would then be impossible to edit the file.

As in the previous case, the primary permission permit_calls for parameters must be set, in order to allow the terminal module to be called. However, the secondary parameter permissions (in the capability for calling the file module/editor) defining permit_file, permit_op and permit_enq must be set. Again, permit_calls must be set at the secondary level, as the terminal device driver might need access to other modules not known to the user. And again, the confinement permissions in the parameter capability for the terminal must be set as appropriate to confine that module.

What about Modules which Secretly Create Files?

It may appear that an important issue has been overlooked so far. What is to prevent a Trojan horse in the code of a module from secretly creating a file into which it secretly stores information to be read later by a third party? This is not in fact a problem, as the following considerations show.

First, if it were possible secretly to create a file, this is not sufficient to leak the information which is stored in it, because the third party can only access the information if he has a capability for the file. But the precautions which we have taken against releasing the information equally apply to releasing a capability.

It might however be argued that this is inappropriate in the case where the purpose of a module is actually to create a new file for the user and pass back to him its capability. Such a situation apparently occurs for example when information is to be converted from one form to another. The conversion module apparently needs to create a new file into which it stores the converted version.

But even in this case appearances are deceptive, because there is a simple way to solve the problem without modifying the mechanisms presented so far. The user first creates an "empty" file and then passes its capability as a parameter to the conversion module. Thus the confinement permissions so far defined do not need to be complicated by further permissions, because the unsetting of appropriate permissions in the copy of the capability passed to the converter can be used to solve the problem.

In other words the problem has been reduced to those already described above. Interestingly, it also means that a user who needs a new file has to have an appropriate capability to create it, which is the more secure approach.

This appraoch may at first sight appear to cause a problem for the information hiding principle, according to which a module might create and use another module without the end-user being aware of its existence. But this is not really a problem. If a confined module really needs an auxiliary module whose existence is not known to the end user, it can create this auxiliary module and store its capability for further use later. If it is correctly confined it cannot - but it also does not need to - release the capability to other modules or users. It genuinely is a private module!

Rule Based Confinement

Confinement of information can be subject to particular defined rules. A prominent example is defined by the Bell-LaPadula security model. The use of the SPEEDOS basic confinement mechanisms to implement such rules is illustrated in a separate note.

Confinement of Capabilities

Special problems associated with the confinement of capabilities are also discussed in a separate note.