Fefes Blog

Fragen? Antworten! Siehe auch: Alternativlos

Thu May 9 2019

• [l] Microsoft macht gerade mit Everycrypt Wind, einer Crypto-Library mit formaler Verifikation. Das ist eine Kooperation mit Inria und der Carnegie Mellon Uni und inhaltlich ein Meilenstein (auch wenn ich nicht so ein Fan von formaler Verifikation bin, weil die Komplexität des Korrektheitsbeweises üblicherweise über der Komplexität des als korrekt zu beweisenden Codes ist, und ich es daher nicht offensichtlich finde, wieso ich dem Beweis glauben sollte). Die große Neuerung gegenüber früheren Ansätzen ist, dass sie nicht nur ein paar Primitiven formal verifizieren wollen, sondern einen ganzen TLS-Stack. Wenn ich das richtig verstehe, haben sie allerdings bisher nur das Record Layer von TLS formal verifiziert, und das ist eigentlich nihct das PRoblem. Das Handshake und der Schlüsselaustausch sind das Problem. Mein Hotelinternet ist gerade zu schlecht, um das anzugucken, vielleicht missverstehe ich den Artikel da auch.

  Wiedem auch sei: Die sind weiter gekommen als alle vor ihnen. Und versuchen auch praxisrelevant zu ein, indem nicht nur eine Hochsprachen-Implementation verifiziert wird, sondern auch die plattformspezifischen Assembler-Implementationen.

  Sie haben auch eine verifizierte TLS-Library, aber die ist in F# bzw. F* und da ist nicht klar, wie performant die ist und wie man die in existierende Projekte eingebunden kriegt. Dennoch: Ein großer Schritt vorwärts!