PASE

Aus SDQ-Wiki

-- work in progress --

Overview

Pase (PAlladio Security Extensions) are extensions to Palladio that allow for modelling and analysing data flow in PCM-models. PASE can be used in order to find trade-offs between confidentiality of a software architecture and other properties Palladio can simulate. Hereby, the confidentiality of a software-system depends on:

  • the architecture: How do the components of the system interact? Where are the components of the system deployed?
  • the adversary: What are the capabilities of the adversary? To which parts of the system does she have access to?
  • the usage profile(s): How do users interact with the system?

PASE allows for modelling these aspects by annotating the PCM-model.

PASE workflow

This model, then, can be transformed in an analysis model for ProVerif, a cryptographic protocol verifier. The analysis result, then, is fed back into Palladio.

PASE consists of:

  • extensions of the PCM that allow for modelling data flow
  • transformation of extended PCM-models into an analysis model
  • an analysis using ProVerif a cryptographic protocol verifier

Meta Model

PCM extensions

Overview

The following Image show an overview of the PASE extensions to the PCM

PASE-meta-main.png

These extension are mainly intended to model data flow and knowledge about data.

In order to model data flow specific elements in an PCM-model, we need to introduce annotations for signatures and resource containers. We also need to introduce a way to model the preliminary knowledge of users and components as well as the security properties of resource containers. In order to analyse the confidentiality, we introduce an adversary and a query that will be issued to the protocol verifier after transformation.

In the following, we describe the elements and how they relate to PCM-elements in detail.

Conditions

Users of part of the system may have prior knowledge. This can be modelled with Conditions. Conditions model knowledge of users and components before users interact with the system. A user for example knows its password for an application, and a database component knows the users data. This can be modeled with Conditions. The following image depicts how conditions relate do PCM-elements:

PASE-meta-conditions.png

A Condition refers to a PCM datatype and a Variable Characterisation. A UserPreCondition additionally refers to a UsageProfile, while a ComponentPreCondition refers to an AllocationContext. An AllocationContext can be seen as an allocated instance of a component.

Container

Some resource containers may intrinsically be more secure than others. Consider for example a server with strict surveillance and physical access control with a verified operating system. Such secure resource containers may be prone to attacks, and therefore do not leak information to an attacker. In PASE this can be modelled with the SecureContainer element. This element references a PCM RessourceContainer, as depicted in the following image:

PASE-meta-container.png

Signature

If a user uses a interface of the system, or a component calls another component, they exchange data. In PASE, this can be modelled at a signature level. Data can either flow to the called component, or to the calling component. PCM OperationSignatures are annotated with a InformationFlowSignature, which is either a InformationDisclosingSignature or a InformationRecievingSignature: PASE-meta-signatures.png

Adversary

Security is always considered with respect to an adversary. We model adversaries as entities with access to PCM RessourceContainers. Currently Adversaries are passive. For future work, Attackers already reference a PCM UsageScenario. This enables Attackers to use Signatures of the system and therefore participate in the protocol:

PASE-meta-attacker.png

Query

The query issued to the protocol verifier is modelled with the Query element. Currently only the KnowsVariableQuery is supported. As the Condition, it references a PCM DataType as well as a PCM VariableCharacterisation.

PASE-meta-query.png

Encrypted messages

Currently, we do not model encryption explicitly. This means, there are no elements in the meta model to model encryption. Instead, you can indicate that a variable x the encryption of the variable with the specification m under the key (also a variable) with the specification k by setting the variable specification of x to "m_k". The transformation recognizes and transforms this correctly.

Analysis Model

The analysis meta model is comprises of the following elements:

Basic elements are:

  • atoms
  • objects
  • actions
  • rules
  • declarations

Complex elements are:

  • terms
  • states
  • protocols

In the following, we describe how these elements relate.

atoms and terms

Every atom is a term. Terms represent messages. A term can be build recursively from other terms.

objects and actions

Objects interact with each other by using actions. An action may involve terms and can imply rules. For example is Alice uses a action that sends a message encrypted under a key and the key to bob, if there is a rule that models encryption, bob possesses the message.

declarations and states (and rules)

Declarations are statements about Objects and may involve terms. A state is a set of declarations and a fix point according to the application of rules. A rule describes how a set of declarations implies additional declarations. Consider for example a rule that models encryption. If in the current state, there are declarations that state, that Alice knows the terms m and k. The encryption rule states, that Alice also possesses the encryption of m under the key k.

states and actions

Actions map states to follow up sates.

actions and protocols

A set of actions is a protocol.


Concrete Syntax

The concrete syntax of our model is ProVerif code. ProVerif uses a syntax similar to first-order logic.

For a detailed explanation of the ProVerif syntax, please refer to the ProVerif Manual

We express terms and objects with literals, actions and declarations with formulas, and rules with horn clauses. Literals are bound variables. Actions and declarations contain literals, while rules have free variables.

Transformation

For the transformation from PCM models to analysis models, we use XPand. We map:

  • Users, the Adversary, Components, and RessouceContainers to objects
  • VariableCharacterisations to terms
  • UsageProfiles to protocols
  • Signatures to rules
  • Allocations and Preconditions to declarations

The transformation, however, does not map the elements above into an empty Instance of the analysis metamodel, but into a reference instance. This reference instance contains the following additional elements that are necessary for an analysis:

  • a declaration that models data knowledge: Conditions are mapped to this declaration
  • a declaration modelling containment relations: hierarcical relations between components as well as ressource containers and allocations of components to ressource containers are mapped to this declaration
  • a declaration for secure objects: The PASE Element SecureContainer is mappped to this declaration
  • rules for de- and encryption
  • rules for data-flow:
    • Unless an object O is secure, it leaks information to objects that contain O.
    • If an adversary has access to an Object, al terms the objects possesses are also known by the adversary.

Installation

In order to use PASE, you need:

  1. Installing ProVerif
  2. Install Palladio 3.4
  3. Install PASE Addon

Installing ProVerif

For instructions for installing ProVerif, a cryptographic protocol verifier, please refer to the ProVerif website.

Installing PASE

After having installed Palladio 3.4, install the PASE AddOn into your Palladio installation. Open Palladio, and use the Eclipse update site mechanism to specify the PASE 1.0 release update site:

http://sdqweb.ipd.kit.edu/eclipse/palladio/addons/security/releases/core_3.4/1.0/

Select the PASE feature, install it and restart Eclipse.

After restart, navigate to Window->Preferences. In the Preferences dialog, open the tab "PCM Security Analysis" and specify the system path of the ProVerif executable in the corresponding field. Save and close the dialog.

You can now start using PASE.

Example

The example described in the following is available in the PASE SVN repository using anonymous access at [1].

In order to demonstrate PASE, consider the following scenario: There are two File-Servers, Server1 and Server2. On each Server a StorageService is deployed. The following image depicts this deployment scenario:

PASE example allocation.png


Consequently the overall system consists of two components with the same Interfaces:

PASE example system.png


Additionally, there are two users, Alice and Bob. Before Interacting with the system, Alice knows a secret message m and a encryption key k. This is modelled as UserPreConditions in the security annotations. We do want to know if after Alices' and Bobs interaction, the adversary knows the secret message.This is modeled as a KnowsVariableQuery.

PASE example annnotations.png


The Usage scenario is as follows: First, Alice uploads a encryption of m under key k to Server1 and the key k to Server2. Then Bob downloads the encryption of m and key k and k. This is modelled in the following usage model:

PASE example usage.png


If the adversary has access to both server (see image below, element PCM server Accesses), the ProVerif analysis reports, that the query goal is achievable. The adversary knows the secret message m.

PASE example adversary.png

If on the other hand, the adversary only has access to one Server or we declare one server a secure, the adversary does not have sufficient information in order to get the secret message m. The ProVerif analysis does not find the goal.

Contact and Acknowledgements