1. FairPay – Verlässlichkeit im elektronischen Zahlungsverkehr
Bei diesem Projekt handelt es sich um ein Verbundvorhaben, an dem neben mehreren Universitäten auch zahlreiche auf dem Gebiet des elektronischen Zahlungsverkehrs und der IT-Sicherheit führende Firmen, darunter 2 bedeutende deutsche Banken, beteiligt sind.
Kernthema des FairPay-Projektes ist der elektronische Zahlungsverkehr in offenen Netzen. Das übergeordnete Projektziel besteht in der Entwicklung eines generischen Vorgehensmodells, das als Grundlage einer international konkurrenzfähigen technischen Infrastruktur zur Entwicklung sicherheitskritischer Systeme im Bereich des elektronischen Zahlungsverkehrs dienen kann. Dabei sollen bislang isolierter Ansätze, Methoden und Ergebnisse aus den Kompetenzbereichen der beteiligten Partner zu einem einheitlichen Security Engineering Process zusammengeführt werden.
Im Rahmen dieses Projekts ist das Fachgebiet mit der Entwicklung und Anwendung deduktiver Verfahren und automatischer Verifikationstechniken befasst. Entwurf und Einsatz formaler Techniken bei der Entwicklung von Sicherheitsmodellen und Anwendungsspezifikationen bilden einen zweiten Schwerpunkt. Vorrangiges Ziel ist die Übertragung bestehender Modellierungs- und Verifikationstechniken auf den Bereich des elektronischen Zahlungsverkehrs und damit die Anwendung aktueller wissenschaftlicher Forschung und theoretischer Erkenntnisse auf konkrete und bedeutende Fragestellungen aus der Praxis.
2. VeriFun – A Verifier for Functional Programms
Auch wenn Deduktionssysteme bereits sehr leistungsstark sind und ein hohes Maß an Automatisierung ermöglichen, bedarf die Verifikation von (imperativen oder funktionalen) Programmen noch immer der menschlichen Unterstützung. Die dabei entstehenden Beweisaufgaben sind so komplex, dass sie in der Regel nur mit Hilfe interaktiver Systeme gelöst werden können.
Solch ein interaktives Werkzeug sollte sich von den vollautomatischen Ansätzen durch folgende Eigenschaften abheben:
- eine übersichtliche und intuitive Benutzerschnittstelle, in der auch komplexe Sachverhalte verständlich dargestellt werden
- leistungsfähige automatische Komponenten, die auch (Teil-) Ergebnisse liefern, mit denen der Anwender weiterarbeiten kann
- ein Beweiskalkül, der für den Benutzer verständlich und leicht anwendbar ist
- eine transparente Arbeitsweise des Systems
- die Verwendung von Beweisbibliotheken
Mit VeriFun entsteht ein interaktives System, das diesen Anforderungen gerecht werden soll. Es ermöglicht den Nachweis von Aussagen über Programme, die in einer funktionalen Sprache geschrieben sind.
Die Ergänzung mit automatischen Verfahren (etwa für den Terminierungsnachweis, die Auswahl von Induktionsaxiomen, das Führen von Gleichheitsbeweisen mittels Termersetzungssystemen usw.) trägt wesentlich dazu bei, den Interaktionsbedarf für den Benutzer so weit wie möglich zu verringern.
VeriFun kommt in der Lehre (als didaktisches Werkzeug) und in der Forschung (als System, mit dem neue Techniken leicht erprobt werden können) zum Einsatz. Besondere Schwerpunkte liegen deshalb auf der Gestaltung einer klar strukturierten, auch didaktisch geeigneten Oberfläche, auf einer einfach portierbaren Implementierung (Java) und einem leicht verständlichen und variablen Konzept und Beweiskalkül.
Für Details siehe VeriFun-Homepage.
3. Lernender Beweiser
Diesem Projekt liegt die Arbeitshypothese zugrunde, dass der Automatisierungsgrad von Beweissystemen durch geeignete Maßnahmen – insbesondere durch die Verknüpfung mit anderen Forschungszweigen der Künstlichen Intelligenz – signifikant erhöht werden kann. Der Grad der Automatisierung ist stark davon abhängig,
- wie erfolgreich das System aus dem gegebenen Vorwissen den für die Lösung eines bestimmten Problems relevanten Ausschnitt zu selektieren vermag und
- wie gut es in der Lage ist, die für die Lösung des Problems wichtigen Hypothesen zu synthetisieren. Hinzu kommt
- der in vielen Bereichen der Informatik maßgebliche Aspekt, bereits erarbeitete Problemlösungen so weit wie möglich wiederzuverwenden.
Um diese drei Ziele zu erreichen, werden in dem Projekt Verfahren des Maschinellen Lernens, die innerhalb der Künstlichen Intelligenz entwickelt wurden, in Beweissysteme eingebunden. Bei einem neuen Beweisziel versucht das System zunächst, einen geeigneten, bereits durchgeführten Beweis zu finden und zu übertragen, um so den Aufwand für die Beweissuche zu verringern. Gelingt dies nicht, kann der Benutzer, durch das System unterstützt, interaktiv die neue Aussage beweisen. Der neue Beweis wird – nach einer entsprechenden Abstraktion – in einer Bibliothek gespeichert und steht nun nachfolgenden Beweisaufgaben als Ressource zur Verfügung.
Schlagwörter:
automatisches Beweisen; Beweisen; Deduktion; e-commerce; elektronischer Zahlungsverkehr; FairPay; funktionale Programmiersprache; Inferenz; Internet; Java-Sicherheit; Korrektheit von Programmen; Lernen; lernender Beweiser; Logik; Protokolle für offene Netze; Protokollverifikation; Semantik von Programmiersprachen; Security Engineering Process; Sicherheit; Termersetzung; Terminierung; Verifikation; VeriFun; Verlässlichkeit
Weiterbildungsangebote:
wöchentliches fachgebietsübergreifendes Forschungskolloquium „AIDA-Forum“
Kooperationen:
- Deutsches Forschungszentrum für Künstliche Intelligenz (DFKI), Saarbrücken
- Technische Universität München, Lehrstuhl für Software und Systems Engineering
- Universität Karlsruhe, Institut für Wirtschaftspolitik und Wirtschaftsforschung
- Universität Saarbrücken, Fachrichtung Informatik
- Bayerische Hypo- und Vereinsbank AG
- debis IT Security Services GmbH
- Deutsche Bank AG
- Eurosec GmbH Chiffriertechnik und Sicherheit
- University of Edinburgh, Institute for Representation and Reasoning
- Universite Marseille
