Ja, Programmverifikation mit Spark, zwei wichtige Sachen. Es geht nicht um Apache Spark und es

geht auch nicht um die Computerarchitektur Spark, das wird ganz verwechselt, sondern es geht um die Programmiersprache. Was kurzes zu mir, ich studiere Informationssystemtechnik an der TU. Ich arbeite seit letztem Jahr für die Componolid GmbH, hauptsächlich in der Betriebssystem oder Treiberentwicklung mit Ada, Spark und auch C und C++. Wir

entwickeln sichere komponentenbasierte Systeme im Mobilbereich, im Industriebereich, dass es soweit es möglich ist auf Basis freier Software und wir entwickeln auch selbstfreie Software in offener Entwicklung. Das heißt, wir können uns dann auch auf GitHub folgen, wenn ihr das wollt. Und wir haben uns überlegt, für sichere Systeme brauchen

wir eine sichere Programmiersprache und sind an der Stelle zu Ada gekommen. Ada ist ein ISO-Standard, der existiert schon seit 1987. Der ist kontinuierlich erweitert worden, sodass wir heutzutage eine moderne Sprache haben, die Objektorientierung unterstützt,

die Generics unterstützt und was ganz wichtig in dem Bereich ist, sie unterstützt extensive Compile- und Runtime-Checks. Und wir haben ein sehr, sehr starkes Typsystem, eine einfache Integration in das C for a Function Interface, das heißt, wir können einfach mit in C geschriebenen Binaries interagieren und wir haben

Contract-based Programming. Contract-based Programming heißt, ich habe Verträge an meiner Software, an die ich mich halten muss. Hier ist ein Beispiel aus C. Ich habe die Funktion Apps, die gibt mir den Absolutwert der Eingabe zurück. Das steht in dem Kommentar und das ist ein Kommentar, der wird vom Compiler von allen Sachen

ignoriert. Zum Vergleich dazu Ada. Ich habe die Funktion Apps Value, die tut genau das Gleiche und die hat einen sogenannten Aspect, das heißt, dieser Aspect ist in diesem Fall eine sogenannte Nachbedingung, die angibt, dass das Result der Funktion

Apps Value größer gleich Null sein darf und für den Fall, dass das nicht passiert, würde ich einen Fehler bekommen. Die Implementierung der Funktion Apps in C ist recht einfach. Wenn j größer als Null ist, geben wir j zurück, sonst geben wir minus j zurück. Das funktioniert für minus eins einwandfrei, es funktioniert auch für eins

einwandfrei und für Null. Und es gibt einen Fall, für den das nicht funktioniert. Vielleicht hat jemand eine Idee. Der Integer, der ist nicht symmetrisch und für den kleinsten möglichen Integer Wert, zwei hoch minus 32, gibt es keine positive

Darstellung. Das heißt, die größte mögliche Darstellung ist zwei hoch 32 minus eins. Das heißt, bei dieser Operation läuft der Integer über und wir bekommen den Negativwert dazu zurück. So sieht die gleiche Funktion in

Ada aus. Okay, die Erwartung ist, ich bekomme jetzt den Fehler, dass meine Ausgabe nicht mehr nicht positiv ist. Wir schaffen es aber gar nicht bis dahin, denn Ada hat auch Overflow-Checks auf Integer-Werten und der der Integer an der Stelle minus j überläuft für diesen Wert, beendet das

Programm bereits an der Stelle. So, jetzt können wir unsere Software testen. Software-Tests sind trotzdem wichtig, wir brauchen diese für Integration. Wir müssen validieren, dass die Ideen hinter der Software die richtigen sind, aber wir können niemals alle Werte testen. Also schon für die

einfache Funktion Apps hätten wir über vier Milliarden mögliche Eingabewerte. Wenn wir jetzt zwei Zahlen addieren wollen, dann haben wir vier Milliarden mal vier Milliarden mögliche Eingabewerte und für jede nicht triviale Software wird es einfach so viel, dass es nicht mehr testbar ist. Und selbst das Testen unter besten Bedingungen schafft im besten Fall

ein Fehler alle 1000 Zeilen Code und mit formalen Methoden können wir bis zu 50 bis 100 fach besser werden als das. Das heißt, wir hätten dann einen Fehler auf 100.000 Zeilen Code, was uns die Möglichkeit gibt, auch größere Software-Projekte tatsächlich fehlerfrei zu implementieren. Jetzt

kommen wir zum eigentlichen Thema des Vortrags Spark. Spark ist ein Subset von Ada. Es unterstützt uns bei der statischen Analyse und bei der formalen Verifikation der eben gezeigten Verträge. Das heißt, wir können das alles bereits zur Compile-Time überprüfen und wir haben auch

Datenfluss- und Abhängigkeitsüberprüfungen. Ein Beispiel ist, ich habe eine Verschlüsselungsfunktion, die hängt ab von einem Klartext und von unserem Key und da kommt ein Ciphertext raus und ich könnte mit Spark jetzt beweisen, dass dieser Ciphertext tatsächlich eine Abhängigkeit von sowohl dem Klartext als auch dem Key hat.

Würde ich jetzt dort einen statischen Key in die Funktion einbauen, würde der Beweis an der Stelle fehlschlagen. Und wir haben auch eine Variable T für unsere Verifikation. Das heißt, wenn ich etwas verifizieren will, muss ich nicht sofort all in gehen. Ich kann anfangen mit der einfachsten Variante valid Spark. Das bedeutet, ich habe keine Axis-Types, also für

die C-Menschen, das sind Pointer und Funktionen dürfen zum Beispiel keine Seiteneffekte haben. Wenn ich die Funktion add habe, a und b und return c, darf die keine globale Variable manipulieren zum Beispiel. Eine weitere Stufe wäre die Abwesenheit von Laufzeitfehlern, das heißt, ich habe keine Overflows, keine Exceptions in der Software. Ich kann

beweisen, dass diese Software unter den gegebenen Bedingungen niemals abstürzt und die nächste Stufe, die einen erheblichen Mehraufwand auch fordert, ist ein vollständiger Funktionaler Beweis. Das heißt, ich habe jede Eigenschaft dieser Software bewiesen, nicht nur, dass sie nicht abstürzt, sondern auch, dass sie exakt

das tut, was ich spezifiziert habe. Wie funktioniert das? Wir haben unseren Code, c ist a durch b und unser Tooling, unsere Beweiser generieren daraus nicht irgendwelche Beweise, sondern sie generieren zuerst einmal Beweisverpflichtungen. Wenn ich a durch b teile, darf ich bei der

Division keine 0 nicht durch 0 teilen. Also generieren wir die Beweisverpflichtung, b ist ungleich 0. Wenn ich den Code beweisen möchte, dann muss ich an dieser Zeile Code nachweisen, dass b nicht den Wert 0 annehmen kann. Ich mache das Beispiel von vorhin einmal

weiter. Unten sind jetzt immer die Ausgaben des Toolings, des Knut-Proof bereits. Wir können einen Overflow-Check haben, wenn der Wert

j minus 2 hoch 32 annimmt. Das können wir wiederum verhindern, indem wir in unserem Vertrag angeben, dass die Eingabe in diese Funktion diesen Wert nicht annehmen darf. Integer Tick First bedeutet in diesem Fall, also das Tick ist ein sogenanntes Attribut in Ada und

First ist der erste, sprich der kleinste Wert, den der Integer kennt. In diesem Fall minus 2 hoch 32 und den wir sagen als Vorbedingung für unsere Funktion, wir dürfen diesen Wert nicht übergeben, können wir beweisen, dass unser Overflow-Check, den wir eben hatten, beweist, denn dieser

Wert kann nicht mehr auftreten und unsere Nachbedingungen beweisen an der Stelle sich von ganz allein mit, denn wenn ich alle negativen Werte verhandle, werden sie größer Null. Jetzt benutze ich diese Funktion in einer

ganz normalen Ada-Procedure. Ich führe natürlich den Beweis auch über diese Funktion und an dieser Stelle, ich habe keine weiteren Checks und der sagt mir natürlich, meine Vorbedingungen kann fehlschlagen, wenn der Wert von Value den entsprechenden Wert angenommen hat.

Das kann ich einerseits ganz einfach lösen, indem ich sage, okay, ich rufe die Funktion Apps nur dann auf, wenn der Wert nicht angegeben worden ist, also sagt es mir die Precondition, also die Vorbedingung wurde bewiesen, aber ich

habe vorhin gesagt, Ada hat ein sehr sehr starkes Typ-System und ich kann einfach etwas viel Eleganteres machen, ich sage, ich definiere mir einen neuen Typ, das ist der symmetrische Integer, der geht von minus 2 auf 32 plus 1 bis 2 auf 32 minus 1, das heißt, er ist von plus bis minus im negativen und im

positiven Bereich gleich groß. Ich verliere dadurch einen Wert, aber diesen Wert kann ich sowieso nicht bearbeiten und sage, die Funktion AppsValue darf an der Stelle nur noch diesen Typen verwenden und ich

brauche die Vorbedingung nicht mehr, denn die Vorbedingung wurde implizit durch den Typen erfüllt. Wenn ich das jetzt beweisen möchte, werde ich sehen, dass der Overflow-Check nicht mehr auftritt, denn dieser Integer kann bei der Negierungsoperation nicht mehr überlaufen, da er symmetrisch ist und

wenn ich das an dieser Stelle kann ich auch in der darüberliegenden Funktion einfach sagen, ich verwende einen symmetrischen Integer und kann mir meine manuellen Checks sparen, denn all diese Checks werden von der Sprache übernommen und hier gibt es auch keine Beweisverpflichtung mehr, denn der Typ enthält bereits alle Eigenschaften, die wir haben möchten. So, wo wir das ganze verwendet? In vielen

Dingen, die man im täglichen und nicht ganz so täglichen Leben sehen kann, also im Safety-Bereich, es fliegen Rolls-Royce-Triebwerke, deren Software ist in Spark geschrieben und die hängen, soweit ich mich

entsinnen kann, an dem ein oder anderen Airbus dran, mit dem man in den Flughafen fliegt, im militärischen Bereich, der Eurofighter zum Beispiel verwendet Spark, aber auch Signalsysteme der Bahn, die halt nicht versagen dürfen bzw. auch in der Raumfahrt kann ich es mir nicht leisten, ich kann nicht halt einfach einen Techniker in den Weltraum

schicken und meinen Satelliten patchen, sondern die Software muss funktionieren. Im Security-Bereich gibt es den, wo ein Mikrokern, als ein Mikrokern, also bei dem die Abwesenheit von Laufzeitfehlern bewiesen ist, das heißt, die Software stürzt nicht ab, bzw. von der französischen IT

Sicherheitsbehörde der ANSI gibt es den sogenannten Wookie, der im Prinzip einen USB-Dongle darstellt, dessen Firmware in Spark formal verifiziert worden ist und der gegen diverse USB-Angriffe damit geschützt ist. So, ich versuche noch ein praktisches Beispiel

anzubringen, wenn an der Stelle vielleicht irgendjemand nicht ganz verfolgen kann, mich bitte kurz mit Handzeichen unterbrechen. Eine kurze Einführung, Strings in C, ein String in C ist ein Pointer auf ein Stück Speicher und am Ende liegt eine Null und wenn die Null da nicht liegt, dann laufe ich aus meinem Speicher raus und das geht alles kaputt. Also ich habe auch keine explizite Längenangabe,

wenn die Null da nicht liegt, weiß ich nicht, wie lang der Speicher hinter dem Pointer ist. Strings in Ada sind Arrays, die haben immer einen bestimmten Objektypen, der eingereitet wird, in diesem Fall ein Character, weil es ein String werden soll und alle Arrays in Ada haben eine explizite Größe. In meinem

Beispiel werde ich einmal Ada aus C-Code heraus aufrufen, einfach um quasi zu verdeutlichen, wie schön das Interface ist. Ich werde ein C-String an die Funktion übergeben und den wiederum wandel ich in einen Ada-String um und für diese Umwandlungsfunktion ist das Ziel zu

beweisen, dass sie erstens nicht abstürzt und zweitens ein Nullpointer oder ein Lernstring immer mit einem bestimmten Default-Wert, dafür immer einen bestimmten Default-Wert returned. So, jetzt hoffen wir mal, dass das klappt.

So, wir haben hier unsere Main.C, ganz kurz, wir haben eine Message, die wird nur initialisiert, wenn ich ein Adainit und Adafinal benötige, um bestimmte Runtime-Eigenschaften von Ada zu haben und die Funktion print importiere ich aus

einer eigenen Ada-Bibliothek, die es hier definiert. Also wie gesagt, das ist ein sehr schönes Interface. Ich sage, ich habe die Prozido print, die nimmt eine System- punktadress, das ist ein Pointer und eine maximale Länge und ich exportiere die nach C und die soll dort Print heißen. Implementiert ist die recht simpel.

Eine kurze Anmerkung, das with oben sind im Prinzip wie in C includes, nur sehr viel schöner, also ich pappe nicht einfach irgendwelchen Präprozessor-Code dran, sondern es sind tatsächlich semantische Pakete. Die Funktion print ist implementiert, sie bekommt aus dem

String-Ultis-Paket Convert to Ada, was wir beweisen möchten, übergibt den Pointer, einen Default-String und die Länge und ich erhalte daraus einen Ada-String, den ich danach einfach ausgeben kann. Jetzt kommen wir zum interessanten Teil, die Funktion Convert to Ada.

Die hat eine Nachbedingung, wenn der C-String eine Nulladresse ist, dann soll der Default-String zurückgegeben werden. Kurz zur Einführung noch, ich habe noch eine Funktion Length, das macht im

Prinzip das String Length in C, nur in Ada implementiert und als Nachbedingung sagen wir, das Ergebnis darf maximal so groß sein wie die maximale Länge, sonst wäre es keine maximale Länge. Implementierung ist ganz einfach, wir lesen zuerst die Länge aus,

wir lesen zuerst die Länge aus, denn wir müssen vorher wissen, wie lang der String wird, dann generieren wir ein Objekt der entsprechenden Länge in Zeile 40, das müssen wir irgendwie initialisieren. Das ist eine paskalartige Syntax und wir haben

einen deklarativen und einen Funktionsblock. An der Stelle ist der deklarative Block von dem Ist und Beginn begrenzt, dort müssen wir alle Variablen, die wir verwenden wollen, vorher deklarieren, somit ist sichergestellt, dass wir immer explizit wissen, was wir an Variablen zur

Verfügung haben und auch nicht irgendwo im Code Objekte auftauchen, die wir nicht kennen und im Beginnblock wird der Funktionscode abgehandelt. Genau, wir sagen, wenn die Länge größer 0 ist,

dann iterieren wir über den String, den wir gerade allokiert haben und GetChar nimmt den Pointer und gibt uns den Character an der Speicheradresse zurück und dann fügen wir diesen Character in den String an der entsprechenden Stelle ein und wir haben noch

die Eigenschaft, wenn der Cursor größer gleich dem letzten Element unseres Pointers, also der höchst möglichen Speicheradresse ist, brechen wir die Schleife ab und wenn das nicht der Fall ist, das heißt wir noch nicht an der höchsten Speicheradresse sind, dann können wir inkrementieren. Das schützt uns nicht zwangsläufig

davor, dass wir einen Speicherfehler erhalten, weil der Cpointer kann einfach auf einen Block zeigen, der uns gar nicht gehört und wir können es nicht überprüfen, aber es schützt uns davor, dass wenn wir am Ende des Speichers sind, nicht versehentlich einen Overflow generieren. So, jetzt beweisen wir

das. Schauen, was uns das Programm sagen wird. Das dauert immer alles ein bisschen, also beweisen ist keine einfache Sache. Der Beweiser hat bestimmte Eigenschaften, er ist

nicht deterministisch, aber für alles, was uns bewiesen wird, gilt die Garantie, dass das nicht fehlerhaft ist. Ok, was haben wir hier? Jetzt kommt das nicht mehr. Genau,

jetzt haben wir hier ein, das kann man leider nicht sehen, ihr müsst mit glauben, dass das da steht. Es sagt uns, ein Rangecheck ist bewiesen worden und ein Lengthcheck. Der Rangecheck und der Lengthcheck kommen durch den String, weil wir haben

für L haben wir quasi die Range des Typen und die Länge des Arrays für String. Und der interessante Teil ist das, was nicht bewiesen wurde. Eigentlich sollte uns das da unten, ach genau, das ist die precondition might fail steht dort

und zwar, wenn der Cursor Null ist. Und GetChar, da es auf Speicher zugreift, hat eine Vorbedingung, dass der Cursor niemals Null sein darf. Und was wir haben, ist diese Bedingung if L größer Null und diese Bedingung ergibt sich aus unserer Längsfunktion, denn diese

Längsfunktion läuft über den Speicher und die wiederum hat selbst initialisiert L mit Null und sagt, wenn der Pointer nicht Null ist, dann laufen

wir über das Array bis wir eine Null finden, aber wenn es Null ist, dann returnen wir sofort L. Das heißt, wenn etwas größer als, wenn das Return größer als Null ist, dann gilt die Eigenschaft, dass der Pointer, den wir davor dort reingetan haben, nicht Null

sein kann. Und das müssen wir jetzt irgendwie ausdrücken. Das klingt erst mal recht komplex, aber was wir machen können, ist wir fügen an der Längsfunktion einen sogenannten Contract Case an. Der Contract Case spezifiziert für bestimmte Ausgabewerte, die möglich

sind, bestimmte Eigenschaften. Das heißt, Contract Cases sagen wir Längs.

Halt, jetzt muss ich kurz cheaten. Ach ja, wir haben ein C-String, genau.

Halt, falsch für bestimmte Eingabewerte. Nicht Ausgabewerte. Also unser C-String ist ein Nullpointer. Dann gilt, unser

Result ist kleiner gleich Null. Und im zweiten Fall, also die müssen immer vollständig sein, wir können nicht sagen, wenn das gilt, gilt das an, gilt was bestimmtes, sondern wir müssen jetzt auch, ja, wir returnen

an der Stelle einen Integer. Wenn wir sagen, gleich Null, müssen wir gleichzeitig beweisen, dass der Fall kleiner Null niemals auftritt. Das heißt, wir würden das nicht vollständig beweisen können. Wir können auch sagen, wir returnen nur Werte ab Null. Dann könnte man sagen, gleich Null. So, wir müssen den zweiten Fall

noch betrachten, das heißt, was ist, wenn es nicht Null ist.

Das heißt im Prinzip, wir sagen Null. Das heißt, wir können für die Null keine Aussage treffen. Wenn wir Null

bekommen, wissen wir jetzt an der Stelle nicht, ist es ein Nullpointer oder nicht, aber das macht nichts. Denn wenn wir eine Null bekommen, geben wir eh unseren default-String zurück. So, wir haben jetzt die Eigenschaft, sagt die Zeit, ich habe noch Zeit, versuchen das jetzt zu beweisen. Wir werden gleich sehen. Ich habe mich

nicht vertippt, das ist schon mal gut. So, jetzt sehen wir, es beweist immer noch nicht. Es war geplant. Denn wir haben hier die Funktion toPointer.

Und zwar haben wir unseren Typen pointer und diese Funktion toPointer macht aus unserer system.address einen selbst definierten Pointer-Typen. Und da wir da getChar auf diesen Pointer-Typen verweisen und wir gerade eben bewiesen haben, dass der C-String nicht Null sein kann,

kann diese Verknüpfung noch nicht hergestellt werden. Das heißt, wir müssen uns die Funktion toPointer anschauen. Die steht hier unten. Und die nimmt eine system.address und returnt einen Pointer. Und auch für die müssen wir jetzt Eigenschaften definieren, dass wir sagen, wenn das ein Nullpointer ist, wenn wir

eine Nulladresse bekommen, dann bekommen wir auch ein Nullpointer. Und wenn wir keine Nulladresse bekommen, bekommen wir keine Nullpointer. Das heißt,

oh, dann, ja, ich mach's, fix ich gleich.

So, contract cases. So, was wir gesagt haben, wenn unsere Adresse eine Nulladresse ist, dann returnen wir ein Nullpointer. Wenn es kein ist, returnen wir kein. Jetzt kommt der große Moment, ob ich mich vertan habe. Jetzt beweisen wir das.

Und ich hab mich vertippt. Ja, da fehlt ein Pfeil, tatsächlich.

Und missing semicolon, ja. Das Problem ist, ich sehe auf meinem Laptop nicht ganz alles, weil das Display von meinem Laptop kleiner ist, als das Display von

jetzt kompiliert ist. Und es beweist. Und es dauert. Und precondition might fail, when cursor gleich Null und string gleich others Null. Ja, jetzt haben wir zwar, jetzt können wir sagen,

okay, jetzt können wir aber was anderes machen. Wir, eigentlich müsste es jetzt beweisen. Das heißt, wir checken mal, ob wir hier sagen können, cursor ist ungleich Null. Falsch, nicht da, sondern in dem if.

Nein. Und zwar, ich kann das Pragma hinschreiben. Und der Punkt ist, wenn ich das Pragma hinschreibe, gilt das ab dieser Stelle. Und das Pragma beweist dann nicht mehr. Also, das Pragma muss auch bewiesen werden. Ich habe jetzt auch an dem Pragma

eine grüne Markierung, dass es bewiesen wurde, dass es stimmt. Das heißt, wir haben tatsächlich an der Stelle bewiesen, dass unser cursor dort kein Nullpointer sein kann. Warum kann er das in der Schleife sein? Schleifenaufrufe sind eine komplexe Sache. Wir müssen Spark jetzt erklären, dass sich dieser cursor in der Schleife nicht ändert.

Und dafür gibt es sogenannte Schleifeninvarianten. Und wir schreiben im Prinzip genau das gleiche rein. Wir sagen, diese Assertion gilt in der Schleife für jeden Aufruf. Und beweisen das.

Und es beweist. Das heißt, ich habe jetzt an der Stelle bewiesen, obwohl ich nicht explizit darauf checke, dass der Pointer, den ich verwende, kein Nullpointer ist. Aber durch die Eigenschaft der Funktion Längs und durch die Eigenschaft, dass ich quasi die Länge an die

Eigenschaft des Pointers koppelte, kann ich in der Schleife auch beweisen, dass dieser Pointer niemals Null werden kann. Das heißt, ich habe einen Check gespart. Und das ist immer noch alles Compiletime. Das Programm ist noch niemals gelaufen. Das heißt, ich habe hier im Prinzip eine Klasse von Fehlern ohne einen einzigen Programmaufruf bereits eliminiert.

Genau, also das ist auch was, was nur schwer zu testen wäre. Mir wurde gerade ein Zeitzeichen gegeben. Deswegen würde ich jetzt in die Fragerunde übergehen. Ich hoffe, es hat euch was gebracht.

So, fangen wir hier vorne an. Bitte nur eine Frage. Okay, und zwar mir ist gerade aufgefallen, zum Beispiel bei dem Symmetric Integer.

Dein C-Beispiel war jetzt ja eigentlich Implementation Defined so ein bisschen, weil es kommt ja darauf an, was für eine Integer-Representation du hast. Zweier-Komplement oder Einer-Komplement. Meine Frage ist jetzt, wenn du diese Symmetric Int jetzt als EBI, zum Beispiel für C-Aufrufe, zur Verfügung stellst, könntest du das ja

nicht mehr zur Compile-Zeit checken? Also hättest du dann auch und was wäre bei dem nicht-nullterminierten String passiert? Also, wenn man mit C interagiert, muss man die API-Aufrufe so anpassen, dass die Typen stimmen. Ich kann diesen Symmetric

Int nach C übergeben. Das heißt, der Wertebereich, der in der C-Funktion ankommt, wird immer in diesem Symmetric Int sein, weil ich ja vorher geprüft habe, dass das der Fall ist. Aber in C ist diese Eigenschaft weg. In C habe ich mein Int, der ist 32-Bit auf der entsprechenden Architektur und damit ist die Eigenschaft weg. Ich kann die Typen da nicht verwenden.

Also, der Punkt, das du machen würdest, ist im Prinzip, was ich jetzt gemacht habe. Du übernimmst was aus C und unsere Längsfunktion hat auch keine Vorbedingungen, weil ich weiß nicht, was kommt. Es kann eine Nullpointer kommen, es kann irgendwas kommen, ich kann überhaupt keine Eigenschaften über C beweisen. Das heißt,

du musst dieses Interfacing so bauen, dass du nach C, wenn du etwas zu C übergibst, für dich selbst solche Nachbedingungen wählst, dass C damit umgehen kann und gleichzeitig, wenn du was aus C übernimmst, gar keine Annahmen triffst, weil du weißt nicht, was C alles kaputt gemacht hat davor.

Hat es deine Frage beantwortet? Haben wir eine Wortmeldung? Der Beweis war jetzt nicht besonders umfangreich. Wie lange dauert es, einen realistischen Szenario, einen Beweis

wirklich durchzuführen? Der Beweis, den habe ich vorher schon mal gemacht, den habe ich mir jetzt gerade nicht ausgedacht. Der Punkt ist, man fängt mal, es ist ein deutlicher Mehraufwand, eine Software zu beweisen, weil du schreibst sie und dann funktioniert, dann kannst du sie

auch ausführen, sie funktioniert halt schon erstmal, um dann von dem Punkt zu kommen, du hast jetzt eine Software, die erstmal irgendwie funktioniert und du hast eine Software, über die du formal gezeigt hast, dass sie nicht abstürzt. Brauchst du tendenziell nochmal so lange dafür, dass du die Software geschrieben hast. Der Vorteil ist, du hast Sicherheitsgarantien, die du mit Testen nicht erreichst.

So, zwei Fragen haben wir noch. Das Programm ist in ATA geschrieben. Genau, also Spark ist... Der ATA-Interpreter, der läuft aber auch unter dem C-Interpreter. Also da muss ja eigentlich auch bewiesen werden, dass das C-Programm, was ATA ausführt, auch zu 100%

korrekt terminiert. Der Interpreter ist auch in C geschrieben. ATA ist nicht interpretiert. Auf der spezifischen Prozessarchitektur, der Interpreter 100%ig den ATA-Code ausführt.

ATA ist nicht interpretiert, ATA wird kompiliert direkt nach Bytecode. Es gibt den GCC Frontend für ATA, was im Prinzip in Bytecode kompiliert. Der springende Punkt ist, du vertraust deinem GCC genauso, wie du deinem ATA-Compiler vertraust. An irgendeiner Stelle musst du den Tools vertrauen.

Nichtsdestotrotz finden diese Tools Fehler für dich, die du alleine unter Umständen nicht gefunden oder mit sehr viel mehr Aufwand gefunden hättest. Und der zweite Punkt ist, es gibt immer noch die Garantie, dieses Tool zeigt einen Beweis nur dann als bewiesen an, wenn es ihn tatsächlich bewiesen hat.

Das heißt, das Tool kann ihn nicht zwangsläufig beweisen. Du hast keine false positives, das heißt, du hast keine akzeptierten Beweise, die nicht korrekt sind. Es kann aber passieren, dass das Tool nicht mehr in der Lage ist, etwas zu beweisen. Und dann wirst du es nicht schaffen, das zu beweisen. Aber das heißt nicht, dass es nicht korrekt ist.

Wenn die Korrektheit nachgewiesen wurde, dann ist es korrekt. Die genauen technischen Details darüber würde ich an der Stelle AdaCore, der Firma, die das Tooling entwickelt, überlassen. Jetzt habe ich fast die letzte Slide vergessen. Das wäre die letzte Slide gewesen.

Für die Fragen. Eine Frage können wir noch. Meine Frage war jetzt so, ich versuche das ja für mich zu verkaufen, dass ich jetzt nicht C++ nehme.

Dann wäre es natürlich die Frage, was kann ich jetzt erschlagen, was ich nicht mit dem Static Analyzer. Da wäre eben so meine Frage, bietet denn Ada oder Spark da irgendwie so EBI-Validierungen an? Weil das gerne vorgeschlagene Thema, Beispiel ist von der Ariane-Rakete, war ja dann auch eher so, dass sich intermodulmäßig

dann die Sachen explodiert haben über die EBI. Kannst du da irgendwie Beispiele machen, wo du das verifizieren kannst oder zumindest hast du vielleicht Beispiele, wo du weißt, mit dem Static Analyzer wird es da wirklich schwierig und das habe ich bisher nur mit Spark

verhindern können. Dein Compiler hat bestimmte Annahmen, was die EBI betrifft, Typkreuzen. Ich selbst hatte das Problem, ich habe was bewiesen und es kam auf einmal andere Ergebnisse heraus, also ich eben bewiesen hatte, dass rauskommen können. Der springende Punkt ist, ich habe einen Datentypen verwendet, der war kleiner als 8 Bit und mit Datentypen, die kleiner als 8

Bit sind, haben sich Compiler gerne schwer. An der Stelle muss man sehr genau wissen, wie sich der Compiler verhält. Was du beweisen kannst an der Stelle ist die Semantik deines Codes. Du kannst beweisen, dass bestimmte Datenflüsse in deinem Code so stattfinden, dass er aufgrund dieser Datenflüsse

nicht abstürzt. Wenn dein Compiler auf einer bestimmten Architektur oder aufgrund bestimmter architektureller Annahmen Dinge tut, auf die du keinen Einfluss hast und die dann dazu führen, dass Speicherbereiche sich verändern oder du greifst auf Sensordaten zu und dein Sensor fällt aus und gibt dir Werte, die laut Sensordatenblatt gar nicht erlaubt sind.

Dagegen kannst du dich nicht wirklich schützen. Trotzdem kannst du schon enorm viele Fehler aus deiner Software heraushalten, weil all die Fehler, die du jetzt noch drin hast, die hast du auch drin, wenn du das in C oder C++ schreibst. All die Compiler-Tricks, all die Bugs im Compiler hast du auch in C.

Davor schützt dich auch eine andere Sprache nicht.