Abo
  • IT-Karriere:

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.

Stellenmarkt
  1. Infokom GmbH, Karlsruhe
  2. Lidl Dienstleistung GmbH & Co. KG, Neckarsulm

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.

 Ada - Representation Clauses
  1.  
  2. 1
  3. 2
  4. 3
  5. 4


Anzeige
Top-Angebote
  1. (aktuell u. a. HP 14-Zoll-Notebook für 389,00€, Asus ROG 27-Zoll-Monitor für 689,00€, Corsair...
  2. 26,99€ (Release am 26. Juli)
  3. 339,00€
  4. 269,00€

demon driver 25. Jun 2019 / Themenstart

Von "unabgängiger" kann sich niemand was kaufen, und konsequent dürfte man dann nur noch...

demon driver 24. Jun 2019 / Themenstart

Nix

SirFartALot 13. Jun 2019 / Themenstart

das mag ja fuer Auftragsprogrammierer oder Freelancer normal zu sein, die...

\pub\bash0r 12. Jun 2019 / Themenstart

Wobei ausgerechnet Java (und Applets) eigentlich ein sehr gutes Sicherheitsmodell haben...

kayozz 12. Jun 2019 / Themenstart

Ja, C# bzw. .NET hat auch Schwächen. Aber das Argument würde ich so nicht stehen...

Kommentieren


Folgen Sie uns
       


CO2-Emissionen und Lithium: Ist das Elektroauto wirklich ein Irrweg?
CO2-Emissionen und Lithium
Ist das Elektroauto wirklich ein Irrweg?

In den vergangenen Monaten ist die Kritik an batteriebetriebenen Elektroautos stärker geworden. Golem.de hat sich die Argumente der vielen Kritiker zur CO2-Bilanz und zum Rohstoff-Abbau einmal genauer angeschaut.
Eine Analyse von Friedhelm Greis

  1. Reichweitenangst Mit dem E-Auto von China nach Deutschland
  2. Ari 458 Elektro-Lieferwagen aus Leipzig kostet knapp 14.000 Euro
  3. Nobe 100 Dreirädriges Retro-Elektroauto parkt senkrecht an der Wand

Super Mario Maker 2 & Co.: Vom Spieler zum Gamedesigner
Super Mario Maker 2 & Co.
Vom Spieler zum Gamedesigner

Dreams, Overwatch Workshop und Super Mario Maker 2: Editoren für Computerspiele werden immer mächtiger, inzwischen können auch Einsteiger komplexe Welten bauen. Ein Überblick.
Von Achim Fehrenbach

  1. Nintendo Switch Wenn die Analogsticks wandern
  2. Nintendo Akku von überarbeiteter Switch schafft bis zu 9 Stunden
  3. Hybridkonsole Nintendo überarbeitet offenbar Komponenten der Switch

In eigener Sache: Zeig's uns!
In eigener Sache
Zeig's uns!

Golem kommt zu dir: Golem.de möchte noch mehr darüber wissen, was IT-Profis in ihrem Berufsalltag umtreibt. Dafür begleitet jeder unserer Redakteure eine Woche lang ein IT-Team eines Unternehmens. Welches? Dafür bitten wir um Vorschläge.

  1. In eigener Sache Golem.de bietet Seminar zu TLS an
  2. In eigener Sache ITler und Board kommen zusammen
  3. In eigener Sache Herbsttermin für den Kubernetes-Workshop steht

    •  /