March 27-28, 2024

Tentative Program

The event is scheduled as a two-day meeting. Times are CET.

Day 1. March 27, 2024

  • 9:00-9:15 Registration, Opening & Presentation
    • The EuroProofNet COST Action. WG3 “Program Verification”. Alicia Villanueva (VRAIN - Universitat Politècnica de València (UPV), Spain/EPN WG3 Chair) (slides) (video)
  • 9:15-11:15 Hands-on tutorial
    • 9:15-11:15: ProVerif. Vincent Cheval (University of Oxford, UK) (Assistants: Muhammad Usama Sardar and Georgio Nicolas) (slides) (video)
  • 11:15-11:45 Break
  • 11:45-12:45 Talks
    • 11:45-12:15: Why formal methods remain inaccessible for most cryptographers. Georgio Nicolas (KU Leuven, Belgium) (slides) (video)
    • 12:15-12:45: Verification of cryptographic protocols. ilias Cherkaoui (Walton Institute, Ireland) (slides) (video)
  • 12:45-14:30 Lunch break
  • 14:30-15:30 Talks
    • 14:30-15:30: Platform-level Formal Verification for Public Sector Trustworthy Computing: Considerations and Challenges. Andreas Berg (gematik GmbH, Germany) (slides)
    • 15:30-16:00: Building a vendor-agnostic attestation service: Confidential Containers Trustee. Samuel Ortiz (Rivos Inc, France) (slides) (video)
  • 16:00-16:15 Break
  • 16:15-18:30 Talks & Conclusions of the day
    • 16:15-16:45: Towards Modular Trusted Execution Environments. Carsten Weinhold (Barkhausen Institut, Germany) (slides) (video)
    • 16:45-17:05: An ephemeral virtual TPM device to allow Remote Attestation for Confidential Virtual Machines. Angelo Ruocco (IBM Research, Switzerland) (slides) (video)
    • 17:05-17:35: Attestation for Mobile Network. Ghada Arfaoui (Orange, France) (slides) (video)
    • 17:35-18:05: Attesting the Verticals. Ian Oliver (University of Jyväskylä, Finland) (slides) (video)
    • 18:05-18:20: Role of Formal Verification in Next-Generation Mobile Networks. Ayşe Sayin (Istanbul Technical University, Turkey) (slides) (video)
    • 18:20-18:30: Wrapping-up: Discussion, conclusions of the day & plan.

Day 2. March 28, 2024

  • 9:00-11:00 Talks
    • 9:00-9:30: Some industry-relevant use cases. Thomas Fossati (Linaro, Switzerland) (slides) (video)
    • 9:30-10:00: TLS and TEEs. Arto Niemi (Huawei, Finland) (slides) (video)
    • 10:00-10:30: DICE Protection Environment. Ionut Mihalcea (Arm, UK) (slides) (video)
    • 10:30-11:00: Attested CSR. Hannes Tschofenig (University of Applied Sciences Bonn-Rhein-Sieg, Siemens/Germany) (slides) (video)
  • 11:00-11:30 Break
  • 11:30-12:30 Talks
    • 11:30-12:00: Hardening NVIDIA’s Confidential Computing: A Formally Verified Implementation of the SPDM Device Attestation Protocol. Tobias Reiher (AdaCore, Germany) (slides) (video)
    • 12:00-12:30: A rollercoaster ride on the formal analysis of attested TLS. Muhammad Usama Sardar (TU Dresden, Germany) (slides) (video)
  • 12:30-13:30 Lunch Break
  • 14:30-16:35 Talks
    • 14:30-15:00: Enarx attestation validation with Steward. Richard Zak (Enarx maintainer, USA) (slides) (video)
    • 15:00-15:30: Klave - Trustless Confidential Computing platform. Rui Almeida (Klave, UK) (slides) (video)
    • 15:30-16:15: Model checking for security. Lilia Georgieva (Heriot Watt University, UK) (slides) (video)
    • 16:15-16:35: Interactive theorem proving for protocol verification. Horatiu Cheval (University of Bucharest, Romania) (slides) (video)
  • 16:35-17:00 Break
  • 17:00-18:15 Talks
    • 17:00-17:20: Towards Logical Specification and Checking of Malicious Capabilities. Andrei Mogage (Alexandru Ioan Cuza University, Romania) (slides) (video)
    • 17:20-17:40: Formal correctness-proofs of refactorings. Volker Stolz (Høgskulen på Vestlandet, Norway) (slides) (video)
    • 17:40-17:50: Towards formally-verified remote attestation in SSProve. Jannik Mähn (Barkhausen Institut, Germany) (slides) (video)
    • 17:50-18:15: Wrapping-up: Setting the agenda for the year.

Photos