Persistent Stochastic Non-Interference

• Autorzy: Hillston Jane , Marin Andrea , Piazza Carla , Rossi Sabina

Identyfikatory

DOI

10.3233/FI-2021-2049

• Języki publikacji: EN

Abstrakty

EN

In this paper, we study an information flow security property for systems specified as terms of a quantitative Markovian process algebra, namely the Performance Evaluation Process Algebra (PEPA). 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 of certain actions or its throughput. We introduce the notion of Persistent Stochastic Non-Interference (PSNI) based on the idea that every state reachable by a process satisfies a basic Stochastic Non-Interference (SNI) property. The structural operational semantics of PEPA allows us to give two characterizations of PSNI : 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.

Słowa kluczowe

EN

process algebra; non-interference; stochastic models

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2021
• Tom: Vol. 181, nr 1
• Strony: 1--35
• Opis fizyczny: Bibliogr. 49 poz., rys.

Twórcy

autor

Hillston Jane

• School of Informatics, University of Edinburgh, UK

autor

Marin Andrea

• Dept. of Environmental Sciences, Informatics and Statistics, Università Ca’ Foscari, Venezia, Italy

autor

Piazza Carla

• Dept. of Mathematics, Informatics, and Physics, Università di Udine, Italy

autor

Rossi Sabina

• Dept. of Environmental Sciences, Informatics and Statistics, Università Ca’ Foscari, Venezia, Italy

Bibliografia

• [1] Bortz A, Boneh D. Exposing Private Information by Timing Web Applications. In: Proc. of the 16th International Conference on World Wide Web (WWW). ACM, 2007 pp. 621-628.
• [2] Brumley D, Boneh D. Remote Timing Attacks Are Practical. Comput. Netw., 2005. 48(5):701-716.
• [3] Felten EW, Schneider MA. Timing Attacks on Web Privacy. In: Proceedings of the 7th ACM Conference on Computer and Communications Security (CCS). ACM, 2000 pp. 25-32.
• [4] Focardi R, Gorrieri R. Classification of Security Properties (Part I: Information Flow). In: Focardi R, Gorrieri R (eds.), Proc. of Foundations of Security Analysis and Design (FOSAD’00), volume 2171 of LNCS. Springer-Verlag, 2000 pp. 331-396. doi:10.1007/3-540-45608-2_6.
• [5] Plateau B. On the stochastic structure of parallelism and synchronization models for distributed algorithms. SIGMETRICS Performance Evaluation Review, 1985. 13(2):147-154.
• [6] Marin A, Rossi S. On the Relations between Lumpability and Reversibility. In: Proc. of MASCOTS 2014. 2014 pp. 427-432.
• [7] Marin A, Rossi S. On the relations between Markov chain lumpability and reversibility. Acta Informatica, 2017. 54(5):447-485.
• [8] Goguen JA, Meseguer J. Security Policy and Security Models. In: Proc. of the Symposium on Security and Privacy. IEEE Computer Society Press, 1982 pp. 11-20. doi:10.1109/SP.1982.10014.
• [9] Wittbold JT, Johnson DM. “Information Flow in Nondeterministic Systems”. In: Proceedings of the 1990 IEEE Symposium on Research in Security and Privacy. IEEE Computer Society Press, 1990 pp. 144-161.
• [10] Focardi R, Rossi S, Sabelfeld A. Bridging Language-Based and Process Calculi Security. In: Foundations of Software Science and Computational Structures, 8th International Conference, (FOSSACS’05). 2005 pp. 299-315. doi:10.1007/978-3-540-31982-5_19.
• [11] Sabelfeld A, Myers AC. Language-Based Information-Flow Security. IEEE Journal on Selected Areas in Communication, 2003. 21(1):5-19. doi:10.1109/JSAC.2002.806121.
• [12] Smith G, Volpano DM. Secure Information Flow in a Multi-threaded Imperative Language. In: Proc. of POPL’98. ACM Press, 1998 pp. 355-364. doi:10.1145/268946.268975.
• [13] Bossi A, Piazza C, Rosssi S. Compositional Information Flow Security for Concurrent Programs. Journal of Computer Security, 2007. 15(3):373-416.
• [14] Mantel H. Unwinding Possibilistic Security Properties. In: Proc. of the European Symposium on Research in Computer Security (ESoRiCS’00), volume 2895 of LNCS. Springer-Verlag, 2000 pp. 238-254. doi:10.1007/10722599_15.
• [15] McLean J. A General Theory of Composition for Trace Sets Closed under Selective Interleaving Functions. In: Proc. of the IEEE Symposium on Security and Privacy (SSP’94). IEEE Computer Society Press, 1994 pp. 79-93. doi:10.1109/RISP.1994.296590.
• [16] Abadi M, Blanchet B, Fournet C. The Applied Pi Calculus: Mobile Values, New Names, and Secure Communication. Journal of the ACM, 2018. 65(1):1:1-1:41. doi:10.1145/3127586.
• [17] Bugliesi M, Rossi S. Non-interference proof techniques for the analysis of cryptographic protocols. Journal of Computer Security, 2005. 13(1):87-113. doi:10.3233/JCS-2005-13104.
• [18] Focardi R, Gorrieri R, Martinelli F. Non Interference for the Analysis of Cryptographic Protocols. In: Montanari U, Rolim JDP, Welzl E (eds.), Proc. of Int. Colloquium on Automata, Languages and Programming (ICALP’00), volume 1853 of LNCS. Springer-Verlag, 2000 pp. 744-755. doi:10.1007/3-540-45022-X_31.
• [19] Focardi R, Rossi S. Information flow security in dynamic contexts. Journal of Computer Security, 2006. 14(1):65-110. doi:10.3233/JCS-2006-14103.
• [20] Crafa S, Rossi S. P-congruences as non-interference for the pi-calculus. In: Proceedings of the 2006 ACM workshop on Formal methods in security engineering, (FMSE’06). 2006 pp. 13-22. doi:10.1145/1180337.1180339.
• [21] Crafa S, Rossi S. Controlling information release in the pi-calculus. Information and Computation, 2007. 205(8):1235-1273. doi:10.1016/j.ic.2007.01.001.
• [22] Hennessy M, Riely J. Information Flow vs. Resource Access in the Asynchronous Pi-calculus. ACM Transactions on Programming Languages and Systems (TOPLAS), 2002. 24(5):566-591. doi:10.1145/570886.570890.
• [23] Ryan PYA, Schneider S. Process Algebra and Non-Interference. Journal of Computer Security, 2001. 9(1/2):75-103. doi:10.3233/JCS-2001-91-204.
• [24] Bossi A, Focardi R, Piazza C, Rossi S. A Proof System for Information Flow Security. In: Logic Based Program Development and Transformation, volume 2664 of LNCS. Springer-Verlag, 2003 pp. 199-218. doi:10.1007/3-540-45013-0_16.
• [25] Bossi A, Macedonio D, Piazza C, Rossi S. Information flow in secure contexts. Journal of Computer Security, 2005. 13(3):391-422. URL http://content.iospress.com/articles/journal-of-computer-security/jcs235.
• [26] Aldini A, Bernardo M. A General Framework for Nondeterministic, Probabilistic, and Stochastic Noninterference. In: Foundations and Applications of Security Analysis, Joint Workshop on Automated Reasoning for Security Protocol Analysis and Issues in the Theory of Security, (ARSPAWITS), volume 5511 of LNCS. Springer-Verlag, 2009 pp. 18-33. doi:978-3-642-03459-6_2.
• [27] Di Pierro A, Hankin C, HWiklicky. Approximate Non-Interference. In: Proc. of the IEEE Computer Security Foundations Workshop (CSFW’02). IEEE Computer Society Press, 2002 pp. 3-17. doi:10.1109/CSFW.2002.1021803.
• [28] Focardi R, Gorrieri R, Martinelli F. Real-Time Information Flow Analysis. IEEE Journal on Selected Areas in Communications, 2003. 21(1). doi:10.1109/JSAC.2002.806122.
• [29] Gorrieri R, Locatelli E, Martinelli F. A Simple Language for Real-Time Cryptographic Protocol Analysis. In: Degano P (ed.), Proc. of European Symposium on Programming (ESOP’03), volume 2618 of LNCS. Springer-Verlag, 2003 pp. 114-128. doi:10.1007/3-540-36575-3_9.
• [30] Gao H, Bodei C, Degano P, Nielson H. A Formal Analysis for Capturing Replay Attacks in Cryptographic Protocols. In: Advances in Computer Science - ASIAN 2007. Computer and Network Security, 12th Asian Computing Science Conference, volume 4846 of LNCS. Springer-Verlag, 2007 pp. 150-165. doi:10.1007/978-3-540-76929-3_15.
• [31] Sutherland D. A Model of Information. In: Proc. of the 9th National Computer Security Conference. National Computer Security Center, 1986 pp. 175-183. URL https://csrc.nist.gov/publications/detail/conference-paper/1986/09/15/proceedings-9th-national-computer-security-conference-1986.
• [32] Focardi R, Gorrieri R. A Classification of Security Properties for Process Algebras. Journal of Computer Security, 1994/1995. 3(1):5-33. doi:10.3233/JCS-1994/1995-3103.
• [33] Hillston J, Marin A, Piazza C, Rossi S. Contextual Lumpability. In: Proc. of Valuetools 2013 Conf. ACM Press, 2013 pp. 194-203.
• [34] Bossi A, Focardi R, Piazza C, Rossi S. Bisimulation and Unwinding for Verifying Possibilistic Security Properties. In: Proc. of Int. Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI’03), volume 2575 of LNCS. Springer-Verlag, 2003 pp. 223-237.
• [35] Bossi A, Focardi R, Macedonio D, Piazza C, Rossi S. Unwinding in Information Flow Security. Electronic Notes in Theoretical Computer Science, 2004. 99:127-154.
• [36] Casagrande A, Piazza C. Unwinding biological systems. Theor. Comput. Sci., 2015. 587:26-48. doi:10.1016/j.tcs.2015.02.045. URL https://doi.org/10.1016/j.tcs.2015.02.045.
• [37] Hillston J. A Compositional Approach to Performance Modelling. Cambridge Press, 1996.
• [38] Taubner DA. Finite representations of CCS and TCSP programs by automata and Petri nets, volume 369 of LNCS. Springer-Verlag, 1989. ISBN 3-540-51525-9.
• [39] Baier C, Katoen JP, Hermanns H, Wolf V. Comparative branching-time semantics for Markov chains. Information and Computation, 2005. 200(2):149-214.
• [40] Boudali H, Crouzen P, Stoelinga M. A compositional semantics for dynamic fault trees in terms of interactive Markov chains. In: Proc. of the 5th Int. Conf. on Automated Technology for Verification and Analysis (ATVA’07), volume 4762 of LNCS. Springer-Verlag, 2007 pp. 441-456. doi:10.1007/978-3-540-75596-8_31.
• [41] Deng Y, Hennessy M. On the semantics of Markov automata. Inf. Comput., 2013. 222:139-168. doi:10.1016/j.ic.2012.10.010.
• [42] Milner R. Communication and Concurrency. Prentice-Hall, 1989. ISBN 978-0-13-115007-2.
• [43] Bossi A, Focardi R, Piazza C, Rossi S. Verifying Persistent Security Properties. Computer Languages, Systems and Structures, 2004. 30(3-4):231-258. doi:10.1016/j.cl.2004.02.005.
• [44] Alzetta G, Marin A, Piazza C, Rossi S. Lumping-based equivalences in Markovian automata: Algorithms and applications to product-form analyses. Information and Computation, 2018. 260:99-125. doi:10.1016/j.ic.2018.04.002.
• [45] Valmari A, Franceschinis G. Simple O(m logn) Time Markov Chain Lumping. In: Proc. of Int. Conf. TACAS, volume 6015. Springer Verlag, Paphos, Cyprus, 2010 pp. 38-52. doi:10.1007/978-3-642-12002-2_4.
• [46] Valmari A. Bisimilarity Minimization in O (m logn) Time. In: International Conference on Applications and Theory of Petri Nets, volume 5606 of LNCS. Springer-Verlag, 2009 pp. 123-142. doi:10.1007/978-3-642-02424-5_9.
• [47] Kemeny JG, Snell JL. Finite Markov Chains. D. Van Nostrand Company, Inc., 1960.
• [48] Piazza C, Pivato E, Rossi S. CoPS - Checker of Persistent Security. In: Tools and Algorithms for the Construction and Analysis of Systems, 10th International Conference (TACAS’04). 2004 pp. 144-152. doi:10.1007/978-3-540-24730-2_11.
• [49] Millen JK. Unwinding Forward Correctability. In: Proc. of the IEEE Computer Security Foundations Workshop (CSFW’94). IEEE Computer Society Press, 1994 pp. 2-10. doi:10.1109/CSFW.1994.315952.