Leserreporter: Wer schöne Verschwörungslinks für mich hat: ab an felix-bloginput (at) fefe.de!
[zurück][ältere Posting][neuere Posting] Donnerstag, 09 Mai 2019 | Blog: 4 | No: 43017
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!
[zurück]
[ältere Posting][neuere Posting]
[zurück][ältere Posting][neuere Posting] Donnerstag, 09 Mai 2019 | Blog: 4 | No: 43017
Ein großer Schritt vorwärts!
Microsoft macht gerade mit Everycrypt Wind
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!
Twiter-Ticker
Fefes Latest Youtube Video Links
Der Betrieb der KraftZeitung kostet Geld. Da wir auch weiterhin unabhängig, überparteilich und ohne kommerzieller Werbung für Sie da sein wollen, sind wir auf Ihre Spende angewiesen. Vielen Dank.
