Dr. Michael Kirsten

Wissenschaftlicher Mitarbeiter

🖈
📞
🖷

228 (Gebäude 50.34)
+ 49 721 608-45648
+ 49 721 608-44021
kirstenFlc1∂kit edu

E-Mail-Sicherheit: Verschlüsselte und signierte E-Mails sind ausdrücklich erwünscht.

PGP/GPG-Schlüssel:
Fingerabdruck:

S/MIME-Zertifikat:
Fingerabdruck:
0x8D1179AC09963B79
813A 0534 0FB1 880E 496B 99B5 8D11 79AC 0996 3B79

11914658548371764601139051992
FA 2B D2 BB 0D 89 FA 2A 33 83 2B 08 B1 0C E4 11 B1 CC 0D 6F

KIT  /  Institut für Informationssicherheit und Verlässlichkeit (KASTEL)

Am Fasanengarten 5
Gebäude 50.34
76131 Karlsruhe
Deutschland


ORCID iD icon ORCiD GitHub
Scholar iD icon Google Scholar
DBLP iD icon dblp
Dr.rer.nat. Michael Kirsten KIT + 49 721 608-43856 + 49 721 608-44021 Michael Kirsten

Forschungsinteressen

  • Formalisierung und Verifikation axiomatischer bzw. deklarativer Eigenschaften für:
    • Analyse von Sozialwahlmechanismen (im weiteren Sinne), insbesondere Wahlverfahren
    • (Statische) Programmanalyse auf Informationsflusseigenschaften
  • (Beschränkte) Modellprüfung von Software
  • Deduktive Programmverifikation

Projekte

  • Ende-zu-Ende-verifizierbare und geheime Online-Wahlen am KIT

    Das KIT bietet derzeit die Möglichkeit, Online-Abstimmungen durchzuführen. Dabei sind offene Abstimmungen bspw. im Rahmen von Video-Sitzungen der Gremien recht einfach durchzuführen. Geheime Online-Abstimmungen und -Wahlen stellen aber eine ungleich größere Herausforderung dar – wegen den gegensätzlichen Anforderungen, die sich aus dem Wahlgeheimnis auf der einen Seite und dem Erfordernis nachvollziehbarer Korrektheit und Sicherheit der Wahl auf der anderen Seite ergeben.

    Ziel dieses Projektes ist die Konzeption und die prototypische Umsetzung eines Online-Wahlsystems für Ende-zu-Ende-verifizierbare, geheime Wahlen am KIT. Der Prototyp wird zu einer KIT-weiten Testabstimmung eingesetzt. Ziel ist es insbesondere nicht, die Entscheidungshoheit zu verändern, sondern komplexe technische Sachverhalte zu erklären. Zum einen entwickelt sich ohnehin eine Dynamik in Richtung Online-Wahlen an Hochschulen, derzeit in der Regel aber als Blackbox-System, bei denen starke Sicherheitsannahmen getroffen werden.

    E2E-Wahlen am KIT

  • Vertrauen durch Erklärbarkeit bei verifizierbaren Online-Wahl-Systemen

    Online-Wahlsysteme werden seit Beginn der Pandemie immer häufiger bei geheimen Wahlen und Abstimmungen diskutiert und auch eingesetzt. Einerseits stellt sich bei den eingesetzten Systemen die Frage nach der technisch-organisatorischen Vertrauenswürdigkeit (d. h. wie die Sicherheit dieser Systeme im Zuge einer Evaluierung ihrer Eigenschaften bewertet wird) und anderseits die Frage, wodurch das Vertrauen der Wähler:innen in diese Systeme (und letztendlich das Ergebnis) beeinflusst wird und welche Rolle dabei die Erklärbarkeit spielt (d. h. inwieweit Wähler:innen die Funktionalität und/oder Eigenschaften verstehen).

    Die Ziele des Projektes sind eine Vernetzung der beiden Topics Engineering Secure Systems und Knowledge for Action im Helmholtz-Programm Engineering Digital Futures (innerhalb des Forschungsbereichs em>Information) sowie ein Anschub für besondere Forschungsfragen im Kontext technisch-organisatorischer Vertrauenswürdigkeit und Einflüssen auf Vertrauen in Online-Wahl-Systeme, insbesondere hinsichtlich der Rolle von Erklärbarkeit.

    Erklärbare Online-Wahlen

  • Problemorientierte, forschungsorientierte und interdisziplinäre Lehre in der Informatik

    Das Hauptziel des Projekts LehreForschung-PLUS ist die Verbesserung der Studienbedingungen und kontinuierliche Steigerung der Lehrqualität durch eine flächendeckende Weiterentwicklung der Studiengänge.

    Unser Teilprojekt umfasst hierbei drei wesentliche Maßnahmen, die alle das Ziel verfolgen, projekt- und forschungsorientierte, sowie interdisziplinäre Lehre in den Informatik-Studiengängen umzusetzen und zu stärken.

    Diese beinhalten die Weiterentwicklung und Verbesserung des projekt- und forschungsorientierten Master-Moduls "Praxis der Forschung", des projektorientierten Bachelor-Moduls "Praxis der Softwareentwicklung", sowie die Einführung des interdisziplinären und forschungsorientierten Master-Profils "Internet und Gesellschaft".

    LehreForschung-PLUS

  • Computational Social Choice

    Die rechenbetonte Sozialwahltheorie (Computational Social Choice) ist ein sich rapide entwickelnder Forschungszweig, der sich mit dem Design und der Analyse von Methoden der kollektiven Entscheidungsfindung beschäftigt. Die COST Action IC1205 zu Computational Social Choice ist ein europäisches Forschungsnetzwerk, das aufgebaut wurde, um eine gemeinsame Plattform zur Forschung in diesem Feld europaübergreifend und darüber hinaus herzustellen. Innerhalb dieses Projekts konzentrieren wir uns auf Wahlverfahren, d.h. Methoden individuelle Präferenzen zu einer aggregierten Entscheidung zu kombinieren. Das korrekte Verhalten dieser Verfahren ist unerlässlich für den demokratischen Prozess.

    Das Ziel des Projektes ist die Entwicklung formaler Verifikationstechniken, die es erlauben, Eigenschaften von Wahlverfahren ohne den riesigen Overhead einer für eine voll-funktionale Verifikation notwendigen Nutzer-Interaktion zu überprüfen. Die resultierende Methodik könnte dann in einem iterativen Design- und Implementierungsprozess neuer Wahlverfahren eingesetzt werden.

    COST Action IC1205

  • Spezifikation und Deduktive Verifikation von Sicherheitseigenschaften auf Programmebene

    In den letzten Jahren wurde ein deutlicher Fortschritt in der formalen Verifikation funktionaler Eigenschaften von Programmen erzielt. Gleichzeitig wurden zukunftsweisende Papiere veröffentlicht, die zeigen, dass es grundsätzlich möglich ist, Informationsfluss-Eigenschaften als Beweisverpflichtungen in Programm-Logik zu formulieren. Das Gesamtziel des Projektes ist es, diese Fortschritte — zusammen mit unseren eigenen Erfahrungen im Bereich der formalen Methoden für funktionale Eigenschaften — einzusetzen, um Sicherheitseigenschaften zu spezifizieren und verifizieren.

    DeduSec Projekt
    (Teil des DFG-Schwerpunktprogramms 1496 Reliably Secure Software Systems – RS³ )
  • Spezifikation und funktionale Verifikation von Smart Contracts

    Smart Contracts sind Programme, die in einer Blockchain ausgeführt werden. Sie bilden Verträge und andere Arten von Absprachen zwischen zwei oder mehr Parteien ab und setzen die in ihnen definierten Bedingungen automatisiert und transparent um. Ziel dieses Projekts ist es, Wege für die Spezifikation und formale Verifikation von Smart Contracts zu schaffen. Aufbauend auf existierenden Technologien und Werkzeugen der formalen Verifikation soll eine Basis geschaffen werden, die es ermöglicht, funktionale Eigenschaften von Smart Contracts zu beschreiben und zu beweisen, sodass die Blockchain-/Smart-Contract-Technologie mit all ihren Vorteilen sicher und zuverlässig verwendet werden kann.

    VeriSmart Projekt
  • Integriertes Deduktives Software-Design

    Das KeY-System ist ein Werkzeug zur formalen Softwareentwicklung, das darauf ausgerichtet ist, Entwurf, Implementierung, formale Spezifikation und formale Verifikation objekt-orientierter Software möglichst nahtlos miteinander zu vereinen. Im Zentrum des Systems steht ein neuartiger Theorembeweiser für dynamische Logik erster Ordnung für Java mit einer anwendungsfreundlichen Oberfläche.

    Das Projekt begann im November 1998 an der Universität Karlsruhe. Inzwischen ist es ein gemeinsames Projekt des KIT, der Technischen Hochschule Chalmers in Göteborg und der TU Darmstadt. Das KeY-Werkzeug ist zum freien Herunterladen verfügbar.

    KeY Projekt

Akademische Aktivitäten

Meine akademischen Aktivitäten sind auf einer separaten Seite zu finden.

Software

  • BEAST - Automatisierte Wahlverifikation mittels beschränkter Modellprüfung
  • CombinedApproach - Automatische und präzise Nichtinterferenz-Verifikation von Java-Programmen
  • DIbugger - Verstehen von Gegenbeispielen für relationale Programm-Eigenschaften
  • KeY - Integriertes Deduktives Software-Design

Lehre

Veröffentlichungen (chronologisch gruppiert)

2022
Titel Autor(en) Quelle
Why is Online Voting Still Largely a Black Box?Michael Kirsten, Melanie Volkamer und Bernhard BeckertFirst International Workshop on Election Infrastructure Security (EIS 2022) in conjunction with ESORICS 2022: European Symposium on Research in Computer Security
Algorithmic Fairness and Secure Information Flow (Extended Abstract)Bernhard Beckert, Michael Kirsten und Michael SchefczykEuropean Workshop on Algorithmic Fairness (EWAF '22), Lightning round track
Formal Methods for Trustworthy Voting SystemsMichael KirstenKarlsruhe Institute of Technology (KIT) (Januar 2022)
2021
Titel Autor(en) Quelle
Card-Based Cryptography Meets Formal VerificationAlexander Koch, Michael Schrempp und Michael KirstenNew Generation Computing 39(1)
2020
Titel Autor(en) Quelle
Integration of Static and Dynamic Analysis Techniques for Checking NoninterferenceBernhard Beckert, Mihai Herda, Michael Kirsten und Shmuel TyszberowiczDeductive Software Verification: Future Perspectives - Reflections on the Occasion of 20 Years of KeY, Teil V: Integration of Verification Techniques
Problemorientierte, forschungsorientierte und interdisziplinäre Lehre in der InformatikMichael Kirsten, Robert Bauer, Andreas Fried, Bernhard Beckert, Michael Beigl, Gregor Snelting und Martina ZitterbartCampustage 2020 „Lehre^Forschung-PLUS“
Modular Verification of JML Contracts Using Bounded Model CheckingBernhard Beckert, Michael Kirsten, Jonas Klamroth und Mattias Ulbrich9th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2020), Teil I: Verification Principles
Verified Construction of Fair Voting RulesKarsten Diekhoff, Michael Kirsten und Jonas Krämer29th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2019), Revised Selected Papers
2019
Titel Autor(en) Quelle
Card-Based Cryptography Meets Formal VerificationAlexander Koch, Michael Schrempp und Michael Kirsten25th International Conference on the Theory and Application of Cryptology and Information Security (ASIACRYPT 2019), Teil I
Card-Based Cryptography Meets Formal VerificationAlexander Koch, Michael Schrempp und Michael KirstenIACR Cryptology ePrint Archive 2019(1037)
Formal Property-Oriented Design of Voting Rules Using Composable ModulesKarsten Diekhoff, Michael Kirsten und Jonas Krämer6th International Conference on Algorithmic Decision Theory (ADT 2019), Teil Short Papers
GI Elections with POLYAS: a Road to End-to-End Verifiable ElectionsBernhard Beckert, Achim Brelle, Rüdiger Grimm, Nicolas Huber, Michael Kirsten, Ralf Küsters, Jörn Müller‑Quade, Maximilian Noppel, Kai Reinhard, Jonas Schwab, Rebecca Schwerdt, Tomasz Truderung, Melanie Volkamer und Cornelia WinterFourth International Joint Conference on Electronic Voting (E-Vote-ID 2019)
Understanding Counterexamples for Relational Properties with DIbuggerMihai Herda, Michael Kirsten, Etienne Brunner, Joana Plewnia, Ulla Scheler, Chiara Staudenmaier, Benedikt Wagner, Pascal Zwick und Bernhard BeckertSixth Workshop on Horn Clauses for Verification and Synthesis and Third Workshop on Program Equivalence and Relational Reasoning (HCVS/PERR 2019)
2018
Titel Autor(en) Quelle
Formal Specification and Verification of Hyperledger Fabric ChaincodeBernhard Beckert, Mihai Herda, Michael Kirsten und Jonas Schiffl3rd Symposium on Distributed Ledger Technology (SDLT-2018) co-located with ICFEM 2018: the 20th International Conference on Formal Engineering Methods
Using Theorem Provers to Increase the Precision of Dependence Analysis for Information Flow ControlBernhard Beckert, Simon Bischof, Mihai Herda, Michael Kirsten und Marko Kleine Büning20th International Conference on Formal Engineering Methods - Formal Methods and Software Engineering (ICFEM 2018)
Towards automatic argumentation about voting rulesMichael Kirsten und Olivier Cailloux4ème conférence sur les Applications Pratiques de l'Intelligence Artificielle (APIA 2018)
2017
Titel Autor(en) Quelle
An Introduction to Voting Rule VerificationBernhard Beckert, Thorsten Bormer, Rajeev Goré, Michael Kirsten und Carsten SchürmannTrends in Computational Social Choice, Teil II: Techniques
Formal Fairness Properties in Network Routing Based on a Resource Allocation ModelAlmut Demel und Michael Kirsten9th Workshop on Logical Aspects of Multi-Agent Systems (LAMAS 2017) affiliated with CSL 2017: the 26th EACSL Annual Conference on Computer Science Logic
RIFL 1.1: A Common Specification Language for Information-Flow RequirementsThomas Bauereiß, Simon Greiner, Mihai Herda, Michael Kirsten, Ximeng Li, Heiko Mantel, Martin Mohr, Matthias Perner, David Schneider und Markus TaschTU Darmstadt TUD-CS-2017-0225
Generalized Test Tables: A Powerful and Intuitive Specification Language for Reactive SystemsAlexander Weigl, Franziska Wiebe, Mattias Ulbrich, Sebastian Ulewicz, Suhyun Cha, Michael Kirsten, Bernhard Beckert und Birgit Vogel‑Heuser15th IEEE International Conference on Industrial Informatics (INDIN 2017)
Combining Graph-Based and Deduction-Based Information-Flow AnalysisBernhard Beckert, Simon Bischof, Mihai Herda, Michael Kirsten und Marko Kleine Büning5th Workshop on Hot Issues in Security Principles and Trust (HotSpot 2017) affiliated with ETAPS 2017: European Joint Conferences on Theory and Practice of Software
Automatic Margin Computation for Risk-Limiting AuditsBernhard Beckert, Michael Kirsten, Vladimir Klebanov und Carsten SchürmannFirst International Joint Conference on Electronic Voting – formerly known as EVOTE and VoteID (E-Vote-ID 2016)
2016
Titel Autor(en) Quelle
A Verification-Supported Evolution Approach to Assist Software Application Engineers in Industrial Factory AutomationSebastian Ulewicz, Mattias Ulbrich, Alexander Weigl, Michael Kirsten, Franziska Wiebe, Bernhard Beckert und Birgit Vogel‑HeuserIEEE International Symposium on Assembly and Manufacturing (ISAM 2016)
Automated Verification for Functional and Relational Properties of Voting RulesBernhard Beckert, Thorsten Bormer, Michael Kirsten, Till Neuber und Mattias UlbrichSixth International Workshop on Computational Social Choice (COMSOC 2016)
2015
Titel Autor(en) Quelle
A Hybrid Approach for Proving Noninterference of Java ProgramsRalf Küsters, Tomasz Truderung, Bernhard Beckert, Daniel Bruns, Michael Kirsten und Martin Mohr28th IEEE Computer Security Foundations Symposium (CSF 2015)
A Hybrid Approach for Proving Noninterference of Java ProgramsRalf Küsters, Tomasz Truderung, Bernhard Beckert, Daniel Bruns, Michael Kirsten und Martin MohrIACR Cryptology ePrint Archive 2015(438)
2014
Titel Autor(en) Quelle
Formal Verification of Voting SchemesMichael KirstenITI Beckert, Karlsruhe Institute of Technology (Dezember 2014)
Reasoning About Vote Counting Schemes Using Light-Weight and Heavy-Weight MethodsBernhard Beckert, Thorsten Bormer, Rajeev Goré, Michael Kirsten und Thomas Meumann8th International Verification Workshop (VERIFY 2014) in connection with IJCAR 2014: International Joint Conference on Automated Reasoning
2013
Titel Autor(en) Quelle
Proving Well-Definedness of JML Specifications with KeYMichael KirstenITI Schmitt, Karlsruhe Institute of Technology (November 2013)

Betreute Projekt- und Abschlussarbeiten