The basic access control mechanism in SPEEDOS is based on module capabilities, an idea taken over from Monads. (On the other hand the idea of segment capabilities and associated registers, which also appears in Monads, could not be taken over because of the inadequate hardware base.)

The SPEEDOS Kernel provides a second mechanism which can be used to enhance and complement the capability mechanism by providing additional access controls on an object when it is called. This second mechanism is based on an implementation of attribute types [1] with bracket routines. For a more general description of this technique follow this pointer. In this note we provide some examples of the use of attribute types to enhane access controls on the invocation of the interface routines of modules.

Revocation Lists

A standard problem found in capability based systems is known as the revocation problem. Capabiity based access is analgogous to a lock and key system. In such a system access to a building is provided by keys, which are distributed to users on a need basis. The problem arises that such keys cannot easily be recalled by the owner of the building when a user no longer needs them, because they are held in the private sphere of the user. Similarly in a capability system access to modules is provided by capabilities, which are distributed to users on a need basis. Because these can then be stored in the private space of the user there is a similar problem when the owner of a module wishes to revoke capabilities. In SPEEDOS there are in fact several ways of solving this problem. For example a module can be renamed (i.e. its unique identity can be changed by the owner), which is like changing the lock on a building, and consequently all capabilities are in effect invalidated. Another possibility is to pass a capability as a parameter to a target module with the permit_move metaright unset, so that the capability cannot be copied and is automatically deleted on return from the call to the target module. Such solution work in particular situations but not as a general rule. For this purpose a revocation list can be employed.

We now illustrate how a revocation list can be implemented in SPEEDOS. First we need a type definition for an attribute type revocable, as follows:

fileattr revocable

constr create_revocation_list

rout

op add_user (in new_user: unique_id; in invalid_list: bit_list)

 except user_in_list

op remove_user (in old_user: unique_id)

 except user_not_revoked

op change_perm (in a_user: unique_id; in invalid_list: bit_list)

 except user_not_revoked

enq revocations (in a_user: unique_id): bit_list

 except user_not_revoked

end revocable

Instances of this attribute have their own persistent data which consists of a list of users whose capabilities are revoked. Revocation can occur on the basis of individual access rights, so that for each entry point in the protected module a bit is set or unset in an "invalid list" to indicate whether the right of this user to call the corresponding interface routine is revoked. Users can be added to or removed from the revocation list or the invalid list associated a user can be modified. The current revocations associated with a user can also be examined. (In a real system there would be additional routines, e.g. to provide information about all users in the list.) These operations are themselves protected by the standard capability mechanism.

A partial implementation of the explicit features of the revocable, including a type definition for entries in the list itself, is provided in the following:

impl rev1 for revocable

let rev_list = list of rev_entry

file revoked_list: rev_list

constr create_revocation_list

begin

 revoked_list:- rev_list.new

end create_revocation_list

rout

op add_user (in new_user: unique_id; in invalid_list: bit_list)

filevar new_entry: rev_entry

begin

 new_entry:- revoked_list(user=new_user)

 if new_entry != nil then

 raise (user_in_list)

 else

 new_entry:- rev_entry.new

 new_entry.user:= new_user

 new_entry.revoked_routines:= invalid_list

 revoked_list.insert(new_entry)

 endif

end add_user

op remove_user (in old_user: unique_id)

begin ... end

op change_perm (in a_user: unique_id; in invalid_list: bit_list)

begin ... end

enq revocations (in a_user: unique_id): bit_list

begin ... end

end rev1

objtype rev_entry

var user: unique_id

 revoked_routines: bit_list

endrev_entry

Now that we have seen how the information needed for revoking capabilities/access rights can be obtained and modified by authorised users, we now consider how the access controls are actually implemented. For this purpose we need a bracket routine:

impl rev2 for revocable

reuses rev1

bracket ***

var call_num: int

 this_user: unique_id

begin

 call_num:= kernel.if_routine

 this_user:= kernel.process_owner

 if tis_user not in revoked_list then

 body

 else

 raise (access_denied)

 endif

end bracket ***

end rev2

The notation bracket *** indicates that this bracket routine is automatically executed whenever any interface routine of the qualified object is called. It then calls Kernel environmental instructions to establish the interface routine number of the routine in which it is currently operating and the unique identifier of the owner of the persistent process in which it is executing. It can then use this information to check against the information in the revoked list whether the call is valid. Only if the call is valid is the body statement executed, thus allowing the call to proceed. If the capability access right has been revoked an exception is raised and the call is aborted.

Access Control Lists (ACLs)

Whereas capabilities are associated with subjects, indicating what access rights they have to particular objects, an ACL is associated with an object, indicating what access rights particular users have for that object. In SPEEDOS an ACL can easily be implemented by means of an attribute type with bracket routines. An example is scarcely necessary, as an ACL can be viewed simply as a "positive" version of a revocation list, which indicates which users and with what rights they can (revocation list cannot) access the qualified module.

Notice that the capability mechanism is not in any way disabled when ACLs are used in a SPEEDOS system: capabilities remain a necessary (but not sufficient) condition for access to the interface routines of a module. Nevertheless if a user ­ or a system adminsitrator in a mandatory system ­ wishes to base access rights mainly on ACLs then all that he has to do is to place capabilities for all his objects with unrestricted access rights for all interface routines, in a directory or directory system, and provide a capability with unrestricted access to this in a shared "root" directory. Variants of this technique can for example be used to simulate the Unix file system.

Password Control to Sensitive Files

As a further example of what protection can be achieved by the use of attribute types and bracket implementations, we now consider an attribute password checking. A type definition could be as follows:

fileattr password_checking

constr create_passwd_file (in passwd1: string; in check_list: bit_list)

rout

op set_password_part_a (in part_a: string)

 except invalid_string

op set_password_part_b (in part_b: string)

 except invalid_string

op set_routines_for_checking (in check_list: bit_list)

 except invalid_routines

enq current_password: string

enq current_check_list: bit_list

enq password_checking

When an attribute instance is created two parameters are passed to it, an initial password and an initial bit list of routines (indicating with each bit, if set, whether attempted accesses to the corresponding interface routine requires checking of the password). The password can be changed using the pair of operations set_password_part_a and set_password_part_b, reflecting the technique used in banks for opening a vault: no single process can change the password alone. The list of routies to be checked can also be changed. There are enquiries to return the current password value and for which routines this must be supplied.

An implementation of the constructor and abracket routine are provided in the following. An implementation of the remaining interface routines is straightforward and need not be given here.

impl pc1 for password_checking

file

var password: string

 routine_list: bit_list

constr create_passwd_file (in passwd1: string; check_list: bit_list)

begin

 password:= passwd1

 routine_list:= check_list

end crate_password_file

rout

...                -- implementation of visible routines

bracket ***

var user_input: string

 term: terminal

 call_num: int

begin

 call_num:= kernel.if_routine

 if call_num in routine_list then

 term:- standardio.link

 term.read (user_input)         -- read password

 if user_input = password then

 body

 else

 raise (access_denied)

 endif

 else

 body

 endif

end bracket ***

end pc1

The bracket routine checks whether it is operating in the context of an interface routine which has been designated as requiring a password check. If not, it simply executes the body statement. If a password check is required it links to the current terminal and reads a password. (In reality the communication with the user would be a little more complcated.) If the user inputs the correct password the call to the qualified module proceeds. Otherwise the call is aborted.

Other Access Control Possibilities

As attribute types and bracket routines are user-programmable, it is evident that almost any checks conceivable can be carried out to determine whether access to a module may proceed. Thus in the SPEEDOS system there is no difficulty in implementing arbitrary rule-based access control. When these facilities are used in conjunction with the confinement features of the system and/or with environmental checks, the result is an extremely powerful access control system.

References

[1] Keedy, J. L., Evered, M., Schmolitzky, A. and Menger, G. "Attribute Types and Bracket Implementations", Proceedings of the Conference on Technology of Object-Oriented Languages and Systems, TOOLS 25, Melbourne, Australia 1997, IEEE Computer Society, pp.325-339.