Abstract
SPHINCS+ is a post-quantum signature scheme that, at the time of writing, is being standardized as SLH-DSA. It is the most conservative option for post-quantum signatures, but the original tight proofs of security were flawed- as reported by Kudinov, Kiktenko and Fedorov in 2020. In this work, we formally prove a tight security bound for SPHINCS+ using the EasyCrypt proof assistant, establishing greater confidence in the general security of the scheme and that of the parameter sets considered for standardization. To this end, we reconstruct the tight security proof presented by Hulsing and Kudinov (in 2022) in a modular way. A small but important part of this effort involves a complex argument relating four different games at once, of a form not yet formalized in EasyCrypt (to the best of our knowledge). We describe our approach to overcoming this major challenge, and develop a general formal verification technique aimed at this type of reasoning. Enhancing the set of reusable EasyCrypt artifacts previously produced in the formal verification of stateful hash-based cryptographic constructions, we (1) improve and extend the existing libraries for hash functions and (2) develop new libraries for fundamental concepts related to hash-based cryptographic constructions, including Merkle trees. These enhancements, along with the formal verification technique we develop, further ease future formal verification endeavors in EasyCrypt, especially those concerning hash-based cryptographic constructions.

Abstract
Objectives: The shape is commonly used to describe the objects. State-of-the-art algorithms in medical imaging are predominantly diverging from computer vision, where voxel grids, meshes, point clouds, and implicit surface models are used. This is seen from the growing popularity of ShapeNet (51,300 models) and Princeton ModelNet (127,915 models). However, a large collection of anatomical shapes (e.g., bones, organs, vessels) and 3D models of surgical instruments is missing. Methods: We present MedShapeNet to translate data-driven vision algorithms to medical applications and to adapt state-of-the-art vision algorithms to medical problems. As a unique feature, we directly model the majority of shapes on the imaging data of real patients. We present use cases in classifying brain tumors, skull reconstructions, multi-class anatomy completion, education, and 3D printing. Results: By now, MedShapeNet includes 23 datasets with more than 100,000 shapes that are paired with annotations (ground truth). Our data is freely accessible via a web interface and a Python application programming interface and can be used for discriminative, reconstructive, and variational benchmarks as well as various applications in virtual, augmented, or mixed reality, and 3D printing. Conclusions: MedShapeNet contains medical shapes from anatomy and surgical instruments and will continue to collect data for benchmarks and applications. The project page is: https://medshapenet.ikim.nrw/.

Abstract
In recent years, code-reuse attacks have been used to exploit software vulnerabilities and gain control of numerous software programs and embedded devices. Several measures have been put in place to prevent this type of attack, such as Control-Flow Integrity (CFI) systems, and some of these systems have already been integrated into hardware. Nevertheless, Function-Oriented Programming (FOP) attacks, a form of code-reuse that chains functions to carry out malicious actions, continue to persist. In this work, we present the first analysis of the implications and feasibility of FOP attacks on microcontrollers, focusing on ARM Cortex-M processors that support PACBTI, that is, a hardware feature designed for CFI system implementation. During this process, we identified multiple dispatch gadgets in two common Real-time Operating System (RTOS). Since these gadgets reside within core OS functionalities, they are inherently included in a broad range of embedded operating systems. Furthermore, we also present CortexMFopper - a tool specially built to identify FOP gadgets in embedded devices and to raise awareness of this technique.

Abstract
Distributed Hash Tables (DHTs) remain to this day a central component of modern peer-to-peer (P2P) systems, which rely on complex DHT protocols to scale to millions of nodes. The correct operation of DHTs is therefore essential for the proper functioning of these systems. For this reason, formal methods have been employed to model and verify a range of correctness properties of various DHT protocols. However, these verification efforts have focused on protocol-specific properties, such as topological invariants, instead of functional properties. This focus limits our understanding of the precise guarantees offered by each protocol. We propose a protocol-independent axiomatization of DHT properties using Allen Temporal Logic (ATL). To validate our axiomatization, we have implemented it in the Alloy analyser and used our implementation both to establish a number of DHT-derived properties and to generate a set of DHT execution traces that cover an exhaustive list of DHT corner case behaviours.

Abstract
In this paper we present results on the normalized temperature sensitivity of UV- and fs-induced fiber Bragg gratings in a singlemode fiber with similar to 4.7 mol% GeO2 and having an Ormocer coating. In the 1500-1600 nm wavelength range, the former shows an almost constant value of 6.165x10(-6) K-1, whilst the fs-induced present some variation not related with the strength of the grating but probably due to induced birefringence. The average value obtained was 6.191x10(-6) K-1 which is higher than the former. For the UV-induced gratings in the Corning SMF-28 fiber (3.67 mol% GeO2) the value obtained was 6.143x10(-6) K-1. The achieved values are compatible with the use of Corning 7980 silica-based cladding fiber. Preliminary results also show no measurable impact of the hydrogenation process or the strength of the grating on the normalized temperature sensitivity.

Abstract
The recent updates of the National Energy and Climate Plans (NECPs) for Portugal and Spain have some significant changes compared to the previous 2019 versions, especially for the Portuguese side where a greater demand and renewable generation capacity are foreseen. This work assesses the impact of these new plans on the Iberian electricity market (MIBEL) main outcomes using CEVESA market model. Simulation results allow the analysis of the expected generation mix and prices, CO2 emissions, system cost, system adequacy, interconnections capacity usage, H2 demand impact and its contribution to provide balancing flexibility, under different simulation scenarios.