|
|||||
|
|
|
|
|||
|
Zur
schnellen Umsetzung innovativer Softwaretechniken im industriellen Entwicklungsprozess
wurde das Transferzentrum SiSo (Sichere Software) am DFKI etabliert.
Das Transferzentrum bietet dem Kunden die Unterstützung und Beratung
bei der Entwicklung von mathematisch korrekter Software unter Berücksichtigung
der höchsten Sicherheitsstandards an. Dabei orientiert sich SiSo
an den Anforderungen hoher Stufen (ab E4/EAL5) der internationalen Kriterienwerke
ITSEC und CC, die den Einsatz formaler Techniken fordern. Zentrales
Tool dabei ist das im Auftrag des Bundesamtes für Sicherheit in
der Informationstechnik (BSI) entwickelte Verification Support Environment
(VSE-II). VSE-II erlaubt die Spezifikation von Systemkomponenten und
Sicherheitszielen. Durch maschinell unterstützte Beweisführung
(Deduktion) werden Sicherheitseigenschaften nachgewiesen und Verfeinerungsschritte
verifiziert. Das Dienstleistungsangebot
von SiSO richtet sich an Hersteller sicherheitsrelevanter Softwaresysteme
und -produkte im Bereich „Safety“ und „Security“.
Anwendungsdomänen finden sich unter anderem in den Bereichen Sicherheitsgateways/Firewalls,
E-Commerce, E-Payment, SmartCards und Signaturgesetz-konformen Komponenten.
Ziel ist es, mit dem Kunden gemeinsam formale und semiformale Entwicklungsprozesse
in konkreten Projekten zu realisieren.
Referenzprojekte
von SiSo Im Rahmen des Projektes FM-DIN wurde ein formales Sicherheitsmodell für SmartCards zur Erzeugung und Prüfung digitaler Signaturen entwickelt. Das formale Modell hat Referenzcharakter und wird Chipkartenherstellern für Entwicklungen gemäß ITSEC ab Stufe E4 zur Verfügung gestellt werden. Um dem Referenzcharakter entsprechen zu können, orientierte sich das Modell an der allgemein anerkannten "Spezifikation der Schnittstelle zu Chipkarten mit Digitaler Signatur-Anwendung/Funktion nach SigG und SigV" (DIN V 66391 Teil1).
In FMSP wurde ein allgemeiner Leitfaden (Tutorial) zur Entwicklung und Prüfung formalisierter Sicherheitspolitiken gemäß ITSEC bzw. CC erstellt. Neben der generellen Vorgehensweise wurden die Beziehungen zwischen informellen Sicherheitsvorgaben und dem FMSP behandelt. Weiterhin wurde der Aufbau eines FMSP erarbeitet und die Verifikationsaufgaben spezifiziert. Abschließend wurde der Zusammenhang zwischen dem FMSP und einem realen Produkt untersucht.
|
|
Projekt SAMOA - Sicherheitsaspekte Mobiler
Agenten In SAMOA wird untersucht,
welche Möglichkeiten Agenten-Technologie, bei der Überwachung
und Sicherheitsgewährleistung in privaten Netzen bietet. Insbesondere
wird der Einsatz vieler mobiler Agenten im Sinne eines Multiagentensystems
fokussiert.
In Valikrypt werden deduktive Verifikationstechniken und eine allgemeine formale Entwicklungsmethodik erarbeitet, die die Entwicklung beweisbar korrekter kryptographischer Sicherheitsprotokolle zu ermöglichen. Über die genannten
Projekte hinaus werden im Bereich Formale Methoden am DFKI eine Reihe
von Projekten bearbeitet, die aufgrund ihres Charakters der Geheimhaltung
unterliegen. Alle Projekte beziehen sich auf Entwicklungen gemäß
der hohen Stufen der Kriterienwerke ITSEC und CC.
|
|||
In
DIC sollen Protection Profiles entwickelt werden, die alle Informationsflüsse
von IT-Systemen obligatorisch kontrollieren und gemäß vorgebbarer
Regeln schützen können. Die hierzu umzusetzende benutzerbestimmbare
Informatiosflusssicherheit BISS soll eine Lösung zur obligatorischen
Kontrolle und Absicherung aller Informationsflüsse sein, die zur
Entlastung des Benutzer transparent ablaufen soll.