W. Stephan: "Sicherheit durch formale Methoden"

<BODY> <H1>www.duv24.net : W. Stephan: "Sicherheit durch formale Methoden"</H1> <P> <BR> [<A href="/">www.duv24.net</A>] [<A href="../index.html">back</A>] </P> <TABLE WIDTH=100% BORDER=0 CELLSPACING=0 CELLPADDING=0> <TR> <TD VALIGN=top> <TABLE WIDTH=100% BORDER=0 CELLSPACING=0 CELLPADDING=0> <TR> <TD VALIGN=TOP CLASS=detailBereichRedaktion>Bereich > Redaktion > <B><FONT color="#CC3300">Fachbeiträge</FONT></B></TD> <TD ALIGN=right VALIGN=bottom CLASS=detailDatum>02.11.2001</TD> </TR> </TABLE> </TD> <TD VALIGN=top> </TD> <TD VALIGN=top> </TD> </TR> <TR> <TD VALIGN=top CLASS=detailFirma ID=topSpace>DFKI GmbH Deduction & Multiagent Systems :</TD> <TD VALIGN=top> </TD> <TD VALIGN=top> </TD> </TR> <TR> <TD VALIGN=top CLASS=detailTitel>W. Stephan: "Sicherheit durch formale Methoden"</TD> <TD VALIGN=top> </TD> <TD VALIGN=top> </TD> </TR> <TR> <TD VALIGN=top CLASS=detailSubtitel>Mathematisch fundierte Techniken im Software-Engineering</TD> <TD VALIGN=top> </TD> <TD VALIGN=top> </TD> </TR> <TR> <TD VALIGN=top> <TABLE BORDER=0 CELLSPACING=0 CELLPADDING=0> <TR> <TD VALIGN=top CLASS=detailContent> <TABLE WIDTH=1 BORDER=0 ALIGN=left CELLPADDING=0 CELLSPACING=0> <TR> <TD><IMG width=150 border=0 src="http://www.publish-industry.net/publish-industry/company-resources/publish-industry-master_726146682.jpg"></TD> </TR> <TR> <TD CLASS=detailBildunterschrift></TD> </TR> </TABLE> Mit wachsendem Anteil komplexer Softwarelösungen bei Steuerungs- und Regelungssystemen stellt sich die Frage nach Entwicklungstechniken, die auch in diesem Bereich höchsten Sicherheitsanforderungen gerecht werden. Existierende Konzepte des Software-Engineering müssen dazu um mathematisch fundierte Beschreibungsund Analysetechniken ergänzt werden. Solche Methoden stehen heute anwendungsorientiert aufbereitet und unterstützt durch leistungsfähige Werkzeuge an der Schwelle zum routinemäßigen Einsatz.<BR><BR>Der heute erreichte Qualitätsstand von Software stellt sich sehr uneinheitlich dar. So ist festzustellen, dass zur Erstellung von (Software-) Systemen zur Steuerung und Regelung sicherheitskritischer Systeme deutlich mehr ingenieurmäßige Sorgfalt aufgewandt wird, als dies z.B. bei dem Textsystem, mit dem dieser Beitrag verfasst wurde, der Fall ist. Softwaresysteme, die etwa bei (unbemannten) Raumsonden zum Einsatz kommen, arbeiten so zuverlässig, dass mehrjährige Missionen (nicht immer, aber oft) erfolgreich abgewickelt werden können. Ist die sicherheitskritische Software also hinlänglich sicher? Nachdem schon 1968 auf einem Workshop in Garmisch der Begriff des Software-Engineering geprägt wurde, existiert in dieser jungen Disziplin inzwischen ein weitgehend akzeptierter Grundkanon von Begriffen und Vorgehensweisen. Reichen diese Techniken aus, um das mit komplexen Softwaresystemen verbundene Risiko zu verringern? Wenn beide Fragen negativ beantwortet werden, dann hauptsächlich deswegen, weil es sich abzeichnet, dass die kaum übersehbaren zusätzlichen Möglichkeiten, die softwaretechnische Lösungen bieten, weiter ausgeschöpft werden. Wie steht es z.B. mit den zukünftigen autonomen Raumsonden, also solchen, die bestimmte Abläufe eigenständig planen und die Ausführung solcher Pläne wie auch das Funktionieren bestimmter Komponenten selbstständig überwachen? Dieser Beitrag befasst sich mit Beschreibungsund Analysetechniken, die durch ihre mathematische Fundierung zu einem deutlichen Sicherheitsgewinn im Sinne einer zuverlässigen Vorhersagbarkeit von Eigenschaften führen. Dabei geht es um softwaretechnische Probleme wie die Gesamtarchitektur, die interne Modellbildung, die z.B. den oben erwähnten Planungsverfahren zugrunde liegt, und die Interaktion zwischen verschiedenen Softwarekomponenten. <BR><BR>Softwareentwicklung<BR><BR>Die hier vorgestellten Methoden sind in den Gesamtrahmen der Softwareentwicklung eingebettet. Abbildung 1 zeigt Artefakte, die im Software-Engineering üblicherweise betrachtet werden. Neu gegenüber der bisher verbreiteten Praxis ist die Art und Weise, wie diese Artefakte gegeben sind, sowie sich daraus ergebende zusätzliche Validierungstechniken. Ausgangspunkt ist eine in natürlicher Sprache abgefasste, grobe und kurz gehaltene Fixierung der Anforderungen in Form eines Lastenhefts. Im Rahmen eines Requirements-Engineering werden danach die grundlegenden Begriffe, (Lösungs-) Konzepte und Anforderungen auf abstrakter Ebene präzisiert. Wir haben dabei zwischen Setzungen, d.h. der abstrakten Systembeschreibung, und Forderungen, d.h. den zur Systembeschreibung begrifflich passenden (zunächst nur) postulierten Eigenschaften (Anforderungen), unterschieden. Aus der abstrakten Systemspezifikation (Produktmodell) entsteht dann der Entwurf (auf hoher Ebene) als Ausgangspunkt der Realisierung, die mit dem lauffähigen Programm abschließt. Erst im Laufe von Entwurf und Realisierung werden die Vorgaben der Analysephase - was soll wie erreicht werden? - durch technische Gesichtspunkte angereichert wie: Architektur und Aufteilung in Komponenten, Kommunikationsstruktur, Effizienz und programmiertechnische Randbedingungen. Bei den heute üblichen Beschreibungsmitteln ist nur die abschließende Implementierung vollständig objektiviert, d.h. eindeutig festgelegt, und überprüfbar. Daher ist gerade bei sicherheitskritischen Anwendungen ein erheblicher Testaufwand notwendig und üblich. Weiter liegt hierin eine Motivation für Prozessmodelle, die in iterativer Weise jeweils bis hinunter zur Implementierung gehen. Analysen auf Programmebene vermischen jedoch immer konzeptionelle Fragen mit Aspekten der technischen Realisierung. Formale Methoden bieten Beschreibungsmittel für die Zwischenstufen, die gleichzeitig abstrakt und objektiviert (präzise) sind. Auf dieser Grundlage können schon vor der eigentlichen Implementierung Eigenschaften überprüft werden. Zum Beispiel wird es so möglich, die gestellten Anforderungen allein auf Grundlage der abstrakten Systemspezifikation entweder nachzuweisen oder, was in der Praxis weit häufiger vorkommt, Fehler schon in der abstrakten Lösungsbeschreibung aufzudecken. Die Darstellung der Softwareentwicklung in Abbildung 1 ist stark vereinfacht. So können auf dem Weg vom Entwurf auf hoher Ebene zum Programm verschiedene Zwischenstufen auftreten. Bei Ansätzen, die auf Transformationen beruhen, können diese Schritte sehr feingranular sein. Auch ist es denkbar, dass zu den ursprünglichen Anforderungen auf der abstrakten Ebene zusätzlich gewünschte Eigenschaften hinzukommen, die erst auf den konkreteren Ebenen formulierbar sind. Die Anforderungen können selbst komplexer Natur sein und anwendungsspezifische Beschreibungsmittel notwendig machen. Abbildung 2 zeigt in stark vereinfachter Weise die Spezifikation des gewünschten (Zeit-) Verhaltens eines Gasbrenners in Bezug auf einen möglichen Gasaustritt (Leck).<BR><BR>Formale Modellierung<BR><BR>Formale Methoden bieten Objektivierung durch Rückgriff auf mathematische Begriffsbildungen. Man unterscheidet dabei zwischen Sprachen zur (endlichen) Beschreibung von Systemen (Syntax) und der Zuordnung von Bedeutung zu solchen Beschreibungen (Semantik). Die formale Festlegung von Beschreibungssprachen folgt dem aus dem Bereich der Programmiersprachen bekannten Muster. In Ergänzung zu textuellen Darstellungen und sich daraus ergebenden Strukturen (Syntaxbaum) findet man oft auch grafische Darstellungen von Systemen. Die Spezifikation in Abbildung 2 ist ein Beispiel hierfür. Man beachte jedoch, dass auch im Fall der Syntax mathematische Strukturen zur Präzisierung herangezogen werden. Den ausschlaggebenden Punkt bildet allerdings die Festlegung der Semantik mit Hilfe von mathematischen Objekten. Diese i.A. unendlichen Gegenstände des mathematischen Denkens definieren das &bdquo;Verhalten“ von Systemen in intersubjektiv verbindlicher Art und Weise. Zwar kann man dieser Objekte nicht unmittelbar habhaft werden, sie bilden jedoch die Grundlage für äußerst nützliche Berechnungsverfahren. Dies ist im Prinzip nichts Ungewöhnliches. Gegenstand von Kurvendiskussionen in der Schulmathematik sind ebenfalls unendliche Objekte des mathematischen Denkens (Funktionen). Endlich und handhabbar sind Beschreibungen dieser Funktionen (y = x?) und Berechnungen (Steigung, Nullstellen), die auf diesen Beschreibungen operieren. Beschreibungen und Berechnungen werden &sbquo;real‘ durch Werkzeuge, wie z.B. Computer-Algebra-Systeme, in denen sie implementiert sind.<BR><BR>Formale Analyse<BR><BR>Ganz analog ist die Situation bei formalen Methoden: Mathematisch fundierte Festlegungen der Syntax und Semantik bilden die Grundlage für implementierte Berechnungsverfahren, mit denen Eigenschaften der Systeme nachgewiesen werden können. Für zustandsendliche Systeme arbeiten die Verfahren zur Überprüfung von Eigenschaften auf internen Darstellungen der Systeme selbst. Zur Formulierung der Sicherheitseigenschaften wird eine Sprache benötigt. Diese ist formal in dem Sinn, dass genau definiert ist, wann eine durch einen sprachlichen Ausdruck gegebene Eigenschaft auf das Verhalten eines Systems zutrifft. Allgemeiner anwendbar, aber auch aufwändiger, ist die axiomatische Methode. Hier wird das Systemverhalten durch Aussagen einer logischen Sprache beschrieben, für die eindeutig festgelegt ist, welche mathematischen Strukturen eine Aussage &sbquo;wahr machen‘. Wie im Fall der Analysis bedeutet dies jedoch zunächst nur einen Erkenntnisgewinn. Erst durch die Verwendung von Regeln, die es gestatten, allein auf syntaktischer Basis aus den Axiomen der Systembeschreibung Schlussfolgerungen zu ziehen, wird dieser Ansatz potenziell nützlich. Wichtig ist, dass sowohl im Fall der Modellanalyse (Modelchecking) als auch bei der Herleitung von Schlussfolgerungen (Deduktion) im Gegensatz zum Testen alle möglichen Abläufe eines Systems erfasst werden. <BR><BR>Werkzeugunterstützung<BR><BR>Wie die meisten ingenieurtechnischen Verfahren wird eine tatsächliche Anwendung dieser Methoden nur durch entsprechende Werkzeugunterstützung ermöglicht. In diesem Bereich gibt es neben Werkzeugen, die sich auf spezielle Aspekte oder anwendungsspezifische Techniken beschränken, auch solche, die als eine Art Case Tool die formale Entwicklung auf breiter methodischer Basis umfassend unterstützen. VSE (Verification Support Environment), das vom DFKI zusammen mit der Universität Ulm und einem Unternehmen im Auftrag des Bundesamtes für Sicherheit in der Informationstechnik entwickelt wurde, gehört in letztere Kategorie. VSE bietet zunächst Unterstützung beim Editieren und Visualisieren von umfangreichen Entwicklungen. VSE verwaltet diese Entwicklungen in konsistenter Weise in einer internen Datenbank und unterstützt den Benutzer bei der Durchführung von Beweisen (Abb. 3). VSE ist in zahlreichen industriellen Entwicklungsprojekten erfolgreich eingesetzt worden.<BR><BR>Fazit<BR><BR>Die sich abzeichnenden komplexen Softwarelösungen machen die Erweiterung der bisher vorherrschenden Techniken des Software-Engineering um mathematisch fundierte Methoden notwendig. Das inzwischen etablierte Angebot an solchen Methoden vollzieht für den Softwarebereich nach, was in anderen Ingenieurdisziplinen seit längerem zum Standard gehört. Die streng mathematisch fundierte Vorgehensweise wird dabei praktisch möglich durch den Einsatz von Werkzeugen wie VSE.<BR><BR>Abb. 1: Üblicher Design-Flow im Software-Engineering<BR><BR>Abb. 2: Vereinfachte Darstellung der Spezifikation des gewünschten Zeitverhaltens eines Gasbrenners in Bezug auf ein mögliches Leck<BR><BR><BR>Abb. 3: Screenshot eines &sbquo;Entwicklungsgraphen‘, der eine Gesamtübersicht über die einzelnen Bestandteile einer Systementwicklung gibt und den Einstiegspunkt für alle Arbeiten mit dem VSE bildet<BR><BR>more @ click DV61452<a name="toolbox"></a ></TD> </TR> <TR> <TD CLASS=detailQuelle> </TD> </TR> </TABLE> </TD> <TD WIDTH=28 VALIGN=top><IMG NAME="" SRC=/pi/spacer.gif WIDTH=1 HEIGHT=1 ALT=""></TD> <TD WIDTH=174 VALIGN=top></TD> </TR> <TR> <TD VALIGN=top><IMG NAME="" SRC=/pi/spacer.gif WIDTH=393 HEIGHT=1 ALT=""></TD> <TD WIDTH=28 VALIGN=top><IMG NAME="" SRC=/pi/spacer.gif WIDTH=28 HEIGHT=1 ALT=""></TD> <TD WIDTH=174 VALIGN=top><IMG NAME="" SRC=/pi/spacer.gif WIDTH=174 HEIGHT=1 ALT=""></TD> </TR> </TABLE> <P><I>Diese Seite wurde am 25.09.2004, 13:12 Uhr aktualisiert</I></P> </BODY>