Software für sicherheitskritische Anwendungen

Software für sicherheitskritische Anwendungen beginnt vor allen Dingen 
lange bevor die erste Zeile Code geschrieben wird. Da wird viel mehr und 
viel länger in der Spezifikations- und Designphase gearbeitet.

> Nächste Frage: Was ist, wenn der Compiler einen Fehler hat

auch der Compiler muss natürlich sauber definiert und spezifiziert sein 
was damit beginnt, dass erst mal die Sprache klr definiert werden muss. 
Compiler werden für sicherheitskritische Aspekte zertifiziert.
D.h. der übersetzt erst mal 100-erte von Testprogrammen und Experten 
sehen sich an, ob das Übersetzungsergebnis stimmt. Hat man das erst mal 
geschafft, dann werden neue Compilerversionen dadurch verifiziert, dass 
man ihre Ergebnisse mit den Ergebnissen früherer Versionen vergleicht 
und sich ansieht, wo der Compiler unterschiedlichen Code generiert und 
warum. Das erste Testprogramm, dass ein vollständiger Compiler meistens 
zu Gesicht bekommt ist sein eigener Source Code. So ein Compiler ist 
selbst ein nicht triviales Programm. Hat sich der Compiler einmal selbst 
übersetzt, dann wird mit dieser Erstübersetzung der eigene Source Code 
noch einmal übersetzt. Die Überstzungsergebnisse des zweiten und dritten 
Laufes müssen Byte für Byte übereinstimmen. Tun sie das nicht, dann 
stimmt schon sowieso erst mal iregendetwas nicht. Und da Compiler 
nichttriviale Programme sind, hat man so dann auch schon viele Aspekte 
eiens Compilers einer ersten intensiveren Prüfung unterzogen.
Die Möglichkeit eines derartigen Tests ist auch der Grund warum Compiler 
gerne in ihrer eigenen Sprache geschrieben werden. Der Ur-Compiler muss 
natürlich in einer anderen Sprache geschrieben werden. Aber diese 
Urversion muss gerade gut genug sein, dass er einen einfachen 
Erstcompiler übersetzen kann. Ab da Übersetzt sich der Compiler dann 
selbst und profitiert damit immer als erstes Programm von etwaigen 
Verbesserungen im Compiler. Den ganzen Vorgang nennt man Bootstrappen.



> , oder der
> Prozessor - ist ja alles schon vorgekommen.

Ja kommt schon mal vor. Aber auch hier wieder: viel Aufwand in der 
Vorbereitung; Spezifikationen aus denen man automatische Tests 
generieren kann; die das Design schon durchtesten; viele viele 
Testläufe.

Thomas K. schrieb:
> Eine Möglichkeit: 3 Computer parallel: verschiedene Hardware,
> verschiedene Betriebssysteme, verschiedene Programmiersprachen und die
> Programmierteams dürfen während der Entwicklungszeit nicht miteinander
> reden.
>
> Wenn die 3 Computer abweichende Ergebnisse liefern wird
> Mehrheitsentscheid gemacht.
>
> :) Ob das tatsächächlich so praktiziert wird weiß ich nicht...

Ich kenne 2 derartige Projekte

  Apollo
    Der Primary Computer und das AGS (Abort Guidance System) hatten
    unterschiedliche Hardware und unterschiedliche Programme. Das AGS
    fungierte aber rein als Backup für PNGS (Primary Navigation Guidance
    System). Dazu kam natürlich, dass bei Apollo das meiste in Huston
    gerechnet wurde und die Ergebnisse raufgefunkt wurden. Aber mit
    PNGS bzw AGS hätten die Crews auch autonom operieren können. Wobei
    mit AGS keine Landung möglich gewesen wäre.

  Und dann natürlich Shuttle
    5 Computer die meines Wissens 2 unterschiedliche Programme fahren
    und einen Mehrheitsentscheid machen, welche Ergebnisse die
    richtigen sind. 1 Computer darf ausfallen und würde noch nicht
    zu einem Missionsabbruch führen.

Aus der Erfahrung heraus würde ich niemals eine Software schreiben
von der mein Leben abhängt.

Gruss k.

Zurück zur ersten Frage

> Wie stellt man jetzt sicher, dass da keine Fehler drin sind? Also
> sprich, wie wird das getestet. Schaut da ein Experte drüber, oder wird
> ein "Stresstest" gemacht, oder betrachtet man das alles als Black Box
> und testet nur das Gerät von außen, ob es korrekte Ausgangssignale für
> alle Eingangssignale liefert, etc.

Du kannst nur Szenarien entwerfen und testen wie auf die Fehler reagiert 
wird. Also die entsprechend behandeln bzw. abfangen. Dazu geht z.Bsp. 
FMEA

Ein Test auf Fehlerfreiheit geht aus Prinzip nicht.

Das mit den Experten geht schon mal in die richtige Richtung -> Vier 
Augen Prinzip.

Und der beste Punkt, nimm ein Betriebssystem, eine Programmiersprache 
und einen entsprechneden Compiler die für solche Anforderungen gemacht 
sind.
Mit Windows, C bzw. C++ brauchst du das nicht anfangen.

OS - meist eine spezielle Version von VxWorks
Sprache - Ada...

mfg Rene

Rene Schube schrieb:
> Mit Windows, C bzw. C++ brauchst du das nicht anfangen.

Zumindest C wird sowohl im Automotive-Bereich als auch im 
Schienenverkehr eingesetzt. In Letzterem geht die Reise allerdings weg 
von C und hin zu den IEC 61131 Sprachen wie z.B. Structured Text, 
Function Block Diagram. Ob das eine Verbesserung ist, sei dahingestellt.

Hallo zusammen,
das mit dem C ist natürlich etwas provokativ.
Fast jeder der richtig C programmiert, kennt die Fallstricke und weis 
wie schnell man sich damit in den Fuss schiessen kann. C++ ist nur eine 
Erweiterung und 'Verumbiegung' von C. Die alten Sprachen Fortran, COBOL, 
Ada usw. kann heute kaum noch jemand. Und die 'Neumodischen' Graphischen 
Programmierungen LabView, HP-VEE führen auch ein Nischendasein.

Eine echte Alternative gibt es dazu allerdings nicht wirklich.

Generierter Code ist eine Variante, aber auch nur wenn der Generator 
sicher ist. Alternative Sprachen kommen und gehen, nach wie vor sind 
fast 80% der Software in C geschrieben. In der letzten Ct war ein 
Artikel über googels neue Sprache GO. Die soll auf Grund ihres Aufbaus 
viele Probleme von C und C++ vermeiden.

Also wird zwar viel erzählt aber dann doch nur mit Wasser gekocht. Ich 
habe die Erfahrung selbst gemacht. Im Automotiv Bereich, im 
Medizintechnik Bereich und auch bei der Bahn-Technik. Alle haben schöne 
Vorträge gehalten und wenn man sich die Sachen angesehen hat, war es 
meist nur warme Luft.

Der erste Start der Ariane 5 ging in die Hose, nicht weil die Software 
fehlerhaft war sondern weil die Spezialisten dachten: Eine alte Software 
Version von der Ariane 4 geht auch...

mfg Rene

Rene Schube schrieb:
> Die alten Sprachen Fortran, COBOL,
> Ada usw. kann heute kaum noch jemand.

Naja, FORTRAN oder Cobol würde ich nicht für sicherheitskritische
Anwendungen benutzen.  FORTRAN ist doch auch nur bei den Physikern
so beliebt, weil da vor 50 Jahren Leute irgendwelche Modelle in
Sourcecode gehackt haben, den aufgrund der hübschen 6-Zeichen-
Bezeichner ohnehin kein Schwein mehr versteht, sodass man ihn auf
immer und ewig weiterbenutzt. ;-)

Jörg Wunsch schrieb:
> ORTRAN ist doch auch nur bei den Physikern
> so beliebt,
Bist du sicher, das du nicht von Zeiten von vor 20 oder 30 Jahren 
sprichst :-)? Ich habe mir vor kurzem eine Bibliothek zur Simulation und 
Analyse von Teilchenkollisionen von Cern angesehen, das war C++.

Jörg Wunsch schrieb:
> den aufgrund der hübschen 6-Zeichen-
> Bezeichner ohnehin kein Schwein mehr versteht

Immerhin kann man die Namen mit Leerzeichen nach Belieben auflockern, 
das hat doch auch was.

Und seit Fortran-77 bzw. auch mit 90 sind doch einige Änderungen 
gekommen. Das klassische Fortran hat sich weiter entwickelt.

Der wesentliche Punkt bei Fortran ist aber das genaue festlegen von 
reellen Zahlen. Das kann C und C++ nicht. Also auf jeder Maschine immer 
die Sicherheit das die Zahlen gleich aussehen.

Ausserderm gibt es da noch ein paar andere Dinge:
- Arithmetisches IF
- Nichtganzzahliger DO-Index
- Beendigung von DO-Schleifen auf anderen Anweisungen als CONTINUE
  oder END DO
- Sprung auf END IF von Anweisungen außerhalb des IF-Blocks
- Abschluß mehrerer DO-Schleifen auf derselben Anweisung
- alternativer Rücksprung mit RETURN
- ASSIGN und assigned GOTO (gesetzte Sprunganweisung)
- assigned FORMAT

Alles in allem eine schöne Sprache. Und deutlich besser als z.Bsp. BF 
obwohl das mit seinen 8 Befehlen auch was für sich hat. ;)

Rene Schube schrieb:
> Ausserderm gibt es da noch ein paar andere Dinge:

Ich zitiere dazu mal ein wenig aus "Real Programmers Don't Use 
PASCAL"[1]:

> - Arithmetisches IF

Real Programmers enjoy Arithmetic IF statements because they make
the code more interesting.

> - ASSIGN und assigned GOTO (gesetzte Sprunganweisung)

Since FORTRAN doesn't have a structured IF, REPEAT ... UNTIL, or
CASE statement, Real Programmers don't have to worry about not using
them. Besides, they can be simulated when necessary using assigned
GOTOs.

Und natürlich der allgemeine Leitsatz:

Real Programmers aren't afraid to use GOTOs.

Edit: ein Nachsatz noch, der auch da drin steht:

Besides, the determined Real Programmer can write FORTRAN programs
in any language.

;-)

[1] http://www.ee.ryerson.ca/~elf/hack/realmen.html

Ich zitiere nur:
"Real Computer Scientists don't program in assembler. They don't write 
in anything less portable than a number two pencil."[1]
[1] http://www.suslik.org/Humour/Computer/Langs/real_prog2.html

Was sie in FORTRAN nicht machen können machen sie in ASSEMBLER, was sie 
in ASSEMBLER nicht machen können, lassen sie verächtlich liegen!

> Es gibt Menschen die sich genau damit beschäftigen: zu erforschen, eine
> Software beweisbar fehlerrei zu erstellen.

Ja, das es Leute gibt die sich damit beschäftigen ist das eine und die 
Erforschung eine andere Sache.

Aber es gibt auch Leute die sich mit der Existenz von Göttern, Geistern, 
Ufos usw beschäftigen.

Und die Forscher, da gab es mal vor eine Weile eine Nachricht die um die 
Welt ging. Forscher haben die 'Kalte Fusion' im Griff und fast den 
Nobelpreis im Sack.

Also das will ich erstmal sehen! Bisdahin bleibe ich bei meiner Aussage:
> Ein Test auf Fehlerfreiheit geht aus Prinzip nicht.
Sobald ich etwas anderes gesehen habe revidiere ich meine Meinung gern.
Aber in den letzten 20 Jahren, was ich mich damit rumschlage, hat sich 
diese Meinung immer als richtig erwiesen.

mfg Rene

Ausschnitt aus wikipedia:
...
Fehlerfreiheit

Völlige Fehlerfreiheit für Software, die eine gewisse Komplexitätsgrenze 
überschreitet, ist weder erreichbar noch nachweisbar. Mit steigender 
Komplexität sinkt die Überblickbarkeit, insbesondere auch, wenn mehrere 
Personen an der Programmierung beteiligt sind. Selbst teure oder 
vielfach getestete Software enthält unweigerlich Programmierfehler. Man 
spricht dann bei gut brauchbaren Programmen nicht von Fehlerfreiheit, 
sondern von Stabilität und Robustheit. Eine Software gilt dann als 
stabil bzw. robust, wenn Fehler nur sehr selten auftreten und diese dann 
nur kleinere Unannehmlichkeiten mit sich bringen und keine größeren 
Schäden oder Verluste verursachen.

In Spezialfällen ist ein Beweis der Fehlerfreiheit eines Programms 
möglich. Insbesondere in Bereichen, in denen der Einsatz von Software 
mit hohen finanziellen, wirtschaftlichen oder menschlichen Risiken 
verbunden ist, wie z. B. bei militärisch oder medizinisch genutzter 
Software oder in der Luft- und Raumfahrt, verwendet man zudem eine 
(formale) Verifizierung genannte Methode, bei der die Korrektheit einer 
Software formal-mathematisch nachgewiesen wird. Dieser Methode sind 
allerdings wegen des enormen Aufwands enge Grenzen gesetzt und sie ist 
daher bei komplexen Programmen praktisch unmöglich durchzuführen (siehe 
auch Berechenbarkeit). Allerdings gibt es mittlerweile Werkzeuge, die 
diesen Nachweis laut eigenen Angaben zumindest für Teilbereiche 
(Laufzeitfehler) schnell und zuverlässig erbringen können.

Neben der mathematischen Verifizierung gibt es noch eine praxistaugliche 
Form der Verifizierung, die durch die Qualitätsmanagement-Norm ISO 9000 
beschrieben wird. Bei ihr wird nur dann ein Fehler konstatiert, wenn 
eine Anforderung nicht erfüllt ist. Umgekehrt kann demnach ein 
Arbeitsergebnis (und damit auch Software) als fehlerfrei bezeichnet 
werden, wenn es nachweisbar alle Anforderungen erfüllt. Die Erfüllung 
einer Anforderung wird dabei durch Tests festgestellt. Wenn alle Tests 
das erwartete Ergebnis bringen, ist eine Anforderung erfüllt.
...

It's not a bug, it's a feature...

Karl Valentin schrieb:
> Udo Schmitt schrieb:
>> Ein Test auf Fehlerfreiheit geht aus Prinzip nicht.
> ?
> Es gibt Menschen die sich genau damit beschäftigen: zu erforschen, eine
> Software beweisbar fehlerrei zu erstellen. mWn geht das prinipiell ist
> aber zu aufwändig.

Das Problem an der Sache ist, dass man die "Fehlerfreiheit" einer 
Software im Grunde auf etwas anderes zurückführt. Fehlerfreiheit 
definiert sich durch: Verhält sich genau so, wie es die Spezifikation 
erfordert.

Und, man ahnt es schon, erstens ist es sauschwer in einer Spezifikation 
tatsächlich alle nur denkbaren Situationen zu berücksichtigen, zweitens 
hat eine derartige Spezifikation für reale Programme einen derartigen 
Umfang, dass man wiederrum nicht trivial feststellen kann, ob nicht die 
Spezifikation in sich schon widersprüchlich oder gar falsch ist.

In meinem ersten Jahr an der Uni haben wir das in Mathe durchgezogen: 
formal bewiesen, dass ein Bubble-Sort tatsächlich algorithmisch richtig 
ist.

Der Beweis hat 4 DIN-A4 Seiten verschlungen und wir haben eine halbe 
Stunde Vorlesungszeit dafür aufgewendet die mathematische Spezifikation 
in allen Einzelheiten im Vorfeld zu erstellen (unter reger Beteiligung 
des Auditoriums).

Seither hat sich natürlich auf dem Gebiet des automatischen Beweisens 
einiges getan (ist ja doch schon fast 30 Jahre her), aber das 
Grundproblem ist immer noch: Ohne exakte und fehlerfreie Spezifikation 
kannst du eine Korrektheit nicht beweisen.

Rene Schube schrieb:
> Ausserderm gibt es da noch ein paar andere Dinge:

- ENTRY
  (damit muß man ein UP nicht von Anfang an laufen lassen, sondern
  kann alternativ bei der ENTRY-Anweisung einsteigen)