Semantische Modellierung, Analyse und Verifikation von sprachbasierter Software-Sicherheit

点击翻译按钮获取中文摘要

Software-Sicherheitsanalysen sind heute unverzichtbar. Aber: Quis Custodiet Ipsos Custodes? Die beiden Antragsteller kooperieren im vorliegenden Projekt, um Fortschritte in Beweisertechnologie und Programmanalyse für die Verifikation von Sicherheitsanalysen (Information Flow Control, IFC) zu nutzen. In der ersten Projektphase wurden fundamentale (intraprozedurale) Verfahren zur Programmanalyse und IFC formalisiert und mittels Isabelle/HOL korrekt bewiesen; dies führte auch zu Erweiterungen der Java-Semantik. Gleichzeitig wurden die Möglichkeiten zur Gegenbeispielerzeugung in Isabelle erweitert und auf einen Teil der entwickelten Isabelle Theorien angewendet. In der Fortsetzung sollen die Beweise auf inter prozedurale Analysen nebenläufiger Programme sowie explizite Sicherheitsstufen verallgemeinert werden. Dies erfordert nichttriviale Erweiterungen der Formalisierung von Java-Semantik, Abhängigkeitsgraphen und Nichtinterferenz. Die Gegenbeispielerzeugung muss sowohl in punkto Skalierbarkeit als auch Präzision noch signifikant verbessert werden. Als Maßstab dienen im Projekt bei der Entwicklung der formalen Beweise aufgetretene und systematisch erfasste Fehler.