Benutzer: Gast  Login
Originaltitel:
Verified Java Bytecode Verification 
Übersetzter Titel:
Verifizierte Java Bytecode-Verifikation 
Jahr:
2003 
Dokumenttyp:
Dissertation 
Institution:
Fakultät für Informatik 
Betreuer:
Nipkow, Tobias (Prof. Ph.D.) 
Gutachter:
Basin, David (Prof. Ph.D.) 
Format:
Text 
Sprache:
en 
Fachgebiet:
DAT Datenverarbeitung, Informatik 
Stichworte:
Java; Bytecode Verification; Theorem Proving; Isabelle 
Übersetzte Stichworte:
Java; Bytecode Verifikation; Theorembeweiser; Isabelle 
Schlagworte (SWD):
Java ; Computersicherheit; Byte-Code; Automatisches Beweisverfahren; Verifikation 
Kurzfassung:
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...    »
 
Übersetzte Kurzfassung:
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...    »
 
Veröffentlichung:
Universitätsbibliothek der TU München 
Mündliche Prüfung:
17.02.2003 
Dateigröße:
1402761 bytes 
Seiten:
190 
Letzte Änderung:
04.07.2007