KIT | KIT-Bibliothek | Impressum
Open Access Logo
URN: urn:nbn:de:swb:90-368506

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 t ... mehr

Zugehörige Institution(en) am KIT Institut für Theoretische Informatik (ITI)
Publikationstyp Hochschulschrift
Jahr 2013
Sprache Englisch
Identifikator KITopen ID: 1000036850
Verlag KIT, Karlsruhe
Abschlussart Abschlussarbeit - Bachelor
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft KITopen Landing Page