Gesellschaft für Informatik e.V.

         Dieser besteht aus zwei Sessions a 90 Minuten, die einen dreißig minütigen Vortrag zum Thema "Parameter- Confidentiality" beinhalten.

Zeitplan

Kurzzusammenfassungen

         Software ist überall, auch da wo man sie nicht vermuten würde. Dass Software dabei häufig fehlerhaft ist, gilt vielen Herstellern und Anwendern von 'Standard-Software' als ärgerliche Nebenwirkung, mit der man leben muss wie mit der sommerlichen Stechmückenplage.

         Anders ist dies bei sicherheitskritischen Anwendungen, an die traditionell hohe Zuverlässigkeits- und Qualitätsanforderungen gestellt werden. Programme entscheiden heute, ob und wann im Automobil der Airbag ausgelöst wird. Software steuert Raumfahrzeuge, Produktionsanlagen und Flugzeuge, von denen manche schon nicht mehr ohne Computer fliegen können. In diesen Bereichen wirken Sicherheitsanforderungen verstärkt auf die Art und Weise zurück, wie die Software entwickelt wird.

         Formale Methoden bieten die Möglichkeit einer systematischen Analyse von Sicherheits- und Zuverlässigkeitseigenschaften von Systemen. Der Vortrag beleuchtet den Stand der Dinge und zeigt an konkreten Anwendungen, wie vertrauenswürdige Software im Zusammenspiel unterschiedlicher formaler Methoden und klassischer Sicherheitsanalyse entwickelt werden kann.

         Im Vortrag wird ein Prozessmodell für Security Engineering vorgestellt, das objektorientierten Systementwurf um die systematische Erfassung und Realisierung von Sicherheitsanforderungen erweitert. Unser Ansatz integriert die Beschreibung von Sicherheitsanforderungen, die Bedrohungs- und Risikoanalyse auf der einen Seite mit der Modellierung von Geschäftsprozessen, Use Cases und dem Entwurf der Software-Architektur auf der anderen Seite. Der Vortrag geht auf die erweiterten Artefakte des Prozesses und deren Abhängigkeiten, sowie auf spezifische Beschreibungstechniken für Sicherheitsanforderungen ein.

         Confidentiality of certain parameters is an essential security requirement for many security sensitive applications. In terms of formal language theory we introduce the notion of parameter-confidentiality relative to an agent's knowledge about the system. By considering publicly known dependencies of parameter values, exact specifications of the required confidentiality properties are possible. The new notion complements previous concepts of non-interference, secrecy and indistinguishability.

         Formale Korrektheit von Software ist zwar dringend erwünscht, aber nur sehr aufwendig zu realisieren. Programmprüfung zielt darauf ab, diese Kosten zu reduzieren. Anstatt Software zu verifizieren, weist man lediglich nach, dass ihr Ergebnis korrekt ist. In diesem Vortrag zeigen wir, wie Programmprüfung in praktischen Fällen angewandt werden kann. Als durchgehendes Beispiel diskutieren wir den Nutzen von Programmprüfung bei dem Nachweis, dass Implementierungen von Übersetzern (engl. Compiler) korrekt sind. Übersetzer sind gut geeignet, um einen solchen potentiellen Nutzen zu demonstrieren, weil sie oft über eine lange Zeit gewartet werden und daher viele für die Praxis typische Probleme aufweisen. Insbesondere stellen wir die Methode der Programmprüfung mit Zertifikaten vor, für die wir die klassische Black-Box Programmprüfung erweitert haben. Außerdem etablieren wor Programmprüfung mit Zertifikaten als eine sicherheitsskalierbare und praktisch verwendbare Methode, um die Korrektheit ernstzunehmender Applikationen sicherzustellen. Dabei motivieren wir unsere Erweiterung mit Konzepten der Komplexitätstheorie und zeigen die damit verbundenden praktischen Konsequenzen für Implementierung und Verifikation der Programmprüfer.