Home  |  deutsch  |  Legals  |  Data Protection  |  Sitemap  |  KIT

FoMSESS Jahrestagung 2019

15. Treffen der GI Fachgruppe FoMSESS
29. November 2019
KARLSRUHE, Fakultät der Informatik

Die Jahrestreffen dienen zum informellen Austausch zu aktuellen Forschungsfragen auf diesem Gebiet. Sie bieten (insbesondere für jüngere Nachwuchswissenschaftler) eine einmalige Gelegenheit zur Präsentation ihrer aktuellen und laufenden Arbeiten. Im Programm der Jahrestreffen ist deshalb u.a. Raum für ingeladene Vorträge: Vorträge über aktuelle Forschungsprojekt-Initiativen, Fachvorträge, in denenüber konkrete Arbeits- und Forschungsergebnisse berichtet wird oder Übersichtsvorträge, die das Profil einzelner Arbeitsgruppen beschreiben.

Zielsetzung dieser Fachgruppe ist es, im Bereich Computer- und Informationssicherheit ein Diskussionsforum im deutschsprachigen Raum zu bieten, das sich mit der Grundlagenforschung und Anwendung formaler oder mathematisch präziser Techniken im Software-Engineering beschäftigt. Von Interesse für die FG ist Sicherheit im Sinne sowohl von Safety als auch von Security.

Die Tagung findet im Gebäude 50.34 Raum 301 statt (s.u.).
Am Donnerstag (28.11.) treffen wir uns um 19:00 zu einem gemeinsamen Abendessen im Hoepfner Burghof (Reservierung auf Schiffl). Alle Teilnehmenden sind herzlich willkommen!

Programm

Start Titel Speaker
09:00 Sicherheit im Zeitalter großskaliger Angreifer … Tim Günesyu
10:10 Kaffeepause  
10:40 CriSGen: Constraint based Generation of Critical Scenarios for Autonomous Vehicles Andreas Nonnengart
11:10 Automatic Modularization of Large Programs for Bounded Model Checking Marko Kleine Büning
11:40 IT-Sicherheit in Häfen: Das Projekt SecProPort Dieter Hutter
11:55 Probabilistische Nichtinterferenz mit dem RLSOD-Kriterium Simon Bischof
12:25 Program-level Noninterference Verification of the Credential Generation in the GI Election Software Michael Kirsten
12:40 Tagung der Fachgruppe  
13:00 Mittagspause  
14:00 Provably Forgetting of Information in Manufacturing Systems Alexander Weigl
14:30 Heuristiken und Modellierungen für die Wertebereichsanalyse von Steuerungssoftware mit Policy Iteration Marcus Völker
15:00 Integration of Safety- and Security Reasoning in Automotive Systems Rhea Rinaldo
15:30 Kaffeepause  
16:00 Smart Contracts: Applications for Deductive Program Verification Jonas Schiffl
16:15 WIM: An Expressive Formal Model of the Web Infrastructure Guido Schmitz
16:30 A Problem Meta-Data Library for Research in SAT Markus Iser
16:45 Ende
Simon Bischof
Probabilistische Nichtinterferenz mit dem RLSOD-Kriterium
Bei parallelen Programmen können geheime Daten bereits durch unterschiedliche Wahrscheinlichkeiten der öffentlichen Ausgaben geleakt werden. Das sogenannte LSOD-Kriterium kann solche Lecks erkennen, ist allerdings unpräzise. In diesem Vortrag werde ich das an unserem Lehrstuhl entwickelte präzisere RLSOD-Kriterium vorstellen. Zudem werde ich einen kurzen Überblick über den Korrektheitsbeweis und den Stand der Formalisierung im Theorembeweiser Isabelle geben."
Tim Günesyu
Sicherheit im Zeitalter großskaliger Angreifer - Ein Überblick zum Exzellenzcluster CASA und dem MPI für Cybersicherheit in Bochum (Invited Talk)
Dieter Hutter
IT-Sicherheit in Häfen: Das Projekt SecProPort (Short)
Markus Iser
A Problem Meta-Data Library for Research in SAT (Short)
Experimental data and benchmarks play a crucial role in developing new algorithms and implementations of SAT solvers. Besides comparing and evaluating solvers, they provide the basis for all kinds of experiments, for setting up hypothesis and for testing them. Currently – even though some initiatives for setting up benchmark databases have been undertaken, and the SAT Competitions provide a “standardized” collection of instances – it is hard to assemble benchmark sets with prescribed properties. Moreover, the origin of SAT instances is often not clear, and benchmark collections might contain duplicates. In this paper we suggest an approach to store meta-data information about SAT instances, and present an implementation that is capable of collecting, assessing and distributing benchmark meta-data.
Michael Kirsten
Program-level Noninterference Verification of the Credential Generation in the GI Election Software (Short)
Electronic voting (e-voting) systems used in public elections need to fulfill strong requirements concerning both safety and security, such as, e.g., reliability, robustness, privacy of votes, coercion resistance, and various versions of voter verifiability. Currently, the GI premiers to perform their annual elections using an e-voting system that provides a cryptographic eligibility verifiability mechanism. As a core requirement for this mechanism, the employed voter credentials are not allowed to leak to the e-voting provider, possibly compromising the eligibility verifiability. This case study employs the deductive information-flow calculus of the KeY theorem prover, providing a precise proof that the source code of the employed credential generation component cannot leak the voter credentials to untrusted parties. In this talk, I report on our experiences and the current state of the case study, verifying a non-trivial security property for a small real-world program of a rich fragment of Java.
Marko Kleine Büning
Automatic Modularization of Large Programs for Bounded Model Checking
The verification of real-world applications is a continuous challenge which yielded numerous different methods and approaches. However, scalability of precise analysis methods on large programs is still limited. We thus propose a formal definition of modules that allows a partitioning of the program into smaller code fragments suitable for verification by bounded model checking. We consider programs written in C/C++ and use LLVM as an intermediate representation. A formal trace semantics for LLVM program runs is defined that also takes modularization into account. Using different abstractions and a selection of fragments of a program for each module, we describe four different modularization approaches. We dene desirable properties of modularizations, and show how a bounded model checking approach can be adapted for modularization. Two modularization approaches are implemented within the tool QPR-Verify, which is based on the bounded model checker LLBMC. We evaluated our approach on a medium-sized embedded system software encompassing approximately 160KLoC.
Andreas Nonnengart
CriSGen: Constraint based Generation of Critical Scenarios for Autonomous Vehicles (Short)
Ensuring pedestrian-safety is paramount to the acceptance and success of autonomous cars. The scenario-based training and testing of such self-driving vehicles in virtual driving simulation environments has increasingly gained attention in the past years. A key challenge is the automated generation of critical traffic scenarios which usually are rare in real-world traffic, while computing and testing all possible scenarios is infeasible in practice. In this talk, we present a formal method-based approach, CriSGen, for an automated and complete generation of critical traffic scenarios for virtual training of self-driving cars. These scenarios are determined as close variants of given but uncritical and formally abstracted scenarios via reasoning on their non-linear arithmetic constraint formulas, such that the original maneuver of the self-driving car in them will not be pedestrian-safe anymore, enforcing it to further adapt the behavior during training.
Rhea Rinaldo
Integration of Safety- and Security Reasoning in Automotive Systems
Safety has always been a prior concern in automotive development, but with the growing connectivity requirements due to the increasing demand for autonomous features, security concerns are rising dramatically. Safety and security are partly intertwined, as security incidents can affect the system's safety and the other way round. Consequently, evaluating both properties separately is illusive in general, yet still widely adapted in automotive development. In this talk we address the described problem by introducing an approach for the integrated safety and security reasoning. Thereby we abstract the system from details and focus on the interleaving effects of safety and security, measured by probabilities. On this basis we define a transformation into a Discrete-Time Markov Chain (DTMC), which allows for the application of probabilistic model checkers. We describe the analysis of the system by means of an example and show how possible weaknesses in the communication structure or due to data dependencies can be found. \end{talk}
Jonas Schiffl
Smart Contracts: Applications for Deductive Program Verification (Short)
Smart contracts are programs that run on a distributed ledger platform. They usually manage resources representing valuable assets. Moreover, their source code is visible to potential attackers, they are distributed, and bugs are hard to fix. Thus, they are susceptible to attacks exploiting programming errors. Their vulnerability makes a rigorous formal analysis of the functional correctness of smart contracts highly desirable. We show that the architecture of smart contract platforms offers a computation model for smart contracts that yields itself naturally to deductive program verification. We discuss different classes of correctness properties of distributed ledger applications, and show that design-by-contract verification tools, e.g., the KeY tool, are suitable to prove these properties.
Guido Schmitz
WIM: An Expressive Formal Model of the Web Infrastructure (Short)
Marcus Völker
Heuristiken und Modellierungen für die Wertebereichsanalyse von Steuerungssoftware mit Policy Iteration
Im Bereich der statischen Programmanalyse ist die Wertebereichsanalyse ein wichtiges Werkzeug, um Wertebereiche für Programmvariablen abzuschätzen. Ein Algorithmus für die Wertebereichsanalyse ist die sogenannte Policy Iteration, bei der das Programm mittels einer Heuristik in ein einfacher zu analysierendes Programm transformiert wird. Dieses wird dann mit einem Standardansatz wie z.B. Fixpunktiteration analysiert und die Ergebnisse auf Korrektheit in Bezug auf das ursprüngliche Programm getestet. Sollten die Ergebnisse inkorrekt sein, werden andere Vereinfachungen ausprobiert, bis korrekte Ergebnisse erzielt werden. Da die Standardheuristik bei der Programmtransformation bestimmte Annahmen über das Programm trifft, ist es möglich, eine bessere Heuristik zu konstruieren, wenn zuerst eine Voranalyse feststellt, ob diese Annahmen korrekt sind oder nicht und eine auf die gefundenen Programmeigenschaften passende Transformation auswählt. Ein weiteres Thema ist die Modellierung des Eingabeprogramms auf eine Art und Weise, sodass die Heuristik angewandt werden kann. Hierbei werden beispielsweise polynomielle Ungleichungen, die im Programm als Schleifenbedingungen vorkommen, umgeformt und durch lineare Ungleichungen approximiert werden, die die Heuristik behandeln kann.
Alexander Weigl
Provably Forgetting of Information in Manufacturing Systems (Short)
During the manufacturing process, information are generated and aggregated that constitute a business secrets and therefore need a high protection. On the other hand, if we can prove, that an information is absented, the effort for the protection for this system could be invested on different information, aspects or systems. For this, we develop the notion of information forgetting of a reactive system. This notion describes that a reactive system needs to forget the information about a secret within a certain amount of cycles. This property limits the amount of historical information an attacker can learn by observing a manufacturing system. Moreover, we formalise and prove the notion of an information forgetting system with Relational Test Tables. We evaluate the verification on the industry demonstrator for KASTEL SVI project, which was provided by the Fraunhofer IOSB and developed by industrial third-party contractor. In this demonstrator, we are able to show, that a selected business secret &endash; the number of wheel turns &endash; is not forgotten. We suggest and prove a fix of the leak. We close with an elaborate discussion on the verification and results and also with remarks to the how information forgetting relates supports quantifiable security.

Anreise

Fakultät der Informatik
Karlsruher Institut für Technologie
Am Fasanengarten 5
76131 Karlsruhe

Das Treffen findet im Raum 301 (3. OG) statt.
Von der Straßenseite betreten Sie den Ostflügel (rechter Eingang) des Gebäudes. Mit der Wendeltreppe oder Aufzug kommen Sie ins dritte Stockwerk. Der Raum ist dann direkt in der rechten Ecke des Etagenfoyers.

Hinweis: Der Raum verfügt über einen 4:3 Beamer mit VGA und eine Kreidetafel.

Campusplan oder auf Google Maps

Öffentlicher Nahverkehr: KVV

Der Campus ist über die Haltestellen Durlacher Tor/KIT Campus Süd und Karl-Wilhelms-Platz zu erreichen. Hinweis: Die Haltestelle Durlacher Tor/KIT Campus - Süd ist auf Google-Maps noch falsch eingetragen. Dort heißt die richtige Haltestelle Durlacher Tor/KIT.

Vom Durlacher Tor aus: Halten Sie sich nördlich entlang des Adenauerrings. Am östlichen (rechts) Ende Fußgängerbrücke über den Adenauerring ist die Faktultät.

Vom Karl-Wilhelms-Platz gehen nördlich in die Parkstraße, bei der ersten Kreuzung halten Sie sich westlich (links) auf der gegenüberliegenden Straße. Das Gebäude ist das letzte vor der Fußgängerbrücke (rechts).

Vom Hauptbahnhof aus sind folgende Linien zu empfehlen:

  • 2— Wolfahrtsweier,
  • S4—Bretten/Gölshausen (oder Heilbronn),
  • oder 4—Waldstadt (Fährt bis Karl-Wilhelms-Platz).

Unterkünfte

In direkter Nähe der Fakultät, liegt nur die

  • Hoepfner Burghof, Haid-und-Neu-Straße 18, 76131 Karlsruhe
Noch in Laufweite wären:
  • sevenDays Karlsruhe Hotel BoardingHouse, Gerwigstraße 47, 76131 Karlsruhe
  • Hotel "Am Gottesauer Schloss", Gottesauer Str. 32-34, 76131 Karlsruhe
  • Hotel Am Markt, Kaiserstraße 76, 76133 Karlsruhe

Mehr Hotels gibt es im Westen, achten Sie auf Nähe zu einer S-Bahn Station. Nahezu jede Linie fährt am Campus vorbei: S2, S4, S5, S7, S8, S52, 1, 2, 4, 5

Registrierung

Bitte registrieren Sie sich, wenn Sie eine Teilnahme am Jahrestreffen planen. Es gibt zwei Arten von Beiträgen:

  • Einen Fachvortrag von 15 oder 30 Minuten (inkl. Fragenrunde) über aktuelle Forschungsthemen oder Veröffentlichungen.
  • Ein Poster zu einem Forschungsthema.
  • Ein Tutorial von 120 Minuten zu einem am Lehrstuhl entwickeltem Werkzeug.

Bitte melden Sie Ihre Teilnahme per E-Mail bei fomsess19@lists.kit.edu an. Geben Sie bitte dabei an, ob Sie einen Beitrag planen (Vortrag oder Tutorial; Titel und Abstract), sowie ob Sie am informellen Abendessen teilnehmen. Die lokale Organisation liegt bei Jonas Schiffl und Alexander Weigl.

Navigation

Wichtige Termine

  • 29.11.2019: FoMSESS