50 Jahre KIT-Fakultät für Informatik

Vor genau 50 Jahren wurde in Karlsruhe Informatikgeschichte geschrieben. Das damals neue Fach Informatik wurde mit großer Anstrengung und viel Pioniergeist an der damaligen Universität Karlsruhe (TH) in institutionelle Formen gegossen. So entstand in Karlsruhe die erste Fakultät für Informatik an einer deutschen Hochschule.

Diese Jubiläum, möchten wir mit einem Festakt gebührend feiern. Im Tagesprogramm werfen wir einen Blick auf die vergangenen 50 Jahre Fakultätsgeschichte und schauen mit vier hochrangig besetzten Keynotes aber auch auf die Zukunft der Informatik.

alle Bilder von der Jubiläumsveranstaltung gibt es in unserer Galerie.

Programm

Vorträge

Breaking and Fixing Modern Payment Protocols with Tamarin
Prof. Dr. David Basin, ETH Zurich

The security of payment systems is critical as their exploitation can lead to widespread, large-scale financial loss.  We show how to use Tamarin, a security protocol model checker, to find serious exploitable vulnerabilities in the EMV payment protocols.  EMV is the international protocol standard for smartcard payment that is used in over 9 billion payment cards worldwide. Despite the standard’s advertised security, various issues have been previously uncovered, deriving from logical flaws that are hard to spot in EMV’s lengthy and complex specification, running over 2,000 pages.

We have formalized a comprehensive model of EMV in Tamarin. We use our model to automatically discover new flaws that lead to critical attacks on EMV.  In particular, an attacker can use a victim's EMV card (e.g., Mastercard or Visa Card) for high-valued purchases without the victims PIN.  Said more simply, the PIN on your EMV card is useless!  We describe these attacks, their repair, and more generally why using formal methods is essential for critical protocols like payment protocols.

"Networking as Civil Infrastructure: The Role of Policy and Economics"
Prof. Dr. Henning Schulzrinne, Columbia University, New York, USA

The internet has assumed a pivotal role as one of the four civilizational infrastructures, along with the drinking and waste water systems, transportation, and energy. Indeed, these other infrastructures increasingly depend on the safe and reliable operation of the internet or IP-based networks to function. Together, they form society's lifelines. Networking research, however, may not have adjusted to this newfound responsibility. Despite their different roles, all of these infrastructures share a number of features, such as their relatively slow evolution, the co-existence of old and new technology, and the persistence of long-term interfaces that are technically outdated, but "good enough". For civil infrastructures, reliability and cost matter more than new features or incorporating the latest science. With that background, I will discuss why, despite the flood of research, networks are conservative and resistant to change, that standards are unusually important compared to other areas of computer science, and that we should think beyond the well-known web and entertainment applications. I will reflect on some lessons on where the impact and shortcomings of networking technology have been harmful and that networking, in particular, needs to move beyond an individualized "be good" ethic. We need to consider responsible networks, not just responsible AI.

Probabilistic and Machine Learning Approaches for Autonomous Robots and Automated Driving
Prof. Dr. Wolfram Burgard, Technische Universität Nürnberg

For autonomous robots and automated driving, the capability to robustly perceive their environments and execute their actions is the ultimate goal. The key challenge is that no sensors and actuators are perfect, which means that robots and cars need the ability to properly deal with the resulting uncertainty. In this presentation, I will introduce the probabilistic approach to robotics, which provides a rigorous statistical methodology to solve the state estimation problem. I will furthermore discuss how this approach can be extended using state-of-the-art technology from machine learning to bring us closer to the development of truly robust systems that serve us in our everyday lives.

Fueling the SAT Revolution in Automated Reasoning
Prof. Dr. Armin Biere, Albert-Ludwigs-Universität Freiburg

The SAT problem, arguably the most prominent NP-complete problem, tries to determine whether a given logical formula with propositional variables, assuming true or false as value, has a satisfying consistent assignment making the formula true.  In the last century determining that a certain problem such as SAT is NP-complete was often the end of the story. These problems would have been considered to admit only exponential algorithms and thus were discarded as being impractical or alternatively weakened and reformulated to admit heuristic or approximative answers.  With the capacity increase of modern SAT solvers, which now routinely can handle millions of variables, this view changed completely.
Encoding a given problem into a propositional formula and solving it by a SAT solver is considered a practical solution.  As a consequence today's automated reasoning tools are built around a SAT solver core. They are applied in many domains, starting of course with formal verification of software and particularly hardware systems, within constraint solving over optimization to theorem proving.  Generalizations of SAT beyond propositional theories opened up many additional applications, for instance checking access lists in cloud computing billion times a day as a recent prominent example.  This development paved the way to what has been called the golden age of automated reasoning.  In this talk we review this change of perspective and what led to the SAT revolution we are witnessing today, both from the application as well as the technological side.