SCOLL & SCOLLAR
Analyzing Safety in Patterns of Collaborating Entities

Last updated : 27 March 2006 by Fred Spiessens
Status: Definitions at the end need more work.

Overview

1. To check if a given pattern guarantees a set of safety properties without necessarily preventing another set of liveness properties
   For instance, subject alice should never get access to subject bob (safety), but there should at least be one possible scenario in which bob gets access to alice ( liveness) .
2. To search for (all) safe ways to restrict the interaction between the subjects in the pattern, such that:
   • no safety property is violated
   • no liveness property is prevented
   • every set of restrictions (solution) is minimal for safety: adding a restriction is not necessary, removing a restriction will break at least one safety property.
   The user will indicate what restrictions can actually be imposed. Typically, the imposable restrictions affect only the behavior of the subjects the user can program or control himself, and possibly part of the initial configuration of the pattern (eg: part of the initial access rights).
   Using SCOLLAR in this way is most useful when designing/programming secure patterns of interaction between some trusted (relied upon) and some untrusted (unknown) subjects.
3. Secure Interoperation: to search for (all) safe ways to restrict a set of patterns that share some of their subjects, such that:
   • interconnecting the patterns does not lead to effects that can violate the policy of any of the individual patterns
   • additional safety properties are guaranteed
   • additional liveness properties are not prevented
   • every solution is minimal for safety.

All three modes of operation are described in detail further on in this document.

The restrictions SCOLLAR can suggest:
When searching for minimal sets of restrictions, SCOLLAR will - at least in principle - check all combinations of these restrictions, and only report the minimal sets that guarantee the safety and liveness requirements the user has specified. (The actual algorithm is somewhat smarter of course, but will not be describe here.)
There are two kinds of restrictions:

1. Restrictions in the maximal behavior of one or more subjects.
   If the user wants to search for the necessary restrictions in the behavior of a subject, he/she should turn the subject into a search subject. To that end the subject's name must be preceded by the search option in the "subject" part of the pattern description.
   SCOLLAR will try to maximize the behavior of all search subjects. The atomic facts about the behavior of a search subject are called targets. Instead of saying that SCOLLAR searches for minimal sets of restrictions, we could also say that SCOLLAR searches for maximal sets of targets.
   If the user assigns behavior to a search subject, SCOLLAR will interpret it as a lower bound for the subjects behavior.
2. Restrictions in the initial configuration.
   The "config" part of the pattern description will typically contain initial access rights. Marking these rights with the search option turns them into targets. SCOLLAR will find what maximal subsets of these targets can safely be set to true in an initial configuration, and consequently report the complementary (minimal) subsets of necessary restrictions.

SCOLLAR's most important features are:

1. Behavior and configuration are equally important:
   Authority propagation is not just a matter of how rights are distributed in the initial configuration (who has the ability to use what right to whom) but must also take the behavior of the subjects into account (who is willing to use what right to whom in what circumstances).
   Both can be specified with equally expressive power.
2. Behavior is based on knowledge:
   Behavior is the "intention" of an subject to do something. A subject can use its knowledge (about itself and other subjects) to decide to be more "collaborative". Knowledge is both a prerequisite for and a result of succeeded interaction.
   Subjects have a set of subject rules that generate their behavior from their knowledge.
   "Effects" of interaction correspond to knowledge.
   "Intentions" to interact correspond to behavior. A technical explanation of these terms can be found further on.
3. Subject interaction is mediated explicitly by a "system":
   Ultimately, the rules that decide what conditions lead to what effects are the same for every subject. These are modeled explicitly as system rules that generate certain effects in certain conditions. System rules, like subject rules, are parametrized by subject variables.
   The system, by it rules, decides what knowlegde can become available to itself and to the subjects. If such a rule is conditional in the behavior of at least two subjects, it is said to be a collaboration rule .
4. Safe but Precise Approximation
   The general problem of precisely calculating if a configuration in a system can lead to the violation of a safety property is not computable. Harrison, Ruzzo and Ullman proved this in 1974 by showing how every Turing machine defines a safety problem that is safe exactly when the Turing machine will come to an halt. In 1936, Turing proved that the halting problem for Turing machines is not computable.
   We only consider the maximal behavior of the subjects, and require the subject rules and system rules to be monotonic. This forces the model to be a safe and computable approximation of the actual problem.
   Within the limits stated above, the approximation can be arbitrary precise. If an approximative model is too crude, one can always refine the system rules to make them generate more precise knowledge from more precise conditions, so that behavior can also be expressed with improved precision.
   For instance, a system with only binary knowledge of the form access(Subject1, Subject2) could specify how this access was achieved : receivedFrom(Subject1, InvokedSubject, Subject2). This will inform Subject1 that it has successfully invoked InvokedSubject, whom returned Subject2.

1. Improve performance and scalability
   • Complex patterns with precise system knowledge and large patterns with many subjects or subsystems take a long time to calculate. The time complexity of the current implementation is in NP. We are experimenting with sat solvers and linear programming, to provide faster solutions for certain problem instances.
     The current online implementation of SCOLLAR uses Finite Domain Integer Constraints in Mozart/Oz.
2. Improve expressive power
   • provide collaboration contexts that help express precise behavior conditions related to a single invocation/collaboration.
   • provide explicit support for creation of subjects.
   • provide support for the propagation of data.
   • allow arbitrary complex liveness and safety properties (constraints rather than simple predicates)
   • allow search on subject initialization.
     Subject behavior can be initialized, just as the configuration is. In the current version of SCOLLAR, subject initialization facts cannot be turned into targets.
3. Improve usability
   • provide robustness for SCOLLAR online.
   • provide support for computer assisted modeling of SCOLL patterns, for instance for mapping code.
   • improve this documentation
   • users can now save their patterns online for their private use, if they use cookies. This should be made more robust and secure.
   • allow rules to have more than one predicate in the right hand side, for concise representation.
   • allow generation and visualization of (access) graphs, derived from (binary) predicates in the configurations, the solutions, and the fixpoints.

SCOLL: "Safe Collaboration Language"

Introduction to some technical concepts in SCOLL

• Predicates and Facts
  Apart from the subjects themselves, the most central concepts in SCOLL are the relations between the subjects. Every relation that is used corresponds to a predicate with the same arity.
  • A predicate is a Boolean function that indicates if a certain tuple is in the relation.
    We denote a predicate as :
    <label>(A B ... X)
    where <label> names the relation
    and A ... X are variables ranging over the subjects.
    For instance read(A B) is a binary predicate.
    
  • We call an individual tuple a fact.
    For instance access(alice bob) is a fact. If it is true, it means that alice stands in the relation access to bob.
    The first subject in a fact is called the base subject and has a special status: it is the subject the fact is about.
    The role of the base subject is clarified in the next paragraph.
  
  
• Knowledge and Behavior We distinguish between two kinds of predicates:
  • Knowledge predicates correspond to relations that are part of the state of the system.
    For instance, the predicate access(A B) could be used to indicate that a subject A has access to a subject B.
    Similarly, the predicate hasInvoked(A B X) could be used to indicate that a subject A has succesfully invoked a subject B and passed a subject X as an input argument in the invocation.
    The base subject is the only subject that can "detect" it, when a knowledge fact becomes true. Normally the system can also detect it, except if it is private knowledge. Private knowledge will be explained later i n the behavior part.
    
    
  • Behavior predicates correspond to relations that express the intention of a subject towards the system and towards other subjects. The base subject of a behavior fact is the subject who's behavior is expressed by the fact.
  
  The following simple rules sum it up:
  • The right of an entity to change the state of the system in a certain way, is a knowledge predicate.
  • The right of an entity to interact (collaborate) with another entity in a certain way, is also a knowledge predicate.
  • The internal state of an entity is also a knowledge predicate.
  • The possibility of an entity performing an action (eg: invoking another entity with a certain input argument) is a behavior predicate.
  • The possibility of an entity cooperating in an action (eg: being invoked with a certain input argument, or returning an output argument) is a behavior predicate.
  
  
• Rules Rules in SCOLL are a mechanism to derive new facts from existing facts.
  Rules are separated with a ';'. Every rule has the form of a Horn clause:

  P Q ... => R ;

  P ... R are predicates over a finite number of variables.
  Predicate labels start with a lower case letter, variables with an upper case letter, like this:

  accessTo(From To)

  access(A B)

  The left hand side of the rule is called its body, the right hand side is its head
  The body can be empty, the head always consist of exactly one predicate.

  For instance, this could be a simple system rule:
  access(A B) access(B C) isTransparent(B) => access(A C)

  During the execution of a SCOLL program, the rules will be instantiated: all variables will be substituted for actual subjects.
  The body of every instantiated rule then represents a conjunction (AND) of the facts . An instantiated rule is a simple logical implication: the head will become true if all facts in the body are true.

  SCOLL rules never rely on the identity of subjects. Though many programming languages provide some form of instant identification (like an object equality test), SCOLL requires that the use of such a facility would be modeled explicitly . Therefor SCOLL never allows constant arguments (only variables) in the predicates of the rules.

  Counter example :
  access(A alice) => access(alice A)	invalid syntax
  Good example:
  isAlice(X) access(A X) => access(X A)

  In the future we may provide the special predicates ==(X Y) and \=(X Y) for this purpose, and allow the use of constants in these predicates only.

Describing SCOLL Patterns

The five parts of a SCOLL program:

1. The "system" part :

   The system part consists of a list of system rules that each model the preconditions (body) for an (inter-) action of a certain type to happen, and the effects (head) the (inter-) action will have.
   The body of a system rule can contain knowledge predicates as well as behavior predicates, but its head is always a knowledge predicate. In fact, this is how SCOLL can tell the difference: if the predicate is used in the head of a system rule, it is a knowledge predicate. If it is used in the body of a system rule, but not in any head, it is a behavior predicate, that has to be derived somewhere in the behavior part of the program.

   Thus, system rules create knowledge from behavior and/or knowledge.

   Example 1 :
   sees(A B) likes(A B) isReceptive(B) => sees(B A);
   sees(A B) likes(A B) isReceptive(B) => isSeenBy(A B);

   In these system rules, sees/2 and seesMe/2 are knowledge predicates (they occur on the right hand side). Note that sees(B A) is B's knowledge that the collaboration succeeded while isSeenBy(A B) is A's knowledge of it. Probably likes/2 and isReceptive/1 are behavior predicates, but we can only be sure of that after we have examined all the remaining rules in the system part.
   

   Example 2 :
   access(A B) access(A X) givesTo(A B X) receives(B) => hasGiven(A B X);
   access(A B) access(A X) givesTo(A B X) receives(B) => hasReceived(B X);
   access(A B) access(A X) givesTo(A B X) receives(B) => access(B X);

   A's knowledge hasGiven(A B X) lets A be aware of its successful collaboration with B, and of the fact that B now has access to X.
   B's knowledge hasReceived(B X) is a refinement of its knowledge access(B X), telling B something about how it got access to X. Note that, in this example, B is not told whom it got the access from. The example models invocation (of B by A) with an input argument (X) in systems that do not reveal the invoker.
   A and B can use their new knowledge to differentiate their behavior towards the subjects they have access to, as is explained in the next part.
   The knowledge access(B X) is generated for subsequent use by the same system rules.

   Multiple (sub-) systems
   Currently, only one set of systems rules can be provided.
   If SCOLLAR is to be used in interoperation mode, all the subsystems will use the same rules. If that is not suitable for your purposes, we suggest using different knowledge predicates for every subsystem.

2. The "behavior" part :

   The behavior part consists of a list zero or more behavior classes. A behavior class consists of a name and a list of zero or more subject rules, and has this form:
   

   <NAME> { <rule> <rule> ... <rule> }

   The subject rules have the same format as the system rules: they are simple Horn clauses having zero or more knowledge predicates in their body (left hand side) and exactly one predicate in their head.

   For instance, here is a simple behavior class, corresponding to example 2 above:
   RECEPTIVE { => receives()}
   Notice that the predicate receives() has one less argument than it has in the system rules of example 2. The base subject is always dropped in subject rules, for reasons which will be explained soon.

   Subject rules are a monotonic approximation of how subjects of a certain behavior class decide under what circumstances they want to collaborate in what way. The head of a subject rule is usually a behavior predicate, but it can also be a private knowledge predicate.

   Private knowledge is knowledge that is generated by the base subject and therefor available only to the subject itself, not to the system. Private knowledge is useful for concisely representing combinations of non-private knowledge the subject has learned during interactions, or to represent the subject's internal "state".

   IMPORTANT: Subject rules should of course only use knowledge that is available to the subject itself, and generate behavior (or private knowledge) for the subject itself. Instead of demanding that every predicate in a subject rule should have the same base-subject variable, we simply drop the first argument in the predicate (make it implicit)! The reason for making the base-subject implicit is not just simplification. To understand the importance of it, consider the following counter example of a subject rule in which the first argument is explicit:

   Counter example subject rule :
   => likes(A A);

   This rule would mean that every subject of this behavior class likes itself. Using this rule makes the following implicit assumptions :

   1. The real system that is being modelled in SCOLL, provides and infallible identification facility that allows every subject (or at least every subject of this behavior class), to differentiate between itself and other subjects.
   2. The subjects modeled in this behavior always (!) use this identification before making any decision.
   These assumptions are very strong and do not hold in most cases, particularly the second one.
   If the first assumption does hold, it should be expressed explicitly in the system rules, for instance by a system rule like :  => self(A A);
   If the second assumption also holds, the use of the identification knowledge in a subject rule should be explicit, for instance: self(A) => likes(A);

   Example of a behavior:
   

   FORWARDER{	=> receives();
   	hasReceived(X) => givesTo(A X);}

   FORWARDER is the behavior for subjects that are willing to receive subjects, and forward them to all other subjects. The example assumes that hasReceived/2 is a knowledge predicate, while receives/1 and givesTo/2 are behavior predicates.

   DEFAULT behavior
   If the name of a behavior class is "DEFAULT", all subjects in the subject part that have behavior assigned explicitly, will have this behavior.
   If the behavior class DEFAULT is not specified, the default behavior is defined as the empty set:
   DEFAULT {}

3. The "subject" part :

   The subject part is a list of structured records, each representing a subject of the form:

   <subjectName> : <BEHAVIORNAME> { <fact> <fact> <fact> ...}

   or, if the subject has DEFAULT behavior:

   <subjectName>

   Subject start with a lower case letter.
   The subjectName identifies the subject, the behaviorName identifies its subject rules.
   The facts are private knowledge facts that will be set to true, to initialize the subject's behavior.
   Just like in the subject rules, these facts have an implicit base subject.

   search option
   The keyword search can precede the subject name, to indicate that SCOLLAR should maximize the behavior of this subject, using the given behavior as a lower bound. Every individual atomic fact of the subject's behavior will be considered a target. These behavior targets are derived from the behavior predicates, which are defined by the system rules in the system part.
   For convenience, search can be replaced by a simple question mark (?).

   Example :
   

   alice : FORWARDER {	isSelf(alice)
   	mustForwardTo(bob)}
   bob : COMPLEXBEHAVIOR {}
   search carol

   In this example, subject alice is given initial knowledge about who she is and whom she is supposed to forward to. This private knowledge will only "mean" something if the FORWARDER behavior uses it in its subject rules to, directly or indirectly, derive behavior facts from it.

   Subject carol is preceded by with the "search" flag. That indicates that SCOLLAR should find solutions that maximize carol's behavior (in excess of carol's DEFAULT behavior) while respecting the safety and liveness constraints in the config part.

   Interoperation

   • The subject part of a SCOLL program is also the place where:
     • subsystems are declared
     • subjects are assigned to them
     A subsystem is a group of subjects, enclosed within curly brackets, and preceded by the name of the subsystem.
     If subsystems are present, SCOLLAR will automatically switch to interoperation mode, when searching for solutions.
     For instance:
     s1{?a ?b ?c ?d ?e}
     s2{?a ?b ?d ?f ?g}
     s3{?c ?f ?g ?h ?i}
     In this example, s1, s2 and s3 are subsystems, each containing a list of search subjects.
     SCOLLAR will first calculate the maximal fixpoint for each subsystem separately, and consider all unreachable knowledge in any of them as forbidden (safety properties) in the global system (the union).
     
     
   • A subject can have only one behavior, and that behavior has to be repeated in every subsystem of which it is part. This is a temporal restriction in SCOLLAR. We will address this when the need arises.
     For now, if the behavior of a subject differs depending on the subsystem, we suggest introducing subsystem-specific predicates in the system and behavior parts.
   
   
   

4. The "config" part :

   The config part is a list of (non-private) knowledge facts that represent the initial configuration of the pattern. This is mostly used to set up the initial access graph or matrix.
   These facts have explicit base subjects.
   Note that knowledge facts in SCOLL are not restricted to binary predicates, and knowledge facts of different arity can be used here as well, to precisely describe the starting state of the system.

   Example :

   access(alice bob)

   hasSendTo(bob carol alice)

   isActivated(childOfAlice)

   
   search option
   Every configuration fact can be preceded by the search flag, that turns it into a target. SCOLLAR will search for solutions that maximally set these targets to true.

   Example :

   search access(alice bob)

   access(bob carol)

   For concise notation, when many configuration facts are optional, curly brackets can extend the scope of the search prefix like this:

   Example :

   search { access(alice bob) access(alice carol) }	/* targets */
   access(bob carol) access(alice alice)	/* facts */

   The search option in the config part can be used in combination with the search option in the subject part. SCOLLAR will search for solutions that maximally set all targets to true.

   Interoperation
   When subsystems are declared in the subject part, every fact and target in the config part should be qualified by a subsystem. This is done simply by specifying the subsystem as an extra first argument.
   For instance:
   access(s1 a bb) access(s1 b c)
   search{access(s2 b e) access(s2 e f)}
   
   

5. The "goal" part :

   The goal part is a list of:

   • knowledge facts that represent the liveness properties
   • negations of knowledge facts that represent the safety properties.
   
   Negation is indicated by a ! prefix. (Negation is not allowed in any other part.)
   When SCOLLAR is searching for solutions (in search mode or interoperation mode), it will only report solutions that comply with these goals.

   Example :

   !read(carol alice)	/* safety property */
   access(bob carol)	/* liveness property */

   SCOLLAR will search for solutions that guarantee that carol will never have read alice, while bob can get access to carol, at least if every subject always uses its maximal behavior.

   IMPORTANT:
   Remember that SCOLL programs do not model exact behavior, but safe (over-)approximations of behavior. Safety properties guaranteed in the approximation will be guaranteed in the real problem too. However, liveness properties cannot be guaranteed at all, since the modeled behavior will usually be a strict over-approximation of the actual behavior. The only reason we consider liveness properties, is to require a lower bond to the maximally possible generation of facts in the pattern.
   If SCOLLAR is to be used in interoperation mode, the goal part should contain only inter-subsystem goals. The intra-subsystem safety goals will be derived from the maximal fixpoints of the individual subsystems.

SCOLL Syntax

PredLabel or SubjectID cannot start with one of the following words:
"system", "behavior", "subject", "config", "goal", "search".

Using Scollar Online to Analyze Safety in Patterns of Collaborating Entities

SCOLLAR can be used in three operation modes:

1. To compute the maximal propagation of authority starting from a given configuration.
   This is a simple fixpoint calculation. The system rules and behavior rules are instantiated over de set of subjects, and applied to the initial configuration, until no new facts can be derived. Because the rules are monotonic, and the number of derivable facts is finite, such a fixpoint is always reached.

   The search predicates that are specified in the subject part and/or the config part, are

   • either completely disregarded : minimal fixpoint
   • or completely taken into account : maximal fixpoint.

   The result is shown on a separate page, containing a table for every subject, showing the reachable predicates as 1, and the unreachable predicates as either 0 or _. The difference between 0 and _ is implementation related, and only relevant for debugging purposes.

   The goal part is not taken into account when computing a fixpoint.
   However, the resulting tables do indicate the cells containing a safety predicate in red and the ones containing a liveness predicate in green.

   Subsystems are not taken into account: fixpoints are calculated on the merged system (the union of all subsystems).
   Any subsystem specific facts specified in the config part are "generalized" into facts of the merged system.

   Conclusions from fixpoint calculations:

   • If the maximal fixpoint is safe and alive (no red cells contain 1 while all green cells do), then there is only one trivial solution: the set of all search predicates. Consequently, the pattern is safe as it is, and no restrictions have to be applied.
   • If the maximal fixpoint is not live, there is no solution.
   • If the minimal fixpoint is not safe, there is no solution either.
   
   
2. To compute maximal sets of search predicates that provide a safe and live solution
   In this mode SCOLLAR will look for those subsets of the search predicates that are at the same time:
   • safe with respect to the safety properties in the goal part.
   • alive with respect to the liveness properties in the goal part.
   • maximal, in the sense that setting any other target to true will break safety.

   Every solution is presented as a minimal set of restrictions (disallowed targets), rather than as a maximal set of allowed targets.
   Every solution can be viewed individually as set of tables, one for every subject, indicating which facts are reachable from the proposed solution.

3. To compute safe reconfigurations for interoperating subsystems
   This mode is automatically chosen instead of the previous one, if one or more subsystems are specified in the subject part.

   The problem that is analysed here it the following:
   Consider several patterns (subsystems) that are assumed to be completely safe by themselves. Interoperation happens when a subject occurs in more than one subsystem: in the combined system, facts may very well become reachable, that are not reachable in a any subsystem. Of these facts, we consider only those that are about a set of subjects that is completely included in at least one subsystem: we say that that subsystem is "responsibe" for that fact. This does not mean that the fact's reachability is caused by the subsystem, but rather that its reachability can be prevented (managed) by restricting the subsystem.
   The problem of secure interoperation is:

   • Find (all) minimal sets of restrictions for the subsystems, that are necessary to avoid new facts becoming reachable by interoperation for which the subsystem is responsible.

   The goal part. of the pattern is now intended to contain only inter-system safety and liveness requirements for the interoperating system (the union of all subsystems): those for which no subsystem is responsible.

   In practice, this mode differs from the previous one only in that it automatically derives all intra-system safety requirements from the subsystems, and adds them to the safety requirements in the goal part, before calculating solutions to the complete (interoperating) system.

SCOLLAR's online user interface

• SCOLLAR calculations :
  
  • 
    This button starts a calculation in the first mode : to compute the set of all facts that are reachable from the configuration. This set corresonds to the maximal propagation of authority in the actual problem that was modelled as a SCOLL pattern.
    The search options (targets) specified in the subject part or in the config part are not considered to be part of the configuration.
    Subsystems are not taken into account: fixpoints are calculated on the merged system (the union of all subsystems).
    
    
  • 
    This button starts a calculation in the first mode >: to compute the set of all facts that are reachable from the configuration. This set corresonds to the maximal propagation of authority in the actual problem that was modelled as a SCOLL pattern.
    This time, the search options (targets) specified in the subject part and/or in the config part are considered to be part of the configuration.
    Subsystems are not taken into account: fixpoints are calculated on the merged system (the union of all subsystems).
    
    
  • 
    This button causes SCOLLAR to start calculating all solutions it can find in 30 seconds.
    When no subsystems are specified, this button starts a calculation in the second mode : to find those solutions that at the same time:
    • are safe with respect to the safety properties in the goal part.
    • are alive with respect to the liveness properties in the goal part.
    • maximize the targets: the behavior of the search subjects in the subject part, and the targets in the config part.
      
    Every solution will list a minimal set of restrictions: targets that need to prevented in the behavior of search subjects or in the configuration, to guarantee the goals.
    
    When subsystems are defined in the subject part, this button starts a calculation in the third mode.
    
    
  • 
    This button is similar to the previous one, but the calculation is stopped as soon as a first solution if found.
    
    
• Saved Patterns
  This part of the user interface allows the user to manage examples of complete patterns. You can only save patterns if your browser's cookies are enabled. The cookie we create is called "storageKey" and has a random value assigned to it. You can only delete the patterns you saved yourself. You cannot change or save predefined patterns, but if you try to, a personal (private) copy will be made of that pattern.
  The availability of the buttons in this section depends on the context and on whether you have cookies enabled in your browser.
  • choose empty (*) caretaker (*) my test caretaker minimal ...
    This menu button provides some instructive examples of complete SCOLL patterns.
    Choose "empty" to clear all fields of the input pattern.
    The patterns you saved while using your current cookie "storageKey" are also available, recognizable by the "(*)" prefix.
    You cannot use patterns you saved with another value of the "storageKey" cookie.
    I intend to fix this as soon as somebody expresses a need for it.
    
    
  • 
    This button allows you to save the current pattern under a different name.
    Use only alpha-numeric characters for the name of the pattern. Do not use "(*)" to indicate your private patterns, that information will be derived automatically.
    If you use the name of a pattern you saved previously, it will be overwritten without warning.
    If you use the name of a non-private pattern, your private copy will be overridden instead, or one will be created if it does not exist.
    
    
  • 
    This button allows you to save changes to the pattern you last loaded, under the same name.
    If the current pattern is not private, your private copy of it will be overridden instead, or one will be created if it does not exist.
    "<pattern name>" will contain the name of the pattern you last loaded.
    
    
  • 
    This button allows you to remove the pattern you last loaded.
    If the current pattern is not private, your private copy of it will be removed instead, or nothing will happen if it did not exist.
    "<pattern name>" will contain the name of the pattern you last loaded.
    
    
• Saved Systems
  This part of the user interface allows the user to manage examples of reusable system parts for patterns. You can only save systems if your browser's cookies are enabled. The cookie we create is called "storageKey" and has a random value assigned to it. The same cookie is used for saving complete patterns. You can only delete the systems you saved yourself. You cannot change or save predefined system examples, but if you try to, a personal (private) copy will be made of that system.
  The availability of the buttons in this section depends on the context and on whether you have cookies enabled in your browser.
  • choose empty (*) capabilities (*) my test capabilities transitivity ...
    This menu button provides some instructive examples of reusable system parts for SCOLL patterns.
    Choose "empty" to clear the system field of the input pattern.
    The Systems you saved while using your current cookie "storageKey" are also available, recognizable by the "(*)" prefix.
    You cannot use systems you saved with another value of the "storageKey" cookie.
    I intend to fix this as soon as somebody expresses a need for it.
    
    
  • 
    This button allows you to save the current system under a different name.
    Use only alpha-numeric characters for the name of the system. Do not use "(*)" to indicate your private systems, that information will be derived automatically.
    If you use the name of a system you saved previously, it will be overwritten without warning.
    If you use the name of a non-private system, your private copy will be overridden instead, or one will be created if it does not exist.
    
    
  • 
    This button allows you to save changes to the system you last loaded, under the same name.
    If the current system is not private, your private copy of it will be overridden instead, or one will be created if it does not exist.
    "<system name>" will contain the name of the system you last loaded.
    
    
  • 
    This button allows you to remove the system you last loaded.
    If the current system is not private, your private copy of it will be removed instead, or nothing will happen if it did not exist.
    "<system name>" will contain the name of the system you last loaded.
    
    

Definitions

Many of these definitions are based on :

• Paradigm Regained, a paper by Mark S. Miller and Jonathan S. Shapiro

• Behavior

  Fine grained safety analysis makes the distinction between an subject having a right and that subject being ready and able to exert this right. Many classical models [take-grant] [hru] express this distinction as a difference between active subjects and passive objects: a subject is able to exert every right it has, whereas an object can be relied upon to never exert any right it has. It is considered unimportant for safety analysis whether or not an object refrains from using its rights because out of its own will (refusal vs inability).

  The difference between active subjects and passive objects is one of behavior : the conditions in which a subject can be relied upon to not exert a certain right.

  There is another aspect of behavior that is relevant for collaborative systems: the conditions in which a subject A can be relied upon to not collaborate with an subject B that exerts a right on A. In most classical models [take-grant] [hru], the collaborative aspect of behavior is not explicitly considered.

  Behavior can be static and/or dynamic. Dynamic behavior is expressed in terms of the subject's environment, whereas static behavior is not. To model realistic and practical systems, dynamic behavior should be expressed in terms of the subject's own perception of its environment (what it can know about its environment). Knowledge-Behavior Systems formalize this concept. collaboration rights .

• Collaboration

  We use collaboration to mean interaction between two (or more) subjects whereby the behavior of either subject can reduce the effect of the interaction. For example, consider a subject Alice, having access to both Bob and Carol, and Alice wants to give Bob access to Carol. If Bob has no way to refuse such access, then what is modelled is no real collaboration, as the interaction is controlled by Alice only.

  On the other hand, if Bob can (in principle) refuse such access, then the interaction requires collaboration between Alice and Bob : both have to play along to enable the propagation of access, and Alice's access right to Bob gives her merely the right to collaborate with Bob.

• Collaborative Systems

  Collaborative Systems are systems that model collaboration rights .

• Purely Collaborative Systems

  Purely Collaborative Systems only model collaboration rights. Capability Systems, as defined in [Paradigm Regained,... ], are a fine example of Purely Collaborative Systems.

• Rights

  A Right represents the ability of a subject to directly influence the system (changing something that is considered relevant) on its own, without any collaboration being necessary.

• Collaboration Rights

  These rights, when exerted, have the effect of enabling (e.g. initiating) collaboration with a subject (subjects). The collaborating subject (subjects) is (are) thereby enabled to fully or partially cooperate (collaborate in a positive way) and thereby completely or partially bring about the envisioned actual effect(s) .

• Authority

  Authority represents the ability of a subject to directly or indirectly influence the system (changing some things that are considered relevant).

  A subject's authority depends not only on its own current set of rights, but also on the rights of other subjects, and on the rights that it (and other subjects) can acquire directly or indirectly.

  In many systems, rights are only propagated when rights are exerted (*). In these systems the subject's authority will depend not only on the distribution of rights in the system, but also on the behavior of the subjects in the system, and therefore possibly also on its own behavior.

  In collaborative systems, authority can be controlled partially by means of behavior. In purely collaborative systems, it becomes possible to completely control authority by means of behavior restrictions in trusted subjects.

  (*) HRU commands have preconditions on the existence of rights in the rights matrix. Take-grant systems have similar requirements regarding the availability of either a take or a grant right. The creation of new subjects is usually considered to be a universal right, the exertion of which is a matter of behavior: active subjects do it, passive objects do not.

• Patterns

  A pattern is a finite configuration of subjects, each with their own behavior, initial knowledge and initial (collaboration) rights, that evolves monotonically following the rules set by a coordinating system. Patterns are described in the declarative SCOLL language, for the SCOLLAR analysis tool to investigate if they are safe for a given set of safety properties while not necessarily preventing a given set of other properties.

• Knowledge Behavior Systems

• Safe Approximation

• Safety Properties

  The safety properties in a pattern are the properties of which SCOLLAR will, if possible, guarantee that they are not violated in any actual configuration of subjects that can be safely approximated by the pattern.

• "Liveness" Properties

  We use liveness properties to indicate properties of which SCOLLAR will guarantee, if possible, that there exist at least one actual system that is safely approximated by the pattern, and that will have the safety properties. This is not the usual definition of liveness properties. To calculate real liveness properties the pattern would have to approximate every subject behavior from below, which would in most cases lead to an unsafe approximation. If the SCOLLAR liveness properties are violated, they will be violated by any actual system safely approximated by the pattern, rendering the pattern useless for the purpose they indicate.