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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
Given a graph \(G=(V,Lab,E,w)\) the use of LCW(G) in this paper corresponds to a call to \(LCW(G,V\times V)\) in [1].
References
Alzetta, G., Marin, A., Piazza, C., Rossi, S.: Lumping-based equivalences in markovian automata: algorithms and applications to product-form analyses. Inf. Comput. 260, 99–125 (2018)
Bortz, A., Boneh, D.: Exposing private information by timing web applications. In: Proceedings of the 16th International Conference on World Wide Web (WWW), pp. 621–628. ACM (2007)
Brumley, D., Boneh, D.: Remote timing attacks are practical. Comput. Netw. 48(5), 701–716 (2005)
Crafa, S., Rossi, S.: Controlling information release in the pi-calculus. Inf. Comput. 205(8), 1235–1273 (2007)
Felten, E.W., Schneider, M.A.: Timing attacks on web privacy. In: Proceedings of the 7th ACM Conference on Computer and Communications Security (CCS), pp. 25–32. ACM (2000)
Focardi, R., Gorrieri, R.: Classification of security properties. In: Focardi, R., Gorrieri, R. (eds.) FOSAD 2000. LNCS, vol. 2171, pp. 331–396. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-45608-2_6
Gao, H., Bodei, C., Degano, P., Riis Nielson, H.: A formal analysis for capturing replay attacks in cryptographic protocols. In: Cervesato, I. (ed.) ASIAN 2007. LNCS, vol. 4846, pp. 150–165. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-76929-3_15
Goguen, J.A. Meseguer, J.: Security policy and security models. In: Proceedings of the 1982 Symposium on Security and Privacy, pp. 11–20. IEEE Computer Society Press (1982)
Hillston, J.: A Compositional Approach to Performance Modelling. Cambridge Press, Cambridge (1996)
Hillston, J., Marin, A., Piazza, C., Rossi, S.: Contextual lumpability. In: Proceedings of Valuetools 2013 Conference, pp. 194–203. ACM Press (2013)
Kemeny, J.G., Snell, J.L.: Finite Markov Chains. D, Van Nostrand Company Inc., New York (1960)
Marin, A., Rossi, S.: On the relations between Markov chain lumpability and reversibility. Acta Inf. 54(5), 447–485 (2017)
Marin, A., Rossi, S.: On the relations between lumpability and reversibility. In: Proceedings of MASCOTS 2014, pp. 427–432 (2014)
McLean, J.: A general theory of composition for trace sets closed under selective interleaving functions. In: Proceedings of the IEEE Symposium on Security and Privacy (SSP 1994), pp. 79–93. IEEE Computer Society Press (1994)
Ryan, P.Y.A., Schneider, S.: Process algebra and non-interference. J. Comput. Secur. 9(1/2), 75–103 (2001)
Sabelfeld, A., Myers, A.C.: Language-based information-flow security. IEEE J. Sel. Areas Commun. 21(1), 5–19 (2003)
Smith, G., Volpano, D.M.: Secure information flow in a multi-threaded imperative language. In: Proceedings of ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 1998), pp. 355–364. ACM Press (1998)
Sutherland, D.: A model of information. In: Proceedings of the 9th National Computer Security Conference, pp. 175–183 (1986)
Valmari, A., Franceschinis, G.: Simple O(m logn) time Markov chain lumping. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 38–52. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-12002-2_4
Acknowledgments
The work described in this paper has been partially supported by the Università Ca’ Foscari Venezia - DAIS within the IRIDE program, by the Università di Udine PRID ENCASE project, and by GNCS-INdAM project Metodi Formali per la Verifica e la Sintesi di Sistemi Discreti e Ibridi.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer Nature Switzerland AG
About this paper
Cite this paper
Hillston, J., Marin, A., Piazza, C., Rossi, S. (2018). Information Flow Security for Stochastic Processes. In: Bakhshi, R., Ballarini, P., Barbot, B., Castel-Taleb, H., Remke, A. (eds) Computer Performance Engineering. EPEW 2018. Lecture Notes in Computer Science(), vol 11178. Springer, Cham. https://doi.org/10.1007/978-3-030-02227-3_10
Download citation
DOI: https://doi.org/10.1007/978-3-030-02227-3_10
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-02226-6
Online ISBN: 978-3-030-02227-3
eBook Packages: Computer ScienceComputer Science (R0)