KIT | KIT-Bibliothek | Impressum | Datenschutz

Combining Static and Dynamic Program Analysis Techniques for Checking Relational Properties

Herda, Mihai

Abstract:
Die vorliegende Dissertation ist im Bereich der formalen Verifikation von Software angesiedelt.
Sie behandelt die Überprüfung relationaler Eigenschaften von Computerprogrammen, d.h. solche Eigenschaften, die zwei oder mehr Programmausführungen betrachten.
Die Dissertation konzentriert sich auf zwei spezifische relationale Eigenschaften: (1) Nichtinterferenz und (2) ob ein Programm ein Slice eines anderen Programms ist.
Die Nichtinterferenz-Eigenschaft besagt, dass die Ausführung eines Programms mit den gleichen öffentlichen Eingaben die gleichen öffentlichen Ausgaben produziert und dies unabhängig von den geheimen Eingaben (z.B. ... mehr

Abstract (englisch):
The topic of this thesis belongs to the research area of formal software verification. It deals with checking relational properties of computer programs (i.e., properties that consider two or more program executions). The thesis focuses on two specific relational properties: (1) noninterference and (2) whether a program is a correct slice of another. The noninterference property states that running a program with the same public input values will always produce the same public outputs, regardless of the secret inputs (e.g., a password). This means that the secret inputs do not influence public outputs. ... mehr

Open Access Logo


Volltext §
DOI: 10.5445/IR/1000104496
Veröffentlicht am 09.01.2020
Cover der Publikation
Zugehörige Institution(en) am KIT Institut für Theoretische Informatik (ITI)
Kompetenzzentrum für angewandte Sicherheitstechnologie (KASTEL)
Publikationstyp Hochschulschrift
Publikationsjahr 2020
Sprache Englisch
Identifikator KITopen-ID: 1000104496
Verlag Karlsruhe
Umfang XVII, 174 S.
Art der Arbeit Dissertation
Fakultät Fakultät für Informatik (INFORMATIK)
Institut Institut für Theoretische Informatik (ITI)
Prüfungsdatum 13.12.2019
Referent/Betreuer Prof. B. Beckert
Schlagwörter Program Verification, Relational Properties, Noninterference, Information-flow Security, Program Slicing
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft
KITopen Landing Page