embedded-cal: A Formally Verified Cryptographic
Provider for Embedded Platforms

Elsa Lopez Perez, William Takeshi Pereira, Thomas Watteyne, Christian Amsüss, Franziskus Kiefer, Jonas Schneider-Bensch, Karthikeyan Bhargavan, Mališa Vučinić

► To cite this version:

Elsa Lopez Perez, William Takeshi Pereira, Thomas Watteyne, Christian Amsüss, Franziskus Kiefer, et al.. embedded-cal: A Formally Verified Cryptographic Provider for Embedded Platforms. IoTSPT 2026 - 15th International Workshop on Security, Privacy, Trust for Internet of Things, IEEE International Conference on Pervasive Computing and Communications (PerCom), Mar 2026, Pisa, Italy. hal-05524081

HAL Id: hal-05524081

https://hal.science/hal-05524081v1

Submitted on 23 Feb 2026

**HAL** is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons CC BY 4.0 - Attribution - International License
# embedded-cal: A Formally Verified Cryptographic Provider for Embedded Platforms

Elsa Lopez Perez<fnref n="1" />, William Takeshi Pereira<fnref n="5" />, Thomas Watteyne<fnref n="2" />, Christian Amsüss<fnref n="3" />, Franziskus Kiefer<fnref n="4" />, Jonas Schneider-Bensch<fnref n="4" />, Karthikeyan Bhargavan<fnref n="4" />, Mališa Vučinić<fnref n="1" />

***Abstract***—Cryptographic mechanisms are essential for ensuring secure communication and data protection on embedded devices. Differences in hardware acceleration and energy constraints across microcontrollers make it challenging to achieve consistent and verifiable cryptographic performance. We present embedded-cal, a lightweight cryptographic abstraction layer designed for constrained embedded systems. This software library unifies access to hardware-accelerated and software-based cryptographic primitives – such as AES, SHA-256, and ECDSA – through a modular Rust interface, while enabling formal verification of critical properties, such as constant-time behavior. We report representative measurements of execution time, current draw, and flash usage for cryptographic operations on two ARM Cortex-M platforms (STM32WBA55CG and nRF54L15). Hardware implementations show lower execution time and code size, while their instantaneous current depends on how each platform activates cryptographic peripherals. The resulting power profiles reflect the underlying architectural design of the devices rather than any specific cryptographic algorithm.

***Index Terms***—Rust, Embedded devices, Cryptography, Hardware-acceleration, Formal Verification.

## I. INTRODUCTION

The Internet of Things (IoT) ecosystem is rapidly expanding, with constrained devices handling increasingly sensitive data. These devices operate under strict resource limitations: low memory, processing power, and energy availability. This makes software-only cryptographic libraries impractical.

Hardware cryptographic accelerators help mitigate performance and energy constraints, but integrating them securely is non-trivial. Implementations must also defend against side-channel attacks, which can leak secret information.

Rust has emerged as a compelling language for IoT and embedded development due to its memory safety, concurrency guarantees, and performance [1]. An increasing number of embedded projects are replacing memory unsafe C to switch to Rust.

The current landscape of cryptography in Rust is scattered with respect to the available implementations of cryptographic primitives. Different Rust projects rely on custom implementations that are not mature and properly vetted, or wrap memory-unsafe, often pre-compiled, C libraries such as `mbedTLS`<fnref n="1" /> or `wolfSSL`<fnref n="2" />. This introduces two major problems:

* Safety and verification gaps: reliance on C wrappers removes Rust's memory safety guarantees, opening the door to vulnerabilities such as buffer overflows. Furthermore, these implementations often lack formal verification for critical properties like resistance to side-channel attacks.

* Inconsistent implementations: different embedded Rust projects frequently re-implement cryptographic primitives to integrate with specific hardware accelerators. This duplication of effort leads to inconsistent, non-standardized, and potentially insecure code.

While projects like `RustCrypto` [2] offer a unified cryptographic API for general purpose Rust environments, they lack tools for portable hardware support and cryptographic agility. Algorithms and their implementations need to be chosen manually by the application. `embedded-cal` directly addresses this gap by building a generic, high-assurance cryptographic provider module for popular IoT platforms that leverages their native hardware acceleration capabilities.

Developing a high-assurance, high-performance cryptographic provider for heterogeneous embedded systems presents several challenges.

**Platform Heterogeneity.** IoT platforms differ widely in the cryptographic hardware they provide, ranging from hash engines, AES blocks and elliptic-curve arithmetic units up to secure enclaves for computation and shielded key storage. We want to exploit these accelerators to reduce execution time, and leverage secret protection, yet maintain code that is portable across platforms with varying capabilities. Balancing platform-specific optimizations with a clean, generic design remains a central challenge.

**API Design.** Traditional C-based cryptographic providers typically expose high-level functions to hide complexity and minimize critical errors. While this approach works well for general-purpose applications, it is too restrictive for modern lightweight protocols used in IoT, which often require fine-grained control over cryptographic operations.

**Side-Channel Resistance.** Public-key operations, such as ECDH or ECDSA, rely on hardware-accelerated arithmetic, but ensuring constant-time execution across heterogeneous hardware interfaces is difficult. Vendor-specific hardware accelerators differ in capabilities and timing behavior, complicating efforts to maintain uniform, side-channel-resistant implementations.

**Verification of Hardware Interfaces.** Although formally verified software cryptographic libraries exist, verification of

<footnote n="1">¹ Inria, Paris, France. first.last@inria.fr</footnote>

<footnote n="2">² twatteyne@gmail.com</footnote>

<footnote n="3">³ christian@amsuess.com</footnote>

<footnote n="4">⁴ Cryspen, first@cryspen.com</footnote>

<footnote n="5">⁵ Inria, Paris, France. william.a.pereira@inria.fr</footnote>

<footnote n="1">¹ https://github.com/Mbed-TLS/mbedtls</footnote>

<footnote n="2">² https://github.com/wolfSSL/wolfssl</footnote>
hardware-dependent implementations is still largely unexplored. Hardware accelerators are accessed through memory-mapped registers whose precise behavior is rarely specified beyond high-level datasheets. Without formal, machine-readable models of these interfaces, it becomes challenging to prove correctness or reason about side-channel properties.

embedded-cal proposes a formally verified hardware cryptographic provider in Rust. The module combines Rust's inherent memory safety with formal verification guarantees. The module leverages available hardware acceleration for primitives on popular microcontrollers (MCUs). It fills in any hardware gaps using formally verified software implementations provided by *libcrux* [3]. The module is formally verified for correctness, runtime safety, and secret independence using the *Hax framework*, a toolchain that translates a subset of Rust code into formal proof assistants [4].

The contributions of this paper are three-fold:

* We develop a high-assurance, reusable, and verified cryptographic provider module in Rust<fnref n="3" />, optimized for popular embedded IoT platforms (incl. nRF, STM32).

* We provide formally verified resistance to timing and data dependent side channels at the Rust-level semantics using the Hax framework. These guarantees ensure that the verified code is secret-independent before compilation.

* We define a high-performance API, designed to accommodate the complex requirements of lightweight security protocols like EDHOC.

The remainder of this paper is organized as follows. Section II surveys related work, including the particularities of cryptographic libraries for IoT systems and formal verification techniques in cryptography. Section III presents the architecture of *embedded-cal* and the associated formal verification methodology. Section IV describes the experimental setup, methodology, and preliminary benchmark results. Section V lists use cases for *embedded-cal*. Finally, Section VI concludes the paper.

## II. RELATED WORK

The implementation of cryptography in IoT devices faces unique challenges due to severe resource constraints, including limited bandwidth and memory, low processing power, and limited energy. These constraints make typical high-level, software-only cryptographic libraries (such as OpenSSL) impractical for microcontroller-class devices [5]. As a result, IoT implementations often require highly optimized, sometimes assembly-level code, and rely on hardware cryptographic accelerators to achieve acceptable performance and energy efficiency.

IoT devices are also exposed to a wide range of attacks, including side-channel attacks, where an adversary can infer secret information by observing physical phenomena such as timing, power consumption, or electromagnetic emissions [6]. Consequently, implementations must be designed and verified

to resist such attacks, making security a first-class concern alongside efficiency.

### A. Formal Verification Techniques in Cryptography

A software component is considered “security-critical” if any design flaw or implementation bug can be exploited by an attacker to break the security of the larger system it supports [4].

The evolution of protocols such as TLS shows that every component of a crypto implementation is security-critical and vulnerable to attacks, including (1) flaws in specialized cryptographic constructions [7], (2) bugs in the core protocol logic (weakening authentication or confidentiality) [8], [9], (3) ambiguities in message formatting (leading to authentication attacks) [10], [11] or (4) vulnerabilities in dependent system libraries [12]. Any flaw in these layers can lead to high-profile vulnerabilities and costly security patches. Consequently, this type of code is typically subjected to rigorous security audits, comprehensive testing, and fuzzing before deployment.

Formally verifying a complete cryptographic protocol implementation is inherently challenging as different components require different specialized verification tools and techniques.

**HAC-L/HACL\* (High-Assurance Cryptography Library).** The High-Assurance Cryptography Library (HACL\*) is a foundational work providing formally verified, portable C implementations of modern cryptographic primitives (e.g. ChaCha20-Poly1305, Curve25519) [13]. HACL\* was verified using the F\* proof assistant, providing guarantees for functional correctness and side-channel resistance. The F\* proof assistant is a general-purpose, higher-order, purely functional programming language integrated with a sophisticated program verifier [14].

**Libcrux.** Libcrux is a formally verified cryptographic library for Rust, developed by Cryspen [3] and used in several prominent projects including Firefox, Signal, and OpenSSH. It aggregates verified artifacts, including those generated from HACL\*. Libcrux provides a set of cryptographic services in a safe Rust API, targeting high-performance environments that often rely on instruction set extensions (e.g. AES-NI, NEON) for acceleration. While it provides a high-assurance source for software-only primitives, our target environment of resource-constrained IoT MCUs requires leveraging vendor-specific hardware accelerators that are often outside the scope of general-purpose libraries. Libcrux is critical for filling hardware gaps in our implementation with verified software implementations.

**The Hax Framework.** Hax is a generic formal verification framework for Rust programs that translates the source code into the input languages of multiple backend provers, including F\*, Rocq, ProVerif, and SSProve [4], [15], [16]. Unlike efforts that verify assembly or C, Hax allows security properties, such as secret independence (a constant-time check), to be proven on the original Rust source code. This simplifies the development cycle and ensures that the verified properties apply directly to the high-level implementation.

<footnote n="3">³Available open-source at https://github.com/lake-rs/embedded-cal</footnote>
## B. Embedded Cryptographic Libraries

a) *RustCrypto*: The `RustCrypto` project [2] provides a comprehensive collection of pure-Rust cryptographic implementations. This approach maximizes portability and fully adheres to Rust's memory safety paradigm. These are primarily software-only implementations and are suitable for a wide range of general-purpose embedded platforms. However, for severely resource-constrained MCUs with low clock speeds and limited flash memory, the lack of hardware acceleration can make these software-only primitives too slow for lightweight protocols that require frequent cryptographic operations.

b) *C Wrappers (mbedTLS, wolfSSL)*: Libraries like `mbedTLS` and `wolfSSL` are frequently used in embedded C/C++ development and have strong hardware acceleration support. Utilizing these libraries in Rust requires employing the Foreign Function Interface (FFI). This necessity breaks Rust's core safety model, reintroducing the threat of low-level vulnerabilities (e.g. buffer overflows, memory corruption) common in C. Furthermore, the high-assurance guarantees afforded by formal verification are typically not maintained when interfacing with them. This shifts the overall security burden back to the less-safe C codebase, undermining the assurance gained from using Rust.

c) *Platform-Specific HALs*: The Rust Embedded ecosystem often relies on Hardware Abstraction Layers (HALs) to access MCUs peripherals, including cryptographic accelerators [17]. Despite being highly effective, it results in a scattered landscape where each platform's accelerator is accessed differently, leading to non-reusable and non-standardized cryptographic service code. This is the problem `embedded-cal` aims to solve: providing a unified, verified layer above these different HALs.

# III. EMBEDDED-CAL

## A. Architecture

The center point of `embedded-cal` is a singleton "CAL" object, composed of multiple implementations of cryptographic operations. These implementations may include explicitly configured hardware accelerations exposed by the MCU, software implementations for performance-critical paths (e.g. optimized for a single instruction set, possibly using inline assembly), and a generic, fully verified software implementations for fallback when hardware support is unavailable.

The CAL object provides a unified interface to other libraries and applications, such as hashing, AEAD, and elliptic curve operations (ECDH/ECDSA). It also manages key generation, key storage and algorithm selection.

The CAL also provides lower-level building blocks needed to assemble these operations, such as stand-alone AES functions used by AES-GCM, or finite-field arithmetic required for elliptic-curve protocols. These components are not part of the public interface, but support the implementation of the higher-level primitives.

<figure><img src="image_2.png" /><figcaption>Fig. 1: Interactions between objects leading up to the use of an ECDH secret. Not depicted: All operations on CAL-defined objects also involve exclusively accessing the CAL.</figcaption></figure>

Typical usage patterns are illustrated in Figure 1: An application obtains a CAL object from the system, and instructs it to generate a long-term private ECDH key from a given algorithm (1; e. g. during an onboarding process). This produces a key object, which the application can store (2). The application later instructs the CAL to combine that key object with an ephemeral key received from a peer (3), producing a secret that serves as input to follow-up symmetric operations. The generated secret can be fed into subsequent operations (4a; with any secret protection afforded by the backends), or be exposed to the application for further use (4b).

The execution flow depends on the particular composition of the CAL, as illustrated by one example in Figure 2. The setup depicted provides no secure area for storing secrets, and thus keys in RAM are only protected by Rust's type system. Here, a CSPRNG is chosen that does not utilize the available AES acceleration. On a different system with hardware managed keys, ECDH might still be implemented in software, but would operate on ECC points in protected memory accessed by handles, and the short-term secret produced can likewise be expressed by a handle unless exposed or encapsulated for storage.

Its design utilizes several patterns which are not novel individually, but in combination provide the required flexibility:

* *Traits* (Rust's implementation of described software interfaces) are used to layer multiple drivers: Any driver can wrap the previous and can access its accelerations.

<figure><img src="image_3.png" /><figcaption>Fig. 2: The CAL and its components, traversed for operations (1) and (3) of Figure 1. Assignment of components between software and hardware is illustrative, and varies by setup.</figcaption></figure>
The verified software implementation provides a top layer which, unlike other layers, preferably calls out to lower layers.

* *Constant evaluation* is used to guarantee that fallback code paths that never need to be taken are reliably eliminated at build time.

* *Associated types* allow offloading allocations (e.g. for state between processing hash inputs) to the application as part of type state. This creates no overhead due to the availability of niche optimizations and uninhabited types in Rust.

* *Synchronous API* design: As hardware accelerators are typically faster than software alternatives, operations block until completion, avoiding unnecessary async complexity.

* *Exclusive references* (also called “mutable references”) delegate the need for queue management in the library. This allows applications that perform cryptographic operations only in a single thread to use simple low-overhead access, while complex applications have full control over prioritization.

* *Generic types* are used sparingly to avoid excessive code sizes. They are predominantly used where there is effectively only one monomorphization for a single CAL instances.

Algorithm agility is facilitated by providing ecosystem-specific constructors to algorithm types. This allows working in TLS environments (e.g. selecting a signature algorithm from an 8-bit TLS SignatureAlgorithm) or in COSE environments (selecting using CBOR numeric COSE Algorithm identifier).

## B. Formal Verification Methodology

Our verification objective is to ensure that the cryptographic operations exposed by `embedded-cal` are:

* *functionally correct*: their input-output behavior matches the mathematical specification of the target algorithm;

* *runtime safe*: the code does not crash with a *panic* at runtime, e.g because of an out-of-bound array access or integer over- or under-flow;

* *secret independent*: their control flow, memory accesses, and timing behavior do not depend on secret data.

To achieve these goals we use the *hax* toolchain [4]. This toolchain has recently been used for the comprehensive verification of a TLS 1.3 implementation for both security and functional properties [15], as well as for the formal verification of cryptographic algorithms in *libcrux*.

The *hax* toolchain consists of three phases. The *frontend* plugs into the Rust compiler to extract a typed abstract syntax tree (AST) from the input Rust crate. Then, the *engine* applies verification-oriented transformations to the input AST. Lastly, *backends* translates the result into the input language of a chosen proof system.

Different backends support different goals: the F\* backend is suited for proving safety properties such as crash-freedom, ProVerif is useful for protocol-level security properties, and

Rocq is adequate for proving mathematical correctness of numeric rutines.

Developers express desired guarantees directly in Rust using invariants and pre/post-conditions, and Hax dispatches these to the appropriate verifier. The framework is extensible, and additional backends – such as one for the Lean prover – are currently being developed.

## IV. EVALUATION

In this section, we present results on two representative constrained platforms. We measure execution time, current consumption, and flash usage, and report hardware-accelerated implementations and *RustCrypto* software-only implementations.

### A. Setup and Methodology

We evaluate `embedded-cal` on two typical constrained platforms, based on the ARM Cortex-M core: (1) the nRF54L15 featuring a Cortex-M33 processor running at 64 MHz, 1.5 MB of flash memory, 256 kB of RAM, (2) the STM32WBA55CG chip featuring an ARM Cortex-M33 processor running at 32 MHz, with 128 kB of RAM and 512 kB of flash memory. We do not aim to compare the platforms, rather to present the representative evaluation results of cryptographic implementations.

We used the Otii Arc power profiler to measure both the current draw and the time operations take. We configure it to sample current at 50 kHz, and power both chips at 3 V. We configure the nRF54L15 to run at 64 MHz and we use the internal 16 MHz HSI clock on the STM32WBA55CG. To measure the time operations take, we toggle a GPIO pin connected to the Device Under Test (DUT) at the beginning and the end of the computation of the corresponding operation. We report the average values for time, current and power consumption over 10 executions to account for measurement variability and reduce noise. We also measure the flash footprint: we use *cargo size*, and sum up the instructions bytes (`.text`), static initializers (`.data`) and read-only data (`.rodata`).

All binaries were compiled using Rust's `--release` profile to ensure optimized, production-grade code generation. This profile enables advanced compiler optimizations, aggressive in-lining, and dead-code elimination, producing code that reflects realistic deployment conditions.

### B. Cryptographic Operations

We evaluate the following cryptographic operations:

* **Hash Function:** We implement SHA2-256 on a 128-bit (16-bytes) message.

* **Symmetric Encryption:** we implement AES-ECB-128 in ECB mode, using a 128-bit key and a 128-bit plaintext block.

* **Signature/verification algorithms:** ECDSA is implemented on P-256 curve, with curve parameters following the standard P-256 specification. The private key, nonce (*k*), and message hash are each 256-bits in length. The
<table><caption>TABLE I: Execution time of cryptographic operations on STM32 and nRF platforms (hardware accelerated (HW) vs. RustCrypto implementation (RC)).</caption><thead><tr><th rowspan="2">Operation</th><th colspan="2">STM32</th><th colspan="2">nRF</th></tr><tr><th>HW (ms)</th><th>RC (ms)</th><th>HW (ms)</th><th>RC (ms)</th></tr></thead><tbody><tr><td>AES-ECB-128</td><td>0.02</td><td>0.31</td><td>0.02</td><td>0.18</td></tr><tr><td>SHA2-256</td><td>0.02</td><td>0.24</td><td>0.02</td><td>0.15</td></tr><tr><td>ECDSA verify</td><td>181.17</td><td>1077.47</td><td>1.82</td><td>598.84</td></tr><tr><td>ECDSA sign</td><td>171.94</td><td>1168.11</td><td>2.31</td><td>653.25</td></tr><tr><td>ECC mult</td><td>193.16</td><td>540.17</td><td>1.68</td><td>300.21</td></tr></tbody></table>

public key is represented by a point on the curve with 256-bit *x* and *y* coordinates.

* **Elliptic Curve Operations:** We use 256-bit operands (scalar and curve point).

### C. Benchmarking Results

Table I and Figure 3 present representative measurements of execution time, average current, and average power consumption for several cryptographic primitives on the STM32WBA55CG and nRF54L15 platforms.

Across both devices, symmetric primitives (AES-ECB-128 and SHA2-256) complete within tens of milliseconds, while elliptic-curve operations (ECDSA and ECC multiplication) take several orders of magnitude more time due to their inherently more complex arithmetic.

The current and power profiles of the two platforms reflect their architectural differences. The nRF54L15 employs a modern low-power design with a dedicated CRACEN cryptographic accelerator, allowing it to maintain a much lower current envelope (4–12 mA). Hardware-accelerated operations draw slightly more current because enabling CRACEN activates additional logic, though execution time is significantly shorter. The overall energy profile remains consistent with a low-power architecture designed for wireless operation.

The STM32WBA55CG shows a relatively constant current draw (15–19 mA) across both hardware and RustCrypto execution. This behavior is characteristic of its subsystem organization, in which CPU, memory, and clock domains remain active independently of whether a hardware accelerator is invoked or an operation is implemented entirely in software. Consequently, variations in energy consumption are primary due to differences in execution time rather than changes in current draw.

Flash usage follows the expected pattern for MCU-class systems. Software-only cryptographic primitives require full algorithm implementations resulting in a higher use of flash storage on both platforms. Hardware-backed operations need only thin peripheral access crates reducing the overall flash footprint.

## V. USE CASES

This Section introduces use cases where `embedded-cal` would be particularly well-suited.

a) *Ariel OS and Lightweight Security Frameworks: The Ariel Operating System (Ariel OS)*<fnref n="4" /> is an emerging

research platform designed for secure, networked embedded systems [18]. It provides a lightweight runtime and modular architecture that supports verified components, with a focus on isolation, predictable timing, and secure inter-process communication. `embedded-cal` can be used as a formally verified, hardware-aware cryptographic module that can be integrated into operating systems such as Ariel OS or similar secure IoT runtimes.

b) *Lightweight Protocols: EDHOC and OSCORE:* The Ephemeral Diffie-Hellman Over COSE (EDHOC) protocol, standardized by the IETF in RFC 9528 [19], is a lightweight protocol for constrained environments. The lakers<fnref n="5" /> project implements EDHOC in Rust, as a secure foundation for IoT communications. The current cryptographic provider layer within lakers relies on external or non-verified cryptographic libraries, which may use unsafe memory operations or lack constant-time guarantees. IoT devices frequently depend on microcontrollers with hardware accelerators for cryptographic operations such as AES, SHA, or ECDH. Existing Rust-based cryptographic crates do not provide a unified, hardware-aware abstraction to leverage these accelerators efficiently and securely. Similarly, the libOSCORE<fnref n="6" /> library uses its own bespoke cryptographic layer. This motivates the development of `embedded-cal`, a dedicated cryptographic provider that is both hardware-accelerated and formally verified.

## VI. CONCLUSIONS AND FUTURE WORK

This paper introduces `embedded-cal`, a high-assurance cryptographic provider module for popular IoT platforms that leverages their native hardware acceleration capabilities. `embedded-cal` bridges the gap between high-assurance cryptographic software and the hardware-accelerated environments found in IoT MCUs, providing a guaranteed resistance to certain class of side-channel attacks. Moreover, `embedded-cal` is designed as a reusable, formally verified cryptographic foundation for the Rust embedded ecosystem, reducing the need for custom and unverified cryptographic code.

The current work establishes the design principles and implementation architecture of the module, as well as an evaluation on representative IoT platforms. We show some preliminary results on two typical constrained platforms: nRF54L15 and STM32WBA55CG. We include time, current and energy measurements of commonly used cryptographic operations, including AES encryption, SHA-256 hash function, or ECDSA sign/verify algorithm. Using both hardware-accelerated or RustCrypto implementations.

Future work includes replacing RustCrypto operations by `libcrux`, which is the formally verified library that `embedded-cal` will rely on. We also aim at extending hardware support to additional MCUs families. We plan to integrate `embedded-cal` into existing deployments such as Ariel OS and the lakers EDHOC implementation to validate

<footnote n="4">⁴ https://ariel-os.org</footnote>

<footnote n="5">⁵ https://github.com/lake-rs/lakers</footnote>

<footnote n="6">⁶ https://oscore.gitlab.io/liboscore/</footnote>
<figure><img src="image_4.png" /><figcaption>Fig. 3: Comparison of Hardware vs RustCrypto implementations for nRF (top row) and STM (bottom row).</figcaption></figure>

interoperability, portability, and scalability in real-world IoT
deployments.

VII. ACKNOWLEDGMENTS

This project was funded through the NGI0 Commons Fund
with financial support from the European Commission's Next
Generation Internet program, the aegis of DG Communications
Networks, Content and Technology under grant agreement
No 101135429, the Swiss State Secretariat for Education,
Research and Innovation (SERI), the French government under
the France 2030 ANR program "PEPR Networks of the
Future", grant agreement ANR-22-PEFT-0009, the European
Union's Horizon Europe Framework Program under Grant
Agreement No. 101093046 (project "OpenSwarm").

REFERENCES

[1] F. Petrillo, “Should we use rust platform in our iot applications? a multivocal review,” in *2025 IEEE/ACM 7th International Workshop on Software Engineering Research & Practices for the IoT* (SERP4IoT), 2025.

[2] RustCrypto Developers, “RustCrypto: A collection of cryptographic libraries written in pure rust,” https://github.com/RustCrypto, 2024, community Project.

[3] Cryspen, "Libcrux: A formally verified post-quantum cryptographic library in rust," https://github.com/cryspen/libcrux, 2024, software Ar-tifact.

[4] K. Bhargavan, M. Buyse, L. Franceschino, L. L. Hansen, F. Kiefer, J. Schneider-Bensch, and B. Spitters, “hax: Verifying Security-Critical Rust Software Using Multiple Provers,” in *Verified Software. Theories, Tools and Experiments: 16th International Conference, VSTTE 2024, Prague, Czech Republic, October 14–15, 2024, Revised Selected Papers*, 2025.

[5] I. K. Dutta, B. Ghosh, and M. Bayoumi, “Lightweight Cryptography for Internet of Insecure Things: A Survey,” in *2019 IEEE 9th Annual Computing and Communication Workshop and Conference (CCWC)*, 2019.

[6] A. Heuser, S. Picek, S. Guilley, and N. Mentens, “Side-Channel Analysis of Lightweight Ciphers: Does Lightweight Equal Easy?” *Lecture Notes in Computer Science* (including subseries *Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics*), vol. 10155, pp. 91–104, 2017.

[7] N. J. Al Fardan and K. G. Paterson, “Lucky Thirteen: Breaking the TLS and DTLS Record Protocols,” in *2013 IEEE Symposium on Security and Privacy*, 2013.

[8] D. Adrian, K. Bhargavan, Z. Durumeric, P. Gaudry, M. Green, J. A. Halderman, N. Heninger, D. Springall, E. Thomé, L. Valenta, B. Vander-Sloot, E. Wustrow, S. Zanella-Béguelin, and P. Zimmermann, “Imperfect Forward Secrecy: How Diffie-Hellman Fails in Practice,” in *Proceedings of the 22nd ACM SIGSAC Conference on Computer and Communications Security*, 2015.

[9] K. Bhargavan, A. D. Lavaud, C. Fournet, A. Pironti, and P. Y. Strub, “Triple Handshakes and Cookie Cutters: Breaking and Fixing Authentication over TLS,” in *2014 IEEE Symposium on Security and Privacy*, 2014.

[10] N. Mavrogiannopoulos, F. Vercauteren, V. Velichkov, and B. Preneel, “A cross-protocol attack on the TLS protocol,” in *Proceedings of the 2012 ACM Conference on Computer and Communications Security*, 2012.

[11] K. Bhargavan and G. Leurent, “Transcript Collision Attacks: Breaking Authentication in TLS, IKE, and SSH,” in *Network and Distributed System Security Symposium – NDSS 2016*, 2016.

[12] C. P. García and B. B. Brumley, “Constant-Time callees with Variable-Time callers,” in *26th USENIX Security Symposium (USENIX Security 17)*, 2017.

[13] J.-K. Zinzindohoué, K. Bhargavan, J. Protzenko, and B. Beurdouche, “HACL*: A Verified Modern Cryptographic Library,” in *Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security*, 2017.

[14] N. Swamy, C. Hriţcu, C. Keller, A. Rastogi, A. Delignat-Lavaud, S. Forest, K. Bhargavan, C. Fournet, P.-Y. Strub, M. Kohlweiss, J.-K. Zinzindohoue, and S. Zanella-Béguelin, “Dependent types and multi-monadic effects in F*,” *SIGPLAN Not.*, vol. 51, p. 256–270, 2016.

[15] K. Bhargavan, L. L. Hansen, F. Kiefer, J. Schneider-Bensch, and B. Spitters, “Formal security and functional verification of cryptographic protocol implementations in rust,” in *Proceedings of the 2025 ACM SIGSAC Conference on Computer and Communications Security*. Association for Computing Machinery, 2025.

[16] Cryspen, "Hax: A toolchain for formal security and correctness verification for rust programs," https://github.com/cryspen/hax, 2024, software Artifact.

[17] Rust Embedded Working Group, “The Embedded-HAL project,” https://github.com/rust-embedded/embedded-hal, 2024, community Project.

[18] E. Frank, K. Schleiser, R. Fouquet, K. Zandberg, C. Amsüss, and E. Baccelli, “Ariel OS: An Embedded Rust Operating System for Networked Sensors & Multi-Core Microcontrollers,” 2025.

[19] G. Selander, J. Preuß Mattsson, and F. Palombini, *Ephemeral Diffie-Hellman Over COSE (EDHOC)*, IETF Std. 9528, 2024.