Verified Java Bytecode Verification

dc.contributor.author	Klein, Gerwin
dc.contributor.editor	Wagner, Dorothea
dc.date.accessioned	2017-09-22T20:42:05Z
dc.date.available	2017-09-22T20:42:05Z
dc.date.issued	2004
dc.description.abstract	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.	de
dc.identifier.isbn	978-3-88579-408-X
dc.identifier.pissn	1617-5468
dc.identifier.uri	https://dl.gi.de/handle/20.500.12116/4471
dc.language.iso	de
dc.publisher	Gesellschaft für Informatik
dc.relation.ispartof	Ausgezeichnete Informatikdissertationen 2003
dc.relation.ispartofseries	Lecture Notes in Informatics (LNI) - Dissertations, Volume D-4
dc.title	Verified Java Bytecode Verification	de
gi.citation.endPage	100
gi.citation.publisherPlace	Bonn
gi.citation.startPage	91

Dateien

1 - 1 von 1