User: Guest  Login
Original title:
Verified Java Bytecode Verification
Translated title:
Verifizierte Java Bytecode-Verifikation
Year:
2003
Document type:
Dissertation
Institution:
Fakultät für Informatik
Advisor:
Nipkow, Tobias (Prof. Ph.D.)
Referee:
Basin, David (Prof. Ph.D.)
Format:
Text
Language:
en
Subject group:
DAT Datenverarbeitung, Informatik
Keywords:
Java; Bytecode Verification; Theorem Proving; Isabelle
Translated keywords:
Java; Bytecode Verifikation; Theorembeweiser; Isabelle
Controlled terms:
Java ; Computersicherheit; Byte-Code; Automatisches Beweisverfahren; Verifikation
Abstract:
The bytecode verifier is an important part of Java's security architecture. This thesis presents a fully formal, executable, and machine checked specification of a representative subset of the Java Virtual Machine and its bytecode verifier together with a proof that the bytecode verifier is safe. The specification consists of an abstract framework for bytecode verification which is instantiated step by step with increasingly expressive type systems covering all of the interesting and complex pro...    »
Translated abstract:
Der Bytecode Verifier ist ein essentieller Bestandteil der Sicherheitsarchiktektur der Programmierplattform Java. Die Dissertation präsentiert eine formale, ausführbare Spezifikation des Bytecode Verifiers sowie den Beweis, dass dieser korrekt ist. Die Formalisierung im Theorembeweiser Isabelle besteht aus einem abstrakten Framework für Bytecode-Verifikation, das mit zunehmend ausdrucksstarken Typsystemen instantiiert wird. Diese decken sämtliche interessanten Eigenschaften der Java-Plattform ab...    »
Publication :
Universitätsbibliothek der TU München
Date of submission:
28.11.2002
Oral examination:
17.02.2003
File size:
1402761 bytes
Pages:
190
Last change:
04.07.2007
 BibTeX