Jahrestreffen 2021

Programm

(kleinere Änderungen sind noch möglich)

Montag, 04.10.2021

Dienstag, 05.10.2021

ABSTRACTS

Carsten Schürmann, IT University of Copenhagen

Public Confidence and Internet Voting

TBD

Mario Gleirscher, Universität Bremen

Verifikation und Test von Sicherheitssteuerungen in der Mensch-Maschine-Zusammenarbeit

Moderne Mensch-Maschine-Zusammenarbeit strebt nach feinerer Interaktion zwischen Mensch und Maschine sowie mehr Autonomie der beteiligten Roboter und sonstigen Maschinen, um die Produktivität, die Aufgabenkomplexität und die ergonomische Arbeitsteiligkeit zu erhöhen. Die Einhaltung von Arbeitsschutz und Betriebssicherheit erfordert eine regelmäßige Überarbeitung nötiger Sicherheitsfunktionen (z.B. Überwachungs-, Leit- und Abschalteinrichtungen), sodass selbst solche Teilsysteme komplexe Logiken (u.U. auch mit KI-Unterstützung) beinhalten können, um eine optimale und sichere Zusammenarbeit von Mensch und Maschine in verschiedenen Anwendungen, wie z.B. Produktion, Logistik, Transport, Medizin-, Agrar-, Gebäude- und Heimanwendungen, zu ermöglichen.  In diesem Vortrag wird ein zweistufiges Verfahren zur Entwicklung korrekter Steuerungslogiken für Sicherheitsfunktionen in den genannten Einsatzbereichen vorgestellt.  Die erste Stufe nutzt eine einfache Form der Aufgaben- und Risikomodellierung sowie stochastische Modellprüfung für Korrektheitsbeweise und optimale abstrakte Logikselektion.  Die zweite Stufe nutzt moderne Verfahren des vollständigen Konformanztests, um selektierte und übersetzte konkrete Steuerungslogiken zu validieren.  Der Vortrag gibt einen Einblick zum aktuellen Forschungsstand.

Ralf Küsters, Universität Stuttgart

Ordinos and Kryvos: Verifiable Tally-Hiding E-Voting

In this talk,  I will cover some of the main security properties modern e-voting system should satisfy and discuss their sometimes surprising relationships. I will also present a security property called tally-hiding, which has been less considered in the literature so far but which is of increasing importance, and present two recent systems, Ordinos and Kryvos, which provide tally-hiding verifiable e-voting. Finally, I discuss the formal analysis of such and other e-voting systems.

Jan Jürjens, Universität Koblenz-Landau

Software-Sicherheitsanalyse bei Systemänderungen

Sicherheitszertifizierungen großer und komplexer Systeme sind mit großem Aufwand verbunden. Eine besondere Herausforderung ist, dass IT-Systeme heutzutage sehr langlebig und ständig Änderungen unterworfen sind. Nach jeder Änderung muss die Zertifizierung eigentlich vollständig wiederholt werden, um die Vertrauenswürdigkeit der Systeme aufrechtzuerhalten, was aber viel zu aufwendig ist.
Der Vortrag präsentiert einen werkzeuggestützten Ansatz für Software-Sicherheitsanalysen, der bei Änderungen den Aufwand für die erneute Zertifizierung minimiert. Dabei wird die Auswirkung von Evolution auf die Einhaltung von Anforderungen mit automatischen Werkzeugen analysiert (z.B. bei Einsatz von Designtechniken wie Verfeinerung und Architekturprinzipien wie Modularisierung). Damit wird ein werkzeuggestützter Ansatz für evolutionsbasierte Softwareanalyse vorgestellt, der den Aufwand für die erneute Analyse minimiert. Er erlaubt eine automatische änderungsbasierte Sicherheitsanalyse, zum einen auf der Spezifikationsebene und zum anderen auf der Implementierungsebene. Dabei wird die Nachverfolgbarkeit der Anforderungen von der Modellierungs- zur Implementierungsebene sichergestellt und die Einhaltung der Anforderungen durch die Implementierung mittels statischer Analyse und Runtime-Verification überwacht.

Peter Ryan, University of Luxembourg

Hyperion: a voter-friendly, verifiable, coercion resistant voting scheme

TBD

Michael Kirsten, KIT

Modular Construction of Verified Voting Rules

Voting rules aggregate multiple individual preferences in order to make collective decisions. Commonly, these mechanisms are expected to respect a multitude of different fairness and reliability properties, e.g., to ensure that each voter’s ballot accounts for the same proportion of the elected alternatives, or that a voter cannot change the election outcome in her favor by insincerely filling out her ballot. However, no voting rule is fair in all respects, and trade-off attempts between such properties often bring out inconsistencies, which makes the construction of arguably practical and fair voting rules non-trivial and error-prone.
In this talk, I present a formal and systematic approach for the flexible and verified construction of voting rules from composable core modules to respect such properties by construction. Formal composition rules guarantee resulting properties from properties of the individual components, which are of generic nature to be reused for various voting rules. We provide a prototypical logic-based implementation with proofs for a selected set of structures and composition rules within the theorem prover Isabelle/HOL and a Prolog-based extension for automatic synthesis of voting rules and the corresponding proofs. The approach can be readily extended in order to support many voting rules, e.g., from the literature, by extending the set of modules and composition rules.

Dieter Hutter, DFKI

Sichere Workflows in Seehäfen

Die Digitalisierung in Seehäfen verknüpft die IT-Infrastruktur verschiedener Akteure (z. B. Reedereien, Terminals, Zoll, Hafenbehörden), um komplexe Arbeitsabläufe im Hafen digital zu begleiten. Die Sicherheit der digitalen Arbeitsabläufe hängt dabei nicht nur von der Sicherheit jedes einzelnen Akteurs ab, sondern die Akteure müssen auch zusätzliche Garantien für andere Akteure bieten, wie z.B. die Einhaltung von Verpflichtungen in Bezug auf empfangene Daten oder die Überprüfung der Integrität der bisher beobachteten Arbeitsabläufe. In diesem Vortrag werden die globalen Sicherheitsanforderungen (z.B. Zurechenbarkeit, Integrität, Vertraulichkeit) der Workflows analysiert und entsprechend der Art und Weise, wie die Workflow-Daten gespeichert und verteilt werden, in Anforderungen und Verpflichtungen für die einzelnen Akteure zerlegt. Es werden Sicherheitsmechanismen zur Erfüllung der sich daraus ergebenden Anforderungen vorgestellt, die zusammen mit den Garantien aller einzelnen Akteure die Sicherheit des gesamten Workflows gewährleisten.