Certification Using the Mobius Base Logic

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.

• Type: Conference
• Year: 2007
• Where: FMCO
• Authors: Lennart Beringer, Martin Hofmann, Mariela Pavlova
• Keywords: Core Proof Rules, FMCO 2007, Formal Methods, Mobius Base Logic, Program Logic