logo

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

Scoll is a tool-based approach to analyze safety in patterns of collaborating entities (subjects). The tool itself is called Scollar can be used in two ways:
  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:

    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.
Note that Scoll merges both kinds of restrictions into one set to be minimized because both types are usually inter-dependent: imposing a restriction of one kind may very well undo the need for a restriction of the other kind.

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

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

Program ::= Declare System BehaviorTypes Subjects Configuration Goals
Declare ::= "declare" StatePreds BehaviorPreds KnowledgePreds
StatePreds ::= "state:" PredDecl*
BehaviorPreds ::= "behavior:" PredDecl*
KnowledgePreds ::= "knowledge:" PredDecl*
PredDecl ::= PredLabel "/" Arity
PredLabel ::= ["a"-"z"] ["a"-"z " "A"-"Z" "0"-"9"]*
Arity ::= ["1"-"9"] ["0"-"9"]*
System ::= "system" Rule+
Rule ::= Pred* "=>" Pred (";")?;
Pred ::= PredLabel "(" VarID* ")"
VarID ::= ["A"-"Z"] ["a"-"z" "A"-"Z"]*
BehaviorTypes ::= "behavior" BehaviorType* (American English spelling)
BehaviorType ::= behaviorTypeID "{" Rule* "}"
BehaviorTypeID ::= ["A"-"Z" "_"]+
Subjects ::= "subject" (Subject)+
Subject ::= ("?" | "search") ? SubjectID ( ":" behaviorTypeID "{" Fact* "}")?;
SubjectID ::= ["a"-"z"] ["a"-"z " "A"-"Z" "0"-"9"]*
Configuration ::= "config" (Fact | SearchFact)*
Fact ::= PredLabel "(" SubjectID* ")"
SearchFact ::= ("?") Fact>
Goals ::= "goal" (SafetyRequirement | LivenessRequirement)*
SafetyRequirement ::= "!" Fact
LivenessRequirement ::= Fact

Syntax Remarks

Using Scollar

Definitions

Scoll's wish list:

  1. Improve performance and scalability
  2. Improve expressive power
  3. Improve usability
  4. Extend Application Domain