Subscribe

Issue No.05 - September/October (2010 vol.36)

pp: 719-734

Ruggero Lanotte , Università dell'Insubria, Como

Andrea Maggiolo-Schettini , Università di Pisa, Pisa

Angelo Troina , Università di Torino, Torino

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TSE.2010.4

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. It is already known that systems that are proven to be secure in a possibilistic framework may turn out to be insecure when time or probability is considered. 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 a Noninterference security property and a Nondeducibility on Composition security property, which allow expressing information flow in a timed and probabilistic setting. We then compare these properties with analogous ones defined in contexts where either time or probability or neither of them are taken into account. This permits a classification of the properties depending on their discerning power. As an application, we study a system with covert channels that we are able to discover by applying our techniques.

INDEX TERMS

Probabilistic timed automata, multilevel security, information flow analysis, weak bisimulation.

CITATION

Ruggero Lanotte, Andrea Maggiolo-Schettini, Angelo Troina, "Time and Probability-Based Information Flow Analysis",

*IEEE Transactions on Software Engineering*, vol.36, no. 5, pp. 719-734, September/October 2010, doi:10.1109/TSE.2010.4REFERENCES

- [1] J. Agat, "Transforming Out Timing Leaks,"
Proc. Symp. Principles of Programming Languages, pp. 40-53, 2000.- [2] A. Aldini, M. Bravetti, and R. Gorrieri, "A Process-Algebraic Approach for the Analysis of Probabilistic Non Interference,"
J. Computer Security, vol. 12, pp. 191-245, 2004.- [3] A. Aldini and A. Di Pierro, "Estimating the Maximum Information Leakage,"
Int'l J. Information Security, vol. 7, pp. 219-242, 2008.- [4] R. Alur, C. Courcoubetis, and D.L. Dill, "Verifying Automata Specifications of Probabilistic Real-Time Systems,"
Proc. Workshop Real-Time: Theory in Practice, pp. 28-44, 1992.- [5] R. Alur and D.L. Dill, "A Theory of Timed Automata,"
Theoretical Computer Science, vol. 126, pp. 183-235, 1994.- [6] C. Baier and H. Hermanns, "Weak Bisimulation for Fully Probabilistic Processes,"
Proc. Int'l Conf. Computer Aided Verification, pp. 119-130, 1997.- [7] R. Barbuti and L. Tesei, "A Decidable Notion of Timed Non-Interference,"
Fundamenta Informaticae, vol. 54, pp. 137-150, 2003.- [8] D. Beauquier, "On Probabilistic Timed Automata,"
Theoretical Computer Science, vol. 292, pp. 65-84, 2003.- [9] R.E. Bellman,
Dynamic Programming. Princeton Univ. Press, 1957.- [10] M. Boreale, "Quantifying Information Leakage in Process Calculi,"
Information and Computation, vol. 207, pp. 699-725, 2009.- [11] P. Bouyer, "Timed Automata May Cause Some Troubles," BRICS Research Report RS-02-35, 2002.
- [12] F. van Breugel and J. Worrel, "Towards Quantitative Verification of Probabilistic Systems (Extended Abstract),"
Proc. Int'l Colloquium Automata, Languages, and Programming, pp. 421-432, 2001.- [13] S. Cattani and R. Segala, "Decision Algorithm for Probabilistic Bisimulation,"
Proc. Int'l Conf. Concurrency Theory, pp. 371-385, 2002.- [14] K. Cerans, "Decidability of Bisimulation Equivalences for Parallel Timer Processes,"
Proc. Int'l Conf. Computer Aided Verification, pp. 302-315, 1992.- [15] D. Clark, S. Hunt, and P. Malacaria, "Quantitative Information Flow, Relations and Polymorphic Types,"
J. Logic and Computation, vol. 18, pp. 181-199, 2005.- [16] K. Chatzikokolakis, G. Norman, and D. Parker, "Bisimulation for Demonic Schedulers,"
Proc. Int'l Conf. Foundations of Software Science and Computational Structures, pp. 318-332, 2009.- [17] K. Chatzikokolakis and C. Palamidessi, "Making Random Choices Invisible to the Scheduler,"
Proc. Int'l Conf. Concurrency Theory, pp. 42-58, 2007.- [18] D. Chaum, "The Dining Cryptographers Problem: Unconditional Sender and Recipient Untraceability,"
J. Cryptology, vol. 1, pp. 65-75, 1988.- [19] J. Desharnais, V. Gupta, R. Jagadeesan, and P. Panangaden, "The Metric Analogue of Weak Bisimulation for Probabilistic Processes,"
Proc. Ann. IEEE Symp. Logic in Computer Science, 2002.- [20] A. Di Pierro, C. Hankin, I. Siveroni, and H. Wiklicky, "Tempus Fugit: How to Plug It,"
J. Logic and Algebraic Programming, vol. 72, pp. 173-190, 2007.- [21] A. Di Pierro, C. Hankin, and H. Wiklicky, "Quantitative Relations and Approximate Process Equivalences,"
Proc. Int'l Conf. Concurrency Theory, pp. 508-522, 2003.- [22] A. Di Pierro, C. Hankin, and H. Wiklicky, "Approximate Non Interference,"
J. Computer Security, vol. 12, pp. 37-82, 2004.- [23] A. Di Pierro, C. Hankin, and H. Wiklicky, "Measuring the Confinement of Probabilistic Systems,"
Theoretical Computer Science, vol. 340, pp. 3-56, 2005.- [24] A. Di Pierro, C. Hankin, and H. Wiklicky, "Quantifying Timing Leaks and Cost Optimisation,"
Proc. Int'l Conf. Information and Comm. Security, pp. 81-96, 2008.- [25] N. Evans and S. Schneider, "Analysing Time Dependent Security Properties in CSP Using PVS,"
Proc. Symp. Research in Computer Security, pp. 222-237, 2000.- [26] R. Focardi and R. Gorrieri, "A Classification of Security Properties,"
J. Computer Security, vol. 3, pp. 5-33, 1995.- [27] R. Focardi, R. Gorrieri, R. Lanotte, A. Maggiolo-Schettini, F. Martinelli, S. Tini, and E. Tronci, "Formal Models of Timing Attacks on Web Privacy,"
Electronic Notes in Theoretical Computer Science, vol. 62, pp. 229-243, 2001.- [28] R. Focardi, R. Gorrieri, and F. Martinelli, "Information Flow Analysis in a Discrete-Time Process Algebra,"
Proc. 13th IEEE Computer Security Foundations Workshop, pp. 170-184, 2000.- [29] J.A. Goguen and J. Meseguer, "Security Policy and Security Models,"
Proc. Symp. Research in Security and Privacy, pp. 11-20, 1982.- [30] J.W. GrayIII, "Toward a Mathematical Foundation for Information Flow Security,"
J. Computer Security, vol. 1, pp. 255-294, 1992.- [31] P.R. Halmos,
Measure Theory. Springer-Verlag, 1950.- [32] T.A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine, "Symbolic Model Checking for Real-Time Systems,"
Information and Computation, vol. 111, pp. 193-244, 1994.- [33] H. Howard,
Dynamic Programming and Markov Processes. MIT Press, 1960.- [34] M. Kwiatkowska, G. Norman, R. Segala, and J. Sproston, "Automatic Verification of Real-Time Systems with Discrete Probability Distribution,"
Theoretical Computer Science, vol. 282, pp. 101-150, 2002.- [35] M. Kwiatkowska, R. Norman, and J. Sproston, "Symbolic Model Checking of Probabilistic Timed Automata Using Backwards Reachability," Technical Report CSR-03-10, Univ. of Birmingham, 2003.
- [36] R. Lanotte and D. Beauquier,
A Decidable Probability Logic for Timed Probabilistic Systems, CoRR cs.LO/0411100, 2004.- [37] R. Lanotte, A. Maggiolo-Schettini, and A. Troina, "Information Flow Analysis for Probabilistic Timed Automata,"
Proc. Int'l Workshop Formal Aspects in Security and Trust, Aug. 2004.- [38] R. Lanotte, A. Maggiolo-Schettini, and A. Troina,
Weak Bisimulation for Probabilistic Timed Automata, http://www.di.unito.it/~troinaPTA_WB.pdf , 2008.- [39] F. Laroussinie, K.G. Larsen, and C. Weise, "From Timed Automata to Logic—And Back,"
Proc. Int'l Symp. Math. Foundations of Computer Science, pp. 27-41, 1995.- [40] K.G. Larsen and Y. Wang, "Time Abstracted Bisimulation: Implicit Specifications and Decidability,"
Information and Computation, vol. 134, pp. 75-101, 1997.- [41] D. McCullough, "Noninterference and the Composability of Security Properties,"
Proc. Symp. Research in Security and Privacy, pp. 177-186, 1988.- [42] J.K. Millen, "Hookup Security for Synchronous Machines,"
Proc. IEEE Computer Security Foundations Workshop, pp. 84-90, 1990.- [43] R. Milner,
Communication and Concurrency. Prentice Hall, 1989.- [44] A. Troina, "Probabilistic Timed Automata for Security Analysis and Design," PhD thesis, Univ. of Pisa, 2006.
- [45] Y. Wang, "Real-Time Behaviour of Asynchronous Agents,"
Proc. Int'l Conf. Concurrency Theory, pp. 502-520, 1990. |