The annual meetings serve as an informal exchange on current research issues in this field. They offer a unique opportunity (especially for young scientists) to present their current and ongoing work. The program of the annual meetings therefore includes space for invited lectures: Presentations on current research project initiatives, specialist presentations reporting on specific work and research results or overview presentations describing the profile of individual working groups.

The aim of this specialist group is to provide a discussion forum in the German-speaking area in the field of computer and information security that deals with basic research and the application of formal or mathematically precise techniques in software engineering. Of interest to the FG is security in the sense of both safety and security.

- fg-fomsess.gi.de

Invited Speakers

• Gidon Ernst
• Silvia Lizeth Tapia Tarifa
• Jan Richter-Brockmann

Call for Contribution

Please use this form to register a  research talk of 15 or 30 minutes (including a time for questions) on current research topics or publications.

Registration

If you want to attend the annual meeting, please register yourself: 

Registration Form

We are charge a registration fee of 50 EUR.

If you travel with the Deutsche Bahn, you might want to consider using Helmholtz special offer (fix prices for train tickets within Germany). 

The local organization is the responsibility of Dr. Alexander Weigl.

Preliminary Programme

Monday, 7th October

Tuesday, 8th October

Abstracts

Gidon Ernst: Reasoning across abstraction boundaries—what is needed to fully
automate proofs of data and algorithm refinement?

Abstract: Fully automated proofs of "shallow" properties like memory safety is nowadays readily automated at real-world scale. In contrast, proofs of "deep" properties, notably correctness with respect to a precise but abstract behavioral model, heavily rely on human input to provide key annotations and proof steps. We will explore ideas on the quest towards fully automating such proofs, which suggest that the key challenge, which traditionally viewed to be invariant inference, may better be regarded as a lemma synthesis problem.

Maike Schwammberger: Modelling and Analysis in Mobility Software Engineering

Maximilian Kodetzki: Correctness-by-Construction for Non-Functional Properties

Correctness-by-Construction is a refinement-based approach to developing software incrementally on the basis of a formal specification. By applying defined rules, functional correctness can be guaranteed with respect to the specification. In addition to functional correctness of software, non-functional properties also play an important role in today's software development. In particular, energy and resource consumption are becoming increasingly important in times of climate crisis, rising energy prices, and high inflation. We therefore want to extend the by-Construction approach for non-functional properties. The aim is to be able to develop software that is not only functionally correct, but also complies with defined limits of consumption parameters (energy, memory, etc.) by developing it in a refinement-based and incremental manner and verifying compliance with a specification.

Nils Lommen: KoAT: An Automatic Complexity Analysis Tool for Integer Programs

Silvia Lizeth Tapia Tarifa: Integrating Data Privacy Compliance into Active Object Languages

As users of digitalized services are more and more required to share their personal data, it becomes increasingly important for applications to comply with users’ consent to handle their personal data. Ensuring compliance with such consent requires reasoning globally about both the flow of information and the interaction of different parties handling personal data. In this direction, privacy by design principles cultivate a philosophy that endorses the development of systems with built-in abilities to demonstrate compliance with data privacy to guarantee the protection of personal data. However, there is an apparent mismatch in translating such abstract principles into explicit methods that support systematic solutions for integrating data privacy by design and default. To this end, in this talk, I present a language-based privacy integration approach into a core privacy-aware active object language. 

Zoltan Mann: Urgency in cybersecurity risk management: toward a solid theory

Jens Leicht: PriPoCoG: A Prolog-Based Framework for Handling GDPR-Compliant Privacy Policies

The General Data Protection Regulation of the European Union (GDPR) introduced rules regarding privacy policies. These rules made the process of creating compliant privacy policies a complex process. We created the Privacy Policy Compliance Guidance framework (PriPoCoG), that supports all parties involved in handling privacy policies. During policy creation our privacy policy editor gives compliance feedback and guidance to policy authors, ensuring that policies are GDPR-compliant. The framework uses a formal privacy policy language called Prolog-Layered Privacy Language (P-LPL), which also partially formalizes the GDPR. The editor can also be used by data protection authorities to check existing P-LPL policies for GDPR-compliance. Privacy Policy Based Access Control (P2BAC) ensures that the data handling described inside the privacy policy is enforced. It ensures that no further processing of data, other than what is described in the policy, is performed by data controllers and data processors. Our privacy policy interface presents privacy policies in a comprehensible way to data subjects. Data subjects can customize the privacy policies and provide partial consent. We provide a management component which ensures that all parties involved in handling a data subject’s data act according to the customized privacy policy. The management component updates all parties about any changes in the customized policies using a sticky policy approach. All in all, our framework aims at improving the overall privacy policy landscape.

Malte Josten: Large Language Models as a Cyber Threat

The rapid advancement and increased accessibility of large language models (LLMs) have significantly expanded their utility across various disciplines. However, this widespread adoption also raises significant security concerns, particularly in the realm of cybersecurity. Their growing sophistication and affordability make them both easy and cost-effective to use, opening the door to a wide range of applications, from benign to malicious. We have already demonstrated that LLM-generated spam emails pose a credible threat to modern spam filters. For example, using OpenAI's ChatGPT, we found that 70% of previously detected spam emails were reclassified as legitimate.
In this talk, I will present our latest findings and highlight other potential areas of concern - beyond just spam and phishing - while emphasizing the urgent need to strengthen the robustness of text-based security mechanisms.

Fabian Hauck: Formal Web Security Analysis

Standardized protocols form the basis for the World Wide Web, which is indispensable in our modern world. It is crucial to guarantee the security of these protocols to strengthen trust in the web and enable security-critical applications like online banking or digital identities. Formal methods play a key role not only in finding vulnerabilities in protocol specifications but also in proving protocols secure with respect to an attacker model. In this talk, we will present two tools based on formal methods to prove the security of high-risk protocols. The first tool is the pen-and-paper Web Infrastructure Model (WIM), which is the most comprehensive model of web infrastructure to date and has proven effective in i) finding vulnerabilities in many widely used international Web Standards and ii) proving security properties for new versions of these standards which we have helped shape. The second tool is DY*, a mechanized model written in F* and designed to analyze crypto protocols. DY* allows a fine-grained analysis up to the implementation level featuring machine-checked proofs that anyone can verify with the push of a button. This tool is actively being developed and has already demonstrated its value in several analyses, including a study of the Signal messaging protocol.

Jan Richter-Brockmann: Computer-Aided Verification of Countermeasures against Physical Attacks

Venue

The meeting takes place in the seminar room (50.34, R131) in the main building of the faculty.

Campus map or on Google Maps

The room is on the first (not ground) floor. If you take the east entry of the building (the one with the library), you reach the directly to the left.

Local transport

Public transportation: KVV

You reach the building via the stops Durlacher Tor/KIT Campus (Line 1-5, S2, S4, S5, S7, S8, S52) or Karl-Wilhelm-Platz (Line 3 and 4). 

Note that: Durlacher Tor/KIT Campus is a station with multiple tracks, some of them are also in  the underground (denoted by a U, Line 1 and 2). Also, the Oct, 7th is the end of the track construction season, you should not be effected by the construction heavily, as these are happening in the west of Karlsruhe, but the lines can switch their routes back to normal on this day or the night.

From Durlacher Tor: Keep heading north along the Adenauerring (North is when you see a mint colored KIT building to your left). Faktulty is at the right end of the first-reached pedestrian bridge over Adenauerring.

From Karl-Wilhelms-Platz go north into Parkstraße, at the first intersection keep west (left) on the opposite street. The building is the last one before the pedestrian bridge (on the right).

The following lines are recommended from the main train station:

• 2- Wolfahrtsweier,
• S4-Bretten/Gölshausen (or Heilbronn),
• or 3-Waldstadt

There is no difference between the S and not-S lines within Karlsruhe (same ticket, different companies). The difference is that S-lines are regional trams and can go far outside of Karlsruhe, where as the not-S lines are operating within the city boundaries.

Accommodation

In the immediate vicinity of the faculty, there is only the

• Hoepfner Burghof, Haid-und-Neu-Straße 18, 76131 Karlsruhe

Still within walking distance would be:

• 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

There are more hotels in the west, make sure they are close to an S-Bahn station. Almost every line passes the campus: S2, S4, S5, S7, S8, S52, 1, 2, 3, 4, 5.

Therefore, you can also stay at the InterCity Hotel at the train station or the ACHAT Hotel Karlsruhe City.