„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)
Subscribe: RSS
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.
Ich hab mir noch nicht genug Gedanken gemacht, um einen ausführlichen Kommentar zu schreiben, aber: SEHR interessant! 🙂 Ich hör den Podcast inzwischen zum dritten Mal, da es für mich als (noch) nicht Informatiker eher bahnhofig klingt, aber es macht riesig Spaß, euch beim fachsimpeln zuzuhören.
Ich habe schon oft versucht, mich dem Thema über Wikipedia zu nähern. Dieser Podcast hat allerdings viel mehr Spaß gemacht. Bitte mehr Podcasts über Typtheorie und automatische Beweise!
Es gibt aktuell bereits ein Softwareentwicklungsverfahren, welches zwar nicht mathematische Beweisbarkeit garantiert, aber zumindest dafür sorgt, dass die gewünschte Funktionsweise eines Programms zu jedem Zeitpunkt sichergestellt ist. Das ganze nennt sich „test-driven development“ und zeichnet sich dadurch aus, das man zuerst automatisierbare Testszenarien erstellt, die festlegen, wie sich ein Programm in verschiedenen Situationen verhalten soll. Erst danach beginnt man mit der eigentlichen Implementierung und entwickelt solange, bis man alle Tests erfolgreich absolvieren kann.
btw: Es gibt auch Programmierer die mit Mathematik sehrwohl etwas anfangen können 😉
Hatte mir schon den Vortrag auf dem 27C3 angehört war aber trotzdem noch mal sehr interessant.
btw finde ich Andreas Stimme irgendwie total angenehm zum zuhören.
Hallöchen,
da ich nun ein DieWeisheit-Hörer bin, dachte ich, ich guck auch mal in DieWahrheit. Sehr angenehm anzuhören.
Der Podcast ist zwar ziemlich lange her, aber was ich nicht verstand war der Bezug auf Windows Vista. Das normale Konsumenten eher genervt von Sicherheit waren als diese zu wollen…Ich habe seinerzeit nichts Gutes von Windows Vista und höherer Sicherheit gehört (außer als Vermarktungsgrundlage und im Bezug zur Benutzerkontenführung). Die Aussage hätte mich detailierter interessiert.
DerWeisheit – Asche über mein Haupt
„[…] sind die Rechner und zugrundeliegenden Systeme so sicher, dass nur das abstürzt, was gerade abstürzt.“
Das wäre dann … BeOS!