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. As an application, we study a system with covert channels that we are able to discover by our techniques.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
A. Aldini, M. Bravetti, R. Gorrieri: A Process-algebraic Approach for the Analysis of Probabilistic Non-interference. Journal of Computer Security, to appear.
R. Alur, C. Courcoubetis, D. L. Dill: Verifying Automata Specifications of Probabilistic Real-Time Systems. Real-Time: Theory in Practice, Springer LNCS 600, 28–44, 1992.
R. Alur, D.L. Dill: A Theory of Timed Automata. Theoretical Computer Science 126:183–235, 1994.
C. Baier, H. Hermanns: Weak Bisimulation for Fully Probabilistic Processes. Proc. of CAV'97, Springer LNCS 1254, 119–130, 1997.
R. Barbuti, L. Tesei: A Decidable Notion of Timed Non-interference. Fundamenta Informaticae, 54(2–3): 137–150, 2003.
D. Beauquier: On Probabilistic Timed Automata. Theoretical Computer Science, 292:65–84, 2003.
N. Evans, S. Schneider: Analysing Time Dependent Security Properties in CSP Using PVS. Proc. of Symp. on Research in Computer Security, Springer LNCS 1895, 222–237, 2000.
R. Focardi, R. Gorrieri: A Classification of Security Properties. Journal of Computer Security, 3(1):5–33, 1995.
R. Focardi, R. Gorrieri, F. Martinelli: Information Flow Analysis in a Discrete-Time Process Algebra. Proc. of 13th CSFW, IEEE CS Press, 170–184, 2000.
J. A. Goguen, J. Meseguer: Security Policy and Security Models. Proc. of Symp. on Research in Security and Privacy, IEEE CS Press, 11–20, 1982.
J. W. Gray III. Toward a Mathematical Foundation for Information Flow Security. Journal of Computer Security, 1:255–294, 1992.
P. R. Halmos: Measure Theory. Springer-Verlag, 1950.
M. Kwiatkowska, G. Norman, R. Segala, J. Sproston: Automatic Verification of Real-time Systems with Discrete Probability Distribution. Theoretical Computer Science, 282:101–150, 2002.
M. Kwiatkowska, R. Norman, J. Sproston: Symbolic Model Checking of Probabilistic Timed Automata Using Backwards Reachability. Tech. rep. CSR-03-10, University of Birmingham, 2003.
R. Lanotte, A. Maggiolo-Schettini, A. Troina: Weak Bisimulation for Probabilistic Timed Automata and Applications to Security. Proc. of SEFM'03, IEEE CS Press, 34–43, 2003.
D. McCullough: Noninterference and the Composability of Security Properties. Proc. of Symp. on Research in Security and Privacy, IEEE CS Press, 177–186, 1988.
J. K. Millen: Hookup Security for Synchronous Machines. Proc. of 3rd CSFW, IEEE CS Press, 84–90, 1990.
R. Milner: Communication and Concurrency. Prentice Hall, 1989.
J. T. Wittbold, D. M. Johnson: Information Flow in Nondeterministic Systems. Proc. of Symp. on Research in Security and Privacy, IEEE CS Press, 144–161, 1990.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 International Federation for Information Processing
About this paper
Cite this paper
Lanotte, R., Maggiolo-Schettini, A., Troina, A. (2005). Information Flow Analysis for Probabilistic Timed Automata. In: Dimitrakos, T., Martinelli, F. (eds) Formal Aspects in Security and Trust. IFIP WCC TC1 2004. IFIP International Federation for Information Processing, vol 173. Springer, Boston, MA. https://doi.org/10.1007/0-387-24098-5_2
Download citation
DOI: https://doi.org/10.1007/0-387-24098-5_2
Publisher Name: Springer, Boston, MA
Print ISBN: 978-0-387-24050-3
Online ISBN: 978-0-387-24098-5
eBook Packages: Computer ScienceComputer Science (R0)