KIT | KIT-Bibliothek | Impressum | Datenschutz

Efficient Logic-Based Information Flow Analysis of Object-Oriented Programs

Ruch, Fabian

In this thesis, the JavaDL logic is amended by a new modality for the verification of termination-insensitive, object-sensitive, flow-sensitive noninterference of memory locations in object-oriented programs, that is local variables and heap object fields. Noninterference is a security model applied in information flow analysis and the amended JavaDL logic improves the information flow analysis of Java Card programs using the JavaDL sequent calculus. JavaDL formulae are a superset of first-order logic formulae and the logic additionally contains dynamic logic modalities as well as a concept called updates for the transition and evaluation of Java Card program states. Noninterference of memory locations is a property of programs and the respective pairs of start and end states of their executions.
The satisfaction of the property implies that a particular set of memory locations does not interfere with the memory locations not included in this set. A set of memory locations does not interfere with another set if the evaluations of the included memory locations in the end state of any execution are independent of the evaluations of the memory locations included in the other set.
... mehr

Volltext §
DOI: 10.5445/IR/1000036850
Cover der Publikation
Zugehörige Institution(en) am KIT Institut für Theoretische Informatik (ITI)
Publikationstyp Hochschulschrift
Publikationsjahr 2013
Sprache Englisch
Identifikator urn:nbn:de:swb:90-368506
KITopen-ID: 1000036850
Verlag Karlsruher Institut für Technologie (KIT)
Art der Arbeit Abschlussarbeit - Bachelor
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft
KITopen Landing Page