Die Benutzeroberfläche für das Graph Rendering zeichnet sich nun durch ansprechende Farben, Icons und Schriften aus. Sie bietet darüber hinaus erweiterte Funktionalitäten für effiziente Navigation.
Inhalt dieses Projektes ist eine Neukonzeption und Neuentwicklung des Rendering von Graphen innerhalb der interaktiven Nutzeroberfläche des Tamarin Prover . Das neue Werkzeug ersetzt die bisherige Darstellung als statisches Bild und generiert einen dynamisch, durch den Browser gerenderten Graphen in SVG/HTML/CSS. Damit erlaubt es interaktive Analysen von Ergebnisgraphen des Tamarin-Prover-Protokoll-Beweissystems, durch performante Navigation selbst in komplexen Graphen. Die Implementierung basiert auf React (TypeScript) mit MUI.
Der Tamarin-Prover [1] ist ein Werkzeug zur Modellierung und Analyse von Sicherheitsprotokollen [2]. Dabei bietet die Software eine web-basierte Benutzeroberfläche zur Analyse. In dieser Oberfläche spielt die Darstellungen von Graphen eine große Rolle. Diese Graphen zeigen den Ablauf des Protokolls, meistens in verschiedenen Abschnitten.
Bis dato werden diese Graphen als statische Bilder dargestellt. Die Aufgabe bestand nun darin die Darstellungen der Graphen zu überarbeiten und den Nutzern diese Graphen interaktiv zugänglich zu machen.
Die neue Oberfläche für die Graphen wurde möglichst unabhängig von dem alten Frontend konzeptioniert. Bei dem Design wurden die Nutzer des Tamarin Provers einbezogen und die Ideen mit ihnen abgestimmt. Gespräche wurden unter anderem mit Cas Cremers, Aurora Naska und Niklas Medinger geführt.
Das Design der neuen Oberfläche umfasst alle Grundlagen: Farben, Icons, Fonts und eine konsistente Designsprache.
Darüberhinaus wurden neue Features entworfen:
Technologie
Es war von Anfang an klar, dass das neue Tool Teil des bestehenden Frontends des Tamarin Provers wird. Das Frontend basiert auf einer Webview, also mussten auch das neue Tool mit HTML, SVG, CSS und Javascript umgesetzt werden. Damit die Entwicklung komfortabler und sicherer wird, wurde statt Javascript in Typescript entwickelt. Die ganze Anwendung basiert letzten Endes auf React. Folgende Schlüssel-Technologien und Libraries wurden genutzt:
Graph
Die größte Herausforderung bestand im Layouting und Rendering des Graphen. Vom Backend wird der Graph als JSON übermittelt und geparsed. Anschließend gilt es den Graphen übersichtlich, korrekt und visuell ansprechend darzustellen.
Bei der Implementierung orientierte man sich an dem Algorithmus des dot-Graph-Rendering [3]. Kurz gesagt, der Graph wird geladen und anschließend Graph analysiert. Die Graphknoten werden anhand ihrer Beziehungen von unten nach oben reihenweise in ein Gitter einsortiert. Danach werden die Kanten segmentiert und falls notwendig unsichtbare Hilfsknoten in den Graphen eingebaut, um die Kanten korrekt zu führen.
Der analysierte und strukturierte Graph wird dann als Hierarchie von React-Komponenten in ein SVG gerendert. Das Innere der Knoten wiederum ist HTML im SVG.
Features
Es wurden nicht alle angedachten Features umgesetzt. Hier die wichtigsten.
Navigation
Der Graph kann mittels der Maus bewegt werden. Außerdem kann man hinein- und herauszoomen, per Maus und per Buttons. Ebenso gibt es die Möglichkeit die Ansicht zurückzusetzen.
Detailstufen
Die Knoten des Graphen können in drei verschiedenen Detailstufen angezeigt werden.
1. https://github.com/tamarin-prover/tamarin-prover
2. https://tamarin-prover.com/manual/master/book/001_introduction.html