European Research Network on Formal Proofs
COST action CA20111
COST logo
EU flag and COST acknowledgement
COST (European Cooperation in Science and Technology) is a funding agency for research and innovation networks. Our Actions help connect research initiatives across Europe and enable scientists to grow their ideas by sharing them with their peers. This boosts their research, career and innovation.

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