• 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. targens GmbH, München, Stuttgart
  2. TenneT TSO GmbH, Bayreuth

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
    3./4. Mai 2021, online
  2. Python kompakt - Einführung für Softwareentwickler
    19./20. April 2021, online
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


Anzeige
Hardware-Angebote
  1. (u. a. PS5 + HD Kamera für 549,99€)

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
       


Gopro Hero 9 Black - Test

Ist eine Kamera mit zwei Displays auch doppelt so gut?

Gopro Hero 9 Black - Test Video aufrufen
Programm für IT-Jobeinstieg: Hoffen auf den Klebeeffekt
Programm für IT-Jobeinstieg
Hoffen auf den Klebeeffekt

Aktuell ist der Jobeinstieg für junge Ingenieure und Informatiker schwer. Um ihnen zu helfen, hat das Land Baden-Württemberg eine interessante Idee: Es macht sich selbst zur Zeitarbeitsfirma.
Ein Bericht von Peter Ilg

  1. Arbeitszeit Das Sechs-Stunden-Experiment bei Sipgate
  2. Neuorientierung im IT-Job Endlich mal machen!
  3. IT-Unternehmen Die richtige Software für ein Projekt finden

Weclapp-CTO Ertan Özdil: Wir dürfen nicht in Schönheit und Perfektion untergehen!
Weclapp-CTO Ertan Özdil
"Wir dürfen nicht in Schönheit und Perfektion untergehen!"

Der CTO von Weclapp träumt von smarter Software, die menschliches Eingreifen in der nächsten ERP-Generation reduziert. Deutschen Perfektionismus hält Ertan Özdil aber für gefährlich.
Ein Interview von Maja Hoock


    Fiat 500 als E-Auto im Test: Kleinstwagen mit großem Potenzial
    Fiat 500 als E-Auto im Test
    Kleinstwagen mit großem Potenzial

    Fiat hat einen neuen 500er entwickelt. Der Kleine fährt elektrisch - und zwar richtig gut.
    Ein Test von Peter Ilg

    1. Vierradlenkung Elektrischer GMC Hummer SUV fährt im Krabbengang seitwärts
    2. MG Cyberster MG B Roadster mit Lasergürtel und Union Jack
    3. Elektroauto E-Auto-Prämie übersteigt in 2021 schon Vorjahressumme

      •  /