Open Source im professionellen Einsatz

Wireguard-Protokoll formal verifiziert

18.07.2017

Wireguard ist ein noch recht junges Projekt, das eine Aufnahme in den Linux-Kernel anstrebt und als mögliche Alternative zu Open VPN gilt. Nun haben die Projektteilnehmer die Sicherheit das Wireguard-Protokolls mit Hilfe des Tamarin-Provers formal verifiziert.

295

Das virtuelle, verschlüsselte Tunnelinterface Wireguard soll in Zukunft im Kernel andocken, sich einfach nutzen lassen und verspricht zugleich eine hohe Sicherheit und dank weniger Kontextwechsel eine gute Performance. Damit sehen einige es bereits als Nachfolger oder Ergänzung zu Open VPN. Ein IP-gebundener "Cookie-MAC-Mechanismus" soll gegen DoS-Angriffe helfen, zugleich antwortet Wireguard nicht auf nicht-authentifizierte Pakete (Stealthiness).

Die Wireguard-Entwickler haben das Protokoll des Projekts nun mit Hilfe eines Tools namens Tamarin einer formalen Verifizierung unterzogen. Das Werkzeug ist eine Entwicklung von der ETH Zürich, steht auf Github als Open-Source-Software bereit und kann Security-Merkmale von Protokollen uneingeschränkt Verifizieren und Falsifizieren. Mit diesen Tests lässt sich also herausfinden, ob die Sicherheitsmerkmale zumindest mathematisch halten, was sie versprechen.

Um das zu tun, zieht Tamarin vereinfacht gesprochen das Modell eines Security-Protokolls heran und spezifiziert Aktionen, die Agents in unterschiedlichen Rollen ausführen. Ein Agent ist dann zum Beispiel der Protokoll-Initiator, einer übernimmt die Rolle des Antwortenden und so weiter. Als Aktionen werden Angreifer spezifiziert ebenso wie die Sicherheitsmerkmale, die das Protokoll mitbringen soll. Mit Tamarin lässt sich dann automatisiert beweisen, dass das Protokoll trotz paralleler Nutzung und Aktionen eines Angreifers seinen Merkmalen gerecht werden kann.

Laut diesen Tests mit Tamarin besitzt das Wireguard-Protokoll verschiedene Security-Merkmale: Es ist formal korrekt und verfügt über eine starke Schlüsselvereinbarung & Authentizität. Es widersteht Personifizierungen mit gestohlenen Schlüsseln, so genannten Key Compromise Impersonations. Wenn also Eve den Schlüssel von Alice stiehlt, kann sie sich nicht Alice gegenüber als andere Person ausgeben. Auch lassen sich Schlüssel nicht so teilen, dass nicht alle Teilnehmer davon erfahren (Unknown Key-share Attack). Wireguard beherrscht Key Secrecy und Forward Secrecy, unwiederholbare Sessions und versteckt die Identität. Die Details lesen Interessierte in einem Paper des Projekts nach.

Ähnliche Artikel

  • Dockercon 2017: Linuxkit und Moby angekündigt

    Auf der Dockercon kündigte der Container-Hersteller Docker an, seine Werkzeugkiste um zwei Neuzugänge zu erweitern: Linuxkit und Moby. Sie richten sich an Baumeister für Container-Plattformen respektive Window-Admins mit Linux-Bedarf.

  • Webserver Monkey mit neuen Features und Apache-Lizenz

    Der HTTP-Server Monkey ist in Version 1.5.0 mit neuen Features erschienen. Gleichzeitig haben die Entwickler die Lizenz von LGPLv2.1 in Apache 2.0 geändert.

  • 26c3: Blitzableiter nimmt Spannung aus Flash-Inhalten

    Ungewohnte Zusammenarbeit: Auf Anregung des Bundesamtes für Sicherheit in der Informationstechnik (BSI) hat Felix 'FX' Lindner der Hackergruppe Phenoelit neues Terrain betreten, die Sicherheit von Flash untersucht und schließlich Schutzmaßnahmen erdacht - nahm er doch bislang vornehmlich die Rolle des Angreifers ein, der Lücken aufzeigt.

  • Abhörsicherheit

    Allerspätestens seit Ed Snowden ist klar, dass Geheimdienste – und wer weiß, wer sonst noch – IP-Telefonate abhören. Magazin-Autor Eitel Dignatz wundert sich, wie wenige Firmen Maßnahmen dagegen ergreifen, und streut zugleich Sand ins ratternde Offener-Quellcode-ist-sicher-Getriebe.

  • Adobe bringt AIR und Flex für Webanwendungen

    Adobe Systems hat die Verfügbarkeit der Beta-Ausgaben von Adobe Integrated Runtime (AIR) und Adobe Flex 3 angekündigt. Beide Versionen sollen Adobes Engagement im Open-Source-Bereich untermauern, jedoch steht eine freie Variante der AIR für Linux noch aus.

comments powered by Disqus

Ausgabe 11/2017

Digitale Ausgabe: Preis € 6,40
(inkl. 19% MwSt.)

Stellenmarkt

Artikelserien und interessante Workshops aus dem Magazin können Sie hier als Bundle erwerben.