• IT-Karriere:
  • Services:

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. Stadt Cuxhaven, Cuxhaven
  2. SySS GmbH, Tübingen, Frankfurt am Main, München, Wien (Österreich)

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.

Bitte aktivieren Sie Javascript.
Oder nutzen Sie das Golem-pur-Angebot
und lesen Golem.de
  • ohne Werbung
  • mit ausgeschaltetem Javascript
  • mit RSS-Volltext-Feed
 Ada - Representation Clauses
  1.  
  2. 1
  3. 2
  4. 3
  5. 4


Anzeige
Top-Angebote
  1. 27,90€ (zzgl. Versand)
  2. 79,00€ (zzg. 1,99€ Versand)
  3. 129,99€ (Release am 2. Juni)
  4. (u. a. Akku Stichsäge für 134,99€, Akku Säbelsäge für 137,99€, Akku Winkelschleifer für...

demon driver 25. Jun 2019

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

demon driver 24. Jun 2019

Nix

SirFartALot 13. Jun 2019

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

\pub\bash0r 12. Jun 2019

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

kayozz 12. Jun 2019

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


Folgen Sie uns
       


TES Morrowind (2002) - Golem retro_

Eine gigantische Spielwelt umgeben von Pixelshader-Wasser: The Elder Scrolls 3 Morrowind gilt bis heute als bester Teil der Serie. Trotz sperriger Bedienung war Morrowind dank der dichten Atmosphäre, der spielerischen Freiheit und der exzellenten Grafik ein RPG-Meilenstein.

TES Morrowind (2002) - Golem retro_ Video aufrufen
Amazon, Netflix und Sky: Disney bringt 2020 den großen Umbruch beim Videostreaming
Amazon, Netflix und Sky
Disney bringt 2020 den großen Umbruch beim Videostreaming

In diesem Jahr wird sich der Video-Streaming-Markt in Deutschland stark verändern. Der Start von Disney+ setzt Netflix, Amazon und Sky gehörig unter Druck. Die ganz großen Umwälzungen geschehen vorerst aber woanders.
Eine Analyse von Ingo Pakalski

  1. Peacock NBC Universal setzt gegen Netflix auf Gratis-Streaming
  2. Joyn Plus+ Probleme bei der Kündigung
  3. Android TV Magenta-TV-Stick mit USB-Anschluss vergünstigt erhältlich

Fitnesstracker im Test: Aldi sportlich abgeschlagen hinter Honor und Mi Band 4
Fitnesstracker im Test
Aldi sportlich abgeschlagen hinter Honor und Mi Band 4

Alle kosten um die 30 Euro, haben ähnliche Funktionen - trotzdem gibt es bei aktuellen Fitnesstrackern von Aldi, Honor und Xiaomi spürbare Unterschiede. Als größte Stärke des Geräts von Aldi empfanden wir kurioserweise eine technische Schwäche.
Von Peter Steinlechner

  1. Wearable Acer und Vatikan präsentieren smarten Rosenkranz
  2. Apple Watch Series 5 im Test Endlich richtungsweisend
  3. Suunto 5 Sportuhr mit schlauem Akku vorgestellt

Kailh-Box-Switches im Test: Besser und lauter geht ein klickender Switch kaum
Kailh-Box-Switches im Test
Besser und lauter geht ein klickender Switch kaum

Wer klickende Tastatur-Switches mag, wird die dunkelblauen Kailh-Box-Schalter lieben: Eine eingebaute Stahlfeder sorgt für zwei satte Klicks pro Anschlag. Im Test merken unsere Finger aber schnell den hohen taktilen Widerstand.
Ein Test von Tobias Költzsch

  1. Keychron K6 Kompakte drahtlose Tastatur mit austauschbaren Switches
  2. Charachorder Schneller tippen als die Tastatur erlaubt
  3. Brydge+ iPad-Tastatur mit Multi-Touch-Trackpad

    •  /