Original-URL des Artikels: https://www.golem.de/news/ada-und-spark-mehr-sicherheit-durch-bessere-programmiersprachen-1906-141211.html    Veröffentlicht: 11.06.2019 12:07    Kurz-URL: https://glm.io/141211

Ada und Spark

Mehr Sicherheit durch bessere Programmiersprachen

Viele Sicherheitslücken in Software sind auf Programmierfehler zurückzuführen. Diese Fehler lassen sich aber vermeiden - und zwar unter anderem durch die Wahl einer guten Programmiersprache. Ada und Spark gehören dazu, leider sind sie immer noch wenig bekannt.

Es klingt auf den ersten Blick unwahrscheinlich, ist aber wahr: Die Wahl der Programmiersprache hat maßgeblichen Anteil daran, ob Fehler passieren. Gerade bei systemnaher Programmierung wie bei Mozilla und Embedded-Programmierung wie bei Nvidia können Softwarefehler viel Schaden anrichten. Mozilla verwendet für seine neue Rendering-Engine Rust, Nvidia für bestimmte Firmware-Elemente Ada und Spark. Warum haben sie sich für diese Sprachen entschieden statt etwa für Haskell oder Kotlin? Vor allem, weil Rust und Ada anders als die beiden anderen ohne Virtual Machine und Garbage Collector auskommen. Rust haben wir schon in einem früheren Artikel auf Golem.de vorgestellt, jetzt ist Ada dran.

Was sind Ada und Spark?

Ada ist eine prozedurale Programmiersprache wie C oder C++, enthält aber auch unverzichtbare Elemente wie Objektorientierung und Generics. Die Syntax orientiert sich eher an Pascal und nicht am C-typischen Stil mit den geschweiften Klammern. Beim Design wurde großer Wert auf die Lesbarkeit und Fehlervermeidung gelegt.

Die erste Version von Ada wurde 1983 standardisiert, im selben Jahr, in dem auch die erste Version von C++ erschien. Die Programmiersprache wurde ursprünglich für das US-Verteidigungsministerium entwickelt, bis heute ist Ada sehr präsent in Industrien wie der Luftfahrt und der Verteidigung. Teure Compiler ohne Open-Source-Alternativen machten eine weitere Verbreitung in den 1980er Jahren schwierig - heutzutage hat aber jeder Zugriff auf GCC, das Ada unterstützt.

Weitere Versionen der Sprache folgten in den Jahren 1995, 2005 und 2012. Die nächste Version soll Ada 2020 heißen und demzufolge nächstes Jahr erscheinen. Spark ist eine Schwestersprache von Ada, die einige Sprachfeatures entfernt, um noch mehr Sicherheit erreichen zu können. Jedes Spark-Programm ist also ein Ada-Programm, aber nicht unbedingt umgekehrt. Allerdings ermöglicht Spark weitreichende statische Analysen und kann zum Teil starke Garantien geben - dazu später mehr.

Die ersten Schritte

Der einfachste Weg, einen Eindruck von Ada zu bekommen, ist die Adacore-Learn-Webseite: Auch ohne Installation können Interessierte gleich mit Ada und Spark loslegen. Für eigene Projekte sollten die nötigen freien Werkzeuge für Ada und Spark von der Webseite von Adacore heruntergeladen und installiert werden. In der Entwicklungsumgebung mit dem Namen GNATstudio kann man entweder sein eigenes Programm schreiben ("Create New Project" im ersten Dialog) oder die vielen Beispiele ansehen (im Menu Help -> GNAT -> Examples).

Eines der grundlegendsten Features von Ada sind die numerischen Typen.

Ada - numerische Typen

In vielen Programmiersprachen stehen Programmierern eine Reihe von vordefinierten Ganzzahltypen zur Verfügung, die zum Beispiel 8, 16, 32 und 64 Bit einnehmen (in der Regel gibt es noch Varianten mit oder ohne Vorzeichen). Andere Wertebereiche sind nicht möglich.

In Ada hingegen können Programmierer ihre eigenen Ganzzahltypen völlig frei definieren, so dass sie am besten zum Anwendungsbereich passen. Ist zum Beispiel ein Winkel in Grad gefragt, kann der Typ so definiert werden:



Werte außerhalb dieses Bereichs sind für Variablen dieses Typs nicht zulässig. Eine Zuweisung, die diese Eigenschaft verletzen würde, zum Beispiel



erzeugt entweder einen Fehler zur Laufzeit oder der Fehler wird, in einfachen Fällen wie diesem, sofort vom Compiler entdeckt.

Ein Fehler ist es ebenfalls, zu einem Winkel von 359 Grad ein Grad zu addieren, denn man würde ja den Wertebereich verlassen. Aber wäre es nicht praktischer, wieder bei 0 Grad anzukommen? Das kann in Ada mit sogenannten modularen Typen erreicht werden:



Diese Deklaration definiert wieder einen Typ mit einem Wertebereich von 0 bis 359, jetzt werden aber Berechnungen mit diesem Typ modular ausgeführt:



Diese numerischen Typen sind ein Beispiel dafür, wie Ada es ermöglicht, näher an der zu lösenden Aufgabenstellung zu sein als mit vielen andere Programmiersprachen. Natürlich kann für einen Winkel einfach eine 16-Bit-Variable verwendet werden, dann muss aber überall überprüft werden, dass Berechnungen korrekt sind und keine unsinnigen Winkel berechnet werden.

Ada ermöglicht es Programmierern zu dokumentieren, was diese 16-Bit-Variable (denn auch in Ada wird der Compiler vermutlich 16 Bit für unseren Winkel reservieren) darstellen soll; der Compiler beziehungsweise die Laufzeitchecks nehmen die nötigen Überprüfungen automatisch vor.

Diese numerischen Typen sind ein Beispiel dafür, wie Ada es Programmierern leichter macht, in der Problemdomäne zu bleiben, in der die Begriffe des zu lösenden Problems verwendet werden (Winkel, Temperatur, Geschwindigkeit und so weiter), statt gleich in die Lösungsdomäne zu wechseln, wo andere Begriffe wichtig sind, zum Beispiel die Auswahl zwischen 8 Bit oder 16 Bit für den Winkel. Der nächste Abschnitt ist ebenfalls ein Beispiel dafür.

Ada - Representation Clauses

Eines der Probleme der Embedded-Programmierung ist, dass einerseits hardwarenahe Programmierung und bitgenaue Auslegung der Daten nötig sind, andererseits solche Details eigentlich einfachen Code umständlich und fehleranfällig machen. Die Antwort auf dieses Problem in Ada sind Representation Clauses. Diese ermöglichen es, die bekannten Datenstrukturen wie Arrays und Records wie gewünscht im Speicher auszulegen und sie effizient und einfach zu benutzen. Ein einfaches Beispiel wäre:



Die erste Zeile definiert einen Typ von Arrays, die genau 8 Boolesche Werte enthalten. Normalerweise hat der Compiler eine gewisse Wahl, wie viel Speicher genau für ein solches Array verwendet wird. Aus Effizienzgründen reserviert der Compiler zum Beispiel 8 Byte, also ein Byte pro Booleschem Wert.

Die zwei weiteren Zeilen erklären dem Compiler aber, nur 8 Bit, also 1 Byte, zu verwenden - genau 1 Bit für jeden Booleschen Wert. Das kann notwendig sein, wenn der Speicher auf dem Embedded-Chip knapp ist oder wenn eine Schnittstelle (zur Hardware oder zum Beispiel ein Kommunikationsprotokoll) die Auslegung von Daten eben genau so verlangt.

In C kann man zwar auch ein Byte für ein solches Array reservieren. Um damit umzugehen, sind dann aber Bitmasken und Bitshifts nötig - dies ist fehleranfällig und verschleiert, dass der Code einfach nur ein Array manipuliert. In Ada können solche Arrays wie oben definiert im Weiteren ganz normal verwendet werden - mit Zugriff auf jeden beliebigen Index. Der Compiler generiert automatisch den korrekten Code. Representation Clauses ermöglichen noch viel mehr, als dieses einfache Beispiel zeigt, und sind ein unverzichtbares Werkzeug für hardwarenahe Ada-Programmierer.

Ada 2012 - Design by Contract

Seit der Ada-2012-Sprachversion unterstützt Ada Design by Contract. Diese Art der Programmierung umfasst in der Regel eine Reihe von Sprachfeatures ähnlich den Assertions. Zum Beispiel kann man in Ada mit dem Schlüsselwort "Pre" einer Funktion eine sogenannte Precondition (Vorbedingung) hinzufügen, also eine Bedingung, die vor der Ausführung der Funktion zutreffen soll. In diesem Beispiel soll die Prozedur Put_Line nur dann aufgerufen werden, wenn der übergebene Datei-Handle auch wirklich zu einer offenen Datei zeigt:



Diese Precondition funktioniert wie eine Assertion am Anfang der Funktion oder wie zusätzlicher Code am Anfang der Funktion, der eine bestimmte Bedingung überprüft und abbricht, falls die Bedingung nicht zutrifft (das nennt man auch Defensive Code). Der Unterschied ist aber, dass die Precondition zur Spezifikation gehört und nicht zur Implementation, wie es der Fall für die Assertion oder den Defensive Code wäre.

Dies hat einige Vorteile. Zum einen, zum Beispiel im Fall einer API-Funktion einer Bibliothek, ist die Precondition auch für Benutzer der API sichtbar, während die anderen Ansätze letztendlich ein Implementationsdetail bleiben. Damit kann die Precondition auch als Dokumentation für akzeptable Aufrufe der Funktion dienen. Zum anderen kann die Precondition, ähnlich wie Assertions in anderen Sprachen, für einen Release-Build abgeschaltet werden, um effizienteren Code zu erhalten. Defensive Code wird immer mitkompiliert. Schließlich kann die Precondition auch von anderen Tools verwendet werden. Insbesondere Spark wird mithilfe von Contracts zu einem mächtigen Werkzeug.

Analog zu Preconditions gibt es auch Postconditions, die konzeptuell direkt nach dem Return der Funktion überprüft werden. Der Name Design by Contract kommt von dem Zusammenspiel von Pre- und Postcondition. Hat der Programmierer beide zu einer Funktion hinzugefügt, fungieren sie wie ein Vertrag zwischen aufrufender und aufgerufener Funktion. Die aufrufende Funktion muss gemäß diesem Vertrag die Precondition garantieren und bekommt im Gegenzug von der aufgerufenen Funktion die Postcondition garantiert. Es gibt noch einige andere Formen von Assertions, sie zu beschreiben würde aber an dieser Stelle zu weit führen.

Spark kann automatisch potenzielle Fehler anzeigen

Spark ist eine Teilmenge von Ada. Das heißt, Spark ist im Wesentlichen die gleiche Sprache wie Ada, auch die unterstützenden Werkzeuge wie IDE und Compiler sind gleich. Jedoch müssen einige Sprachfeatures von Ada in Spark zusätzlichen Regeln folgen. Zum Beispiel können Exceptions zwar ausgelöst, aber nicht behandelt werden, Zeiger müssen einem Rust-ähnlichen Ownership-Modell folgen, und so weiter.

Als Belohnung für die Einhaltung dieser strikten Regeln erhalten Spark-Programmierer ein neues Werkzeug: die Möglichkeit der formalen Verifikation. Diese kommt in Form eines zusätzlichen Menüs in der Entwicklungsumgebung daher. Führt der Programmierer mithilfe dieses Menüs die Verifikation durch, kann Spark automatisch potenzielle Programmierfehler wie arithmetische Überläufe und Pufferüberläufe signalisieren.

Hat der Programmierer Pre- und Postconditions hinzugefügt, werden diese in den Verifikationsprozess einbezogen und möglicherweise inkorrekte Verträge auch signalisiert. Wenn Spark keine Fehler findet, dann heißt das erstens, dass das Programm frei von Programmierfehlern ist, wie eben arithmetische Überläufe und Pufferüberläufe, Division durch 0 und so weiter, und das für alle möglichen Eingaben des Programms. Zweitens sind alle Pre- und Postconditions korrekt, das gilt ebenso für alle möglichen Eingaben.

Insbesondere Postconditions können auch funktionale Eigenschaften ausdrücken, so dass mit Spark Software geschrieben werden kann, die genauso funktioniert, wie sie soll.

Software-Sicherheit in Ada und Rust

Sowohl Ada als auch Rust versprechen mehr Sicherheit als C. Wer genauer hinsieht, sieht aber große Unterschiede. Der große Vorteil von Rust ist die Memory Safety. Das innovative Typsystem von Rust kann sogenannte Use-after-free-Fehler, wo Programmierer auf eigentlich schon freigegebenen Speicher zugreifen, komplett ausschließen, ebenso wie Race Conditions, bei denen mehrere Threads in den gleichen Speicherbereich schreiben wollen.

Memory Safety ist aber nur ein Teil der Softwaresicherheit. Andere mögliche Fehlerquellen sind die schon genannten arithmetischen Überläufe und Pufferüberläufe - und natürlich die funktionale Sicherheit (also: Macht die Software, was sie soll?). Für arithmetische Korrektheit und Überläufe hat Rust dynamische Laufzeitchecks, für funktionale Sicherheit gibt es in Rust keinen Mechanismus.

Adas Typsystem zur Vermeidung von Use-after-free ist weniger weitreichend als das von Rust und kann auch keine so starken Garantien geben. Für Laufzeitfehler werden auch bei Ada dynamische Laufzeitchecks eingesetzt. Durch die flexiblen numerischen Typen sind diese Checks aber viel nützlicher. Die Ada 2012 Contracts machen aus Ada eine der ganz wenigen systemnahen Programmiersprachen, die Mechanismen zum Erreichen der funktionalen Sicherheit enthalten. Ada punktet auch durch die hohe Lesbarkeit, die effektivere Codereviews ermöglicht.

Kurz gefasst könnte man sagen, dass Ada den Begriff der Softwaresicherheit viel weiter fasst, während Rust in der enger definierten Memory Safety einen besseren, da völlig statischen Mechanismus integriert.

Spark übertrifft sowohl Ada als auch Rust bei weitem: Es kann auf den weitreichenden Fähigkeiten von Ada aufbauen, ermöglicht aber eine statische Verifikation statt dynamischer Laufzeitchecks. Programmierfehler wie Pufferüberläufe und arithmetische Überläufe können komplett ausgeschlossen werden, Zeiger können dank des Rust-ähnlichen Modells ebenfalls keine Probleme machen. Spark ist damit auch in der Memory Safety so sicher wie Rust. Durch Ada Design by Contract kann auch die funktionale Sicherheit formuliert und mithilfe der Spark-Tools statisch erreicht werden. Einzig sogenannte nichtfunktionale Fehler wie die Ausschöpfung des Stack- oder Speicherbereichs müssen noch durch andere Mittel erkannt werden.

Wer Sicherheit braucht, sollte sich Ada ansehen

Die Programmiersprache Ada galt lange als wenig attraktiv und die von C sehr verschiedene Syntax schreckte viele Interessenten ab. Doch der Trend zu sicheren Programmiersprachen macht Ada zu einem aussichtsreichen Kandidaten. Dank des umfassenden Sicherheitskonzepts und innovativer Technologien wie Spark ist Ada nicht zu ignorieren und wird vermehrt in Umgebungen mit hohen Anforderungen an die Sicherheit und Cyber Security eingesetzt. Für solche Anwendungen oder Anwendungen im Embedded-Bereich ist Ada auf jeden Fall einen Blick wert.  (jkn)


© 1997–2019 Golem.de, https://www.golem.de/