SPEEDOS provides a set of basic mechanisms which can be used to implement solutions for confinement problems. Elsewhere we have provided some examples illutrating how these can be used in a general way to solve particular confinement problems. Here we consider how rule based confinement can be implemented in the SPEEDOS environment.

Implementing Access Control Rules

SPEEDOS provides a general mechanism which can be used to implement a wide variety of access control rules ­ not only in relation to confinement problems. The fundamental idea is that a major module of the system can be qualified by attribute types [3]. An attribute type can have its own (separately addressable and separately protected) persistent data segments, which may for example hold access control information. It can also have bracket routines, which consist of code dynamically linkedby the Kernel to an attributed module in such a way that a defined bracket routine starts executing when an interface routine of the attributed module is called. Execution continues until a body statement is encountered, at which point the interface routine (or an inner bracket routine) is entered. After the interface routine (or inner bracket) exits, control is returned to the statement following body in the bracket routine. After the bracket routine terminates control is returned to the calling module (or an outer bracket routine).

From the viewpoint of exercising access controls, a bracket routine with access to security information in the form of persistent data segments can either

• decide not to enter the interface routine of the attributed module, by not executing a body statement (and thus supporting general rule based access controls), or
• reduce the protection environment of the attributed module by switching off confinement and/or environmental permissions before executing the body statement.

The second alternative can be used for example to implement confinement restrictions based on security models such as those proposed by Bell-LaPadula [1], Biba [2] and similar. We now use a variant of the Bell-LaPadula security model to illustrate this.

A Bell-LaPadula Security System

We define a Bell-LaPadula system using a notation proposed a few years ago by a colleague and myself, which we called the Access Rule Model [4]. This allows rules to be specified as part of the process of defining access rights. The idea is basically very simple. An access rule specifies a condition which must be fulfilled in order that access may proceed. It takes the form

condition: subject -> object.{access_right}

This means that if (and only if) condition is fulfilled, subject may access object using the set of access rights access_rights.

Our Bell-LaPadula system has subjects with an associated clearance and set of projects, and objects with an associated classification and set of projects. Clearance and classification are hierarchically organised, e.g.

unclassified < confidential < secret < top secret

but projects are associated with subjects and objects on a non-hierarchical basis.

There are three basic rules, which control the reading and writing of objects by subjects and the creation of new subjects by existing subjects, as follows:

The Reading Rule (Simple Security Property):

(clearance(Subject) >= classification(Object)) (projects(Subject) projects(Object)): Subject -> Object{read}

The Writing Rule (*- Property):

(clearance(Subject) <= classification(Object)) (projects(Subject) projects(Object)): Subject -> Object{write}

The Subject Creation Rule:

(projects(SubjectT) projects(SubjectS) (clearance(SubjectT) <= clearance(SubjectS)): SubjectS -> SubjectT{create}

An Implementation of this Bell-LaPadula System for SPEEDOS

Several features of SPEEDOS are important for providing the straightforward implementation of this security model, including: the persistent virtual memory, persistent processes, the uniform module structure, attribute types with bracket routines, Kernel instructions for establishing the current environment in which a process/module is executing, and the basic confinement mechanisms.

Subjects are represented by processes and objects by file modules.

Information about subjects is held in a "subjects file". A specification for files of this type is as follows:

filetype Bell-LaPadula_subjects



let pr_list = list of subjects



constr create



rout



op new_subject (in user_id: unique_id; in clearance: int;



in proj_list: pr_list) except subject_exists, not_authorized



op change_subject (in user_id: unique_id; in clearance: int;



in proj_list: pr_list) except subject_invalid, not_authorized



enq sec_dets_for_current_user (out clearance: int;



out projects: pr_list)



enq clearance (in subject: unique_id): int



enq projects (in subject: unique_id): pr_list



end Bell-LaPadula_subjects

One such file is needed for each Bell-LaPadula system. Each record in the file describes a subject in the system, indicating his clearance level and the projects with which he is associated. The clearance is defined here as an integer, but in a particular system a subrange of integers could be used. Each subject is identified using a unique identifier. This corresponds to the address space number of the owner of the persistent process stack on which an interface routine is called, and cannot be forged.

A partial implementation for this file type is now shown:

impl BLS1 for Bell-LaPadula_subjects



let s_list = list of subject_rec



file



var subj_list: s_list



constr create



begin



subj_list:- s_list.new



end create



rout



op new_subject (in user_id: unique_id; inclearance: int;



int proj_list: pr_list)



filevar this_subject, creating_subject: subject_rec



var creating_user: unique_id



begin



this_subject:- subj_list(user = user_id)



if not this_subject = nil then



raise (subject_exists)



endif



creating_user:= kernel.process_owner



creating_subject:- subj_list(user = creating_user)



if creating_subject = nil then



raise (not_authorized)



endif



if clearance <= creating_subject.clearance and



proj_list <= creating_subject.projects then



this_subject:- subject_rec.new



this_subject.user:= user_id



this_subject.clearance:= clearance



this_subject.projects:= proj_list



else



raise (not_authorized)



endif



subj_list.insert(this_subject)



end new_subject



enq sec_dets_for_current_user (out clearance: int; out proj_list: pr_list)



begin



current_user:= kernel.process_owner



clearance:= subj_list(user = current_user).clearance



proj_list:= subj_list(user = current_user).projects



end sec_dets_for_current_user



...



end BLS1

objtype subject_rec



var user: unique_id



clearance: int



projects: pr_list



end subject_rec

Our Bell-Lapadula rule for creating subjects is implemented in the new_subject operation. This adds a new record to the file. (The format of records in the file appears at the end of the implementation.) The change_subject operation, an implementation for which is not shown, must also check that the rule is not violated. An implementation of the enquiry sec_dets_for_current_user is also shown.

The second type needed to implement a Bell-LaPadula system is an attribute type which is associated with each protected file. A type definition for this now follows:

fileattr Bell-LaPadula



create new (in rt_count, obj_class: int; in rt_list: list of bool;



in obj_proj: pr_list; in subjects_link: cap Bell-LaPadula_subjects)



rout



enq routine_count: int;



enq routine_list: list of bool



enq object_classification: int



enq object_projects: pr_list



end Bell-LaPadula

This attribute type is associated with individual files to be protected. The creation routine defines the classification and the projects associated with a particular file. It also sets a count of the routines available for accessing the objects and a list of booleans indicating which of these are read and which are write routines. (This technique was discussed in the context of the attribute type untrusted.) The parameter subjects_link provides a capability via which an instance of this attribute type can access the corresponding subjects file.

In a real system it would probably be useful to introduce further interface routines to allow the system administrator to redefine the security information about the associated file. A partial implementation of the interface routines now follows:

impl BL1 for Bell-LaPadula



file



var rout_count: int



rout_list: bit_list



obj_classification: int



obj_projects: set of int



subjects: cap Bell-LaPadula_subjects



create new (in rt_count, obj_class: int; in rt_list: list of bool;



in obj_proj: pr_list; insubjects_link: cap Bell-LaPadula_subjects)



begin



rout_count:= rt_count



rout_list:= rt_list



obj_classification:= obj_class



obj_projects:= obj_proj



subjects:= subjects_link



end new



rout



...



end BL1

This implementation is then reused in the following example to show how an appropriate bracket routine can be implemented which applies the Bell-LaPadula confinement rules for reading and writing.

impl BL1a for Bell-LaPadula



reusesBL1



bracket ***



var clearance: int



projects: set of int



reader, writer: bool



call_num: int



begin



call_num:= kernel.if_routine



if call_num > rout_count then



raise (hidden_routine_call)



endif



sobjects.sec_dets_for_current_user(clearance, projects)



if clearance >= obj_classification and



obj_projects in projects then



reader:= true



else



reader:= false



endif



if obj_classification >= clearance and



projects in obj_projects then



writer:= true



else



writer:= false



endif



if not reader and not writer then



raise (invalid_call)



endif



if rout_list(call_num) and writer then



kernel.unset_permit_enq



kernel.unset_permit_call



elsif (not rout_list (call_num)) and reader then



kernel.unset_permit_op



else



raise (invalid_call)



endif



body



end bracket ***



end BL1a

When a subject attempts to access a file his clearance and projects information are obtained by calling the sec_dets_for_current_user enquiry of the subjects file. By comparing the clearance and the projects of the subject with the file classification and its projects, the user's status as an authorized reader and/or writer is established and the call is permitted to proceed only if the call is a write call (as defined for the file) and the user is an authorized writer, or if the call is a read call (as defined for the file) and the user is an authorized reader. This is achieved by using Kernel instructions for unsetting the basic confinement permissions permit_enq, permit_op and permit_call.

We have now seen how the Bell-LaPadula rules for creating new subjects and for controlling read and write access to protected files can be realized in a system designed on the basis of the SPEEDOS architecture. It will be evident to the reader that many other security models (e.g. the Biba model [2]) can be implemented using the same basic techniques.

Confinement of Environmental Information

In this example of rule based confinement we have seen how the kernel has instructions which provide the code executing in a particular module in a particular persistent process with information about its environment. For example kernel.process_owner returns to the caller the unique identifier of the user who owns the currently active persistent process. Similarly kernel.if_routine returns the interface routine number of the routine explicitly called by the calling module, and thus allows a bracket routine to establish the environment in which it is currently operating. Elsewhere these environmental instructions are more fully described, and a possibility for restricting access to such information in potentially dangerous situations is also explained.

Confinement of Capabilities

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

References

[1] D. E. Bell and L. J. LaPadula "Secure Computer Systems: Mathematical Foundations", Mitre Corp., Bedford, Massachussets, 1973.

[2] K. Biba "Integrity Considerations for Secure Computer Systems", USAF Electronic System Division, 1977.

[3] J. L. Keedy, M. Evered, A. Schmolitzky and G. Menger "Attribute Types and Bracket Implementations", in Proceedings of the 25th International Conference on Technology of Object Oriented Systems, TOOLS 25, Melbourne, pp. 325-337, 1997.

[4] M. Evered and J. L. Keedy "A Model for Protection in Persistent Object-Oriented Systems", in Security and Persistence, Proceedings of the International Workshop on Computer Architectures to Support Security and Persistence of Information, Springer, 1990.