KIT | KIT-Bibliothek | Impressum | Datenschutz

State-based Usage Control Enforcement with Data Flow Tracking using System Call Interposition

Harvan, M.; Pretschner, A.

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.

DOI: 10.1109/NSS.2009.51
Zugehörige Institution(en) am KIT Institut für Programmstrukturen und Datenorganisation (IPD)
Publikationstyp Proceedingsbeitrag
Jahr 2009
Sprache Englisch
Identifikator ISBN: 978-1-4244-5087-9
KITopen-ID: 1000028572
Erschienen in 3rd International Conference on Network and System Security. NSS 2009, Gold Coast, Surfers Paradise, Australia, 19 - 21 October 2009. Ed.: Yang Xiang
Verlag IEEE, Piscataway (NJ)
Seiten 373-380
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft
KITopen Landing Page