Abstract
Abstract non-interference has been introduced as a weakening non-interference which models attackers as abstract interpretations (i.e., static analyzers) of programming language semantics. In this paper we generalize the notion of abstract non-interference to deal with tree-like models of computation. This allows us to widen the scope of abstract non-interference for modeling security properties in automata, timed automata as models of real-time systems, and concurrent systems. We show that well known definitions of non-interference in these models of computation can be viewed as instances of our generalization. This proves that abstract non-interference can reasonably be considered as a general framework for studying and comparing security properties at different levels of abstraction in both programming languages and systems. Moreover, the most precise harmless attacker of a system is systematically derived by transforming abstract domains, characterizing the security degree of automata and concurrent systems.
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
Preview
Unable to display preview. Download preview PDF.
References
Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science 126(2), 183–235 (1994)
Barbuti, R., De Francesco, N., Santone, A., Tesei, L.: A notion of non-interference for timed automata. Fundamenta Informaticae 51, 1–11 (2002)
Bell, D.E., LaPadula, L.J.: Secure computer systems: Mathematical foundations and model. Technical Report M74-244, MITRE Corp. Badford, MA (1973)
Clark, D., Hankin, C., Hunt, S.: Information flow for algol-like languages. Computer Languages 28(1), 3–28 (2002)
Cohen, E.S.: Information transmission in sequential programs. Foundations of Secure Computation, 297–335 (1978)
Cousot, P.: Constructive design of a hierarchy of semantics of a transition system by abstract interpretation. Theor. Comput. Sci. 277(1-2), 47–103 (2002)
Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proc. of Conf. Record of the 4th ACM Symp. on Principles of Programming Languages (POPL 1977), pp. 238–252. ACM Press, New York (1977)
Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Proc. of Conf. Record of the 6th ACM Symp. on Principles of Programming Languages (POPL 1979), pp. 269–282. ACM Press, New York (1979)
Denning, D.E., Denning, P.: Certification of programs for secure information flow. Communications of the ACM 20(7), 504–513 (1977)
Focardi, R., Gorrieri, R.: A classification of security properties for process algebras. Journal of Computer security 3(1), 5–33 (1995)
Focardi, R., Gorrieri, R.: Classification of security properties (part i: Information flow). In: Focardi, R., Gorrieri, R. (eds.) FOSAD 2000. LNCS, vol. 2171, p. 331. Springer, Heidelberg (2001)
Focardi, R., Martinelli, F.: A uniform approach for the definition of security properties. World Congress on Formal Methods (1), 794–813 (1999)
Focardi, R., Rossi, S., Sabelfeld, A.: Bridging language-based and process calculi security. In: Sassone, V. (ed.) FOSSACS 2005. LNCS, vol. 3441, pp. 299–315. Springer, Heidelberg (2005)
Giacobazzi, R., Mastroeni, I.: Abstract non-interference: Parameterizing non-interference by abstract interpretation. In: Proc. of the 31st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2004), pp. 186–197. ACM-Press, NY (2004)
Goguen, J.A., Meseguer, J.: Security policies and security models. In: Proc. IEEE Symp. on Security and Privacy, pp. 11–20. IEEE Computer Society Press, Los Alamitos (1982)
Honda, K., Vasconcelos, V.T., Yoshida, N.: Secure information flow as typed process behaviour. In: Smolka, G. (ed.) ESOP 2000. LNCS, vol. 1782, pp. 180–199. Springer, Heidelberg (2000)
Hunt, S., Mastroeni, I.: The per model of abstract non-interference. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol. 3672, pp. 171–185. Springer, Heidelberg (2005)
Joshi, R., Leino, K.R.M.: A semantic approach to secure information flow. Science of Computer Programming 37, 113–138 (2000)
Laud, P.: Semantics and program analysis of computationally secure information flow. In: Sands, D. (ed.) ESOP 2001. LNCS, vol. 2028, pp. 77–91. Springer, Heidelberg (2001)
Mantel, H., Sabelfeld, A.: A unifying approach to the security of distributed and multi-threaded programs. Journal of Computer Security 11(4), 615–676 (2003)
Milner, R.: Communication and Concurrency. Prentice-Hall, Inc., Englewood Cliffs (1989)
Sabelfeld, A., Myers, A.C.: Language-based information-flow security. IEEE J. on selected ares in communications 21(1), 5–19 (2003)
Sabelfeld, A., Sands, D.: A PER model of secure information flow in sequential programs. Higher-Order and Symbolic Computation 14(1), 59–91 (2001)
Sabelfeld, A., Sands, D.: Dimensions and principles of declassification. In: Proc. of 18th IEEE Computer Security Foundations Workshop (CSFW-18). IEEE Comp. Soc. Press, Los Alamitos (2005)
Skalka, C., Smith, S.: Static enforcement of security with types. In: ICFP 2000, pp. 254–267. ACM Press, New York (2000)
Volpano, D.: Safety versus secrecy. In: Cortesi, A., Filé, G. (eds.) SAS 1999. LNCS, vol. 1694, pp. 303–311. Springer, Heidelberg (1999)
Volpano, D., Smith, G., Irvine, C.: A sound type system for secure flow analysis. Journal of Computer Security 4(2,3), 167–187 (1996)
Zanotti, M.: Security typings by abstract interpretation. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol. 2477, pp. 360–375. Springer, Heidelberg (2002)
Zdancewic, S., Myers, A.C.: Robust declassification. In: Proc. of the IEEE Computer Security Foundations Workshop, pp. 15–23. IEEE Computer Society Press, Los Alamitos (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Giacobazzi, R., Mastroeni, I. (2005). Generalized Abstract Non-interference: Abstract Secure Information-Flow Analysis for Automata. In: Gorodetsky, V., Kotenko, I., Skormin, V. (eds) Computer Network Security. MMM-ACNS 2005. Lecture Notes in Computer Science, vol 3685. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11560326_17
Download citation
DOI: https://doi.org/10.1007/11560326_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-29113-8
Online ISBN: 978-3-540-31998-6
eBook Packages: Computer ScienceComputer Science (R0)