Abstract
Non–interference is a semantic program property that assigns confidentiality levels to data objects and prevents illicit information flows from occurring from high to low security levels. In this paper, we present a novel security model for global non–interference which approximates non–interference as a safety property. We also propose a certification technique for global non-interference of complete Java classes based on rewriting logic, a very general logical and semantic framework that is efficiently implemented in the high-level programming language Maude. Starting from an existing Java semantics specification written in Maude, we develop an extended, information–flow Java semantics that allows us to correctly observe global non-interference policies. In order to achieve a finite state transition system, we develop an abstract Java semantics that we use for secure and effective non-interference Java analysis. The analysis produces certificates that are independently checkable and are small enough to be used in practice.
This work has been partially supported by the EU (FEDER) and the Spanish MEC/MICINN under grant TIN 2007-68093-C02-02.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Alba-Castro, M., Alpuente, M., Escobar, S.: Automatic certification of Java source code in rewriting logic. In: Leue, S., Merino, P. (eds.) FMICS 2007. LNCS, vol. 4916, pp. 200–217. Springer, Heidelberg (2008)
Alba-Castro, M., Alpuente, M., Escobar, S.: Automated certification of non-interference in rewriting logic. In: Cofer, D., Fantechi, A. (eds.) FMICS 2008. LNCS, vol. 5596, pp. 182–198. Springer, Heidelberg (2009)
Amtoft, T., Bandhakavi, S., Banerjee, A.: A logic for information flow in object-oriented programs. In: Conference record of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2006, pp. 91–102 (2006)
Barbuti, R., Bernardeschi, C., Francesco, N.D.: Abstract interpretation of operational semantics for secure information flow. Information Processing Letters 83(22), 101–108 (2002)
Barthe, G., D’Argenio, P., Rezk, T.: Secure information flow by self-composition. In: Proceedings of the 17th IEEE workshop on Computer Security Foundations, CSFW 2004, pp. 100–114 (2004)
Bavera, F., Bonelli, E.: Type-based information flow analysis for bytecode languages with variable object field policies. In: SAC 2008, pp. 347–351 (2008)
Clarkson, M.R., Schneider, F.B.: Hyperproperties. In: Proc. IEEE Computer Security Foundations Symposium, CSF 2008 (2008)
Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C. (eds.): All About Maude - A High-Performance Logical Framework. LNCS, vol. 4350. Springer, Heidelberg (2007)
Cousot, P., Cousot, R.: Systematic Design of Program Analysis Frameworks. In: Proc. of Sixth ACM Symp. on Principles of Programming Languages, pp. 269–282 (1979)
Darvas, A., Hahnle, R., Sands, D.: A theorem proving approach to analysis of secure information flow. In: Hutter, D., Ullmann, M. (eds.) SPC 2005. LNCS, vol. 3450, pp. 193–209. Springer, Heidelberg (2005)
Denning, D.E., Denning, P.J.: Certification of programs for secure information flow. Commun. ACM 20(7), 504–513 (1977)
Farzan, A., Chen, F., Meseguer, J., Rosu, G.: JavaRL: The rewriting logic semantics of Java (2007), http://fsl.cs.uiuc.edu/index.php/Rewriting_Logic_Semantics_of_Java
Focardi, R., Gorrieri, R., Focardi, R., Gorrieri, R.: A classification of security properties for process algebras. Journal of Computer Security 3, 5–33 (1994)
Francesco, N.D., Martin, L.: Instruction-level security typing by abstract interpretation. International Journal of Information Security 6(2-3), 85–106 (2007)
Goguen, J.A., Meseguer, J.: Security policies and security models. In: IEEE Symposium on Research in Security and Privacy, pp. 11–20 (1982)
Hunt, S., Sands, D.: On flow-sensitive security types. In: Conference record of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles Of Programming Languages, POPL 2006, pp. 79–90 (2006)
Leavens, G., Baker, A., Ruby, C.: Preliminary design of JML: A behavioral interface specification language for Java. ACM SIGSOFT Software Engineering Notes 31(3), 1–38 (2006)
Meseguer, J., Rosu, G.: The rewriting logic semantics project. Theoretical Computer Science 373(3), 213–237 (2007)
Necula, G.C.: Proof carrying code. In: Proceedings of the 24th ACM SIGPLAN-SIGACT Annual Symposium on Principles of Programming Languages POPL 1997, Paris, France, pp. 106–119 (1997)
Sabelfeld, A., Myers, A.: Language-based information-flow security. IEEE Journal on Selected Areas in Communications 21(1), 5–19 (2003)
Shroff, P., Smith, S., Thober, M.: Dynamic dependency monitoring to secure information flow. In: CSF 2007: Proceedings of the 20th IEEE Computer Security Foundations Symposium, pp. 203–217. IEEE Computer Society, Los Alamitos (2007)
Volpano, D., Smith, G., Irvine, C.: A sound type system for secure flow analysis. Computer Security 4(4), 167–187 (1996)
Warnier, M.: Language Based Security for Java and JML. PhD thesis, Radboud University Nijmegen (2005)
Wasserrab, D., Lohner, D., Snelting, G.: On pdg-based noninterference and its modular proof. In: Proceedings of the ACM SIGPLAN Fourth Workshop on Programming Languages and Analysis for Security (PLAS 2009), pp. 31–44 (2009)
Zanardini, D.: Analysing non–interference with respect to classes. In: Proc. 10th italian Conference on Theoretical Computer Science (ICTCS 2007), pp. 57–69 (2007)
Zanotti, M.: Security typings by abstract interpretation. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol. 2477, pp. 375–2002. Springer, Heidelberg (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Alba-Castro, M., Alpuente, M., Escobar, S. (2010). Abstract Certification of Global Non-interference in Rewriting Logic. In: de Boer, F.S., Bonsangue, M.M., Hallerstede, S., Leuschel, M. (eds) Formal Methods for Components and Objects. FMCO 2009. Lecture Notes in Computer Science, vol 6286. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-17071-3_6
Download citation
DOI: https://doi.org/10.1007/978-3-642-17071-3_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-17070-6
Online ISBN: 978-3-642-17071-3
eBook Packages: Computer ScienceComputer Science (R0)