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.
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
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.
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:
(clearance(Subject) >= classification(Object)) 
(projects(Subject) 
projects(Object)): Subject -> Object{read}
(clearance(Subject) <= classification(Object)) (projects(Subject) 
projects(Object)): Subject -> Object{write}
(projects(SubjectT) projects(SubjectS) (clearance(SubjectT) <= clearance(SubjectS)): SubjectS -> SubjectT{create}
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.
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.
Special problems associated with the confinement of capabilities are discussed in a separate note.
[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.
© 1999 J. L. Keedy. Comments and corrections welcome to keedy@informatik.uni-ulm.de.
