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. Digital Operation Manager (m/w/d)
    Bundeskriminalamt, Wiesbaden
  2. IT-Mitarbeiter (m/w/d) First-Level-Support
    Stadtwerke Emmendingen GmbH, Emmendingen
Detailsuche

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

Golem Akademie
  1. Advanced Python – Fortgeschrittene Programmierthemen: virtueller Zwei-Tage-Workshop
    27.–28. Januar 2022, Virtuell
  2. C++ Programmierung Basics: virtueller Fünf-Tage-Workshop
    13.–17. Dezember 2021, virtuell
Weitere IT-Trainings

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


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...



Aktuell auf der Startseite von Golem.de
Wemax Go Pro
Mini-Projektor für Reisen strahlt 120-Zoll-Bild an die Wand

Der Wemax Go Pro setzt auf Lasertechnik von Xiaomi. Der Beamer ist klein und kompakt, soll aber ein großes Bild an die Wand strahlen können.

Wemax Go Pro: Mini-Projektor für Reisen strahlt 120-Zoll-Bild an die Wand
Artikel
  1. Snapdragon 8cx Gen 3: Geleaktes Qualcomm-SoC erreicht das Niveau von AMD und Intel
    Snapdragon 8cx Gen 3
    Geleaktes Qualcomm-SoC erreicht das Niveau von AMD und Intel

    In Geekbench wurde der Qualcomm Snapdragon 8cx Gen 3 gesichtet. Er kann sich mit Intel- und AMD-CPUs messen, mit Apples M1 aber wohl nicht.

  2. Air4: Renault 4 als Flugauto neu interpretiert
    Air4
    Renault 4 als Flugauto neu interpretiert

    Der Air4 ist Renaults Idee, wie ein fliegender Renault 4 aussehen könnte. Mit der Drohne wird das 60jährige Jubiläum des Kultautos gefeiert.

  3. MS Satoshi: Die abstruse Geschichte des Bitcoin-Kreuzfahrtschiffs
    MS Satoshi
    Die abstruse Geschichte des Bitcoin-Kreuzfahrtschiffs

    Kryptogeld-Enthusiasten kauften ein Kreuzfahrtschiff und wollten es zum schwimmenden Freiheitsparadies machen. Allerdings scheiterten sie an jeder einzelnen Stelle.
    Von Elke Wittich

Du willst dich mit Golem.de beruflich verändern oder weiterbilden?
Zum Stellenmarkt
Zur Akademie
Zum Coaching
  • Schnäppchen, Rabatte und Top-Angebote
    Die besten Deals des Tages
    Daily Deals • Black Friday Wochenende • LG UltraGear 34GP950G-B 999€ • SanDisk Ultra 3D 500 GB M.2 44€ • Boxsets (u. a. Game of Thrones Blu-ray 79,97€) • Samsung Galaxy S21 128GB 777€ • Premium-Laptops (u. a. Lenovo Ideapad 5 Pro 16" 829€) • MS Surface Pro7+ 888€ • Astro Gaming Headsets [Werbung]
    •  /