Programmiersprachen der Sicherheitstechnik
Markus Kuhn beschrieb in einem Posting das Problem ziemlich gut:

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 ckzurück © 1996-2019 Lutz Donnerhacke @ IKS GmbH Jena Saturday | 24.Aug.2019