Posted by: Andy Tickner | 23rd August 2011

SERSCIS Access Modeller

The SERSCIS Access Modeller (SAM) takes a model of a system (e.g. a set of objects within a computer program or a set of machines on a network) and attempts to verify certain security properties about the system, by exploring all the ways access can propagate through the system.

It is designed to handle dynamic systems (e.g. systems containing factories which may create new objects at runtime) and systems where behaviour of some of the objects is unknown or not trusted.

Once you have a model that meets the goals, it should tell you:

  • what behaviours must be ensured for components you own
  • what behaviours you require of other parties you rely on

Behaviours are defined using a simple Java-like syntax. For example, a simplified ground handler could be modelled as:

class GroundHandler {
    private Object myCatering;

    public GroundHandler(RampService catering) {
        myCatering = catering;
    }

    public GHTask doTurnaround(AcispTask flights) {
        GHTask ghTask = new GHTask(flights, myCatering);
        ghTask.doTurnaround();
        return ghTask;
    }
}

SAM converts this into a set of Datalog rules (e.g. “if a GroundHandler’s doTurnaround method may be called with some argument X then a GHTask may be created and it may get access to X”).

Evaluating these rules and the initial configuration gives an upper bound on the possible behaviours of the real system (if something does not happen in the model, and the model is an over-approximation of the real system, then it cannot happen in the real system either).

Untrusted entities can be modelled using the Unknown behaviour. These will perform any action that they can. For example, the screenshot below shows a model containing a ground handler that behaves as defined above (“ghMe”, representing the ground handler doing the modelling), and a group of ground handlers (“ghOthers”, shown in red), representing competing ground handlers. Here, SAM has detected a flaw in the access control policy of the ramp service, which may allow other ground handlers access to this one’s tasks:

Detecting access problems with SAM

Detecting access problems with SAM

For more documentation and installation instructions, see http://www.serscis.eu/sam/.


Categories