Skip to main content
SpringerLink
Log in

Certification Using the Mobius Base Logic

  • Conference paper
Formal Methods for Components and Objects (FMCO 2007)

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

Included in the following conference series:

Abstract

This paper describes a core component of Mobius’ Trusted Code Base, the Mobius base logic. This program logic facilitates the transmission of certificates that are generated using logic- and type-based techniques and is formally justified w.r.t. the Bicolano operational model of the JVM. The paper motivates major design decisions, presents core proof rules, describes an extension for verifying intensional code properties, and considers applications concerning security policies for resource consumption and resource access.

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. Albert, E., Puebla, G., Hermenegildo, M.V.: Abstraction-carrying code. In: Baader, F., Voronkov, A. (eds.) LPAR 2004. LNCS, vol. 3452, pp. 380–397. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  2. Appel, A.W.: Foundational proof-carrying code. In: Halpern, J. (ed.) Logic in Computer Science, p. 247. IEEE Press, Los Alamitos (invited talk, 2001)

    Google Scholar 

  3. Aspinall, D., Beringer, L., Hofmann, M., Loidl, H.-W., Momigliano, A.: A program logic for resource verification. In: Slind, K., Bunker, A., Gopalakrishnan, G.C. (eds.) TPHOLs 2004. LNCS, vol. 3223, pp. 34–49. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  4. Bannwart, F.Y., Müller, P.: A program logic for bytecode. In: Spoto, F. (ed.) Bytecode Semantics, Verification, Analysis and Transformation. Electronic Notes in Theoretical Computer Science, vol. 141, pp. 255–273. Elsevier, Amsterdam (2005)

    Google Scholar 

  5. Barthe, G., Fournet, C. (eds.): TGC 2007 and FODO 2008. LNCS, vol. 4912. Springer, Heidelberg (2008)

    MATH  Google Scholar 

  6. Beckert, B., Hähnle, R., Schmitt, P.H. (eds.): Verification of Object-Oriented Software. LNCS, vol. 4334. Springer, Heidelberg (2007)

    Google Scholar 

  7. Beckert, B., Mostowski, W.: A program logic for handling JAVA cARD’s transaction mechanism. In: Pezzé, M. (ed.) FASE 2003. LNCS, vol. 2621, pp. 246–260. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  8. Beringer, L., Hofmann, M.O.: A bytecode logic for JML and types. In: Kobayashi, N. (ed.) APLAS 2006. LNCS, vol. 4279, pp. 389–405. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  9. Beringer, L., Hofmann, M.: Secure information flow and program logics. In: IEEE Computer Security Foundations Workshop. IEEE Press, Los Alamitos (2007)

    Google Scholar 

  10. Beringer, L., Hofmann, M., Momigliano, A., Shkaravska, O.: Automatic certification of heap consumption. In: Baader, F., Voronkov, A. (eds.) LPAR 2004. LNCS, vol. 3452, pp. 347–362. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  11. Besson, F., Jensen, T., Pichardie, D.: Proof-Carrying Code from Certified Abstract Interpretation and Fixpoint Compression.Theoretical Computer Science (2006)

    Google Scholar 

  12. Besson, F., Jensen, T., Pichardie, D., Turpin, T.: Result certification for relational program analysis. Inria Research Report 6333 (2007)

    Google Scholar 

  13. Cachera, D., Jensen, T.P., Pichardie, D., Schneider, G.: Certified memory usage analysis. In: Fitzgerald, J.S., Hayes, I.J., Tarlecki, A. (eds.) FM 2005. LNCS, vol. 3582, pp. 91–106. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  14. Chang, B., Chlipala, A., Necula, G.: A framework for certified program analysis and its applications to mobile-code safety. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 174–189. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  15. Chang, B., Chlipala, A., Necula, G., Schneck, R.: The open verifier framework for foundational verifiers. In: Morrisett, J., Fähndrich, M. (eds.) Proceedings of TLDI 2005: 2005 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, pp. 1–12. ACM Press, New York (2005)

    Chapter  Google Scholar 

  16. MOBIUS Consortium. Deliverable 1.1: Resource and information flow security requirements (2006), http://mobius.inria.fr

  17. MOBIUS Consortium. Deliverable 3.1: Bytecode specification language and program logic (2006), http://mobius.inria.fr

  18. Cousot, P., Cousot, R.: Automatic synthesis of optimal invariant assertions: mathematical foundations. In: ACM Symposium on Artificial Intelligence & Programming Languages, Rochester, NY; ACM SIGPLAN Not 12(8), 1–12 (1977)

    Google Scholar 

  19. Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Conference Record of the Fifth ACM Symposium on Principles of Programming Languages, pp. 84–97 (1978)

    Google Scholar 

  20. Czarnik, P., Schubert, A.: Extending operational semantics of the java bytecode. In: Barthe, Fournet [5], pp. 57–72

    Google Scholar 

  21. Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. Journal of the ACM 52(3), 365–473 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  22. Feng, X., Ni, Z., Shao, Z., Guo, Y.: An open framework for foundational proof-carrying code. In: Proc. 2007 ACM SIGPLAN International Workshop on Types in Language Design and Implementation (TLDI 2007), pp. 67–78. ACM Press, New York (2007)

    Chapter  Google Scholar 

  23. Hähnle, R., Pan, J., Rümmer, P., Walter, D.: Integration of a security type system into a program logic. In: Montanari, U., Sannella, D., Bruni, R. (eds.) TGC 2006. LNCS, vol. 4661, pp. 116–131. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  24. Hofmann, M., Pavlova, M.: Elimination of ghost variables in program logics. In: Barthe, Fournet [5], pp. 1–20

    Google Scholar 

  25. Kleymann, T.: Hoare Logic and VDM: Machine-Checked Soundness and Completeness Proofs. PhD thesis, LFCS, University of Edinburgh (1998)

    Google Scholar 

  26. Müller-Olm, M., Seidl, H.: Precise interprocedural analysis through linear algebra. In: Proc. ACM POPL 2004, pp. 330–341 (2004)

    Google Scholar 

  27. Necula, G.C.: Proof-carrying code. In: Principles of Programming Languages, pp. 106–119. ACM Press, New York (1997)

    Google Scholar 

  28. Nelson, G.: Techniques for program verification. Technical Report CSL-81-10, Xerox PARC Computer Science Laboratory (June 1981)

    Google Scholar 

  29. Nipkow, T.: Hoare logics for recursive procedures and unbounded nondeterminism. In: Bradfield, J. (ed.) CSL 2002 and EACSL 2002. LNCS, vol. 2471, pp. 103–119. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  30. Pichardie, D.: Bicolano – Byte Code Language in Coq. Summary appears in [7] (2006), http://mobius.inia.fr/bicolano

  31. Quigley, C.L.: A Programming Logic for Java Bytecode Programs. In: Basin, D.A., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol. 2758, pp. 41–54. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  32. Wildmoser, M.: Verified Proof Carrying Code. PhD thesis, Institut für Informatik, Technische Universität München (2005)

    Google Scholar 

  33. Wildmoser, M., Nipkow, T., Klein, G., Nanz, S.: Prototyping proof carrying code. In: Levy, J.-J., Mayr, E.W., Mitchell, J.C. (eds.) Theoretical Computer Science, pp. 333–347. Kluwer Academic Publishing, Dordrecht (2004)

    Google Scholar 

  34. Woo, T.Y., Lam, S.S.: A semantic model for authentication protocols. In: RSP: IEEE Computer Society Symposium on Research in Security and Privacy (1993)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institut für Informatik, Universität München, Oettingenstrasse 67, 80538, München, Germany

    Lennart Beringer & Martin Hofmann

  2. Trusted Labs, Sophia-Antipolis, France

    Mariela Pavlova

Authors
  1. Lennart Beringer
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Martin Hofmann
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Mariela Pavlova
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Centre for Mathematics and Computer Science, CWI,, Kruislaan 413, 1098 SJ, Amsterdam, The Netherlands

    Frank S. de Boer

  2. Leiden Institute of Advanced Computer Science, Leiden University, P.O. Box 9512, 2300 RA, Leiden, The Netherlands

    Marcello M. Bonsangue

  3. VERIMAG, 2 Avenue de Vignate, Centre Equitation,, 38610, Grenoble-Gières, France

    Susanne Graf

  4. Institute of Computer Science and Applied Mathematics, Christian-Albrechts University, Kiel,Hermann-Rodewald-Straße 3, 24118, Kiel, Germany

    Willem-Paul de Roever

Rights and permissions

Reprints and permissions

Copyright information

© 2008 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Beringer, L., Hofmann, M., Pavlova, M. (2008). Certification Using the Mobius Base Logic. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, WP. (eds) Formal Methods for Components and Objects. FMCO 2007. Lecture Notes in Computer Science, vol 5382. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-92188-2_2

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-92188-2_2

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-92187-5

  • Online ISBN: 978-3-540-92188-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation