Certification using the Mobius base logic

Lennart Beringer, Martin Hofmann, Mariela Pavlova

Research output: Chapter in Book/Report/Conference proceedingConference contribution

4 Scopus citations


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.

Original languageEnglish (US)
Title of host publicationFormal Methods for Components and Objects - 6th International Symposium, FMCO 2007, Revised Papers
Number of pages27
StatePublished - 2008
Externally publishedYes
Event6th International Symposium on Formal Methods for Components and Objects, FMCO 2007 - Amsterdam, Netherlands
Duration: Oct 24 2007Oct 26 2007

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume5382 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference6th International Symposium on Formal Methods for Components and Objects, FMCO 2007

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'Certification using the Mobius base logic'. Together they form a unique fingerprint.

Cite this