TY - GEN
T1 - Certification using the Mobius base logic
AU - Beringer, Lennart
AU - Hofmann, Martin
AU - Pavlova, Mariela
PY - 2008
Y1 - 2008
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=58849101791&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=58849101791&partnerID=8YFLogxK
U2 - 10.1007/978-3-540-92188-2_2
DO - 10.1007/978-3-540-92188-2_2
M3 - Conference contribution
AN - SCOPUS:58849101791
SN - 3540921877
SN - 9783540921875
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 25
EP - 51
BT - Formal Methods for Components and Objects - 6th International Symposium, FMCO 2007, Revised Papers
T2 - 6th International Symposium on Formal Methods for Components and Objects, FMCO 2007
Y2 - 24 October 2007 through 26 October 2007
ER -