“Defense is not dead. Why we will have more secure computers – tomorrow” hieß einer der Vorträge auf dem 27. Chaos Communication Congress, die von Anfang an auf meiner Liste standen. Das Versprechen sichererererer Computer bekommt man schließlich nicht alle Tage.
Der Vortrag von Andreas Bogk war interessant und gespickt mit Dingen, die ich mir gerade so merken, aber nicht sofort verstehen konnte. Lambda-Kalkül zum Beispiel. Oder mein persönliches Lieblingswortungetüm: Curry-Howard-Isomorphismus. Oder mit anderen Worten: Hä?
Grundidee ist: In Zukunft werden keine Programme mehr runtergeschrieben, sondern so formuliert, dass sie mathematisch beweisbar sind. Grob vereinfacht gesagt, gibt es im Idealfall keine Fehler mehr, jeder Zustand eines Programms ist wohldefiniert und vorhersehbar. Und falls nicht, sind die Rechner und zugrundeliegenden Systeme so sicher, dass nur das abstürzt, was gerade abstürzt. Sonst nichts.
Das hört sich natürlich ziemlich fantastisch an und ist bei weitem nicht so einfach. Andreas hat sich glücklicherweise die Zeit genommen, mich in seine Küche einzuladen und die Idee der Beweisbarkeit von Hard- und Software noch einmal ganz genau zu erklären. Nebenbei erfahrt ihr außerdem, warum die Computer, die wir heutzutage benutzen, aufgrund eines einzelnen Videospiels entstanden sind und dass der Begriff “Account” tatsächlich aus der Buchhaltung kommt.
Podcast: Play in new window | Download (Duration: 1:08:06 — 64.6MB)
Einen Cameoauftritt hatten in dieser Folge von Der Wahrheit außerdem der einzige Starcraft-2-Fan, der das Spiel noch mehr liebt, als mein Chef, sowie Coq und Coq. Andreas’ Literaturempfehlung zum tieferen Einstieg in das Thema: Benjamin Pierce – Software Foundations.
