PUMA
Istituto di Informatica e Telematica     
Martinelli F. Real Time Information Flow Analysis. In: IEEE JOURNAL ON SELECTED AREAS IN COMMUNICATIONS (06406J0), vol. 21/1 pp. 50 - 59. IEEE, 2003.
 
 
Abstract
(English)
In previous work, we have studied some non-interference properties for information flow analysis in computer systems on classic (possibilistic) labeled transition systems. In this paper, some of these properties, notably BNDC, are reformulated in a real-time setting. This is done by first enhancing the Security Process Algebra with some extra constructs to model real-time systems (in a discrete time setting), and then by studying the natural extension of these properties in this enriched setting. We prove essentially the same results known for the untimed case: ordering relation among properties, compositionality aspects, partial model checking techniques. Finally, we illustrate the approach through two case studies, where in both cases the untimed specification is secure, while the timed specification may show up interesting timing covert channels.
Subject Bisimulation
information flow security
k.5


Icona documento 1) Download Document PDF


Icona documento Open access Icona documento Restricted Icona documento Private

 


Per ulteriori informazioni, contattare: Librarian http://puma.isti.cnr.it

Valid HTML 4.0 Transitional