In multilevel systems it is important to avoid unwanted indirect information flow from higher levels to lower levels, namely the so called covert channels. Initial studies of information flow analysis were performed by abstracting away from time and probability. Recently, work has been done in order to consider also aspects either of time or of probability, but not both. In this paper we propose a general framework, based on Probabilistic Timed Automata, where both probabilistic and timing covert channels can be studied. We define properties that allow one to express information flow in a timed and probabilistic setting. As an application, we study a system with covert channels that we are able to discover by applying our techniques.

Information Flow Analysis for Probabilistic Timed Automata

LANOTTE, RUGGERO;
2004-01-01

Abstract

In multilevel systems it is important to avoid unwanted indirect information flow from higher levels to lower levels, namely the so called covert channels. Initial studies of information flow analysis were performed by abstracting away from time and probability. Recently, work has been done in order to consider also aspects either of time or of probability, but not both. In this paper we propose a general framework, based on Probabilistic Timed Automata, where both probabilistic and timing covert channels can be studied. We define properties that allow one to express information flow in a timed and probabilistic setting. As an application, we study a system with covert channels that we are able to discover by applying our techniques.
2004
Theodosis Dimitrakos, Fabio Martinelli (Eds)
Formal Aspects in Security and Trust
0387240500
Formal Aspects in Security and Trust 2004
Toulouse, France
August 22-27, 2004
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11383/1789316
 Attenzione

L'Ateneo sottopone a validazione solo i file PDF allegati

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? 1
social impact