Authodox Version 0.2.0 Manual

Begin by saving a copy of the empty system to disk. This will enable us to save future changes easily. Select File->Save As to display the Save As dialog. Choose a new file in which to save the new system, such as /tmp/ConfusedDeputy.xml then click Save As. Now, further changes to the system can be saved to file simply by clicking the Save toolbar button, or by pressing Ctrl-S.

The first thing to do is to set the global properties of our system. In this case we need to tell Authodox that the various operations that we model in our system are parameterised. The operations that we will model include reading and writing to and from a file (such as when Carol writes to Bill), and executing a program (such as when Alice executes Carol). When executing Carol, Alice is able to specify the name of a file that is to receive the compilation output. This file name must be specified as a parameter to the operation that Alice performs on Carol to execute her. Hence, we need to tell Authodox that our operations are parameterised.

Click on the System row of the system tree view, displayed on the left-hand side of the main window. This should be the topmost row of the tree and is used for setting global system properties. The right-hand pane should change to display a window labelled System that contains a checkbox labelled Operations are Parameterised. Check this checkbox. You'll notice that the tree view has changed so that the Status of the System component is now (modified). This means that part of this component (which represents the global system properties) has been changed but that the changes are yet to be applied.

Figure 3. Setting Global System Properties

Click the Commit button to apply the change. Then save the modified system to disk by clicking the Save toolbar button.

Having set the global system properties, we must now tell Authodox what sorts of operations are modelled in our system. To model the Confused Deputy scenario, we will use the following operations:

To create the operations, click on the Operations row of the system tree view. Type the name of the first operation, Read, into the text box underneath the words "Add An Operation" and click the Add button.

Figure 4. Adding an Operation

Repeat the process to add each of the other operations to the system. You should now be able to expand the Operations row so that underneath it is listed each of the four operations.

Figure 5. Viewing the Operations

We must now define each of the different kinds of behaviour that entities within our system can exhibit. In our example, there are only three:

In Authodox each behaviour is specified as a (usually parameterised) CSP process (see the section called “Authodox CSP Reference”). The send channel is used to send invocations to other objects in the system, while incoming invocations are received on the recv channel.

An event send.target.op.arg represents the invocation of the object target to perform the operation op, passing the argument arg. arg is either an object name or is the value null. In systems that have no parameterised operations, the arg part is omitted.

An event recv.from.op.arg represents the reception of an invocation from the object from to perform the operation op, with the argument arg. Again, arg is either an object name or is the value null. In systems that have no parameterised operations, the arg part is omitted.

The invocation by object source of object target to perform the operation op with argument arg can proceed only when both source is willing to perform send.target.op.arg and target is willing to perform recv.source.op.arg. At this point the invocation may proceed.

Let us take each of the behaviours in turn and show how they may be defined.

File

We define the behaviour File(acl) to represent the behaviour of a file. Notice that File takes a parameter, acl, which represents the file's access control list. acl is the set of objects that are allowed to access the file in question.

To add this behaviour to the system, click on the Behaviours row of the system tree view. Type the name File(acl), into the text box underneath the words "Add A Behaviour" and click the Add button.

Figure 6. Adding a Behaviour

We now need to define the actual workings of the File behaviour. To do this, expand the Behaviours row of the tree and then click on the File(acl) child row, which will alter the display so as to allow us to define the workings of the behaviour.

The job of a file is to accept requests to Read from it and to Write and Append to it by those objects that are allowed to do so (i.e. those that are members of the set acl). Hence, we may define its behaviour simply as follows.

File(acl) = recv?from:acl?op:{Read,Write,Append}!null -> File(acl)
      

File(acl) is willing to engage in any event recv.from.op.null where from is a member of the set acl and op is a member of the set {Read,Write,Append}. Its environment may choose which event is performed, after which point it returns to its initial state. Observe that we use the null parameter value for these operations, since we are not interested in modelling the actual data that is read from or written to a file but merely the fact that such an event has occurred.

Type (or paste) the definition above into the text box underneath the words "Update the code for File(acl)" and then click the Commit button.

Figure 7. Defining the File Behaviour

Note

If you're wondering what the "Update refines statement for File(acl)" box is for, fear not; we come to it later on.

Compiler(acl,logFile) = recv?from:acl!Exec?arg:Object -> 
                        send.arg.Write.null -> 
                        send.logFile.Append.null -> Compiler(acl,logFile)
      

User = (send?other?op:{Read,Write,Append}!null -> User []
        send?other!Exec?arg:Object -> User)
       |~| STOP
      

Having defined each of the different behaviours in our system, we must now define each of the objects. Each object instantiates one of the behaviours defined above. Our scenario comprises the following objects.

To instantiate each of the objects, begin by clicking on the Objects row of the tree. Type the name of the first object, Alice, into the text box labelled Name underneath the words "Add An Object". Then select the corresponding behaviour, User, from the drop-down list underneath the text box. Click the Add button to add this object to the system.

To instantiate Bill repeat the process as above. Once the corresponding behaviour, File(acl), has been selected from the drop-down list a text box will appear underneath allowing you to specify the value for Bill's acl. Enter the value {Carol} and click the Add button to add Bill to the system.

Figure 8. Adding an Object

Repeat the steps above to add Carol to the system. When defining her behaviour, select Compiler(acl,logFile) from the drop-down list and enter the appropriate values, {Alice} and Bill, for the parameters, acl and logFile, respectively.

Let's begin by exploring the behaviour of Bill. Expand the Objects row of the tree if you haven't already done so and click on the row labelled Bill. This brings up a pane allowing you to edit Bill's properties, including his behaviour. Click on the Explore button. This will open a new window allowing you to explore Bill's behaviour.

Behaviours are explored in terms of the finite-state machines that represent them. The newly opened window allows you to explore the FSM that represents Bill's behaviour. The tree view on the left allows you to expand the state-space of the FSM. Toggling the check button labelled Render Graph displays the FSM in terms of a directed graph whose nodes are the states of the FSM and whose edges are its transitions. The part of the FSM that corresponds to the currently highlighted row of the tree is automatically highlighted in the graph. Exploring an object's FSM allows you to ensure that it behaves as you would expect it to, by enabling you to step through its potential behaviours.

Figure 9. Exploring an Object's Behaviour

We can see here that Bill's behaviour is a single-state FSM that can perform any of three events, recv.Carol.Append.null, recv.Carol.Read.null and recv.Carol.Write.null which will cause a transition back to its initial state. This makes sense, given that Bill is a file that should allow reading, writing and appending only by Carol. Hence, we can see that Bill's behaviour is accurately captured in our model of the confused deputy scenario.

The behaviour of the other objects in the system can be examined similarly.

The behaviour of the entire system can be explored by clicking on the Explore System toolbar button. This brings up a similar window allowing you to explore the evolution of the entire system in terms of the FSM that characterises it.

The events of this FSM are either the special event _tau or they are of the form ioe_.o1.o2.op.arg and represent the occurrence of the operation op on object o2 by object o1, with argument arg.

The FSM for the entire system is very complicated. In particular, it contains a very large number of nodes and most of the edges are labelled with the special event _tau. This event represents a nondeterministic choice. These _tau events exist because of the high level of nondeterminism present in the definition of Alice's behaviour, User. Later, we will see how to simplify the system by refining the User behaviour to something more deterministic.

In order to do so, we must first specify the authority that Alice is allowed to have. She has excess authority, if her actual authority exceeds that which she is allowed to have.

Alice's allowed authority is defined by selecting the Alice row from the tree view and then filling in the text boxes underneath the words "Edit Alice's Allowed Authority". For this example, we are not interested in negative causation (where the occurrence of events causes another to not occur) so we can leave the check box labelled Include Negative Causation unchecked. The distinction between strong and weak causation is not relevant to this example. (The presence of strong causation implies the presence of weak causation.) If Alice can weakly cause Bill to be overwritten then we still consider her to have excess authority. Hence, for now, we can ignore strong causation and leave the Include Strong Causation check box unchecked.

We must first consider the permissions that Alice is allowed to acquire. She already has permission to invoke Carol, so this must be included. However, Alice shouldn't be allowed to acquire any further permissions. Alice's acquirable permissions should therefore be limited to the ability to Exec Carol.

Permissions are expressed in terms of send events that represent them. For example, the permission to Read from Bill would be represented by the event send.Bill.Read.null. Hence, we can define Alice's acquirable permissions simply as the set of events {|send.Carol.Exec|}.

Enter the expression above into the text box labelled Acquirable Permissions: to define the permissions that Alice is allowed to acquire.

Alice's acquirable authority in terms of positive causation (in which the occurrence of events causes another to occur) is defined as the set of events that Alice is allowed to cause to occur. Usually, we would expect that the invoker of Carol would be allowed to cause the file that they specify in the invocation to be written to. However, in our scenario, Alice doesn't have permission to Write to any files. Hence, she shouldn't really be allowed to cause Carol to do so on her behalf. She should be allowed to cause Carol to Append to Bill, since this occurs naturally as part of Carol's normal operation.

Causation authority is expressed in terms of events of the form ioe_.o1.o2.op.arg and represent the ability to cause object o1 to perform operation op on object o2, with argument arg. By definition, an object cannot cause its own events to occur. Hence, when defining the allowed authority of Alice, we should be careful to exclude all events that have either o1 or o2 as Alice.

We may define the set of events that Alice is allowed to (weakly) cause to occur simply as {|ioe_.Carol.Bill.Append|}. Enter this expression into the text box labelled Weak Positive Causation: and click the Commit button to define the events that Alice is allowed to cause to occur.

Figure 10. Defining an Object's Allowed Authority

We are now ready to test whether Alice has excess authority. To do so, click the toolbar button labelled Detect Excess Authority.

Doing so brings up a window in which the progress and results of the tests performed to detect excess authority may be examined. In this case, there are two tests. The first tests whether Alice can acquire excess permission. The second tests whether Alice can cause any events to occur that she shouldn't be allowed to cause.

Figure 11. Detecting Excess Authority

The test for Alice acquiring excess permission passes, meaning that Alice cannot acquire excess permission. However the test for Alice being able to cause unwanted events fails, indicating that Alice does indeed have excess authority. Clicking on the row for this test, labelled Alice can't weakly cause any event to occur ... allows us to view a counterexample demonstrating how Alice can wield her excess authority. In this case, we see that the occurrence of the event ioe_.Alice.Carol.Exec.Bill causes the event ioe_.Carol.Bill.Write.null to occur. In other words, by executing Carol passing the name Bill, Alice can cause Carol to overwrite Bill.

We see that Alice's excess authority has clearly been detected in this example.

The Revocation/ directory contains examples that model capability patterns relating to revocation. The following patterns are modelled here:

The SealerUnsealer/ directory contains examples that model small instances of a particular implementation of the Sealer-Unsealer pattern. The implementation here was first developed by Marc Stiegler in the context of the object-capability programming language E.

The ConfusedDeputy/ directory contains the Confused Deputy scenario considered in the section called “A Tutorial Introduction to Authodox”.