Beweisbar sichere Software
This is a modal window.
The media could not be loaded, either because the server or network failed or because the format is not supported.
Formal Metadata
| Title |
| |
| Title of Series | ||
| Number of Parts | 15 | |
| Author | ||
| License | CC Attribution - ShareAlike 4.0 International: You are free to use, adapt and copy, distribute and transmit the work or content in adapted or unchanged form for any legal purpose as long as the work is attributed to the author in the manner specified by the author or licensor and the work or content is shared also in adapted form only under the conditions of this | |
| Identifiers | 10.5446/50683 (DOI) | |
| Publisher | ||
| Release Date | ||
| Language |
Content Metadata
| Subject Area | ||
| Genre | ||
| Abstract |
|
Datenspuren 20201 / 15
1
2
4
5
6
10
11
12
14
00:00
SoftwareHypermediaCompilerSQLHASKELLKernel (computing)CLOU <Programm>Proof theoryUDP <Protokoll>InternetdienstUniform resource locatorProgram codeSoftwareProgramming languageALT <Programm>Systems <München>Operating systemFirefox <Programm>Open sourceStack (abstract data type)EncryptionCategory of beingPlane (geometry)Computer programComputer sciencePropositional formulaLaptopHigh-level programming languageServer (computing)Project <Programm>Geometric primitiveKommunikationComputerHausdorff spaceCodeRepresentation (politics)Computer hardwareRandAlgorithmWebsiteElliptic curveWritingLogic gateAtomic nucleusEnde <Graphentheorie>Numerisches GitterCodeDatabaseTheoremBlogWalkthroughCompass (drafting)EckeComputer animationLecture/Conference
10:09
UDP <Protokoll>InternetdienstQuantificationGreatest elementComputer programmingImplikationExclusive orComputer programProgramming languageFunction (mathematics)Interior (topology)Systems <München>Field extensionComputer programMathematicianTypPropositional formulaSeries (mathematics)ImplementationComputer programmingProgramming languageTheoryGreatest elementTypsystemSchool of NamesSoftwareTheoremAlgorithmKonstruktive LogikTime zonePopulation densityParameter (computer programming)Uniformer RaumComputerServer (computing)Eigenvalues and eigenvectorsMathematicsPoint (geometry)Route of administrationAbgeschlossenheit <Mathematik>StandardfunktionParallelenHASKELLString (computer science)BeweissystemCodeComputer animation
19:53
Programming languageHASKELLSoftwareIndexFunction (mathematics)Prime numberMassComputer programServer (computing)TypEncryptionSimilarity (geometry)Value-added networkIndexLengthInvariant (mathematics)CryptographySystems <München>ZugriffData structureTheorySocial classCodeAutomationC++TypsystemTupleLINUXDistanceRAMVersion <Informatik>Operator (mathematics)Direction (geometry)Parameter (computer programming)Raster graphicsMathematicsProgramming languageHASKELLCodeIntermediate languageObjective CAMLInterior (topology)Project <Programm>Firefox <Programm>Computer animation
29:38
HASKELLTypInversion <Mathematik>CompilerIndexProof theoryTypComputer programPattern languageNormaleElement (mathematics)Parameter (computer programming)LengthZahlWritingNatural numberHASKELLInterior (topology)String (computer science)ImplikationPressureOccamGIPSY <Programm>Liste <Informatik>EstimationMultitier architectureNoten <Programm>Large eddy simulationFunction (mathematics)OperatorNumberRepresentational state transferCodeComputer animation
39:23
TypCompilerComputerInversion <Mathematik>outputDegree (graph theory)MatroidHASKELLParsingNatural numberProgramming languageHypothesisImplikationTypParameter (computer programming)LengthIndexPropositional formulaStrich <Typographie>AutomationVersion <Informatik>Computer programHASKELLFunction (mathematics)NumberSIMPL <Programmiersprache>TERMINUS <Programm>WeightWAIS <Programm>Sharp <Marke>Systems <München>Variable (mathematics)Physical lawStress (mechanics)Order theoryList of unsolved problems in mathematicsKanteAutomatonSoftware developerComputer animation
49:07
ComputerOnline chatComputer animationLecture/Conference
Transcript: German(auto-generated)
00:10
Okay, so bei mir ist jetzt der Marius von Kars macht Schule. Der will uns was über beweisbare Software und Programmcodes erzählen und ich bin gespannt Marius. Die Bühne ist deine.
00:22
Vielen Dank. Ich rede heute über Beweise in Software und das ist eigentlich ein altes Ding. Also Beweise in Software wurden gemacht seit es irgendwie Programmiersprachen gibt und manche von den Systemen, die ich jetzt irgendwie heute zeige, wenn auch vielleicht nicht die
00:41
spannendsten, sind einfach noch aus den 80er Jahren und dieses Thema hat einfach bisher, würde ich sagen, so eine wissenschaftliche Community irgendwie interessiert und ein paar Leute am Rande, aber so richtig irgendwie in den Mainstream der Informatik ist es nie
01:00
gekommen. Das ändert sich aber gerade ein bisschen, vielleicht ein bisschen vergleichbar mit irgendwie dem KI-Thema, wo plötzlich irgendwie wo Rechenleistung da ist, man Sachen automatisieren kann und dass es plötzlich Sachen irgendwie einfacher gehen, weil man es nicht mehr selbst machen oder vielleicht noch nicht mal selbst ganz verstehen muss. So ist
01:21
es bei Softwarebeweisen auch, würde ich sagen. Es gibt mittlerweile irgendwie ganz gute Möglichkeiten, wenigstens Teile des Beweisverfahrens auf Software zu automatisieren und es gibt Bestrebungen, die Beweissoftware, die Theorienbeweise nicht mehr nur als ein
01:43
separates System da zu haben, was irgendwie mit meinem eigentlichen Programm gar nichts zu tun hat, sondern es gibt Bestrebungen Beweise und Beweisbarkeit und irgendwie eine höhere Korrektheit auch in, ich würde sagen, Mainstream-Sprachen reinzubringen und somit
02:07
irgendwie mehr Leuten verfügbar zu machen. Und ein paar von diesen, wie ich finde, spannenden Systemen, die irgendwie irgendwo auf der Grenze zwischen ich beweise etwas selbst und ich lasse irgendwie meine Maschine etwas beweisen, über die wird es jetzt auch
02:24
teilweise gehen. Wieso das Ganze? Meistens, wenn man irgendwie Vorträge über Softwarekorrektheit hat, kommt jetzt hier irgendwie ein konkretes Beispiel, irgendwie häufig diese Ariane-5-Rakete, die einen Softwareback hatte und dann umgedreht ist und ich würde aber eigentlich eher
02:46
argumentieren wollen mit der Art und Weise, wie wir Software verwenden. Also wenn heutzutage mein privates Website-Backend mit ein paar Umfragen für meine Freunde irgendwie die
03:01
kritischste Software wäre, dann würde ich sagen, bräuchten wir auch keine Beweisbarkeit in den Software. Das Gegenteil ist aber der Fall, ein Software kommt in alle möglichen Bereiche rein, in Dinge, wo man nie dachte, dass vielleicht IT auch mal eine Rolle spielen sollte oder könnte. Ich denke in diesem Umfeld vielleicht noch ein bisschen mehr.
03:26
Und was auf jeden Fall irgendwie ganz spannend ist, sich auf Wikipedia mal die Liste auf Softwarebugs anzugucken, ist einfach eine Liste an schwerwiegenden Fehlern in Software, die zu schwerwiegenden Problemen in der realen Welt geführt haben.
03:42
Und wenn man sich jetzt mal überhaupt irgendwie hier die einzelnen Kategorien da anguckt, in denen Software Fehler zum Geldverlust oder teilweise aber auch irgendwie zum Schaden von Menschen geführt haben. Da sind Sachen wie Raumfahrt dabei,
04:04
Medizin, Dinge, die irgendwie unserem IT-System insgesamt angreifen, sowas wie Verschlüsselung. Und das sind alles irgendwie Bereiche, in denen ich gerne möchte, dass die Software, die ich verwende, dass sie auf der einen Seite transparent ist natürlich,
04:23
also irgendwie Open Source und dass sie irgendwie gereviewed ist und dass sie getestet ist vielleicht. Wo ich aber auch möchte, dass meine Software korrekt arbeitet und ich ganz gut das tut. Und hier kommen Softwarebeweise mit ins Spiel. Ich möchte mit zwei Projekten,
04:48
die gerade irgendwie im Entstehen sind, möchte ich aufzeigen, dass das Ganze kein kleines Gespinde von ein paar Randwissenschaftlern mehr ist, sondern dass das wirklich relevante
05:01
Dinge sind, die da passieren. Das eine ist das DeepSpec Projekt, das ist ein übergreifendes Projekt von vielen Unis und auch einzelnen Leuten. Und da geht es darum, ein verifiziertes System, also lokal, zum Beispiel, was irgendwie auf einem Server läuft oder was auf meinem Laptop läuft, zu kreieren. Das beginnt ganz unten bei der Hardware-Ebene, wo wir Beweise
05:29
irgendwie auf Hardware-Seite haben, wo wir irgendwie Hardware-Beschreibungssprachen haben und darüber Beweise führen können, dass mein konkretes Platin-Design und meine konkrete
05:43
Hardware-Implementierung von bestimmten Primitiven genau das macht, was sie auch machen soll. Das geht dann weiter nach oben auf eine Ebene von irgendwelchen Zwischenrepräsentationen oder dann noch ein bisschen höher die C-Ebene bis hin zu ganzen Betriebssystemen. Das ist
06:07
hier auf der linken Seite dieses CertiCos-Projekt, was ein wissenschaftliches Projekt ist und ich weiß auch gar nicht genau, wie anwendbar das ist, aber das war auf jeden Fall das erste Multi-Core-Betriebssystem, der erste Multi-Core-Kern, der bewiesen war. Und
06:26
dann geht es hier hoch bis irgendwie in die Ebenen von Hochsprachen wie Haskell, Theoreenbeweisern wie Coq, da wird es dann nochmal dazu kommen, aber auch so Dinge wie Datenbanken, SQL und so weiter. Dieses Projekt hat insgesamt das Ziel, dass
06:46
wir sozusagen auf unserer lokalen Maschine etwas haben, was wir laufen lassen können und wo wir sicher sein können von ganz oben nach ganz unten in dem gesamten Stack, dass wir irgendwie einen verifizierten Stack haben. Um die Kommunikation zwischen Rechnern
07:07
geht es bei dem Project Everest, das ist ein gemeinschaftliches Projekt dieser Universitäten in Frankreich und Microsoft Research und die versuchen einen komplett
07:22
verifizierten HTTP 2 Stack zu programmieren und zu beweisen. Das beginnt unten bei ganz kleinen Krypto-Algorithmen wie Elliptic Curves und RSA und wieder deren Teilprimitiven
07:40
und das ist auch auf jeden Fall schon irgendwie in einem Status, in dem man das benutzen kann. Das ist nämlich bereits im Linux-Kern als Teil von diesem WireGuard-Protokoll oder als Teil dieses WireGuard-Projektes im Linux-Kern übernommen worden und auch im
08:04
Firefox sind diese verifizierten Krypto-Primitive drin und das ist insbesondere dahingehend spannend, finde ich, weil das alles generierter C-Code im Endeffekt ist. Das heißt, es wird in einer höheren Sprache, in diesem Fall F-Star, da wird es dann auch nochmal später
08:24
drum gehen, wird eine Software geschrieben, werden diese Primitive geschrieben, werden diese Primitive gleich noch bewiesen und dann wird daraus C generiert und die Leute vom Project Everest haben es geschafft, dass dieser generierte C-Code so lesbar und so verständlich
08:44
ist. In einem langen Prozess gibt es einen spannenden Vortrag zu, sodass das durch die Qualitätsanalyse gekommen ist, sowohl bei Firefox, bei Mozilla, wie auch einfach in den Linux-Kern dann und Leute gesagt haben, okay, das ist Code, der ist zwar generiert,
09:04
aber der ist so verständlich, dass wir den übernehmen wollen. Und das ist immer noch ein Projekt, das läuft, aber am Ende steht irgendwie dieses Ziel, dass man einen kompletten HTTP-2-Stack mit allen Teilen, mit TLS 1.3 und allem hat und ich würde sagen, diese
09:24
beiden Projekte zeigen schon, dass wir in diesem Bereich nicht mehr irgendwie an kleine Software-Dinge denken, sondern dass es die Möglichkeit gibt, zumindest, dass wir ganze
09:40
Software-Ebenen austauschen, durch verifizierte Software. Hier sehen wir auf der rechten Seite auch schon drei Systeme, die wir dann noch zumindest kurz besprechen werden. Das Z3 fällt da ein bisschen raus. Das ist ein SMT-Solver, das ist ein Logik-Solver, den
10:03
kann man füttern mit logischen Aussagen und der wird einem hinterher eine Variablebelegung zum Beispiel herausgeben, um diese logischen Aussagen wahrzumachen. Und diese SMT-Solvers
10:20
sind auf jeden Fall ein Fundament von dieser neuen Welle von Programmiersprachen, die teilweise Sachen automatisieren und die Beweise, die ich sonst per Hand führen müsste, an so ein SMT-Solver übergeben. Und dieses Z3, das hört man auf jeden Fall immer wieder. Es gibt eine
10:42
Reihe von bekannten SMT-Solvern, aber das ist das, was von den meisten Projekten im TANAS-Standard benutzt wird. Wie macht man das jetzt nun, das mit den Beweisen und was hat das eigentlich mit Programmierung zu tun? Und das ist schon lange bekannt, dass Beweise und
11:08
Programme eine Parallelität bilden. Das nennt sich Curry-Howard-Isomorphismus, die aufgezeigt haben, dass es eine Parallelität gibt zwischen logischen Formeln, Spezifikationen, die ich
11:27
finde, also sozusagen Dinge, die ich beweisen will über meine Software oder vielleicht auch über eine einzelne Funktion und Typen im Typ-System. Und das ist dann, wenn ich sozusagen in meinen Typen irgendwie diese logischen Spezifikationen habe, dass es dann
11:44
wiederum, dass meine Beweise zu Programm werden können. Das heißt, ich kann eine Programmiersprache verwenden und in meinen Typen kann ich eine Spezifikation, was jetzt eine Funktion genau tun soll, Vorbedingungen, Nachbedingungen, irgendwelche Seitenbedingungen
12:04
definieren und kann dann in dem Programm, was ich da schreibe, kann ich aufzeigen, dass diese logischen Verknüpfungen, dass die wahr sind. Wie genau das funktioniert, werden wir gleich noch sehen, aber die Idee ist so ein bisschen, dass wenn ich jetzt eine normale
12:24
Standardfunktion in irgendeiner Programmiersprache habe und die hat irgendwie eine Funktionsdefinition, die hat ein Parameter, was vielleicht ein Int und ein String ist, dann ist das Programm, was ich da drunter schreibe, also die Funktion, ist eine Art Beweis dafür, dass es eine Funktion
12:43
geben kann, die mit einem Int und einem String vielleicht einen weiteren Int zurückgibt. Und das bringt mir natürlich erstmal noch nicht viel außer dieser Gedanke, dass das schon so eine Art Beweis ist. Und wenn ich aber jetzt meinen Typen, meinen Typ, der über der Funktion steht, wenn ich den sehr viel detaillierter mache, dann muss ich
13:05
auch mein Programm ändern, sodass es sehr viel detaillierter aufzeigt, dass es genau das tut, was ich da definiert habe in den Typen. Und nicht alle Theoremenbeweiser
13:20
oder nicht alle Beweissysteme nehmen das Typsystem als Basis, aber diese Parallelität zeigt, dass es geht und die meisten machen das auch. Das heißt, ich kann sozusagen in meinen Typen, kann ich sehr viel spezifischer werden und kann konkrete Varianten aufzeigen,
13:43
die ich dann im Code aber mit bedenken muss und mit umformen muss, um dem Typsystem, dem erweiterten Typsystem zu zeigen, dass mein Programm wirklich das tut, was ich möchte. Genau, hier sieht man so ein paar Parallelen. Vielleicht irgendwie interessant, weil wir es
14:05
später nochmal haben, ist das im logischen Force ist der Bottom-Type, das kennt man wenn man Haskell schon mal gemacht hat, das ist ein Typ, der keine Werte hat. Also während ein Int die Werte 0, 1, 2, 3, 4, 5 hat, hat der Bottom-Type einfach keine Werte und das
14:25
kommt so ein bisschen aus dem Gedanken konstruktiver Logik und dass wir, wenn wir irgendwo einen Force haben, dass wir daraus nichts konstruieren können, weil wir keine Werte hinter diesem Typ haben. Werden wir dann nochmal sehen, wie das bei einem konkreten Beispiel aussieht.
14:42
Genau, dann haben wir hier sowas wie Quantifizierung, was man vielleicht schon mal gehört hat, wenn man irgendwo Logik in der Uni hatte oder sowas und da sehen wir auf der rechten Seite diese Product- und Sum-Types und das sind Teile von einer
15:02
Erweiterung von Typsystemen, die sich Dependent Types nennen und die ebenfalls in vielen Beweissystemen Anwendung finden. Gucken wir uns mal, welche Sprachen und Systeme es irgendwie in diesem Bereich gibt und wie man sie einordnen kann. Gucken wir erstmal die
15:23
Einordnung. Das eine ist eine Unterscheidung zwischen interaktiv und automatisiert. Interaktiv heißt ich, ich beweise etwas. Das ist irgendwie so das Äquivalent zu, ich nehme mir einen Zettel und mache einen mathematischen Beweis Schritt für Schritt. Nur, dass ich diesen Beweis nicht auf einem Zettel mache, sondern dass ich den in einem Computer
15:42
Programm mache und dass mein Computer Programm hinterher mir auch noch sagen kann, der Beweis, den ich da aufgeschrieben habe, zusammen mit meiner Spezifikation, also dem, was ich beweisen möchte und dem eigentlichen Programm, ergibt einen schlüssigen Beweis. Das habe ich jetzt bei so einem Zettel nicht, da kann ich einen Beweis aufschreiben und kann
16:03
dann irgendwie viele Mathematiker und Logiker fragen, ist das jetzt eigentlich richtig? In dem Fall kann mir sozusagen mein Theorienbeweiser, mein System, kann mir sagen, ob ich korrekt lag mit meinem Beweis oder nicht. Automatisiert ist genau das Gegenteil. Da
16:21
sage ich eben so einem SMT-Server zum Beispiel, bitte versucht das mal für mich zu lösen. Und wenn ich Glück habe oder vielleicht viel Zeit mitbringe, je nachdem, was es für einen Beweis ist, dann kann das durchaus sein, dass ich gar nicht selbst Hand anlegen muss. Und davon hört man in letzter Zeit irgendwie häufiger mal aus ganz anderen Bereichen,
16:43
nämlich irgendwie bei so über die Jahrzehnte oder Jahrhunderte ungelösten mathematischen Problemen, die plötzlich irgendwie mit so einem SMT-Server auf Riesenrechnerfarben irgendwie gelöst wurden. Aber was ich zeigen will, ist, dass wir diese Riesenrechnerfarben für unsere Standardprobleme in der Programmierung nicht brauchen und dass wir mit einfachen,
17:07
automatisierten Ansätzen schon wahnsinnig weit kommen. Dann gibt es irgendwie so ein bisschen eine Unterscheidung dazwischen, ob es jetzt irgendwie ein eigenes, abgeschlossenes System ist, in dem ich Sachen beweise, die häufig auch ihre eigene Programmiersprache mitbringen,
17:23
die aber häufig dann nicht dazu geeignet ist, irgendwie etwas auszuführen oder maximal irgendwie sich noch extrahieren lässt. Oder ob ich eine konkrete Programmiersprache habe, in der ich meine gesamte Implementierung auch mache und die ich einfach erweitere
17:42
vielleicht oder wo ich von vornherein irgendwie ein Beweissystem mitdenke. Bei den interaktiven Theorienbeweisern gibt es noch irgendwie so ein Taktiksystem. Häufig Taktiken sind Schritte in einer Beweisführung oder auch Algorithmen,
18:04
die mich sozusagen in meiner Beweisführung weiterbringen. Häufig braucht man die nicht, aber sie sind eine Vereinfachung, dass ich Werte in meinem Programm schreibe und dadurch Stück für Stück konstruktiv einen Beweis aufbaue. Und wenn ich solche Taktiken verwende,
18:26
dann ist das alles eher ein bisschen versteckt und ich habe eine Domainspecific Language meistens, die mit solchen Taktiken, wo ich den gleichen Beweis führen kann, wie wenn ich Stück für Stück mein Beweisobjekt in den meisten Fällen aufbaue und das
18:46
irgendwie manuell mache. Das heißt, an vielen Stellen kann dieses Taktiksystem dafür sorgen, dass ich einen Beweis schreiben kann, der so einfach wie so ein Beweis auf dem Zettel ist oder noch einfacher, weil ich einzelne Schritte mir weg automatisieren kann und
19:02
in Funktionen packen kann. Und da sehen wir auch schon wieder die Parallelität zu der Programmierung, dass ich auch bei meinen Beweisen kann ich refactoren und kann Sachen abstrahieren und im Endeffekt ist es auch nur ein Software-System.
19:20
Und häufig bauen solche Systeme auf Dependent-Types oder Refinement-Types auf. Dependent-Types ist eine richtig feste Erweiterung von einem Typ-System. Da haben wir schon ein paar Teile vorhin in dieser Gegenüberstellung gesehen und das bedeutet aber bei den Dependent-Types auch, dass meine Werte sich ebenfalls irgendwie verändern. Zum Beispiel
19:43
gibt es diese Product-Types, das ist sozusagen wie ein normaler Wert, den ich sonst auch in meinem Programm hätte, also irgendwie ein Integer zum Beispiel und der ist in einem Product, also in einem Tupel zusammengefasst mit einem Beweis über diesen Wert. Also ich
20:01
könnte sagen, das hier ist ein Int und das ist aber ein Int, der das Beweisbar an dieser Stelle eine Primzahl ist oder was so groß ist wie die Länge von der Liste oder sowas. Und dann muss ich aber eben in meinem Programm, muss ich zum Beispiel diese Tupel, muss ich
20:22
dann auch auseinander bauen und muss immer diesen Beweis mitdenken und so weiter und so fort. Und bei den Refinement-Types, das ist eher, würde ich sagen, ein Zusatz zu einem Typ-System. Das kann man auch in andere Typ-Systeme mit reinbringen von Sprachen, die bereits existieren und was darauf aufbaut, das sehen wir dann noch bei Liquid
20:44
Feskel später. Gibt es aber mittlerweile irgendwie als experimentelles System auch für Python, habe ich gelesen irgendwo, habe ich aber noch nicht ausprobiert. Gucken wir uns ein paar von diesen Systemen an. Coq ist vielleicht ein paar Leuten bekannt,
21:02
dass diese Kategorie Theorienbeweiser, die noch seit den 80ern bestehen, aber es trotzdem einer der bekanntesten und hat sich natürlich seit den 80ern auch ein bisschen weiterentwickelt. Und da kommen Stück für Stück auch immer wieder primitive mit
21:23
Reihen, die es einem sehr viel erleichtern. Coq ist ganz klar auf der interaktiven Seite, das heißt, da ist wenig Automatisierung, ich muss per Hand irgendwie eine Art Beweis kreieren. Lean kommt auch von Microsoft Research, da gibt es jetzt demnächst die Version 4,
21:47
die es ebenfalls nutzbar macht als eine Programmiersprache und zwar sogar als eine Low-Level-Sprache. Da kann man so ein bisschen wie ein Rust zum Beispiel, da kann man irgendwie an manche Funktionen dran schreiben, dass sie zum Beispiel partial
22:01
sind oder dass sie unsafe sind und somit so ein paar Dinge wieder erlauben, die die Sprache eigentlich nicht erlaubt. Und damit kann ich Systeme irgendwie kreieren, die auf der einen Seite ein bestehendes Programm sind und auf der anderen Seite aber direkt diese
22:22
Theorienbeweise-Sachen mit drin haben und dieses Interaktive ein bisschen mehr automatisiert als in Coq, glaube ich, habe ich noch nicht ausprobiert, auch weil es Lean 4 noch in einem Alpha-Stadium ist. Aber das ist auf jeden Fall, glaube ich, ein spannendes System, was noch wichtiger werden wird in der Zukunft. Wir bewegen uns Stück für Stück weiter in die
22:46
automatisierte Richtung. Es gibt F-Star und F-Star ist der Grundbaustein von diesem Project Everest, was wir am Anfang gehört haben, dieser verifizierte HTTP-2-Stack und in F-Star haben Sie auch, da gibt es ein Subset, das nennt sich Low-Star und das kann
23:04
man dann zu C-Code generieren. Das ist sozusagen die Basis von diesen verifizierten Krypto-Primitiven, die jetzt im Firefox und im Linux Kernbretz drin sind. Und F-Star ist tatsächlich schon, da werden wir dann noch ein Beispiel sehen, ein ziemlich guter Kompromiss
23:24
zwischen interaktiv und automatisiert. Ich kann viele von meinen Beweisen führen, einfach dadurch, dass ich sage, probiere mir das mal zu lösen und wenn das nicht geht, dann übernehme ich per Hand mit Taktiken. Ziemlich ähnlich dazu, aber ein anderer
23:42
Ansatz ist Liquid Haskell. Liquid Haskell ist der erste von unseren Sprachen, der auf so einem Refinement-System basiert und damit muss ich noch nicht mal meine bestehenden Programme unbedingt anpassen, sondern das ist etwas, was insofern es automatisiert
24:03
lösbar ist. Kann ich das einfach zusätzlich zu meiner Funktionsdefinition dazu schreiben und in den allermeisten Fällen brauche ich gar nichts mehr tun. Und das ist ziemlich cool. Ich würde sagen, F-Star und Liquid Haskell sind irgendwie jetzt in den Code-Beispielen,
24:22
die wir dann noch sehen, werden wir sehen, dass sie relativ ähnlich sind, auch wenn F-Star noch meiner Meinung nach ein bisschen integrierter ist und ein mächtigeres System ist, was eben auf Dependent Types mit aufbaut zusätzlich, aber beides ziemlich coole Systeme. Gehen wir
24:42
noch weiter in die automatisierte Richtung und leider ist es dann so, wenn wir zu sehr in die automatisierte Richtung gehen, ohne dass wir die Möglichkeit haben, irgendwie interaktiv einzuschreiten, dann funktionieren ganz schnell Sachen nicht mehr, aber das habe ich trotzdem hier mit reingenommen, weil es konkret für C und teilweise für C++ Code
25:03
funktioniert aber nicht so richtig, noch nicht, gibt es konkret auch Beweissysteme. Da kann man bestimmte Sachen ganz gut drin beweisen, irgendwie zum Beispiel, dass irgendwie ein Pointer, den ich bekomme, dass der nicht null ist, was schon ein riesen Ding ist, würde ich sagen,
25:20
für ein C-Programm, aber trotzdem kommt man mit diesem rein interaktiven Ansatz nicht hat den Ansatz von so einer Intermediate Representation, also das hat eine Sprache, die sich YML nennt, die ML ähnlich ist, also ähnlich wie OCaml zum Beispiel und das ist
25:48
aber so gedacht, dass ich diese Sprache, wenn ich will, kann ich sie selbst schreiben, aber in den allermeisten Fällen generiere ich aus anderen Sprachen, zum Beispiel aus dem was wir vorher gesehen haben, generiere ich diese Sprache und dann kann ich aus dieser Zwischensprache
26:06
sagen, okay, ich möchte jetzt den Z3-Zäuber darauf anwenden oder ich möchte einen anderen Zäuber darauf anwenden und ich glaube, dass man auch interaktive Programme dann da anschließen kann. Auch auf jeden Fall ein spannender Ansatz ist aber auch so eine
26:27
Verstöckelungssache, während irgendwie, würde ich sagen, neuere Ansätze es erlauben, all diese Dinge einfach in einer Sprache zu tun. Gucken wir mal, was so übliche Spezifikationen sind, also Sachen, die ich vielleicht gerne beweisen will, die
26:42
mein Programm macht. Das sind, würde ich sagen, auf jeden Fall irgendwie so was wie Protokolle, wo halt irgendwie klar sind, okay, ich habe hier folgende Datenstrukturen, ich habe einen geregelten Ablauf, dieser Schritt darf nur nach diesem Schritt geschehen und auch nur, wenn folgende Bedingungen geschehen sind, dann mache ich das und ansonsten mache
27:01
ich das. Das ist überall, wo ich eine Design-Dokumentation in irgendeiner Form habe, also wenn ich eine RFC habe, wenn ich irgendwo abstrakt die Eigenschaften oder die Invarianten von meinem System beschrieben habe, vielleicht irgendwie Sicherheitseigenschaften, irgendein Rechte-Management-System, irgendein
27:22
User in Gruppe XY darf nur auf Daten in Gruppe Z zugreifen. All solche Sachen kann ich irgendwie in eine logische Spezifikation überbringen und darüber einen Beweis führen. Dann gibt es natürlich irgendwie so natürliche gegebene Regeln,
27:43
mathematische Regeln aus der Kryptographie gibt es das ganz viel, dass da einfach feststehende Invariante gibt, physikalische Regeln, wie auch immer. Dinge, die einfach feststehen, die mein Programm abbildet und was ich aber dann gerne auch bewiesen haben möchte.
28:01
Und es gibt auch so alltägliche Invarianten. Im Code, da werden wir eben jetzt noch irgendwie ein Beispiel sehen. Das eine ist irgendwie ein Index out of bounds Zugriff. Ich habe irgendeine Struktur. In dem Fall war es irgendwie ein Array. In den Beispielen, die wir jetzt sehen, ist eher eine Liste. Und wenn ich jetzt mit einem Index
28:22
zugreife, der größer ist als die Länge der Liste, dann greife ich irgendwo hin, wo ich nicht hingreifen darf. In C-artigen Systemen führt das vielleicht noch nicht mal direkt dazu, dass das irgendwie abstürzloser wird, sondern das führt vielleicht dazu, dass ich da irgendwie Sachen einlesen kann, die ich gar nicht lesen möchte.
28:42
In diesem Fall zum Beispiel. In anderen Sprachen kann es aber auch einfach sein, dass mein System abstürzt. Und auch das möchte ich nicht, natürlich. Gehen wir mal zu einem Beispiel. Ich habe eine Funktion und die holt sich das I.T.E. Element einer Liste und gibt es zurück.
29:07
Das gibt es in Haskell schon. Das ist dieser zweimal Ausrufezeichen-Operator und der macht auch überhaupt keine Überprüfungen. Wenn ich da irgendwo drüber greife, dann gibt es einfach eine Exception.
29:25
Und weil wir es jetzt aber gerne selber machen wollen, ist hier erstmal die Typdefinition. Also ich habe diese GetEnd-Funktion. Das doppelte Doppelpunkt zeigt, dass dahinter mein Funktionstyp kommt. Das heißt, ich habe zwei Parameter, einen Index und eine Liste von Elementen vom Typ T.
29:45
Zum Beispiel ebenfalls Ints oder Strings, je nachdem was in dieser Liste drin ist. Und dann möchte ich natürlich, wenn ich an einen validen Index gegriffen habe, möchte ich ein Objekt von diesem Typ T zurück. Und weil wir uns jetzt in hauptsächlich funktionalen Sprachen bewegen, wählen wir eine rekursive Herangehensweise. Wir gucken
30:10
uns an, wenn wir das erste Element in dieser Liste suchen, dann geben wir das Kopfelement zurück. Und ansonsten dekrementieren wir i und rufen GetEnd einfach mit der Restliste auf. Normale rekursive Herangehensweise. Und
30:30
das Problem habe ich hier eben schon geschildert, i kann jetzt größer als die Länge der Liste sein. Gucken wir uns mal an, wie dieses Beispiel einfach in normalem Haskell aussehen könnte. Da haben wir
30:42
den ersten Fall, der nie auftreten darf, dass ich mit irgendeinem Index in eine leere Liste reingreife. Und dann haben wir den zweiten Fall, dass ich mit einem Index in eine nicht leere Liste reingreife. Und wenn mein Index null ist, also wenn ich das aktuelle Element haben möchte, dann gebe
31:06
ich das zurück und ansonsten dekrementiere ich den Index und mache mit der Liste weiter ohne das Kopfelement. Genau, aber wenn ich jetzt hier drauf zugreife mit einem Index, der größer als die Länge der
31:24
Liste ist, dann crash das. Und das unschöne, das wollen wir verändern in diesem relativ einfachen Beispiel. Genau, das ist unser Problemfall. Und wir sehen hier schon, wir haben zwei Fallunterscheidungen. Das wird dann gleich noch interessant. Also zum einen machen wir eine Fallunterscheidung über den einen Parameter, nämlich über die Liste und
31:45
gucken uns an, ob die Liste leer ist oder ob da ein Element und eine Restliste drin ist. Das sind die beiden auf der linken Seite und auf der rechten Seite machen wir dann noch eine Fallunterscheidung über unseren Index, ob der null ist oder ob der größer als null ist.
32:06
So sieht das Ganze in Coq aus. Und keine Angst, jetzt erstmal riesiger Codebutton, wir gehen das Stück für Stück durch. Wir haben hier die Funktionsdefinition getEnv und als Teil von getEnv haben wir ein Beweisobjekt.
32:34
Und das schleppen wir mit, dieses Beweisobjekt. Das ist sozusagen einfach ein weiterer Parameter von meiner Funktion. Und dieser Parameter
32:43
ist irgendeine Struktur, die einen Beweis beinhaltet, dass mein Index kleiner als die Länge der Liste ist an diesem Punkt. Und das ist genau das, was wir wollen. Das wollen wir zeigen. Und wir haben das hier an dieser Stelle
33:00
so geregelt, dass wir drei normale Parameter haben, nämlich T, das ist einfach der Typ von den Elementen der Liste. Das habe ich hier in so Curly Braces gemacht, damit der automatisch erkannt wird. Das ist sozusagen einfach die Polymorphie, dass man das nicht nur mit einer Liste von Ints machen kann, sondern auch mit einer Liste von Strings und so weiter.
33:23
Dann haben wir die Liste selbst, dann haben wir den Index und dann machen wir, gibt es hier sozusagen unseren Typ-Operator, das Doppelpunkt, der mir anzeigt, dass ich eine Funktion zurück bekomme von meiner Funktion.
33:43
Also wenn ich jetzt meine Funktion mit Typ, Liste und I aufrufe, dann bin ich dann noch nicht fertig, sondern ich kriege eine anonyme Funktion zurück. Und da muss ich meinen Beweis reingeben und kriege dann dafür mein Objekt T, mein Element der Liste an dieser Stelle I zurück.
34:03
Und wieso man das jetzt so macht, wird sich dann unten nochmal zeigen, dadurch, dass wir eben dieses Proof-Objekt, dass wir das ein bisschen detaillierter schreiben können.
34:20
Wir haben hier auch wieder unsere Fall-Unterscheidungen. Wir unterscheiden bei der Liste auf den Nil-Fall, also ich habe eine Leere-Liste, was der Fall ist, den wir nicht wollen. Unser Fall, der niemals auftreten darf, dass ich mit einem Index in eine Leere-Liste reinrenne.
34:41
Und dann haben wir den zweiten Fall von dieser Unterscheidung, dass die Liste eine nicht Leere-Liste ist. Und dann machen wir noch eine Fall-Unterscheidung über das I, nämlich ob das Null ist oder größer als Null. Und das machen wir hier mit diesen, das nennt sich Piano Numbers.
35:04
Hat vielleicht jemand schon mal gesehen, dass wir die natürlichen Zahlen nicht als 0, 1, 2, 3, 4 definieren, sondern als entweder Null, das hier mit diesem O symbolisiert. Oder mit dem Nachfolger, also dem Successor, deshalb S, von einer natürlichen Nummer.
35:25
Das heißt, meine natürliche Zahl 2 kann ich repräsentieren als S von S von Null, also der Successor von Successor von Null. Genau, und diese Unterscheidung mache ich hier, genauso wie ich die vorhin in Heske mit dem I gleich Null gemacht habe, mache ich die einfach mit dem Pattern Match auf dem I.
35:45
Also entweder ist mein I Null oder ist es ein Successor von irgendeiner anderen Zahl. Gucken wir uns mal den Fall an, der niemals auftreten darf.
36:01
Das muss ich Coq beibringen, dass dieser Fall niemals aufkommen darf und deshalb habe ich sozusagen einen Randbeweis geführt. Und dieser Randbeweis, wir sehen hier, wenn wir in das Match gucken und das Null, dann ist unser Proof Object,
36:23
weil ich sozusagen die Liste, die ich oben noch habe, als Length von LS, die ist an dieser Stelle schon Null. Das heißt, ich habe meinen, deshalb mache ich das auch sozusagen, dass ich eine anonyme Funktion da zurückgebe, weil ich dann sagen kann, okay, mein Proof Object ist hier schon ein konkreteres.
36:44
Ich weiß jetzt, dass an dieser Stelle die Liste Null ist und deshalb kann ich in meinem Beweis I kleiner als Length von LS, kann ich jetzt für LS Null einsetzen und habe deshalb einen konkreteren Beweis, nämlich I kleiner als Length von Null.
37:00
Und da sieht man schon, also ich habe eine natürliche Zahl, die niemals kleiner Null sein kann und mein Beweis sagt mir jetzt, dass mein Index, der niemals kleiner Null ist, kleiner als der Length der leeren Liste ist.
37:22
Die Länge einer leeren Liste ist Null und dementsprechend das I kleiner Null ist Schwachsinn. Das heißt, das ist ein Fall, der nie auftreten kann, wenn ich meine Funktion aufgerufen habe mit so einem Beweisobjekt, was nie existiert, dann existiert auch dieser Fall nicht.
37:41
Und dass das nicht geht, das zeige ich hier in dem oberen Fall. Dieses Lämmer, was ich da definiert habe, not less than zero Length ist das NLTZL, das habe ich kurz gefasst, kann man auch insgesamt wahrscheinlich ein bisschen schöner schreiben. Aber was ich da zeige ist, dass wenn ich einen Typ T habe und einen Index I vom Typ
38:07
Null, dann ist mein I, wenn mein I kleiner als Length von Null ist, dann ist meine Aussage falsch. Das schreibt man so rum in Logik, dass wenn ich eine falsche Aussage
38:22
habe, dann mache ich die Aussage und mache eine Implikation und schreibe false dahinter. Weil false, das haben wir vorhin schon gelernt, ist ein Typ, der keine Werte hat. Das heißt, wenn mein Drücker bewährt false ist, dann kann das nie passieren, weil ich nie etwas zurückgeben kann, weil mein false Typ leer ist.
38:45
Und was man hier sehen kann, ist, dass ich meinen Beweis, den ich unten mache, irgendwie Schritt für Schritt, das werden wir dann noch sehen, irgendwie, und baue den ins Programm mit ein. Aber hier kann ich, wenn ich möchte, meine Funktion ebenfalls mit diesen Taktiken beschreiben.
39:03
Und da würde ich kurz mal wechseln hier in die COG-IDI, da habe ich dieses Beispiel nochmal drin. Und da sieht man das ein bisschen besser, wie das dann aussieht. Ich kann hier Schritt für Schritt, kann ich dieses Programm durchgehen.
39:21
Und mit grün zeigt er mir immer an, dass er bis zu diesem Schritt ist, das System mitgekommen und kann meine Aussagen verstehen, die ich da getroffen habe. Und wenn ich jetzt diese Spezifikation hier habe, dann erscheint die auf der rechten Seite als ein Ziel. Und dieses Ziel kann ich dann beweisen mit diesen Taktiken.
39:45
Da mache ich jetzt erstmal diesen Intro-Schritt, der mir einfach alle, ich zeige nochmal, was sich ändert, der nimmt einfach alle meine Variablen, die ich hier mit den Quantifizierern definiert habe.
40:04
Also das A und das I und meine Hypothese, also der erste Teil dieser Implikation und definiert die als Hypothesen. Alles, was über dem Strich sind, sind Hypothesen und das, was unten ist, möchte ich beweisen.
40:23
Und da ist schon, ich möchte False beweisen, das geht schon mal nicht. Man kann nicht False beweisen, weil man kein Element für False finden kann, weil es das nicht gibt. Deshalb muss man einen anderen Ansatz wählen, nämlich dass man zeigt, dass eine der Hypothesen falsch ist, von denen ich ausgehe.
40:44
Und unsere Hypothese hier, i kleiner als Length von Nil, die ist falsch und das wollen wir zeigen. Deshalb machen wir erstmal einen Schritt, der diese Hypothese simplifiziert und das zeigt schon mal i kleiner Null.
41:00
Und da gibt es dann eine Taktik, die das auflösen kann, die mir sagt, okay, das kann nicht stimmen, i kleiner Null und das ist diese Inversion-Taktik. Und wenn ich die wähle, dann habe ich dieses Lämmer da oben bewiesen, wo ich gezeigt habe, diese eine Hypothese, von der ich ausgegangen ist, die ist übrigens falsch. Dann ist es total egal, was das Gold ist.
41:23
Und dann kann ich im Endeffekt zeigen, das erscheint jetzt hier grün, dass meine Funktion definitiv eine Funktion ist, die meinen Beweis beweist.
41:40
Und kann dann auch zeigen, dass die, wenn ich auf ein valides Programm zugreife, also wenn ich auf die Stelle zwei zugreife in dieser Liste, dann passt das noch. Und wenn ich auf die Stelle drei zugreife, dann ist das nicht ganz so schön, was mir nicht anzeigt, das funktioniert nicht.
42:01
Sondern es zeigt mir einfach nur an, naja, wenn du diesen Beweis hast, dann kannst du das schon machen. Aber da man den nicht konstruieren kann in unserem Programm, das heißt, ich kann keine andere Funktion definieren, die mir so einen Beweis mitgibt und diese Funktion dann aufruft damit, ist das nichtig.
42:23
Von daher, das funktioniert nicht sozusagen. Das muss man hier wissen, aber das sieht man, wenn man damit rumspielt. Genau, das waren die Taktiken. Und jetzt noch zu guter Letzt, ich habe hier dieses Proof-Objekt und diesen ersten Fall haben wir jetzt schon irgendwie abgehandelt.
42:45
Und diesen zweiten Fall, da habe ich schon sozusagen zwei Sachen ausgetauscht. Da habe ich zum einen ausgetauscht, dass jetzt irgendwie die Länge der Liste ohne das Kopfelement ist sozusagen das Gleiche.
43:05
Wenn man das plus eins rechnet, also den Successor nimmt, dann kommt man bei dem gleichen raus wie oben das Length von LS, also das ist die Länge von der Gesamtliste mit dem Kopfelement. Und das ist irgendwie klar, das muss man irgendwie in diesem, beim Pattern-Matching muss man das Coq beibringen.
43:25
Und das checkt er dann und diesen Schritt kann er sozusagen gedanklich mitgehen, das System. Und dementsprechend können wir dann mit dieser veränderten Aussage hier weitermachen. Genau, und das zweite, was wir gemacht haben, ist, dass wir einfach
43:40
unseren Index i ausgetauscht haben durch das, was wir hier gepattern-matched haben. Nämlich, dass das der Successor ist von einem i-Strich, was sozusagen der Vorgänger einfach ist. Und was ich dann machen kann, ist, dass ich auf dieses Proof-Objekt, das sieht
44:04
man hier unten, kann ich, dass das einfach in Coq schon drin irgendwie eine Funktion, die mir die einen Beweis nimmt und einen anderen Beweis dafür herstellt oder mir einen anderen Beweis dafür rückgängig macht, zurückgibt.
44:22
Und das ist in diesem Fall dieses LTSN. Und was das macht, ist, dass es einfach die beiden S wegnimmt. Also das bedeutet sozusagen, wenn ich irgendwie den Successor habe von einer natürlichen Zahl und der ist kleiner als das Successor von einer anderen natürlichen Zahl, dann kann ich dieses beide Successor wegnehmen und gut ist.
44:44
Und was wir damit dann haben, ist den Beweis für den nächsten rekursiven Schritt. Das heißt, wir können jetzt getEnth, können wir aufrufen mit unserer Restliste und dem um 1 verminderten i und haben direkt sozusagen ein Beweis-Objekt für den nächsten Schritt.
45:07
Jetzt kann man sagen, puh, das war unser Ausgang und das soll es jetzt sein. Keine Ahnung. Also das ist cool, um zu wissen, was da eigentlich abgeht, ohne Frage.
45:22
Aber es geht auch so, dass das ganze Ding in Liquid Haskell und das kennen wir irgendwie schon. Wir könnten jetzt sogar dieser Fall, der niemals vorkommt, das habe ich ja da auf undefined gesetzt, den könnten wir auch weglassen. Und was ich sogar noch weglassen könnte, ist den Haskell-Typ an sich, also die zweite Zeile, weil die inferiert wird.
45:49
Aber was ich jetzt hinzugefügt habe, ist eine Annotation, dass dieses Liquid Haskell und diese Annotation besagt, dass ich schon mal als ersten Parameter übrigens nicht irgendeinen Int, was auch negativ sein kann, reinnehme, sondern einen Nutt,
46:04
nämlich das gibt es in Haskell erst mal so nicht, einen Typ, der bei 0 anfängt. Und als zweites kriege ich eine Liste rein und diese Liste ist so groß, dass die Länge der Liste größer ist als mein i.
46:23
Und das im Endeffekt, würde ich sagen, eine ein bisschen konkretere Typdefinition. Und mein Liquid Haskell-System haut das in einen Z3-SMT-Solver rein und kann mir das auflösen.
46:40
Und sagt mir hinterher, okay, passt, du hast irgendwo in deinem Programm diese Funktion aufgerufen mit einem falschen i. Das Gleiche nochmal in F-Star, sieht ziemlich ähnlich aus. Und F-Star ist einfach nur von dem, hier habe ich übrigens den Fall, der nicht auftauchen kann, direkt weggelassen.
47:01
Kann ich hier auch machen. Ist einfach ein bisschen mehr so ML-Schreibweise, Kamel-ähnlich, F-Sharp-ähnlich vielleicht auch. Und ist aber im Endeffekt, wenn wir uns den Typ angucken, was hier ein echter Typ ist, was das Coole ist, ist es mehr oder weniger das Gleiche. Ich kann sagen, ich kriege ein i rein und das i ist auf jeden Fall größer als null.
47:23
Und ich kriege eine Liste rein und die ist so groß, dass es größer ist als mein i. Und was ich hier noch sagen kann, dieses Tot, was ich da vor meinen Typen geschrieben habe, den ich zurückkriege, heißt, dass das ganze total ist.
47:41
Und total bedeutet, dass das terminiert. Und das ist auch ziemlich cool. Das kann mein System mit checken sozusagen. Natürlich, was ein ungelöstes Problem ist und auch nicht gelösbar ist, die Terminierung, kann ich mir das nicht für alles zeigen, aber für die allermeisten Sachen, wo ich es aufzeigen kann.
48:01
Da ich nicht mehr so viel Zeit habe an der Usability, müssen wir noch ein bisschen schrauben. Bei F-Star ist es so, dass man immer exakt, um es zu bauen, um die Standard Library zu bauen, exakt eine Version von Z3 haben muss bis auf die letzte Versionsstelle. Und auch insgesamt die Einordnung in irgendwelche Coding-Systeme nicht so gut.
48:22
Es gibt viele Beispiele, wo ich relativ easy mit Automatisierung weiterkomme. Und mein Fazit ist, Beweise in Programmiersprachen sind toll und mittlerweile sind sie sogar einfach, weil ich es mir automatisieren kann. Und selbst an den Stellen, wo ich nicht mehr weiterkomme, kann ich mithilfe von Automatisierung weitermachen, was viel einfacher ist.
48:45
Und ich kann meine Interfaces ganz klar definieren, was da reinkommt. Und wenn ich einfach Sachen programmiere, und das sind 95 Prozent der Fall, würde ich sagen, dass ich keine riesen logischen Verknüpfungen beweisen möchte, sondern sowas, kaum mehr Aufwand.
49:02
Und ich weiß nicht, ob wir Zeit für Fragen noch haben. Eigentlich haben wir keine Zeit mehr. Interessanterweise hast du jetzt auch ein paar Leute, die dir zuhören, hier vorgezogen. Ich denke, ihr könnt euch sicher nach unten noch mal fragen. Aus dem Chat hatte ich keine Fragen gefunden.
49:21
Ich danke dir erstmal die Leute, die da sind. Applaus für Marius.