CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

Probabilistic Noninterference for Multi-threaded Programs

Andrei Sabelfeld (Institutionen för datavetenskap ; Institutionen för datavetenskap, ProSec) ; David Sands (Institutionen för datavetenskap ; Institutionen för datavetenskap, ProSec)
Proceedings of the 13th IEEE Computer Security Foundations Workshop p. 200-214. (2000)
[Konferensbidrag, refereegranskat]

A program which has access to your sensitive data presents a security threat. Does the program keep your secrets secret? To answer the question one must specify what it means for a program to be secure, and one may wish to verify the security specification before executing the program. We present a probability-sensitive security specification (probabilistic noninterference) for multi-threaded programs based on a probabilistic bisimulation. Some previous approaches to specifying confidentiality rely on a particular scheduler for executing program threads. This is unfortunate since scheduling policy is typically outside the language specification for multi-threaded languages. We describe how to generalise noninterference in order to define robust security with respect to any particular scheduler used and show, for a simple imperative language with dynamic thread creation, how the security condition satisfies compositionality properties which facilitates a straightforward proof of correctness of e.g. security type systems.



Denna post skapades 2006-09-28. Senast ändrad 2015-12-17.
CPL Pubid: 18076

 

Läs direkt!


Länk till annan sajt (kan kräva inloggning)


Institutioner (Chalmers)

Institutionen för datavetenskap (1993-2001)
Institutionen för datavetenskap, ProSec (2002-2004)

Ämnesområden

Datavetenskap (datalogi)

Chalmers infrastruktur