11. Anlage
 
zurück
11.8 Sicherheitsaspekte (Anlage H)


Bei der Entwicklung von Software für sicherheitskritische Applikationen ist der Nachweis der Funktionsfähigkeit auch unter erschwerten Bedingungen ein wesentlicher Vorgang. Ada 95 unterstützt diesen Prozeß indirekt durch Bereitstellung einer Sprachdefinition, die im Vergleich zu anderen Programmiersprachen deutlich weniger potentielle Unsicherheiten aufweist und dadurch die Validation und Verifikation erleichtert. Diese Anlage zum Referenzhandbuch liefert dem Entwickler von Software für sicherheitskritische Applikationen in Verbindung mit einem entsprechenden Ada-Übersetzer die Mittel, um sowohl die Validation als auch die Verifikation durchführen zu können.

"Safety" und "Security"

Der Aufrechterhaltung von zugesicherten Programmeigenschaften auch unter ungünstigen Bedingungen kommt bei den sehr verschiedenen Aufgabenbereichen für Applikationssoftware unterschiedliche Bedeutung zu.

Erhöhte Anforderungen zum Merkmal "Safety" sind typischerweise an Steuersoftware in Flugzeugen und Kernkraftwerken zu stellen. Hier kommt es darauf an, auch unter erschwerten Bedingungen (fehlerhafte Bedienung, Ausfall von Systemteilen) nur richtige Ergebnisse zu liefern, hohe Ausfallsicherheit durch Fehlertoleranz zu bieten und u. U. die Verfügbarkeit durch automatischen Wiederanlauf zu verbessern.

Erhöhte Anforderungen zum Merkmal "Security" sind bei Applikationen für den Bereich der politischen oder militärischen Administration und für Banken angemessen.
Die Erschwerung der Bedingungen wird hier in der Möglichkeit eines Angriffs von außen gesehen. Als Teilmerkmale von "Security" haben Vertraulichkeit (Schutz vor unberechtigtem Zugriff), Integrität (die Richtigkeit der Daten und Funktionen bleibt erhalten), Verfügbarkeit (die Daten bleiben abrufbar) und Verbindlichkeit (der Besitz der vorgenannten Eigenschaften ist beweisbar) zu gelten.


Anforderungen an Software für sicherheitskritische Applikationen
  • Ada ist eine Hochsprache und definiert daher keine Implementierungsspezifika. Jedoch setzen Validation und Verifikation das Wissen über die Implementierung voraus.
  • Wenn die Implementierung in Ada vorgenommen wird, die Validation jedoch auf der Ebene des Objektcodes, ist ein Verständnis der Zusammenhänge zwischen Hochsprache und Objektcode notwendig. Man muß nachvollziehen können, wie der Übersetzer die Ada-Konstrukte in Objektcode übersetzt.
  • Um den Vorgang der Validation und Verifikation möglichst einfach zu halten, ist es wünschenswert, ein abgemagertes Ada-Laufzeitsystem zu besitzen, das ohne problematische Spracheigenschaften auskommt.
Standard für sicherheitskritische Systeme

Ein ausgereifter Standard im sicherheitskritischen Gebiet ist der internationale Standard DO-178B. Der Standard erstreckt sich auf Entwurf, Analyse und Prüfung. Der Nachweis der Verifikation von sicherheitskritischen Applikationen basiert häufig auf den im DO-178B vorgeschriebenen Prüfungen.

Die Verifikation nach diesem Standard ist anhand des Maschinencodes durchzuführen. Nur wenn ein Nachweis vorliegt, daß ein Übersetzer fehlerfrei ist, darf die Verifikation auf der Ebene des Quelltextes vorgenommen werden. Dieser Nachweis ist jedoch schwer zu erhalten (hier ist der Übersetzerhersteller gefordert) und das setzt fast immer voraus, daß
Teile des Sprachumfangs von der Verwendung ausgeschlossen werden.


Unsicherheiten in verbreiteten Programmiersprachen

Da Programmierer fehlbar sind, ist die Verwendung von Programmiersprachen von Vorteil, die Prüfungen für einige Klassen von Fehlern bieten, insbesondere wenn man mittels solcher Prüfungen zur Laufzeit und zugehörigen Ausnahmebehandlungen einfach zu einem sicheren Zustand zurückzukehren kann. Ada 83 (und natürlich Ada 95 als Fortsetzung) nimmt solche
Prüfungen grundsätzlich vor und bietet gleichzeitig Möglichkeiten zur nutzerdefinierten Ausnahmebehandlung. Ada ist daher für sicherheitskritische Anwendungen prinzipiell geeignet.
Weitere Sprachen mit eingebauten Prüfungen und nutzerdefinierten Ausnahmebehandlungen sind C++ und Java, die jedoch (noch) nicht normiert sind.


Sicherheitseinrichtungen und Sicherheitslücken

Die folgende Tabelle gibt einen Überblick über Sicherheitseinrichtungen und Sicherheitslücken von Ada und weiteren Standard-Programmiersprachen:


Sprache Sicherheitseinrichtungen Sicherheitslücken

Ada Laufzeitprüfungen, Möglichkeit nicht initialisierte Zeiger der Initialisierung von Zeigern, und Variable strenge Typisierung, Ausnahmebehandlung
Modula 2 strenge Typisierung, nicht initialisierte Zeiger z. T. Ausnahmebehandlung und Variable
Pascal strenge Typisierung Laufzeitprüfungen optional, nicht initialisierte Zeiger und Variable
C Zusatzwerkzeuge wie z. B. ca. 150 undefinierte Sprachmake und lint eigenschaften, Laufzeitprüfungen optional
Fortran 77 Typprüfung, kein Deklarationszwang, keine Verwendung von Zeigern keine Prüfung über die Grenzen von Prozeduren

Die in der Sprache Ada verbliebenen Unsicherheiten bezüglich sicherheitskritischer Applikationen können durch Wahl einer geeigneten Teilmenge vermieden werden. Diese Einschränkung des Sprachumfangs wird durch das Pragma Restrictions unterstützt. Der Programmierer kann z. B. entscheiden, keine Prozesse zu benutzen. Das hat zur Folge, daß das Laufzeitsystem deutlich kleiner und einfacher ausfällt. Es wird mit diesem Pragma also nicht nur getestet, ob spezielle Konstrukte vermieden wurden, sondern dieses Pragma kann sich auf die erzeugte Applikation grundlegend auswirken.


Nachvollziehbare Programmausführung

Eine Grundvoraussetzung für den Einsatz einer Programmiersprache in sicherheitskritischen Applikationen ist die nachvollziehbare Programmausführung. Ada 95 kommt dieser Forderung durch Bereitstellung von geeigneten Sprachmitteln und Informationen nach:
  • Begrenzte Fehler
    Einige bekannte Fälle von Ada 83, die eine fehlerbehaftete Ausführung (erroneous) zur Folge hatten, können in Ada 95 als begrenzte Fehler behandelt werden.
  • Das Attribut ‘Valid
    Eine Prüfung auf die Gültigkeit von skalaren Werten.
  • Das Pragma Normalize_Scalars
    Vorbesetzung von Variablen skalaren Typs mit Werten, die außerhalb ihres Definitionsbereiches liegen.
  • Dokumentation
    Beschreibung aller Implementierungsspezifika.
Anormale Werte treten in folgenden Situationen auf:
  • nicht initialisierte Gleitpunktvariable
  • Folge einer Abbruchanweisung (abort)
  • Interaktion mit Programmteilen aus anderen Programmiersprachen

Die Verwendung von anormalen Werten hat eine fehlerhafte, nicht vorhersagbare Programmausführung zur Folge, was bei sicherheitskritischen Anwendungen nicht auftreten darf.


Prüfbarer Objektcode

Basis für die Validation und die Verifikation ist die Möglichkeit, sowohl den Quelltext als auch den Objektcode einzusehen, um Prüfungen durchführen zu können. Für diesen Zweck sind Pragmas vorgesehen, die die Aktivitäten des Übersetzers beeinflussen und geeignete Ausgaben produzieren, die das Verständnis des erzeugten Objektcodes erleichtern.


Das Pragma Reviewable

pragma Reviewable;

Dieses Pragma sorgt dafür, daß der Ada-Übersetzer zusätzliche Informationen liefert, um Analyse und Überprüfung des Objektcodes durchführen zu können. Typische Anwendungsfälle für dieses Pragma sind:

  • Generierung eines Assemblerlistings,
  • Angabe der Ausführungszeit von Befehlen oder Befehlsblöcken,
  • Informationen zur Speichernutzung,
  • Aufzeigen des Zusammenhangs zwischen Quelltext und Objektcode.
Das Pragma Inspection_Point

Dieses Pragma sorgt dafür, daß die angegebenen Objekte an der Verwendungsstelle dieses Pragmas verfügbar sind. Der Übersetzer sorgt dafür, daß die Objekte zugreifbar sind und einen aktuellen Wert enthalten. Dieses Pragma verhindert also Optimierungsaktivitäten wie z. B. das Halten von Variablen in Registern und Codeumstellungen. Dadurch wird es einfacher, mit einem Quelltext-Debugger eine Fehlersuche durchzuführen.

Syntax:

pragma Inspection_Point[(object_name {, object_name})];

Dieses Pragma ist ein Konfigurationspragma und wirkt sich auf alle Übersetzungseinheiten aus.

Einschränkungen des Sprachumfangs

Das Pragma Restrictions (pragma <BNF>, restriction <BNF>) definiert verschiedene Einschränkungen des Sprachumfangs von Ada. Durch solche Einschränkungen wird der Nachweis der Korrektheit eines Programmes erst führbar.

Syntax des Pragma Restrictions:

pragma Restrictions(restriction{, restriction});
restriction ::= restriction_identifier | restriction_parameter_identifier => expression

Beispiel:

pragma Restrictions(No_Task_Hierarchy);
pragma Restrictions(Max_Task_Entries=5);


Die angegebenen Einschränkungen werden zur Übersetzungszeit oder zur Laufzeit geprüft und der Übersetzer erzeugt eine dem Verstoß entsprechende Fehlermeldung.

Liste der Einschränkungen mittels Pragma Restrictions

Einschränkungen betreffen im wesentlichen
  • Prozesse,
  • Ausnahmebehandlung und
  • Speicherverwaltung.
Alle weiteren Einschränkungen betreffen unterschiedliche Gebiete der Sprache und lassen sich nicht weiter zuordnen.


 
zurück
 Index   Ada Tour - Dokumentation  
© 2003 Förderverein Ada Deutschland e.V.