Scoll & Scollar Analyzing Safety in Patterns of Collaborating Entities

Last updated : 19 October 2008 by Fred Spiessens
Status: incomplete but up-to-date.
This document should have been completed by the end of October 2008. I'm sorry I still had no time to finish it.

Overview

1. To check if a given pattern guarantees a set of safety requirements without necessarily preventing another set of liveness requirements
   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 solutions (set of restrictions) is minimal for safety: adding a restriction is not necessary, removing a restriction will break at least one safety property.

   The user has to indicate what restrictions can be imposed. Typically, the imposable restrictions affect the behavior of the subjects the user can program or control himself and/or some parts of the initial configuration (eg: some the initial access rights).
   Using Scollar in this way is useful when designing and programming secure patterns of interaction between some trusted (relied upon) and some untrusted (unknown) subjects.

What restrictions can Scoll reason about ?
When searching for minimal sets of restrictions, the tool will - at least in principle - try 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 a "?" in the "subject" part of the pattern description.
   Scollar will try to maximize the behavior of all search subjects. In other words: Scollar searches for minimal sets of restrictions.
   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.

What is so special about Scoll?

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 can be both a prerequisite for and a result of succeeded interaction.
   Subjects have a set of behavior rules that generate their behavior from their knowledge.
   A detailed explanation of these terms can be found further on.
3. Subject interaction is mediated explicitly by a system rules:
   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 behavior rules, are parametrized by subject variables.
   The protections system, by it rules, decides what conditions can cause what state transitions, and what knowledge becomes available to the subjects in these conditions. If a system rule is conditional in the behavior of at least two subjects, we call it a collaboration rule.
4. Conservative 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.
   Scoll models the maximal behavior of the entities, and aggregates the entities into a finite set of subjects. Scoll models are conservative and computable approximation of an actual problem.
   But 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 canAccess(Subject1, Subject2) could specify how this access was achieved : receivedFrom(Subject1, Subject3, Subject2). This is refined knowledge that tells Subject1 that it has successfully invoked Subject3, and got access to Subject2 as a return value from the invocation.

Scoll Concepts

• 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 as the relation.
  • 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.
    Predicate labels and constant subjecgts start with a lower case letter, variables with an upper case letter.
    Exceptions:
    • behavior and knowledge predicates have their first argument in front of the predicate, to stress that this arguments indicates the subject that has the behavior / knowledge.
      e.g.: A: <behaviorLabel>(B, ..., X)
    • in behavior rules, the first argument is implicit (the one who's behavior is described by the rule. Therefor it is dropped.
      e.g. in A's behavior rules: <behaviorLabel>(B, ..., X)
  • We call an instantiated predicate a fact.
    For instance access(alicem, bob) is a fact. If it is true, it means that alice stands in the relation access to bob.
    
• State, Knowledge and Behavior predicates
  We distinguish between three kinds of predicates:
  • State predicates correspond to relations that are part of the security state of the system.
    For instance, the predicate access(A,B) could be used to indicate that subject A has access to subject B.
    
  • Behavior predicates correspond to relations that express the intention of a subject towards the system and towards other subjects.
    For instance, the predicate A:may.sendTo(B,X) could be used to indicate A's intention to invoke B and pass subject X as an input argument in the invocation.
  • Knowledge predicates correspond to relations that are part of the internal state of a subject .
    For instance, the predicate A:did.sendTo(B,X) could be used to indicate A's knowledge that it has succesfully invoked subject B and passed subject X as an input argument in the invocation.
    
  The following guidelines can help when modeling a software pattern in Scoll:
  • The permission of an entity to change the state of the system in a certain way, is a state predicate.
  • The permission of an entity to interact (collaborate) with another entity in a certain way, is also a state predicate.
  • The effects of the (inter-)actions of the entities that are important for security are also state predicates. These effects do not necessarily corresopond to a state in the modeled system. It could for instance be an effect that is only visible in the history of a system.
  • The internal state of an entity is 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 derive new facts from existing facts.
  Every rule has the form of a logical implication from predicates and ends with ';'.
  For example P Q ... => R T; where P, Q, ...,S, T are predicates
  

  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 at least one predicate.

  For instance, this could be a simple system rule:
  access(A,B) access(B,C) isActive(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: all predicates in the head will become true as soon as all facts in the body are true.

  Scoll requires that the ability to identify entities is modeled explicitly when relevant. Therefor Scoll rules can have only variables in their predicates.

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

  In the future Scoll may relax this restriction. For instance Scoll could provide the special predicates ==(X Y) and \=(X Y) for this purpose, and allow the use of constants in these predicates only.

The structure of Scoll programs (patterns).

A Scoll program has 6 parts:

1. The "declare" part :

2. The "system" part :

3. The "behavior" part :

4. The "subject" part :

5. The "config" part :

6. The "goal" part :

Scoll Syntax

Syntax Remarks

• Arbitrary spacing is allowed before and after every syntax element.
  Spacing ::= All white space and everything between the comment signs "/*" and "*/". (No nested comments though)
• PredLabel and SubjectID cannot start with one of the following reserved words:
  "declare","system", "behavior", "subject", "config", "goal", "search".
  
  

Using Scollar

Definitions

Scoll's wish list:

1. Improve performance and scalability
   • Complex patterns with high arity predicates and large patterns with many subjects take a long time to calculate. There are many opportunities to improve the constraints and to enforce extra constraints derived from a simple analysis of the pattern.
2. Improve expressive power
   • Provide explicit support for creation of subjects.
   • Provide support for the propagation of data, instead of modeling data as passive subjects.
   • Allow arbitrary complex liveness and safety requirements (constraints rather than simple predicates).
3. Improve usability
   • Provide support for computer assisted modeling of Scoll patterns, for instance for mapping code.
   • Improve the documentation, provide a rich example set of useful and interesting patterns.
   • Generate, visualize and manipulate rich graphs, derived from the predicates in the configurations, the solutions, and the fixpoints.
4. Extend Application Domain
   • Provide support for calculating minimal behavior requirements (maximal sets of restrictions) for use in trust management problems that concern reachability.
   • Generalize Scoll into a general programming language: extending prolog with constraints and dataset programming with the ability to calculate boundaries on causes for given restrictions to effects.