Jahrestreffen 2022
Das FoMSESS-Jahrestreffen 2022 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 2022 hatten die Möglichkeit, extended Abstracts ihrer Beiträge einzureichen. Hier können Sie die eingereichten extended Abstracts herunterladen.
Beschreibung
Auch 2022 findet das FoMSESS-Jahrestreffen online statt, am 4. und 5. Oktober, jeweils von 15:00 bis 18:00 Uhr.
Die Teilnahme ist kostenlos. Um teilzunehmen, melden Sie sich bitte mit einer formlosen E-Mail an Herrn Zoltan Mann an. Geben Sie dabei bitte auch an, ob Sie einen Vortrag halten möchten.
Im Fokus des Jahrestreffens steht der Austausch zu Themen rund um formale Methoden und Software-Engineering für sichere Systeme. Wir haben dieses Jahr drei renommierte Forscherinnen als Invited Speaker gewinnen können, die verschiedene Bereiche innerhalb von FoMSESS abdecken:
- Ina Schaefer, KIT
- Alena Naiakshina, RUB
- Kristina Hostakova, ETH Zürich
Weitere Informationen finden Sie auf dem Reiter "Programm".
Programm
(kleinere Änderungen sind noch möglich)
Dienstag, 04.10.2022
15:00 – 15:10 | Begrüßung |
15:10 – 15:55 | Invited Talk Kristina Hostakova, ETH Zürich Analyzing security of complex cryptographic protocols |
15:55 – 16:25 | Jan Jürjens, Universität Koblenz-Landau Engineering Trustworthy Data-Intensive Systems |
16:25 – 16:40 | Pause |
16:40 – 17:25 | Invited Talk Ina Schaefer, KIT Ensuring Safety and Security of Variant-Rich Software Systems by Sample-based Testing and Correctness-by-Construction |
17:25 – 17:55 | Philipp Kern, KIT Algorithms for Neural Network Verification |
Mittwoch, 05.10.2022
15:00 – 15:05 | Begrüßung |
15:05 – 15:50 | Invited Talk Alena Naiakshina, RUB Helping Developers with Password Security |
15:50 – 16:20 | Jan Laufer, Universität Duisburg-Essen Automatische Quantifizierung und Priorisierung von Datenschutzrisiken |
16:20 – 16:35 | Pause |
16:35 – 17:00 | Mario Gleirscher, Universität Bremen A Manifesto for Applicable Formal Methods |
17:00 – 17:30 | Tagung der Fachgruppe |
ABSTRACTS
Kristina Hostakova, ETH Zürich
Analyzing security of complex cryptographic protocols
Defining and analyzing the security of cryptographic primitives and protocols can be an extremely challenging task. Especially when the protocol to be analyzed involves multiple parties, runs in parallel to other protocols or might itself be used as a subroutine of a larger system.
In my talk, I will focus on the security analysis of protocols built on top of blockchains using the Universal Composability (UC) model of Ran Canetti. This commonly used framework captures concurrent protocol executions and comes with a composition theorem allowing for modular protocol designs and security proofs. I will explain how existing blockchain protocols utilize the UC model, discuss some generic principles for providing UC security and mention a few shortcomings of the approach.
Jan Jürjens, Universität Koblenz-Landau
Engineering Trustworthy Data-Intensive Systems
Decision-making systems are prone to discrimination against individuals with regard to protected characteristics such as gender and ethnicity. Detecting and explaining the discriminatory behavior of implemented software is difficult. To avoid the possibility of discrimination from the onset of software development, we propose a model-based methodology called MBFair that allows for verifying UML-based software designs with regard to individual fairness. The verification in MBFair is performed by generating temporal logic clauses, whose verification results enables reporting on the individual fairness of the targeted software. We study the applicability of MBFair using three case studies in real-world settings including: a bank services system, a delivery system, and a loan system. We empirically evaluate the necessity of MBFair in a user study and compare it against a baseline scenario in which no modeling and tool support is offered. Our empirical evaluation indicates that analyzing the UML models manually produces unreliable results with a high chance that analysts overlook true-positive discrimination. We conclude that analysts require support for fairness-related analysis, such as our MBFair methodology.
Ina Schaefer, KIT
Ensuring Safety and Security of Variant-Rich Software Systems by Sample-based Testing and Correctness-by-Construction
Modern Software Systems exist in many different variants in order to adapt to different user requirements or application contexts, especially in the automotive domain. Over-the-Air updates are designed to alter existing functionality or add novel functionality to the variants deployed in the field. This poses an additional challenge to ensuring the safety and security of these software systems, as updates to variants and versions of these variants need to be considered for quality assurance. In this talk, I focus on a combination of post-hoc testing and by-construction engineering approaches to ensure the safety and security of variant-rich software systems. First, sample-based testing allows selecting a representative subset of variants deployed in the field which need to be tested to ensure the safety of an over-the-air update. Second, refinement-based program construction can be extended to a correctness-by-construction engineering approach for software variants, considering functional specifications and information flow properties in tandem and allowing to identify functionally correct feature interactions still leading to security vulnerabilities.
Philipp Kern, KIT
Algorithms for Neural Network Verification
Neural networks are increasingly applied in safety critical domains like self-driving cars and collision avoidance for aircraft, where errors can have severe consequences. This necessitates provable guarantees about their behaviour and has made the development of dedicated verification algorithms an active area of research.
I characterize situations where machine learning is usually applied and talk about what can be verified under these circumstances.
This is followed by a brief overview of different proposed verification algorithms, before I focus on one successful method - symbolic interval propagation. Furthermore, I present various optimizations that help to increase verification performance.
Alena Naiakshina, RUB
Helping Developers with Password Security
Software developers' programming security mistakes can threaten millions of end users' data. To deepen insights into developers' security behavior around the security-critical task of user-password storage, Naiakshina et al. conducted laboratory, online, and field studies with computer science students, freelancers, and professional developers from various companies. Besides investigating software developers' processes and security practices while storing user passwords in databases, they tested the usability of different application programming interfaces (APIs) and explored the methodological implications of several security-study parameters, including deception task design, sample variety, and the comparison of qualitative with quantitative research approaches.
Jan Laufer, Universität Duisburg-Essen
Automatische Quantifizierung und Priorisierung von Datenschutzrisiken
Datenverarbeitende Systeme arbeiten in zunehmend dynamischen Umgebungen, wie dem Cloud- oder Edge-Computing. In solchen Umgebungen können Änderungen zur Laufzeit zu einem dynamischen Auftreten von Systemschwachstellen führen, die den Datenschutz verletzen (folgend Datenschutzrisiken). Solche Datenschutzrisiken sind Systemkonfigurationen, bei denen ein Angreifer unbefugten Zugriff auf vertrauliche Daten erlangen könnte. Ein selbst-adaptives System kann solche Datenschutzrisiken durch automatische Selbstanpassungen adressieren. Gibt es mehrere Datenschutzrisiken gleichzeitig, muss das System entscheiden, welche es zuerst auflöst.
Zur Priorisierung von Maßnahmen werden im Bereich der Cybersicherheit risikobasierte Ansätze genutzt, die die Systemsicherheit (Security) am effektivsten verbessern. Traditionell ist die Risikobewertung ein manueller und zeitaufwändiger Prozess. Die Auflösung von Datenschutzrisiken zur Laufzeit erfordert jedoch eine schnelle Entscheidungsfindung, was wiederum eine automatisierte Risikobewertung bedingt.
Diese Präsentation stellt ein mathematisches Modell zur Quantifizierung von Datenschutzrisiken während der Laufzeit vor. Das Modell berücksichtigt die spezifischen Eigenschaften von Datenschutzrisiken wie die Zeit, die ein Angreifer benötigt, um (persönliche) Daten über eine Systemschwachstelle abzugreifen, und den Schaden, der durch den Angriff entsteht. Durch die Risiko-Quantifizierung kann unser Ansatz automatisiert fundierte Entscheidungen über die Priorisierung von Datenschutzrisiken treffen. Experimente zeigen, dass unsere Methode zur Risiko-Priorisierung zu einer Reduktion des Schadens durch Datenschutzrisiken, von bis zu 15,8 % beiträgt.
Mario Gleirscher, Universität Bremen
A Manifesto for Applicable Formal Methods
Formal methods were frequently shown to be effective and, perhaps because of that, practitioners are interested in using them more often. Still, these methods are far less applied than expected, particularly, in critical domains where they are strongly recommended and where they have the greatest potential. Our hypothesis is that formal methods still seem not to be applicable enough or ready for their intended use. In critical software engineering, what do we mean when we speak of a formal method? And what does it mean for such a method to be applicable both from a scientific and practical viewpoint? Based on what the literature tells about the first question, with this manifesto, we lay out a set of principles that when followed by a formal method give rise to its mature applicability in a given scope. Rather than exercising criticism of past developments, this manifesto strives to foster an increased use of formal methods to the maximum benefit.