Treffer: Verified Java Bytecode Verification

Title:
Verified Java Bytecode Verification
Authors:
Klein, Gerwin
Contributors:
Wagner, Dorothea
Publisher Information:
Gesellschaft für Informatik
Publication Year:
2004
Document Type:
other/unknown material
File Description:
application/pdf
Language:
German
Relation:
Ausgezeichnete Informatikdissertationen 2003; Lecture Notes in Informatics (LNI) - Dissertations, Volume D-4; https://dl.gi.de/handle/20.500.12116/4471
Availability:
https://dl.gi.de/handle/20.500.12116/4471
https://hdl.handle.net/20.500.12116/4471
Accession Number:
edsbas.5BF660AB
Database:
BASE

Weitere Informationen

Der Bytecode Verifier ist ein essenzieller Bestandteil der Sicherheitsarchitektur der Programmierplattform Java. Meine Dissertation stellt eine formale, ausführbare Spezifikation des Bytecode Verifiers vor sowie den Beweis, dass diese korrekt ist. Die Formalisierung, vollständig im Theorembeweiser Isabelle durchgeführt, besteht aus einem abstrakten Framework für Bytecode-Verifikation, das mit zunehmend ausdrucksstarken Typsystemen instanziiert wird. Diese decken sämtliche wichtigen Eigenschaften der Java-Plattform ab. Die Formalisierung liefert zwei ausführbare, verifizierte Bytecode Verifier: den Standard-Algorithmus, wie er auf normalen Desktop- Rechnern benutzt wird, sowie einen Lightweight Bytecode Verifier für eingebettete Systeme mit Ressourcenbeschränkungen wie z.B. Java SmartCards.