Skip to main content
SpringerLink
Log in

Automated Certification of Non-Interference in Rewriting Logic

  • Conference paper
Formal Methods for Industrial Critical Systems (FMICS 2008)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 5596))

Abstract

In this paper we propose a certification technique for non-interference of Java programs based on rewriting logic, a very general logical and semantic framework efficiently implemented in the high-level programming language Maude. Non–interference is a semantic program property that prevents illicit information flow to happen. Starting from a basic specification of the semantics of Java written in Maude, we develop an information–flow extension of this operational Java semantics which allows us to observe non-interference of Java programs. Then we develop in Maude an abstract, finite-state version of the information-flow operational semantics which supports finite program verification. As a by–product of the verification, a certificate of non-interference is delivered which consists of a set of (abstract) rewriting proofs that can be easily checked by the code consumer using a standard rewriting logic engine.

This work has been partially supported by the EU (FEDER) and the Spanish MEC/MICINN under grant TIN 2007-68093-C02-02, Integrated Action HA 2006-0007, LERNet AML/19.0902/97/0666/II-0472-FA, and Generalitat Valenciana GVPRE/2008/113.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 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)

    Chapter  Google Scholar 

  2. Barbuti, R., Bernardeschi, C., De Francisco, N.: Abstract interpretation of operational semantics for secure information flow. Information Processing Letters 83(22), 101–108 (2002)

    Article  MathSciNet  MATH  Google Scholar 

  3. Barbuti, R., Bernardeschi, C., De Francisco, N.: Checking security of Java bytecode by abstract interpretation. In: SAC 2002, pp. 229–236. ACM, New York (2002)

    Google Scholar 

  4. Barthe, G., D’Argenio, P., Rezk, T.: Secure information flow by self-composition. In: CSFW 2004, pp. 100–114. IEEE, Los Alamitos (2004)

    Google Scholar 

  5. Barthe, G., Naumann, D., Rezk, T.: Deriving an information flow checker and certifying compiler for Java. In: SSP 2006, pp. 230–242. IEEE, Los Alamitos (2006)

    Google Scholar 

  6. Barthe, G., Pichardie, D., Rezk, T.: A certified lightweight non-interference Java bytecode verifier. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 125–140. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  7. Barthe, G., Rezk, T.: Non-interference for a JVM-like language. In: TLDI 2005, pp. 103–112 (2005)

    Google Scholar 

  8. Beringer, L., Hofmann, M.: Secure information flow and program logics. In: IEEE CSF 2007, pp. 233–248 (2007)

    Google Scholar 

  9. Burdy, L., Cheon, Y., Cok, D., Ernst, M., Kiniry, J., Leavens, G.T., Rustan, K., Leino, M., Poll, E.: An overview of JML tools and applications. IJSTTT 7(3), 212–232 (2005)

    Google Scholar 

  10. Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.: All About Maude - A High-Performance Logical Framework. LNCS, vol. 4350. Springer, Heidelberg (2007)

    MATH  Google Scholar 

  11. Cousot, P., Cousot, R.: Systematic Design of Program Analysis Frameworks. In: POPL 1979, pp. 269–282 (1979)

    Google Scholar 

  12. Denning, D.E., Denning, P.J.: Certification of programs for secure information flow. Commun. ACM 20(7), 504–513 (1977)

    Article  MATH  Google Scholar 

  13. Dufay, G., Felty, A., Matwin, S.: Privacy-sensitive information flow with JML. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS, vol. 3632, pp. 116–130. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  14. 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

  15. Farzan, A., Chen, F., Meseguer, J., Rosu, G.: Formal analysis of Java programs in JavaFAN. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 501–505. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  16. Farzan, A., Meseguer, J., Rosu, G.: Formal JVM code analysis in JavaFAN. In: Rattray, C., Maharaj, S., Shankland, C. (eds.) AMAST 2004. LNCS, vol. 3116, pp. 132–147. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  17. De Francesco, N., Martini, L.: Instruction-level security typing by abstract interpretation. Int. J. of Inf. Sec. 6(2-3), 85–106 (2007)

    Article  Google Scholar 

  18. Giacobazzi, R., Mastroeni, I.: Abstract non-interference: Parameterizing non-interference by abstract interpretation. In: POPL 2004, pp. 186–197 (2004)

    Google Scholar 

  19. Hunt, S., Sands, D.: On flow-sensitive security types. In: POPL 2006, pp. 79–90 (2006)

    Google Scholar 

  20. Jacobs, B., Pieters, W., Warnier, M.: Statically checking confidentiality via dynamic labels. In: WITS 2005, pp. 50–56 (2005)

    Google Scholar 

  21. 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)

    Article  Google Scholar 

  22. Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. TCS 96(1), 73–155 (1992)

    Article  MathSciNet  MATH  Google Scholar 

  23. Meseguer, J., Rosu, G.: The rewriting logic semantics project. TCS 373(3), 213–237 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  24. Myers, A.C.: Jflow: Practical mostly-static information flow control. In: POPL 1999, pp. 228–241 (1999)

    Google Scholar 

  25. Myers, A.C., Nystrom, N., Zheng, L., Zdancewic, S.: Jif: Java information flow. Software release (2001), http://www.cs.cornell.edu/jif

  26. Necula, G.C.: Proof carrying code. In: POPL 1997, pp. 106–119 (1997)

    Google Scholar 

  27. Rose, E.: Lightweight bytecode verification. J. Autom. Reason. 31(3-4), 303–334 (2003)

    Article  MATH  Google Scholar 

  28. Sabelfeld, A., Myers, A.C.: Language-based information-flow security. IEEE J. on Selected Areas in Comm. 21(1), 5–19 (2003)

    Article  Google Scholar 

  29. TeReSe (ed.): Term Rewriting Systems. Cambridge U. Press, Cambridge (2003)

    Google Scholar 

  30. Warnier, M.E.: Language Based Security for Java and JML. PhD thesis, Radboud University Nijmegen (2005)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Universidad Politécnica de Valencia, Spain

    Mauricio Alba-Castro, María Alpuente & Santiago Escobar

  2. Universidad Autónoma de Manizales, Colombia

    Mauricio Alba-Castro

Authors
  1. Mauricio Alba-Castro
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. María Alpuente
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Santiago Escobar
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Rockwell Collins, 7805 Telegraph Rd. 100, 55438, Bloomington, MN, USA

    Darren Cofer

  2. Dipartimento di Sistemi e Informatica, Università di Firenze, Via S. Marta 3, 50139, Firenze, Italy

    Alessandro Fantechi

Rights and permissions

Reprints and permissions

Copyright information

© 2009 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Alba-Castro, M., Alpuente, M., Escobar, S. (2009). Automated Certification of Non-Interference in Rewriting Logic. In: Cofer, D., Fantechi, A. (eds) Formal Methods for Industrial Critical Systems. FMICS 2008. Lecture Notes in Computer Science, vol 5596. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-03240-0_16

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-03240-0_16

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-03239-4

  • Online ISBN: 978-3-642-03240-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation