Welcome to the Scoll project

What is Scoll?

Scoll is a tool-based approach to help design and develop secure programs. It involves:

Download release 1.1.0 of Scollar: scollar_v_1_1_0.zip

  • Installation instructions are included in the README AND LICENCES file
  • Note the different open source licenses for the Oz part (MIT Licence) and the Java/Swing frontend part (GPLv3)
  • Some examples are included in the "scoll patterns" subdirectory
  • Release History

    What is so special about Scoll ?

    Scoll's most important features are:
    1. 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.
    2. 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.
    3. 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.
    4. 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.
    5. 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.

    Online Documentation

    Papers on Scoll