Jahrestreffen 2021
Das FoMSESS-Jahrestreffen 2021 findet am 4. und 5. Oktober, jeweils von 15:00 bis 18:00 Uhr, online statt.
Veranstaltungsort
Online - Link wird den registrierten Teilnehmern zugeschickt bzw. kann bei Herrn Mann erfragt werdenBeschreibung
NEU: Extended Abstracts
Die Vortragenden des Jahrestreffens 2021 hatten die Möglichkeit, extended Abstracts ihrer Beiträge einzureichen. Hier können Sie die eingereichten extended Abstracts herunterladen.
Beschreibung
Das diesjährige FoMSESS-Jahrestreffen findet am 4. und 5. Oktober 2021, jeweils am Nachmittag, als Online-Veranstaltung statt.
Neben einem allgemeinen Austausch zu Themen rund um formale Methoden und Software-Engineering für sichere Systeme hat das diesjährige Jahrestreffen ein besonderes Fokusthema: Sicherheit von Online-Wahlen.
Dazu haben wir mehrere renommierte Experten als Keynote Speaker gewinnen können:
- Ralf Küsters, Universität Stuttgart
- Peter Ryan, University of Luxembourg
- Carsten Schürmann, IT University of Copenhagen
Weitere Informationen finden Sie auf dem Reiter "Programm".
Programm
(kleinere Änderungen sind noch möglich)
Montag, 04.10.2021
15:00 – 15:15 | Begrüßung |
15:15 – 16:00 | Invited Talk Carsten Schürmann, IT University of Copenhagen Public Confidence and Internet Voting |
16:00 – 16:30 | Mario Gleirscher, Universität Bremen Verifikation und Test von Sicherheitssteuerungen in der Mensch-Maschine-Zusammenarbeit |
16:30 – 16:45 | Pause |
16:45 – 17:30 | Invited Talk Ralf Küsters, Universität Stuttgart Ordinos and Kryvos: Verifiable Tally-Hiding E-Voting |
17:30 – 18:00 | Jan Jürjens, Universität Koblenz-Landau Software-Sicherheitsanalyse bei Systemänderungen |
Dienstag, 05.10.2021
15:00 – 15:15 | Begrüßung |
15:15 – 16:00 | Invited Talk Peter Ryan, University of Luxembourg Hyperion: a voter-friendly, verifiable, coercion resistant voting scheme |
16:00 – 16:30 | Michael Kirsten, KIT Modular Construction of Verified Voting Rules |
16:30 – 16:45 | Pause |
16:45 – 17:15 | Dieter Hutter, DFKI Sichere Workflows in Seehäfen |
17:15 – 17:45 | Tagung der Fachgruppe |
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.