KIT | KIT-Bibliothek | Impressum | Datenschutz

Program-level Specification and Deductive Verification of Security Properties

Scheben, Christoph

Abstract:
Programs with publicly accessible interfaces are increasingly used to process confidential data. This makes it all the more important to control the information flow within such applications. This thesis shows how highly precise specification and deductive verification of language-based secure information flow can be made feasible. The approach does not rely on fixed approximations, but makes use of the precision provided by the underlying calculus for Java Dynamic Logic.


Volltext §
DOI: 10.5445/IR/1000046878
Cover der Publikation
Zugehörige Institution(en) am KIT Institut für Theoretische Informatik (ITI)
Publikationstyp Hochschulschrift
Publikationsjahr 2014
Sprache Englisch
Identifikator urn:nbn:de:swb:90-468785
KITopen-ID: 1000046878
Verlag Karlsruher Institut für Technologie (KIT)
Art der Arbeit Dissertation
Fakultät Fakultät für Informatik (INFORMATIK)
Institut Institut für Theoretische Informatik (ITI)
Prüfungsdaten 26.11.2014
Referent/Betreuer Schmitt, P. H.
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft
KITopen Landing Page