Information Flow Security for Stochastic Processes

Jane Hillston, Andrea Marin, Carla Piazza, Sabina Rossi

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

In this paper we study an information flow security property for systems specified as terms of a quantitative process algebra, namely Performance Evaluation Process Algebra (PEPA). Intuitively, we propose a quantitative extension of the Non Interference property used to secure systems from the functional point view by assuming that the observers are able to measure also the timing properties of the system, e.g., the response time or the throughput.
We introduce the notion of Persistent Stochastic Non-Interference (PSNI) and provide two characterizations of it: one based on a bisimulation-like equivalence relation inducing a lumping on the underlying Markov chain, and another one based on unwinding conditions which demand properties of individual actions. These two different characterizations naturally lead to efficient methods for the verification and construction of secure systems. A decision algorithm for PSNI is presented and an application of PSNI to a queueing system is discussed.
Original languageEnglish
Title of host publication15th European Performance Engineering Workshop
Place of PublicationParis, France
PublisherSpringer, Cham
Number of pages15
ISBN (Electronic)978-3-030-02227-3
ISBN (Print)978-3-030-02226-6
DOIs
Publication statusPublished - 3 Oct 2018
Event15th European Performance Engineering Workshop - Paris, France
Duration: 29 Oct 201830 Oct 2018
http://epew2018.lacl.fr/

Publication series

NameLecture Notes in Computer Science
PublisherSpringer, Cham
Volume11178
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349
NameProgramming and Software Engineering
Volume11178

Conference

Conference15th European Performance Engineering Workshop
Abbreviated titleEPEW 2018
CountryFrance
CityParis
Period29/10/1830/10/18
Internet address

Fingerprint

Dive into the research topics of 'Information Flow Security for Stochastic Processes'. Together they form a unique fingerprint.

Cite this