Original-URL des Artikels: https://www.golem.de/news/programmiersprachen-ada-und-spark-sind-sicherer-als-c-2009-150220.html    Veröffentlicht: 01.09.2020 12:07    Kurz-URL: https://glm.io/150220

Programmiersprachen

Ada und Spark sind sicherer als C

Bei der Programmierung von sicherheitsrelevanter Software ist C immer noch beliebt. Sollte es aber nicht, denn Ada und Spark sind gerade für diesen Bereich viel besser geeignet.

Bei der Auswahl einer bestimmten Programmiersprache für ein Projekt spielen oft Faktoren wie die Vertrautheit mit der Sprache, die verfügbaren Werkzeuge sowie die Community eine große Rolle. Viel zu selten wird aber die Eignung der Sprache selbst für die Aufgabe zur Entscheidungsfindung hinzugezogen. Dabei hat jede Programmiersprache Vor- und Nachteile und bestimmte Anwendungsgebiete, in denen sie einfach eine bessere (oder schlechtere) Wahl wäre.

In diesem Artikel wollen wir speziell darauf eingehen, wie Programmiersprachen in sicherheitsrelevanter Software helfen können, bestimmte Ziele der Software zu erreichen. Dabei konzentrieren wir uns auf Ada und Spark, weil wir sie in diesem Kontext für besonders geeignet halten, und stellen sie C gegenüber, das in der Praxis (leider noch) zu oft die Wahl ist.

Was sind Ada und Spark?

Ada ist eine prozedurale Programmiersprache, sie wurde in den 1970er Jahren entwickelt und zuerst 1983 standardisiert. Seitdem wurde sie kontinuierlich weiterentwickelt; die letzte Version ist Ada 2012, die nächste wird wohl kommendes Jahr erscheinen.

Die Sprachfeatures ähneln auf den ersten Blick jenen von C++ oder Java: Es kann auf Objekte sowie Generics zugegriffen werden, es gibt ein umfangreiches Modulsystem. Ein großer Unterschied ist die Syntax. Ada legt großen Wert auf Lesbarkeit und Fehlervermeidung und benutzt auch nicht die für C typischen geschweiften Klammern.

Spark ist eine Schwestersprache von Ada, die einige zusätzliche Einschränkungen einführt. Diese Einschränkungen ermöglichen weitreichende Analysen von Spark-Code und garantieren mehr Sicherheit.

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 von der Webseite von Adacore heruntergeladen und installiert werden. In der Entwicklungsumgebung mit dem Namen GNATStudio können Interessierte entweder ihr eigenes Programm schreiben (Create New Project im ersten Dialog) oder die vielen Beispiele ansehen (im Menu Help -> GNAT -> Examples).

"Security" ist nicht gleich "Safety"

Immer mehr Software hat heutzutage große Auswirkungen auf unser Leben. Sei es, weil menschliche Leben direkt davon abhängen, etwa bei der Steuerungssoftware eines Flugzeugs oder Pkw, oder sei es, weil große Geldbeträge im Spiel sind, etwa in Bankensystemen. Im Englischen wird hier der Begriff "Safety" verwendet.

In manchen Anwendungsszenarien muss auch die Software selbst vor böswilligen oder unbefugten Eingriffen geschützt werden. Oder sie muss auch dann funktionieren, wenn den Eingaben nicht vertraut werden kann. Hier hat sich im Englischen der Begriff "Security" durchgesetzt. Im Deutschen wird meistens für beides der Begriff "Sicherheit" verwendet.

Moderne Ansätze des Softwaredesigns insbesondere in der Security gehen von einer modularen Architektur aus: Die Software wird in kleine Einheiten geteilt, die unterschiedliche Aufgaben haben und unterschiedlich kritisch sind. Jedes Modul hat andere Anforderungen, die die Software möglichst gut erfüllen soll.



Die Sprache nach den Anforderungen aussuchen

Zum Beispiel soll ein Modul eine Benutzereingabe validieren und zur weiteren Verarbeitung weiterleiten. Dieses Modul wird also eine Reihe von Anforderungen zur Validation enthalten sowie Informationen, wohin die Daten befördert werden sollen. Zusätzlich sollte das Modul aber frei von Programmierfehlern sein und insbesondere keine Angriffsflächen wie Pufferüberläufe bieten. Denn das Modul liest direkt Eingaben von potenziell böswilligen Benutzern.

Es gibt eine Klassifizierung von Softwarebugs, genannt CWE, mit Hunderten von Einträgen wie Pufferüberlauf, Dereferenzierung von Nullzeigern und so weiter. Für ein sicherheitskritisches Modul wie das der Eingabevalidierung würde man sie gerne alle vermeiden. Oder zumindest die meisten. Oder wenigstens die häufigsten.

Nach der Einteilung der Software in Module und der Erstellung von Anforderungen für jedes Modul kann im Prinzip mit der Programmierung angefangen werden. Vorher aber sollte man sich fragen: Wie können die Anforderungen am besten und effizientesten eingesetzt werden? Und: Spielt dabei die Wahl der Programmiersprache eine Rolle?

Warum nicht einfach C?

Die Programmiersprache C ist gerade in den Bereichen, in denen Sicherheit am wichtigsten ist, also in der eingebetteten Programmierung sowie Kryptographie, immer noch extrem beliebt. Dabei ist die Sprache dafür gar nicht wirklich gut geeignet. Es gibt einfach zu viele Fehlerquellen.

Die Liste ist lang, hier nur einige Beispiele: Textuelle Inklusion mit #include sowie allgemein der textbasierte Preprozessor machen es schwer, Definitionen zu finden, zu sehen, welcher Code aktiv ist, und manchmal auch, was Code eigentlich bedeutet (insbesondere Makros, die anstelle von Funktionen verwendet werden).

Syntaktische Eigenheiten wie die Zuweisung mit, if-Statements, switch-Statements sowie Schleifen, bei denen mit optionalem Ende-Marker nicht klar ist, wo sie aufhören, machen den Code weniger lesbar und Fehler damit schlechter auffindbar. Gleiches gilt für Abkürzungen wie "i++", deren einziger Vorteil es ist, dass sie einfach zu schreiben sind.

Viele C-Programmierer haben diese Schwächen erkannt, möchten oder können aber nicht die Sprache wechseln. So hat zum Beispiel der Linux-Kernel-Entwickler Kees Cook in einem Vortrag mit dem Titel Making C Less Dangerous Vorschläge gemacht, wie manche der Probleme umgangen werden können. Im eingebetteten Bereich ist der Standard MISRA-C beliebt, der die gefährlichsten C-Konstrukte verbietet.

Die meisten und die am weitesten verbreiteten CWE-Einträge - Ausnahmen sind Bugs, die speziell in Webtechnologien relevant sind, wie Cross-site Scripting - sind in C nicht nur möglich, sondern fast an der Tagesordnung. Ist die Vermeidung von Sicherheitslücken wie CWE ein Ziel, dann ist die Benutzung von C kontraproduktiv.

Ada und C im Vergleich

Ada versucht, eine möglichst klare, lesbare und von Stolpersteinen freie Syntax anzubieten - und vermeidet dabei die größten Probleme der C-Syntax. Die Tabelle gibt einen Überblick, wie die typischen Stolpersteine in C in Ada vermieden werden.



Die Vorteile von Ada gehen jedoch über solche syntaktischen Verbesserungen hinaus. Das Typsystem von Ada ist deutlich besser und strenger, es kann viele Fehler sehr zeitig entdecken. Arrays sind Teil des Typsystems und enthalten ihre Länge, so dass Verwirrung über den belegten Speicherbereich viel seltener ist.

Ein weiteres Feature von Ada sind Laufzeitüberprüfungen. Wenn in C eine Integer-Variable mit Vorzeichen ihren Wertebereich überschreitet, geht die Ausführung in der Regel einfach mit einem falschen Wert weiter. In Ada wird der Überlauf zur Laufzeit entdeckt und eine Exception ausgelöst.



Das Gleiche gilt für die Division durch null, Zugriffe auf Arrays außerhalb der Indexgrenzen, sogenannte Pufferüberläufe und mehr. Für Informationssicherheit sowie Testläufe ist das sehr wertvoll. Denn in der Regel ist es besser, dass die Software abstürzt, als dass ein Angreifer eindringen kann, denn Pufferüberläufe sind oft auch Sicherheitslücken.

In eingebetteten Systemen, wo in der Regel kein Absturz erwünscht ist, können diese Überprüfungen für Produktionscode auch ausgeschaltet werden.

... und was ist jetzt Spark?

Spark ist eine Teilmenge von Ada, jedes Spark-Programm ist auch ein gültiges Ada-Programm. Spark ist also im Wesentlichen die gleiche Sprache wie Ada, die Werkzeuge wie IDE und Compiler sind auch identisch.

Es gibt jedoch in Spark einige zusätzliche Regeln, die befolgt werden müssen. Das Ziel von Spark ist dabei, Ada so zu beschränken, dass Spark-Programme mehr Garantien bieten können, als es für normale Ada-Programme möglich wäre.

Als Belohnung für die Einhaltung dieser strikten Regeln gibt es beim Programmieren in Spark ein neues Werkzeug: die Möglichkeit der formalen Verifikation. Sie kommt in Form eines zusätzlichen Menüs in der Entwicklungsumgebung. Wird mithilfe dieses Menüs die Verifikation durchgeführt, kann Spark automatisch potenzielle Programmierfehler wie arithmetische Überläufe und Pufferüberläufe signalisieren. Meldet Spark keine Fehler, dann können die von Spark überprüften Fehlersituationen nicht auftreten - und das gilt für alle möglichen Eingaben des Programms.

Spark ermöglicht auch das Hinzufügen sogenannter Verträge. Das sind Bedingungen, die vor beziehungsweise nach der Ausführung einer Funktion gültig sein sollen. Im Idealfall kann man hier direkt Anforderungen an die Software ausdrücken.

Wurden Verträge hinzugefügt, werden diese in den Verifikationsprozess einbezogen und möglicherweise inkorrekte Verträge signalisiert. Wieder gilt: Wenn Spark keine Fehler findet, dann sind diese Bedingungen korrekt, und zwar für alle möglichen Eingaben des Programms.

C, Ada und Spark kombinieren

C, Ada und Spark schließen sich gegenseitig nicht aus. Im Gegenteil: Es kann viel Sinn ergeben, Ada, Spark und C zusammen einzusetzen.

Zum Beispiel könnte Ada als Basis ausgewählt werden, denn es bietet einen guten Kompromiss zwischen Sicherheit und Komfort. Spark wäre für hochkritische Teile des Produkts am besten geeignet.

Mancher Code muss ohnehin in C sein, um zum Beispiel gewisse Systemaufrufe oder Bibliotheken benutzen zu können. Ein ähnliches Konzept wurde zum Beispiel im Wookey-Projekt umgesetzt, das auch Rust für einige Komponenten verwendet.



Fazit

Zu oft steht die Wahl der Programmiersprache entweder schon vor Projektstart fest oder es wird sehr zeitig im Projekt nach externen Faktoren entschieden. Zu selten werden jedoch die Anforderungen der Software selbst zur Entscheidung hinzugezogen. In sicherheitsrelevanten Bereichen ist das fatal, denn gerade die oft gewählte Programmiersprache C ist dafür nicht so gut geeignet, es gibt bessere Lösungen.

Moderne Programmiersprachen können durch Vermeidung ganzer Klassen von Fehlern direkt zur Erfüllung von Software-Anforderungen beitragen. Nämlich genau dann, wenn die Vermeidung von solchen Fehlern Teil der Anforderungen ist. Mit fortgeschrittenen Technologien wie Spark können sogar funktionale Anforderungen für alle Eingaben garantiert werden.

Johannes Kanig ist Experte für statische Analysen und Formale Verifikation. Seit 2011 ist er Senior Software Engineer bei AdaCore und entwickelt dort die Spark-Software zur formalen Verifikation von Ada- und Spark-Programmen. Er schreibt regelmäßig Artikel über Ada und Spark auf Basis seiner umfangreichen Erfahrung.  (jkn)


Verwandte Artikel:
Dan Kaminsky: Sichere Zufallszahlen zum Standard machen   
(10.08.2014, https://glm.io/108469 )
BASIC: GOTO 50   
(01.05.2014, https://glm.io/106183 )
Tiobe Index: Objective-C mit höchster Steigerung   
(09.01.2012, https://glm.io/88903 )

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