Links und Funktionen

Sie sind hier: Startseite / 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.



News and Events

For news and events please switch to the German page.