Google and Apple have jointly provided an API for exposure notification in order to implement decentralized contract tracing apps using Bluetooth Low Energy, the so-called “Google/Apple Proposal”, which we abbreviate by “GAP”. We demonstrate that in real-world scenarios the current GAP design is vulnerable to (i) profiling and possibly de-anonymizing infected persons, and (ii) relay-based wormhole attacks that basically can generate fake contacts with the potential of affecting the accuracy of an app-based contact tracing system. For both types of attack, we have built tools that can easily be used on mobile phones or Raspberry Pis (e.g., Bluetooth sniffers). The goal of our work is to perform a reality check towards possibly providing empirical real-world evidence for these two privacy and security risks. We hope that our findings provide valuable input for developing secure and privacy-preserving digital contact tracing systems.

This paper builds on product line CCS (PL-CCS), an algebraic approach to modeling the behavior of software product lines. The semantics of PL-CCS specifications is given in terms of labeled transition systems for individual products as well as for the entire product line and can be derived automatically. In this paper, we extend PL-CCS with a concept for specifying dependencies, show how to integrate it into a development methodology for product lines and validate its practical applicability by modeling a typical reactive system from the automotive domain. Most importantly, due to the algebraic nature of our model, we can derive calculation laws that allow to compute common parts of a product line. The application of the corresponding calculation rules is illustrated in detail with an example. By this, we obtain a formal foundation for restructuring product lines.

Abstract Formal verification of software systems is a challenge that is particularly important in the area of safety-critical automotive systems. Here, approaches like direct code verification are far too complicated, unless the verification is restricted to small textbook examples. Furthermore, the verification of application logic is of limited use in industrial context, unless the underlying operating system and the hardware are verified, too. This paper introduces a generic model stack, allowing the verification of all system layers as well as the concrete application models being used in the upper layers. The presented models and proofs close the gap between the correctness proof for the lower layers of car electronics developed at the Saarland University and the verification procedure for distributed applications developed at the Technische Universität München.

Increasing complexity due to the multitude of different functions and their interactions as well as a rising number of different product variants are just some of the challenges that must be faced during the development of multi-functional system families. Addressing this trend we present an approach combining model-based development with product line techniques aiming at a consistent description of a software product family as well as supporting the configuration of its variants. We integrate the concept of variability in our framework [7] which only supported the representation of single software systems on subsequent abstraction levels so far. For the configuration of a concrete product we extend this framework by a feature-based model which allows to configure and derive single systems from a system family model. Furthermore, we explain how the complexity due to the possibly huge amount of configuration decisions can be handled by means of a staged configuration process.