KIT | KIT-Bibliothek | Impressum
Originalveröffentlichung
DOI: 10.1524/itit.2011.0636

Software Security in Virtualized Infrastructures - The Smart Meter Example

Beckert, Bernhard; Hofheinz, Dennis; Müller-Quade, Jörn; Pretschner, Alexander; Snelting, Gregor

Abstract:
We present a machine-checked formalisation of the Java memory model and connect it to an operational semantics for Java source code and bytecode. This provides the link between sequential semantics and the memory model that has been missing in the literature. Our model extends previous formalisations by dynamic memory allocation, thread spawns and joins, infinite executions, the wait-notify mechanism and thread interruption. We prove the Java data race freedom guarantee for the complete formalisation in a modular way. This work makes the assumptions about the sequential semantics explicit and shows how to discharge them.


Zugehörige Institution(en) am KIT Institut für Programmstrukturen und Datenorganisation (IPD)
Kompetenzzentrum für angewandte Sicherheitstechnologie (KASTEL)
Publikationstyp Zeitschriftenaufsatz
Jahr 2011
Sprache Englisch
Identifikator ISSN: 1611-2776
KITopen ID: 1000027291
HGF-Programm 46.12.03; LK 01
Erschienen in it - Information Technology
Band 53
Heft 3
Seiten 142-151
Projektinformation KASTEL I (BMBF, 01BY1172 / 16BY1172)
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft KITopen Landing Page