Jahrestreffen 2024

Programm

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?

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

Physical attacks pose a serious threat to hardware implementations of cryptographic algorithms. More precisely, the power consumption acquired during a cryptographic operation on a target hardware device in general leaks information about the processed secret key material. Additionally, an adversary who is capable to inject faults in an ongoing encryption or decryption processes can utilize the faulty ciphertexts or plaintexts to extract information about the applied secret key.

Hence, over the last two decades a plethora of countermeasures have been proposed to thwart these attacks individually. However, powerful attackers could combine both attack vectors such that combined protection mechanisms are required. Even for experienced designers, the implementation of such countermeasures is an error-prone and tedious task and practical evaluations are expensive and time-consuming. 

This talk introduces the formal verification framework VERICA which analyzes gate-level netlists of countermeasures against physical attacks. In order to understand how VERICA works, we first introduce power side-channel and fault-injection attacks, discuss how both attack vectors can be modeled, and present established countermeasures. Based on this background, we present novel modeling strategies for hardware circuits providing protection against combined attacks. Eventually, we give more insights into VERICA and present several case studies in which we also reveal flaws in existing desiofgns from the literature.