TAMARIN PROVER
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.
ART
Forschungssoftware
THEMA
Tamarin Prover, Redesign Benutzeroberfläche
JAHR
2023
SOFTWARE
Tamarin Prover, Figma, React, TypeScript, Haskell, Jetbrains IntelliJ Ultimate
SKILLS
User Research, Usability Testing, Conceptual Design, Visual Design, Prototyping, Software Design, Research Software Engineering
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 ist ein Werkzeug zur Modellierung und Analyse von Sicherheitsprotokollen. Dabei bietet die Software eine webbasierte 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.
Diese Graphen wurden zuvor 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.
Das Design der neuen Oberfläche umfasst alle Grundlagen: Farben, Icons, Fonts und eine konsistente Designsprache.
Darüberhinaus wurden neue Features entworfen:
Feinkonzept als Wireframe
Das fertige Visual Design (1/2)
Das fertige Visual Design (2/2)
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:
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. Kurz gesagt, der Graph wird geladen und anschließend 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.
Ein Graph im neuen Tamarin Graph Frontend.
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.
Detailstufe 1: Nur der Name des Knoten wird angezeigt.
Detailstufe 2: Zusätzlich werden die Namen der Vor- und Nachbedingungen sowie Aktionen angezeigt.
Detailstufe 3: Mit der Anzeige der vollständigen Parameter erreicht ein Knoten die detailreichste Darstellung.