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)
  • 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)
  • 11:15-11:45 Break
  • 11:45-12:40 Talks
    • 11:45-12:15: Why formal methods remain inaccessible for most cryptographers. Georgio Nicolas (KU Leuven, Belgium)
    • 12:15-12:25: Towards formally-verified remote attestation in SSProve. Jannik Mähn (Barkhausen Institut, Germany)
    • 12:25-12:40: Verification of cryptographic protocols. ilias Cherkaoui (Walton Institute, Ireland)
  • 12:40-14:00 Lunch break
  • 14:00-15:30 Talks
    • 14:00-15:00: Platform-level Formal Verification for Public Sector Trustworthy Computing: Considerations and Challenges. Andreas Berg (gematik GmbH, Germany)
    • 15:00-15:30: Towards Modular Trusted Execution Environments. Carsten Weinhold (Barkhausen Institut, Germany)
  • 15:30-16:00 Break
  • 16:00-18:15 Talks & Conclusions of the day
    • 16:00-16:30: The RISC-V confidential computing attestation framework. Samuel Ortiz (Rivos Inc, France)
    • 16:30-16:50: An ephemeral virtual TPM device to allow Remote Attestation for Confidential Virtual Machines. Angelo Ruocco (IBM Research, Switzerland)
    • 16:50-17:20: Attestation for Mobile Network. Ghada Arfaoui (Orange, France)
    • 17:20-17:50: Attesting the Verticals. Ian Oliver (University of Jyväskylä, Finland)
    • 17:50-18:00: Role of Formal Verification in Next-Generation Mobile Networks. Ayşe Sayin (Istanbul Technical University, Turkey)
    • 18:00-18:15: Wrapping-up: 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)
    • 9:30-10:00: TLS and TEEs. Arto Niemi (Huawei, Finland)
    • 10:00-10:30: DICE Protection Environment. Ionut Mihalcea (Arm, UK)
    • 10:30-11:00: Attested CSR. Hannes Tschofenig (Siemens, Austria)
  • 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)
    • 12:00-12:30: A rollercoaster ride on the formal analysis of attested TLS. Muhammad Usama Sardar (TU Dresden, Germany)
  • 12:30-13:30 Lunch Break
  • 13:30-15:35 Talks
    • 13:30-14:00: Enarx attestation validation with Steward. Richard Zak (Enarx maintainer, USA)
    • 14:00-14:30: Klave - Trustless Confidential Computing platform. Rui Almeida (Klave, UK)
    • 14:30-15:15: Model checking for security. Lilia Georgieva (Microsoft, UK)
    • 15:15-15:35: Interactive theorem proving for protocol verification. Horatiu Cheval (University of Bucharest, Romania)
  • 15:35-16:00 Break
  • 16:00-17:15 Talks
    • 16:00-16:20: Towards Logical Specification and Checking of Malicious Capabilities. Dorel Lucanu and Andrei Mogage (Alexandru Ioan Cuza University, Romania)
    • 16:20-16:40: Formal correctness-proofs of refactorings. Volker Stolz (Høgskulen på Vestlandet, Norway)
    • 16:40-17:15: Wrapping-up: Setting the agenda for the year.