Links und Funktionen

You are here: Home / Publikationen / Certification Using the Mobius Base Logic


Lennart Beringer, Martin Hofmann, and Mariela Pavlova (2007)

Certification Using the Mobius Base Logic

In: Formal Methods for Components and Objects, 6th International Symposium, FMCO 2007, Amsterdam, The Netherlands, October 24-26, 2007, Revised Lectures, ed. by Frank S. de Boer and Marcello M. Bonsangue and Susanne Graf and Willem P. de Roever, vol. 5382, pp. 25-51, Springer. Lecture Notes in Computer Science (ISBN: 978-3-540-92187-5).

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.

Document Actions