Jahrestreffen 2023
Das FoMSESS-Jahrestreffen 2023 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 2023 hatten die Möglichkeit, extended Abstracts ihrer Beiträge einzureichen. Hier können Sie die eingereichten extended Abstracts herunterladen.
Beschreibung
Auch 2023 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 Forscher als Invited Speaker gewinnen können, die verschiedene Bereiche innerhalb von FoMSESS abdecken:
Das vorläufige Programm finden Sie auf dem Reiter "Programm".
Programm
(vorläufig)
Mittwoch, 04.10.2023
15:00 – 15:05 | Begrüßung |
15:05 – 15:50 | Invited Talk André Platzer, KIT Logic of Autonomous Dynamical Systems |
15:50 – 16:20 | Achim D. Brucker, University of Exeter Towards the Formal Verification of Neural Networks in Isabelle/HOL |
16:20 – 16:35 | Pause |
16:35 – 17:05 | Jens Leicht, Universität Duisburg-Essen GDPR-Compliance by Design: Erstellung von Privacy Policies aus Datenflussdiagrammen |
17:05 – 17:35 | Frank Zeyda, Independent consultant and researcher Rigorous Digital Engineering with Formal Methods: a personal perspective |
Donnerstag, 05.10.2023
15:00 – 15:05 | Begrüßung |
15:05 – 15:50 | Invited Talk Krishna Gummadi, MPI SWS Fact Checking Generative AI Systems |
15:50 – 16:10 | Jonas Schiffl, KIT Ein Praktischer Begriff von Liveness-Eigenschaften in Smart-Contract-Anwendungen |
16:10 – 16:30 | Nicklas Gäbler, Universität Bremen Realisierung einer digitalen Meldestelle im Rahmen des Hinweisgeberschutzgesetz |
16:30 – 16:45 | Pause |
16:45 – 17:30 | Invited Talk Sven Peldszus, RUB Security Compliance: From Requirements to Runtime |
17:30 – 17:50 | Tagung der Fachgruppe |
ABSTRACTS
André Platzer, KIT
Logic of Autonomous Dynamical Systems
This talk highlights some of the most fascinating aspects of the logic of dynamical systems which constitute the foundation for developing cyber-physical systems (CPS) such as robots, cars and aircraft with the mathematical rigor that their safety-critical nature demands. Differential dynamic logic (dL) provides an integrated specification and verification language for dynamical systems, such as hybrid systems that combine discrete transitions and continuous evolution along differential equations. In dL, properties of the global behavior of a dynamical system can be analyzed solely from the logic of their local change without having to solve the dynamics.
In addition to providing a strong theoretical foundation for CPS, differential dynamic logics as implemented in the KeYmaera X prover have been instrumental in verifying many applications, including the Airborne Collision Avoidance System ACAS X, the European Train Control System ETCS, automotive systems, mobile robot navigation, and a surgical robotic system for skull-base surgery. dL is the foundation to provable safety transfer from models to CPS implementations and is also the key ingredient behind autonomous dynamical systems for Safe AI in CPS.
References:
André Platzer. Logical Foundations of Cyber-Physical Systems. Springer, 2018. DOI:10.1007/978-3-319-63588-0
André Platzer. Logics of dynamical systems LICS, 2012: 13-24. DOI:10.1109/LICS.2012.13
Achim D. Brucker, University of Exeter
Towards the Formal Verification of Neural Networks in Isabelle/HOL
Neural networks are being used successfully to solve classification problems, e.g., for detecting objects in images. It is well known that neural networks are susceptible if small changes applied to their input result in misclassification. Situations in which such a slight input change, often hardly noticeable by a human expert, results in a misclassification are called adversarial attacks. Such attacks can be life-threatening if, for example, they occur in image classification systems used in autonomous cars or medical diagnosis.
Systems employing neural networks, e.g., for safety or security critical functionality, are a particular challenge for formal verification, which usually expects a program or algorithm that can be analyzed. Such a program or algorithm does, per se, not exist for neural networks.
In this talk, I will start with an introduction into the area of formal
verification of systems based on machine learning in general, and neural networks in particular. After that, I will present our ongoing work in developing a verification approach for neural networks in Isabelle/HOL.
This is joint work with Amy Stell (University of Exeter, UK).
Jens Leicht, Universität Duisburg-Essen
GDPR-Compliance by Design: Erstellung von Privacy Policies aus Datenflussdiagrammen
Datenschutzerklärungen (Privacy Policies) werden häufig verwendet, um die Transparenzanforderungen von Datenschutzvorschriften wie der EU-Datenschutz-Grundverordnung zu erfüllen. Privacy Policies beschreiben, wie der für die Datenverarbeitung Verantwortliche mit den Daten der betroffenen Personen umgeht. Fach- und Rechtsexperten erstellen diese Richtlinien meist manuell.
In diesem Vortrag stelle ich eine werkzeuggestützte Methode zur Erstellung präziser Privacy Policies vor. Dabei werden Informationen aus der Entwicklungsphase eines Systems genutzt.
Während der Analyse von Datenschutz- und Sicherheitsrisiken werden Informationen über das Systemverhalten in Form von Datenflussdiagrammen gesammelt. Diese Diagramme beschreiben, welche Daten von wo nach wo innerhalb des Systems und zu welchen externen Akteuren diese fließen. Auf Basis dieser Informationen kann das Grundgerüst einer Privacy Policy erstellt werden, in dem die Datenflüsse bereits enthalten sind. Die so extrahierten Informationen sind einer der wichtigsten Teile einer Privacy Policy, da sie Transparenz über die Weitergabe von Daten an externe Parteien schaffen.
Frank Zeyda, Independent consultant and researcher
Rigorous Digital Engineering with Formal Methods: a personal perspective
Rigorous Digital Engineer (RDE) is a methodology and process to create trustworthy, safe and secure hardware and software systems `from the ground up'. It permeates the entire life-cycle of traditional hardware, software and firmware engineering, from requirements and domain models to product-line descriptions, architectural specifications, component and unit design, and implementation. Each life-cycle stage is accompanied by meaningful models that support formal analysis, refinement, validation and verification activities, so that models at different levels of abstraction remain strongly connected to each other in a mathematical sense.
RDE has formed the basis of many projects at Galois, Inc. that require the highest levels of assurance, targeting embedded encryption devices, applications in avionics, space and defense, and secure voting systems - just to name a few. Despite this, the methodology and process of RDE has only recently been clearly articulated, as an adaptable process and methodology that can cater for a large class of heterogeneous systems, from pure software to pure hardware and anything in between.
In this presentation, I will reflect on my personal understanding, experience and view of RDE, and its relationship to the use of Formal Methods and underlying tool support. This entails both my academic experience working on novel formal modeling and verification strategies, i.e., for control, embedded, and cyber-physical systems, and industrial experience working closely with Galois to help advocate, shape and apply their RDE vision as a methodology in its own right.
Krishna Gummadi, MPI SWS
Fact Checking Generative AI Systems
TBD
Jonas Schiffl, KIT
Ein Praktischer Begriff von Liveness-Eigenschaften in Smart-Contract-Anwendungen
Smart Contracts sind Programme, die in Blockchain-Netzwerken automatisiert Ressourcen verwalten. In diesem Kontext sind Liveness-Eigenschaften häufig essentiell: Wenn ich dem Smart Contract Geld überweise, bekomme ich es dann irgendwann zurück? Diese Art von Eigenschaft ist schwer zu spezifizieren und zu verifizieren, vor allem, weil für Beweise von Liveness-Eigenschaften häufig Annahmen über das Verhalten von verschiedenen Akteuren getroffen werden müssen.
Thema dieses Vortrags ist eine pragmatische Herangehensweise an Liveness. Die in der Literatur diskutierten Eigenschaften deuten darauf hin, dass in Smart-Contract-Anwendungen häufig eine bestimmte Art von Liveness erforderlich ist, die mit der Möglichkeit zusammenhängt, bestimmte Zustandsänderungen herbeizuführen (z.B. einen Transfer von Tokens). Wir führen einige intuitive Konzepte zur formalen Spezifikation dieser Art von Liveness ein und zeigen, wie sich damit auch die Verifikation im Vergleich zu existierenden Ansätzen vereinfachen lässt.
Nicklas Gäbler, Universität Bremen
Realisierung einer digitalen Meldestelle im Rahmen des Hinweisgeberschutzgesetz
Das im Juli in Kraft getretene Hinweisgeberschutzgesetz verpflichtet Organisationen, ab einer gewissen Größe, Meldekanäle für hinweisgebende Personen bereitzustellen. Dort soll es möglich sein, Hinweise zu beobachteten oder erfahrenen Verstößen gegen geltendes europäisches oder deutsches Recht an die jeweilige Organisation zu melden. Meine Bachelorarbeit befasste sich mit der Realisierung eines Systems, mit welchem Organisationen einen solchen Meldekanal in digitaler Form online verfügbar einrichten können. Dabei wurde der Fokus auf die sicherheitsrelevanten Aspekte gelegt, die einen Schutz der vertraulichen Informationen gewährleisten, die über diesen Meldekanal mitgeteilt werden. Es wurde dafür nicht nur ein digitaler Meldekanal realisiert, sondern eine digitale Meldestelle, die neben dem Meldekanal einer Organisation zusätzlich ermöglicht, mitgeteilte Meldungen innerhalb dieses Systems entgegenzunehmen und zu bearbeiten. Die erarbeitete Sicherheitsarchitektur ermöglicht den sicheren Austausch zwischen hinweisgebenden Personen und dem Personal der Meldestelle, selbst im Falle anonym getätigter Meldungen. Die Architektur wurde dabei mit der Annahme aufgestellt, dass die digitale Meldestelle von einem externen semivertrauensvollen Anbieter betrieben wird, so dass es erforderlich ist, dass vertrauliche Informationsgehalte zu keinem Zeitpunkt der digitalen Meldestelle selbst bekannt werden. In diesem Vortrag wird die erarbeitete Sicherheitsarchitektur der digitalen Meldestelle vorgestellt und dessen Kernaspekte näher erläutert.
Sven Peldszus, RUB
Security Compliance: From Requirements to Runtime
Modern software-intensive systems often operate in a variety of critical environments, such as healthcare or autonomous driving, under constantly changing environmental conditions. In order to perform their diverse tasks under these conditions, such systems must constantly adapt their operating parameters and reconfigure their systems from time to time. Considering the essential security requirements inherent to these systems and the domains in which they operate, this tremendous dynamism exacerbates the problem of verifying the compliance of the implemented systems. In the end, it is inevitable to verify security at runtime. To do this, we must trace security requirements through the entire software development lifecycle, from requirements to runtime, and verify compliance at each development stage. Current approaches to this problem rely on extensive manual effort or rigorous processes with detailed low-level traceability links, which are typically not feasible for large and complex systems such as robotic systems. One of the main obstacles is the significant differences in how security is addressed at different stages. To develop effective approaches applicable to complex, potentially distributed systems, we need to bridge this gap to systematically incorporate security checks both statically and dynamically at runtime.