|
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.
|
|
|
|
zurück
zum Index |
|
Research
Fellows am DFKI |
|
Die
20. WBR-Sitzung |
|
Veröffentlichungen |
|
Alumni-Treffen
und Events |
|
Forschungsbereich
Deduktion und Multiagentensysteme |
|
Bild
der Wissenschaft:
DFKI nicht an erster Stelle? |
|
Das Virtual Office Projekt |
|
Verein
der Freunde und Förderer des DFKI |
|
Der
Stellenmarkt |
|
Die
Seite der Geschäftsleitung |
|
Impressum |
|