Stand der Technik in Sachen Programmiersprache fuer Mission
Critical Systems bei denen ein Softwarefehler Menschenleben
gefaehrden kann (avionics, air traffic control, Bahnstellwerke,
Medizintechnik, Kernrekatorkontrolle, Prozesssteuerung in der
chemischen Industrie, usw.) ist derzeit wohl die Sprache
SPARK. SPARK ist ein stark zusammengestutztes Subset von Ada.
Man hat jede Menge Dinge herausgeschmissen, die zwar sehr komfortabel
sind, aber eine formale Verifikation der Korrektheit ungemein
erschweren. Dazu gehoert zum Beispiel alles was nach dynamischer
Speicherverwaltung riecht (wenn der Chemiereaktor ueberhitzt darf
es einfach kein "out of memory" geben), ebenso wie die exceptions
(ich sage nur Ariane5 ;-).
Infos dazu gibt es mit AltaVista unter "+ada +spark". Man braucht
keinen extra SPARK compiler, sondern einen ganz normalen Ada
compiler (z.B. GNU's gnat), sowie ein tool oder eine compiler
option die einen warnt dass man ein nicht-SPARK feature benutzt
hat und die bestimmte zusaetzliche formale Kommentare die in
einem SPARK Ada Programm vorhanden sein muessen auf Korrektheit
ueberprueft. Aus diesen formalen Kommentaren kann man dann bei
Codereviews klar sehen, ob einzelne Module eines grossen Systems
irgendwie voneinander abhaengen und sich gegenseitig beeinflussen
koennen, oder getrennt betrachtet werden duerfen.
Wenn ich mich recht entsinne sind beispielsweise die Airbus
fly-by-wire Steuerrechner heute in SPARK implementiert, ebenso
wie verschiedenes Medizin- und Militaergeraet, bei denen die
Kunden oder Zulassungsbehoerden auf formale Verifikation der
Softwarekorrektheit bestehen.
Es gibt also durchaus wesentlich sicherere Alternativen zu C,
nur weis davon der normale Hobbyprogrammierer heute kaum etwas
und pfuscht daher weiter ohne formale Methodik mit seiner
Lieblingshackersprache rum.
Die Norm IEC 1508 definiert vier Levels fuer sicherheitskritische
Software. In den hoechsten Anforderungsklassen SIL4 sind C und
C++ als Programmiersprachen *ausdruecklich* ausgeschlossen,
in SIL3 und SIL2 werden sie "nicht empfohlen", und fuer SIL1
wird C als unter bestimmten bedingungen akzeptabel eingestuft.
C++ wird generell als gefaehrlicher als C eingestuft, da
wesentlich undurchschaubarer.
Wer also kryptographische Sicherheitssoftware entwickeln
will, die einer E6 Evaluation nach ITSEC standhalten soll,
sollte auf keinen Fall sich fuer C oder C++ entscheiden.
Java und Ada sind derzeit wohl wesentlich bessere Kandidaten
fuer Sicherheitsprojekte, wobei man bei beiden noch verschiedene
Zusatztools zur formalen Verifikation einsetzen muss. Fuer
hoechste formale Anforderungen muss man sich wohl mit einer
speziellen Sicherheitssprache wie SPARK anfreunden. E6 ist
die Evaluierungsstufe bei der die BSI-Zertifizierer feuchte
Finger bekommen, da sie auch noch nicht so recht wissen, wie
genau man sowas macht. Ich denke mal, in C++ macht man sowas
garnicht.
Warum all dies heute noch nicht in einem Informatikstudium
gelehrt wird ist mir uebrigens etwas schleierhaft. Literatur
und praktische Industrieerfahrung gaebe es dazu zuhauf.
zurück