Global requirements on effects are translated into local
restrictions on causes:
Requirements about the effects that should be unreachable in a
complex pattern of interacting entities are transformed into
restritions on the behavior of the entities and on the initial
configuration. It is up to the user to define which safety
requirements should be guaranteed, what entities can have their
behavior restricted, and what initial conditions are optional.
Liveness requirements are taken into account too, to avoid overly
restrictive solutions that make them impossible to meet.
Permission usage and security state are equally important
for authority propagation:
Authority propagation is not just a matter of what permissions
become reachable from an initial configuration, but should also
take the use-behavior of the subjects into account: who is willing
to use what permissions in what circumstances.
Both aspects can be specified with equally expressive power in
Scoll.
Behavior is based on knowledge:
Behavior is the intention of a subject to do something. A subject
can use its knowledge (about itself and other subjects) to decide
to be more active or 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.
Subject interaction is mediated explicitly by system
rules:
The rules that decide what conditions lead to what effects are
modeled by the user as system rules.
Conservative but sufficiently 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 a 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.
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 subject behavior can also be expressed
with improved precision.
What is not so good about Scoll ?
Scoll's current analysis tool (called Scollar) is still too slow and not
scalable enough. It is based on constraint programming (CP), which
is a good thing, but it does not yet fully exploit the advantages
of CP to dramatically shrink the search space. There are many
opportunities for improvement however. So there is work to be done
here, before Scoll can become a mature tool for security analysis.
