CTIT University of Twente
Research Business & Innovation About CTIT Research Calls Looking for a job? Intranet

SlaLoM

Security by Logic for Multithreaded applications

Project Manager: Dr. Marieke Huisman

Faculty of Electrical Engineering, Mathematics and Computer Science

Tel.: +31 53 489 46 62

Email: Marieke.Huisman@ewi.utwente.nl

Project website:

Summary

This project develops a uniform verification framework for the protection of data. Key innovation on which the proposal is based is the notion of self-composition. This gives a different view on classical security properties, recasting them into safety properties of a single program, and allows reuse of existing program verification techniques. We believe that this approach can handle a wide range of data-related security properties, such as confidentiality, integrity and anonymity, in a uniform way, allowing easier comparison.  To make the framework usable for realistic applications, which interact with their environment, we concentrate on multithreaded applications, and properties that specify complete executions of an application.

In earlier work, we have shown feasibility of the approach by translating the confidentiality problem for multithreaded programs into a model checking problem. However, to make the approach scale, we propose to address the following topics:

1.

widening the scope of the studied security properties;

2.

development of a realistic program model, containing the main features of a multithreaded language like Java, including unbounded dynamic thread creation and termination;

3.

use of parametrised versions of temporal logic formalisms, to be able to express properties over infinite data domains;

4.

development of decision procedures for appropriate probabilistic properties;

5.

reuse and adaptation of existing tools for algorithmic verification; and

6.

definition of appropriate abstractions, to allow verification of infinite state space programs.

Project duration: 2009-2013

Project budget: 187 k-€

Number of person/years: 1.3 fte

Involved groups: Faculty of Electrical Engineering, Mathematics and Computer Science (EEMCS)