Building secure and dependable information systems is one of the biggest challenges of the 21st century. With ransomware attacks paralyzing whole countries and digital infrastructures for health and essential services under threat, information system security is no longer an academic question, but a necessity.

In this talk, we take a look at those who build secure digital environments: System Administrators. These information workers face multi-facetted challenges, and understanding how they (can) build secure system stretches beyond methods of individual disciplines. Secure cryptographic algorithms may be of no use if their key material is accidentally published. Software updates cannot prevent a compromise if they have never been installed. An intrusion detection system may leave defenders blind if attacks hide in a storm of false positive notifications.

Following a line along prior research, we see how we have to combine methodology from various fields to scientifically approach and improve information system security. First, we see how we can analytically assess challenges for information system security. However, to quantify their impact we then have to develop and apply network measurement techniques. While security related measurements illustrate the scale of vulnerabilities— misconfigurations for example—they lack in explanatory value as to ¬why vulnerabilities occur. Using qualitative methodology here to better understand and explain the interaction of technology, organizations, and human factors then allows us to take a practical perspective on security challenges. Ultimately, this enables us to develop and advocate for solutions that do not only provide the right technology, but also ensure that this technology can be effectively used to create secure information systems.

Given an integer n ≥ 2, let P (n) stand for its largest prime factor. Given integers k ≥ 2 and ℓ ≥ 2, consider the set Ek,ℓ of those integers n ≥ 2 for which P (n + i)ℓ | n + i for i = 0, 1, . . . , k. Each of these sets is very small. For instance, the smallest element of E3,2 is 1 294 298, the smallest known element of E3,3 has 77 digits and no elements of E4,2 are known, even though all these sets are believed to be infinite. In this talk, using elementary, analytic and probabilistic approaches, we will shed some light on these sets and raise several open problems. This is joint work with Nicolas Doyon, Florian Luca and Matthieu Moineau.

---

This talk will be a hybrid event. You can join the meeting in E1 5 room 002 in Saarbrücken, in G26 room 111 in Kaiserlautern or via Zoom. Please contact the Office team for Zoom link information.

Finite-precision programs inevitably introduce numerical uncertainties, which are usually a combination of input uncertainties due to noisy sensors of the underlying hardware and finite-precision errors that can potentially occur at every operation. While these errors are individually small, they propagate through an application and can make its final results meaningless. Furthermore, an implementation on actual hardware necessitates a trade-off between accuracy and efficiency. It is thus essential to verify that the numerical uncertainties remain acceptably small and to optimize the implementations such that the results are accurate enough for the applications.

There exist several static (or dynamic) analyses for finite-precision programs. The static analyses generally perform sound worst-case analysis and primarily focus on straight-line special syntax code, with limited support for conditionals and loops. In contrast, dynamic analyses usually scale well for real-world programs. However, the current dynamic analyses of finite-precision are limited to relatively small programs. Moreover, they do not provide any correctness guarantee that is crucial for critical applications.

In this thesis, we propose analysis and optimization techniques to expand the horizons of the current finite-precision analysis. Our approach captures the probability distributions of inputs and performs probabilistic analysis for small but exciting embedded and neural network examples. Using our analysis, it is possible to (conditionally) verify larger programs (with more than 2K lines of code, including complex programming and data structures). Furthermore, we enable program optimization by soundly generating quantized neural network classifiers with millions of parameters and fewer bits significantly faster than (generic) static fixed-point arithmetic tuners. Finally, we aim to scale the analysis for larger programs with probabilistic inputs.

Automated design of correct-by-construction controllers for continuous dynamical systems is a core algorithmic problem in the design of safety critical cyber-physical systems (CPS). A popular design paradigm constructs simpler but sound discrete abstractions of the original continuous systems, on which known reactive synthesis methods can be used to design controllers. The algorithms following this paradigm are collectively known as the Abstraction-Based Controller Design (ABCD) procedures. In this thesis, we build ABCD procedures which are faster and more modular compared to the state-of-the-art, and can handle problems which were beyond the scope of the already existing techniques.

The thesis has three main parts: In the first part, we address the scalability bottleneck of the existing ABCD procedures by using a multi-layered abstraction of varying granularities. We implemented this multi-layered ABCD algorithm in the tool called Mascot, using which we empirically demonstrate the significant saving in computation time achieved through our approach. In the second part of the thesis, we propose a modular design procedure of sound local controllers for a network of discrete abstract systems communicating via discrete/boolean variables and having local specifications. We propose a sound algorithm, where the abstractions negotiate a pair of local assume-guarantee contracts (and controllers as a by-product), in order to synchronize on a set of non-conflicting and correct behaviors. We show the effectiveness of our algorithm using a prototype tool, called Agnes, on a set of discrete benchmark examples. In the third part, we present a novel ABCD procedure for discrete-time nonlinear stochastic control systems and omega-regular control specifications. We first present a novel 2.5-player game abstraction for the control problem at hand. Alongside our abstraction, we present a direct and efficient symbolic algorithm for solving 2.5-player games for omega-regular specifications. We implemented our algorithms in a prototype tool called Mascot-SDS, using which we empirically show that our approach is both faster and more memory-efficient than an alternate approach that was independently developed around the same time.

This talk will be based on my PhD work on using formal methods to enhance both programming of robotic systems and learning of autonomous agents.

After giving a broad overview of the work, I will focus on the problem of inferring specifications from examples. In particular, we will discuss the problem of inferring a linear temporal logic (LTL) formula from sets of positive and negative example traces, as well as from a set of positive examples only.

Building on this method, I will describe LTLTalk, a tool that helps users of a robotic system transfer their intent into an LTL specification. The approach combines the intent signals from a single demonstration and a natural language description given by a user. A set of candidate specifications is inferred by encoding the problem as a satisfiability problem for propositional logic. This set is narrowed down to a single specification through interaction with the user: the user approves or declines generated simulations of the robot's behavior in different situations.