SiSo - Sichere Software Der von Prof. Dr. Jörg Siekmann geleitete Forschungsbereich hat mit Deduktion und Multiagentensystemen Schwerpunkte , die zu den Kerngebieten der Künstlichen Intelligenz gehören. Der Einsatz softwaregesteuerter Systeme in sicherheits-kritischen Anwendungsbereichen bestimmt in wachsendem Maße das tägliche Leben, etwa bei der Steuerung von Zügen, wo ein Systemversagen eine konkrete Bedrohung der menschlichen Gesundheit darstellt, oder im elektronischen Geldverkehr, der Bedrohungen ausgesetzt ist, die im Extremfall einen Zusammenbruch der Volkswirtschaft auslösen könnten. Während in den Ingenieurwissenschaften mathematische Modelle eine sichere Grundlage bilden, ist eine vergleichbare Fundierung im Bereich des Software-Engineering lange vernachlässigt worden. Bei der Formalen Programmentwicklung bilden mathematische Berechnungsmodelle und die mathematische Logik die Grundlage, auf der es möglich wird, objektivierte Spezifikationen zu erstellen und Sicherheitseigenschaften sowie die Korrektheit von Implementierungsschritten nachzuweisen. Obgleich der Einsatz formaler Methoden in der Informationstechnologie in internationalen Kritierienwerken wie etwa der ITSEC ab einer gewissen Sicherheitsstufe gefordert werden, existierten bislang kaum Werkzeuge, die eine formale Spezifikation und Verifikation von Softwareprodukten oder –systemen erlaubten. Die Arbeitsgruppe Formale Methoden beschäftigt sich mit dem Entwurf von Methoden und Werkzeugen zur formalen Programmentwicklung. Im Auftrag des Bundesamts für Sicherheit in der Informationstechnik (BSI) wurde das Entwicklungstool VSE (Verification Support Environment) entwickelt. VSE erlaubt die abstrakte Spezifikation von Systemkomponenten und Sicherheitszielen. Durch maschinell unterstützte Beweisführung (Deduktion) werden Sicherheitseigenschaften nachgewiesen und Verfeinerungsschritte verifiziert.

Derzeit wird VSE in einer Reihe von Projekten kommerziell eingesetzt. Die Arbeitsgruppe Formale Methoden bietet Mitarbeit und Beratung bei der Umsetzung formaler und

semiformaler Methoden im Softwareentwicklungszyklus und -evaluation. Die Haupteinsatzgebiete sind dabei neben der Softwareentwicklung für komplexe industrielle Steuerkomponenten oder eingebettete Systeme der IT-Bereich. Der elektronische Zahlungsverkehr in offenen Netzen erzeugt einen ansteigenden Bedarf an sicherer Software. Im Herbst letzten Jahres wurde z.B. im Rahmen des Signaturgesetzes die Richtlinien für die Anwendung digitaler Signaturen festgelegt. Da das Signaturgesetz explizit den Einsatz formaler Methoden erfordert, wird derzeit in Zusammenarbeit mit Chipkartenherstellern ein generisches Modell für gesetzeskonforme Signatur-Chipkarten entwickelt.