Matthias Perner - Information Flow Analysis for CIL
Abstrakt:
Bei Softwaresystemen ist es wichtig garantieren zu können, dass
vertrauliche Informationen nicht über öffentliche
Informationsressourcen ermittelbar sind. Es ist möglich eine
Sicherheitsbedingung zu formalisieren und mittels statischer Analysen
zu prüfen, ob ein gegebenes Programm die Sicherheitsbedingung
garantiert einhält. Sicherheitstypsysteme sind statische Analysen bei
denen Informationsressourcen Sicherheitstypen zugewiesen werden.
Anschliessend wird, basierend auf Typisierungsregeln, das Programm auf
Typsicherheit überprueft. Ausserdem ist es möglich zu beweisen, dass
die Typisierungsregeln die formale Sicherheitseigenschaft gewährleisten
können und somit die Sicherheit eines typisierbaren Programms bezüglich
der Sicherheitseigenschaft garantieren. In dieser Bachelor Arbeit wurde
ein Typsystem für einen Teil der Common Intermediate Language
entwickelt und gezeigt, dass das entwickelte Typsystem die vorher aufgestellten Sicherheitsbedingungen garantieren kann.