Thomas Bellier
email: thomas.bellier@isae-supaero.fr

Annafederica Urbano

Joseph Morlier

Cees Bil

Adrian Pudsey

Impact of Life Cycle Assessment Considerations on Launch Vehicle Design

Keywords: Environment, Design, Launcher, LCA, MDAO, Optimization Acronyms

The continuous growth of the small launcher market and the emergence of many new concepts in the past years, combined with the growing need for sustainability in the space sector, raises the question of their environmental impact. The sustainability of space activities is becoming a significant constraint on future space applications. There is a need to integrate sustainability into the framework of micro launchers design at the preliminary phase. This work presents a novel methodology that considers the environmental impact of a launcher in its design phase, using Life Cycle Assessment (LCA) and Multi-disciplinary optimization tools (MDAO). Life cycle analysis studies the environmental impact throughout the launcher life cycle, from conception to disposal. This includes operations, but also development, manufacturing, testing of the launcher, logistics, construction and maintenance of ground facilities, as well as the recovery, refurbishment, and recycling if applicable. This paper focuses on greenhouse gas emissions and their influence on global warming. Multi-disciplinary analysis and optimization (MDAO) has been successfully applied to the design and optimization of space systems, including launcher vehicles. Launchers are usually optimized to fulfill a specific mission while minimizing the overall mass at take-off. The idea developed in the present work is to integrate outputs from the LCA of the launcher in the optimization process. First, the parameters needed to perform the LCA for a generic micro-launcher are identified, based on the dominant design from the many small launchers that are either operational or in development. Then the LCA is then integrated into the multidisciplinary framework to include ecodesign constraints in the optimization loop, using OpenMDAO. Finally, the results of the optimization of the launcher design using global greenhouse gas emissions as the main objectives are discussed, highlighting the current limitation of the model and possible developments of this methodology.

Introduction

The concern for climate change and the everincreasing human impact on Earth, combined with the continued growth of the space sector raises the question of its future impact on the environment, especially the Global Warming Potential (GWP) [START_REF] Miraux | Environmental limits to the space sector's growth[END_REF]. If the impact of commercial aviation has extensively been studied [START_REF] Lee | The contribution of global aviation to anthropogenic climate forcing for 2000 to 2018[END_REF], the impact of the space sector has been ignored for decades and remains today difficult to correctly estimate [START_REF] Wilson | Estimating the CO2 intensity of the space sector[END_REF].This is partly the consequence of the lack of correct models for the high speed and high altitude emissions, as well as all the environmental impacts not linked to the launch event phase. In order to ensure the next generations of space launchers are compatible with the environmental limits of the Earth and the eventual legal constraints that may result from the increased awareness of these issues, environmental constraints will need to be integrated into the development process from the very early stages.

Previous studies have highlighted very large differences in atmospheric impacts during the launch event using different technologies [START_REF] Ross | Radiative forcing caused by rocket engine emissions[END_REF], [START_REF] Kokkinakis | Atmospheric pollution from rockets[END_REF], such as hydrogen or hybrid rocket engines. However, those only assume the radiative forcing caused by the launch event itself and don't consider important factors such as the production of propellant or the launcher itself, and ignore the potential radiative forcing of H 2 O or NO x in the upper atmospheric layers. For example, a hydrogen-based launcher will only produce water vapor but as a result will have an enormous dry mass which could lead in a much higher overall environmental impact. Recent attempts of Life Cycle Assessment (LCA) especially carried out by ESA [START_REF]Space system life cycle assessment (LCA) guidelines[END_REF] and A. R. Wilson [START_REF] Wilson | Advanced methods of life cycle assessment for space systems[END_REF] highlight the importance of correctly analyzing the complete life cycle of the launcher, including design, manufacturing, disposal, and reusability if applicable, while providing tools and databases to carry out such an assessment.

Multidisciplinary Design Analysis and Optimization (MDAO) [START_REF] Sobieszczanski-Sobieski | Multidisciplinary design optimization: An emerging new engineering discipline[END_REF] is a field of engineering that aims to model and optimize complex systems incorporating different disciplines whose couplings and modeling are critical for the overall design. Growing in the late 20 th century with the increasingly available computational power, MDAO is now widely used in aerospace engineering, and many previous studies aiming to optimize micro launcher architectures have been conducted. However, MDAO often focuses on technical or economical objectives, not environmental ones.

This study proposes a new methodology to reduce the impact of newly developed micro launchers by using LCA as a key component and objective inside an MDAO architecture. Section 2 presents the detailed methodology and Section 3 presents the current environmental and technical model being developed. Section 4 presents early results, and Sections 5 and 6 present the current limitations, discussions, and possible developments for the project.

Methodology

The methodology developed to optimize the environmental impact is based on two key techniques: the LCA, to compute the relevant impacts, and MDAO, to implement an optimizer.

Life Cycle Assessment

LCA is a standardized method to evaluate the environmental consequences of a product or activity across its entire life. It's defined by a family of ISO norms [START_REF]Life cycle assessment. Principles and framework[END_REF], from ISO 14040 to ISO 14044, extended by the European ILCD [START_REF] Environment | International Reference Life Cycle Data System (ILCD) Handbook :general guide for life cycle assessment : detailed guidance[END_REF]. The main characteristic of LCA is that it covers the entire life cycle of the launcher, including development, permanent facilities, logistics, etc..., and not only the launch event.

Figure 1 shows the basic scheme of LCA scope for a launcher. In the present work we will only focus on one impact: the Global Warming Potential (GWP) as defined by IPCC [START_REF] Myhre | Anthropogenic and natural radiative forcing[END_REF]. To effectively compare different launchers, the functional unit used is the 1 kilogram of payload injected into a low earth orbit (LEO).

IAC-22,D2,IPB,26,x71719 Specifically, the target orbit is a 700km altitude polar orbit.

MultiDisciplinary Analysis and Optimization

The MDAO problem can be described as an optimization problem, following the MDAO principles [START_REF] Balling | Optimization of coupled systems -a critical overview of approaches[END_REF], [START_REF] Cramer | Problem formulation for multidisciplinary optimization[END_REF]. The problem we define is the minimisation, under constraints, of the Gross Lift-Off Weight (GLOW) with respect to specific design variables: Aerospace engineering has many multi-disciplinary challenges, and always uses the latest development in MDAO techniques. MDAO for generic simple launchers has been the topic of multiple works [START_REF] Balesdent | Multidisciplinary design optimization of launch vehicles[END_REF], [START_REF] Castellini | Multidisciplinary design optimization for expendable launch vehicles[END_REF], and several review papers are available [START_REF] Balesdent | A survey of multidisciplinary design optimization methods in launch vehicle design[END_REF]- [START_REF] Braun | Use of the collaborative optimization architecture for launch vehicle design[END_REF]. Of particular interest in the context of the present paper are recent published works on MDAO for small reusable launchers [START_REF] Contant | Design and optimization of a small reusable launch vehicle using vertical landing techniques[END_REF], and nano launchers [START_REF] Zeeshan | Multidisciplinary design and optimization of expendable launch vehicle for microsatellite missions[END_REF], or reusable launchers with new propellants [START_REF] Dresia | Multidisciplinary design optimization of reusable launch vehicles for different propellants and objectives[END_REF].

One of the major novelties of the present work is in the consideration of the output value for GWP from the LCA as the objective function f in an MDAO of the launcher. This will require to add another discipline in the MDAO code structure.

Modeling

The technical model for the launcher itself has to reflect the current developments of micro launchers, as highlighted by recent surveys of the industry [START_REF] Kulu | Small launchers -2021 industry survey and market analysis[END_REF], [START_REF] Niederstrasser | The small launch vehicle survey -a 2021 update (the rockets are flying)[END_REF]. Several primary architectures are emerging from those developments, however the present work focuses on most popular one, already flying: a 2-stage RP-1 expendable launcher. The LCA of such a launcher also depends on parameters that are not directly related to the launcher design, for instance the location of the factories, the design phases, the location of the launch site, etc...

Technical Model

The technical MDAO model is called Launcher Analysis and Sizing Tool (LAST) and is a tool based on the open-source library OpenMDAO [START_REF] Gray | OpenMDAO: An IAC-22,D2[END_REF]. Some modules are derived from the software FELIN [START_REF] Brevault | FELIN -framework for evolutive launcher optImizatioN[END_REF], developed at ONERA from previous work on MDAO for launchers [START_REF] Balesdent | Multidisciplinary design optimization of launch vehicles[END_REF]. The current rocket model for LAST is a classical 2-stage, expendable rocket, with a 500kg capacity to SSO. The same engine is used for both stages and uses RP-1 and LOX; the first stage has 9 engines and the second stage has 1. Figure 2 shows an example of the shape and components of the launcher simulated by LAST. The current LAST The other design parameters are linked to the trajectory and noted X traj . Those include:

• flight duration of each phase, including the burn time of each stage noted with t meco and t seco ; • pitch over angle; • parameters for the exo atmospheric command law. As shown in Figure 4, LAST has currently 4 modules:

• Propulsion: models the engines.

• Mass & Structure: models the structure and computes the mass of the different parts. • Aerodynamics: simulates the aerodynamic properties of the launcher. • Trajectory: computes the trajectory of the launcher and validates if it can reach orbit. The main objective is the GLOW; the MDA is solved using Gauss-Seidel fixed point iteration method, and the global optimizer algorithm is CMA-ES [START_REF] Hansen | Completely derandomized self-adaptation in evolution strategies[END_REF].

Environmental parameters

The LCA is based on the Strathclyde Space Systems Database (SSSD) [START_REF] Wilson | The strathclyde space systems database: A new life cycle sustainability assessment tool for the design of next generation green space systems[END_REF], an environmental database built for space activities, and is itself based on Ecoinvent [START_REF]Ecoinvent database[END_REF] and ELCD [START_REF] Environment | International Reference Life Cycle Data System (ILCD) Handbook :general guide for life cycle assessment : detailed guidance[END_REF] background inventories. Further information on the SSSD can be found in the work of A. R. Wilson [7]. This is used to build environmental models for the following processes:

• Production and assembly of the launcher (2 stages and the fairing) • Production of propellant • Transportation of the launcher parts to the launch site • Launch event • Build and maintenance of the launch site, development, and design of the launcher. The model assumes 100 launches in the program, dividing the fixed cost of the launch site and design. It also assumes an average distance between the factory on the launch site of 1000 km, and that all activities are carried out in Europe.

The environment model is built in LAST, as the fifth discipline module, outside of the MDA. The GWP is computed from the optimization result.

Preliminary results

Early optimisation results on the generic technical model specified in Section 3 gives a GWP impact of 194 kgCO 2 eq per kg to orbit, or 96.8 tCO 2 eq for a launch with a 500 kg payload. The LCA analysis gives the distribution of this impact among the main phases of each launch presented in Figure 5. We note that if the propellant is responsible for around 50% of the GWP impact, this is mainly due to its production, especially for liquid oxygen. Also, the manufacturing of the launcher, directly related to the properties of the dry parts of the launcher, has a nonnegligible impact. This gives us an overview of the main contributors to the GWP, and thus the main focus points for the improvement in the model and where it's important to improve the accuracy of environmental models.

Limitations and discussions

The early results of this study are limited by many different factors, which limits the conclusion we can draw; however, it also highlights where the most potential improvement lies for the overall model accuracy and thus where the efforts at improving the models should be targeted. Some phases of the launcher life cycle directly impacting the GWP or other impacts are not strongly correlated to the launcher design itself, but to other social and geographical parameters like the location of the facilities or the development cycle. For example, two perfectly identical launchers would have different impacts if they were manufactured and launched from two separate locations in two different countries. The environmental databases such as SSSD or Ecoinvent also assume that the production technique used for materials, propellant, or energy is the average of the geographic area specified; for example, it will assume H 2 is mostly produced from methane, whereas greener techniques exist.

Limitations of the model

Finally, some medium to high uncertainties remain on the exhaust effects of different species. The model assumes that everything, including black carbon [START_REF] Ross | Potential climate impact of black carbon emitted by rockets[END_REF], is burned, and the behavior of water vapor [START_REF] Solomon | Contributions of stratospheric water vapor to decadal changes in the rate of global warming[END_REF] is similar to the lower layers of the atmosphere. However, some studies speculate on the actual impacts of those chemicals without extensive experiment data being available.

Further developments

The current MDAO structure does not directly include the environment module inside an optimization loop, due to performance limitations. In the future, the different outputs of that module could be used directly as objectives for the main optimization loop, as shown on Figure 6 with the GWP.

Those early results only study one impact for one design but can be used as a base to explore and compare other designs. Adapting other architectures, like a three stages launcher, a launcher using different propellants such as hydrogen or methane, or even a completely different design like an airborne launcher or a fully reusable one, would allow for an in-depth comparison of their potential environmental sustainability.

This study focuses on GWP as the main impact, but the LCA methodology, the database used, and the compatibility of MDAO with different optimization algorithms could allow for the inclusion of other environmental impacts either as constraints, or other objectives. These include generic impacts like ozone depletion or more space-specific impacts including mass disposed in the ocean or left in orbit [START_REF]Space system life cycle assessment (LCA) guidelines[END_REF].

Conclusions

The combined usage of MDAO and LCA allows for the optimization of generic launcher design based not on any technical or economical value but on its impact on the environment, a parameter that may become significantly more important in a near future. This study highlights the importance of considering the entire life cycle of a launcher from a very early design stage in order to count all of the phases and activities that may contribute to the overall environmental impact, and subsequently optimize it. It also highlights the need for better environmental models, especially for high-altitude exhaust, to allow for better knowledge of these impacts and thus better reduce them.

Figure 1 :

 1 Figure 1: Generic LCA scope for a launcher

  Objective function : GLOW Design variables : X eng , m pl , X traj , d stage Constraints : ∆V f inal ≥ 0 The model and variables are detailed in Section 3.

Figure 2 :

 2 Figure 2: 3D model output of LAST

Figure 3 :

 3 Figure 3: Current LAST design parameters

Figure 4 :Figure 5 :

 45 Figure 4: Current structure of LAST

  The environmental model from SSSD and the technical model of LAST are based on publicly available IAC-22,D2,IPB,26,x71719 73 rd International Astronautical Congress (IAC) 2022 -Paris, France Copyright 2022 by Mr. Thomas Bellier. Published by the IAF, with permission and released to the IAF to publish in all forms. X eng , m pl , X traj , d stage MDA GLOW, X eng , t meco , t seco N max , d stage , m pl m pl , X traj

	Optimizer
		Propulsion	ṁf , ṁox , M prop		C eng	M prop
	GLOW	GLOW	Mass & Structure	C geom	M dry	M dry	GLOW
				Aerodynamics	Cx, Cz
	∆V f inal	N max			Trajectory
						Environment	GW P

  IAC-22,D2,IPB,26,x71719 73 rd International Astronautical Congress (IAC) 2022 -Paris, France Copyright 2022 by Mr. Thomas Bellier. Published by the IAF, with permission and released to the IAF to publish in all forms. X eng , m pl , X traj , d stage MDA GLOW, X eng , t meco , t seco N max , d stage , m pl m pl , X traj

	Optimizer
		Propulsion	ṁf , ṁox , M prop		C eng	M prop
		GLOW	Mass & Structure	C geom	M dry	M dry	GLOW
				Aerodynamics	Cx, Cz
	∆V f inal	N max			Trajectory
	GW P					Environment	GW P
		Figure 6: Extended structure of LAST

Acknowledgements

This work was supported by the Chair for Advanced Space Concepts (SaCLaB) resulting from the partnership between Airbus Defence and Space, Ariane Group and ISAE-SUPAERO.

The authors would like to thank Andrew Wilson, Mathieu Balesdent, and Catherine Azzaro-Pantel for their assistance in various aspects and disciplines of this project.


Koen Zandberg

Emmanuel Baccelli

Shenghao Yuan

Frédéric Besson

Jean-Pierre Talpin

Femto-Containers: Lightweight Virtualization and Fault Isolation For Small Software Functions on Low-Power IoT Microcontrollers

Keywords: CCS CONCEPTS, Computer systems organization → Embedded systems IoT, Low-Power, Microcontroller, Middleware, Container, Virtual Machine, Function-as-a-Service, Security

Low-power operating system runtimes used on IoT microcontrollers typically provide rudimentary APIs, basic connectivity and, sometimes, a (secure) firmware update mechanism. In contrast, on less constrained hardware, networked software has entered the age of serverless, microservices and agility. With a view to bridge this gap, in the paper we design Femto-Containers, a new middleware runtime which can be embedded on heterogeneous low-power IoT devices. Femto-Containers enable the secure deployment, execution and isolation of small virtual software functions on low-power IoT devices, over the network. We implement Femto-Containers, and provide integration in RIOT, a popular open source IoT operating system. We then evaluate the performance of our implementation, which was formally verified for fault-isolation, guaranteeing that RIOT is shielded from logic loaded and executed in a Femto-Container. Our experiments on various popular microcontroller architectures (Arm Cortex-M, ESP32 and RISC-V) show that Femto-Containers offer an attractive trade-off in terms of memory footprint overhead, energy consumption, and security.

INTRODUCTION

An estimated 250 billion microcontrollers are in use today [START_REF] Collins | Why TinyML is a giant opportunity[END_REF]. An increasing percentage of these microcontrollers are networked and take part in distributed cyber-physical systems and the Internet of Things (IoT) we increasingly depend upon. For example, such lowpower microcontrollers are at the core of hundreds of millions of connected machines such as sensors and actuators relied upon not only in smart homes, but also in other networked areas of the IoT and industrial contexts (Industry 4.0). On such hardware, the total memory available (for the whole system) is in the order of tens or hundreds of kBytes, without virtual memory management (MMU), often also without hardware memory protection (MPU). Neither Linux (or derivatives/equivalents) nor traditional hypervisor can be used as software platform on such hardware, and in effect the challenge of deploying and maintaining distributed low-power IoT software is exacerbated.

Recently, with the wider availability of low-power operating systems alternatives [START_REF] Hahm | Operating Systems for Low-end Devices in the Internet of Things: a Survey[END_REF] and adequate network stacks, low-power IoT software has made giant leaps forward; but fundamental gaps remain compared to current practices for networked software. In fact, current state-of-the-art for managing, programming, and maintaining fleets of low-power IoT devices resembles more PC system software workflow from the 1990s than today's common software practices. Simplistic application programming interfaces (APIs) offer basic performance and connectivity, but no additional comfort.

However, since the 1990s, networked software was revolutionized many times over. Networked software has entered the age of server-less, micro-services and agility. In the field, software modules that are deployed and running are expected to be quickly updatable in terms of functionalities, and in terms of bug fixes. Additional layers and primitives providing cybersecurity, flexibility and scalability became crucial: virtual machines, script programming (e.g. Python, Javascript), lightweight software containerization (e.g. Docker, Function-as-a-Service [START_REF] Fox | Status of serverless computing and function-as-a-service (faas) in industry and research[END_REF] etc.). DevOps [START_REF] Bass | DevOps: A software architect's perspective[END_REF] workflow drastically shortened software development/deployment life cycles to provide continuous delivery of higher software quality.

In such a context, low-power IoT devices based on microcontrollers are the new 'weakest link' within distributed cyber-physical systems. Indeed, state-of-the-art primitives for 'serverless', including lightweight virtual machine (VM) runtimes [START_REF] Morabito | Consolidate iot edge computing with lightweight virtualization[END_REF] and container runtimes (e.g. Docker) are not applicable on low-power devices: they typically depend on operating systems and larger resources which don't fit microcontrollers. In particular, VMs are either too prohibitive in terms of hosting engine memory resource requirements (e.g. standard Java virtual machines), or restricted to very specific use cases (e.g. JavaCard). This lackluster creates bottlenecks that severely impact both flexibility and cybersecurity in the low-power IoT space.

Goals of this paper -We aim to design a middleware function runtime adequate for heterogeneous microcontrollers. Mainly enabling the secure deployment, execution and isolation of small virtual software functions on low-power IoT devices. What we aim for in priority is small start-up time for deployed functions, and negligible overhead w.r.t. memory footprint on the microcontroller when adding a hosted function runtime to the OS, compared to the same functionality implemented natively (in the OS).

Contributions -In this paper, the work we present mainly consists in the following:

• We propose Femto-Containers, a novel middleware for the abstraction, secure deployment, execution and isolation of (multiple, concurrent) software functions on heterogeneous microcontroller-based IoT devices. We design Femto-Containers as an extension of rBPF virtual machines;

• We benchmark ultra-lightweight virtualization techniques based on Python, WebAssembly, JavaScript and eBPF. We show that, comparatively, a Femto-Container runtime based on eBPF virtualization requires 10x less memory footprint;

• We provide an open source implementation of Femto-Containers, which we integrate in practice on a common, general-purpose operating system for low-power networked microcontrollers (RIOT);

• We formally verify key components of our Femto-Container implementation, guaranteeing fault-isolation amongst concurrent Femto-Containers, and the underlying OS;

• We evaluate the performance of Femto-Containers in a variety of use cases, on the most popular 32-bit microcontroller architectures: Arm Cortex-M, ESP32 and RISC-V.

MULTI-TENANT SOFTWARE SCENARIOS ON MICROCONTROLLERS

Software on low-power IoT devices is growing complexity, driven by cybersecurity, interoperability, and device management requirements. In practice, the development of embedded software components is therefore often delegated to distinct entities. For security and privacy reasons these distinct entities have limited mutual trust [START_REF] Thomas | Design and Implementation of a Platform for Hyperconnected Cyber Physical Systems[END_REF]. For example, in this context, prior work such as Amulet [START_REF] Hardin | Application Memory Isolation on Ultra-Low-Power MCUs[END_REF] aim to isolate multiple applications from each other on a microcontroller, and to protect the underlying OS from application code. Furthermore, maintenance of these low-power IoT devices typically requires on-the-fly instrumentation. Safety requires that hot insertion of instrumentation code cannot break running software (already deployed). For example, prior work such as TockOS [START_REF] Levy | Multiprogramming a 64kb computer safely and efficiently[END_REF] aims to enable safe multiprogramming of low-power microcontrollers.

In this context, we identify the following categories of use-cases, depicted in Figure 1:

(1) Use-case 1: Hosting and isolation of a high-level business function. This function can be updated securely, on-demand, remotely over the low-power network. The execution of this type of logic is typically periodic in nature, and has loose (non-real-time) timing requirements. (2) Use-case 2: Hosting and isolation of debug and monitoring code functions at low-level. These are inserted and removed on-demand over the network. The functions must not interfere with existing code on the device. Comparatively, this type of function is short-lived and exhibits stricter timing requirements.

(3) Use-case 3: Hosting and isolation of several functions, managed by several different tenants. Users in the above scenarios are provided with an event-driven programming model and fine-grained computational space, hosted on-demand on fleets of designated low-power IoT devices. Furthermore, the API available for a function fundamentally abstracts away most of the hardware and the OS. Conceptually, these scenarios thus partly mimic a Function-as-a-Service (FaaS) programming model [START_REF] Fox | Status of serverless computing and function-as-a-service (faas) in industry and research[END_REF].

As with FaaS, multiple functions provided by distinct stakeholders must run on a single device. For example OEM firmware may have to be completed/customised by separate components, e.g. different developers/tenants may provide drivers separately, which should be fault-isolated and restricted to using only driver-relevant resources. Meanwhile, OS maintainers can deploy/run debug snippets inserted elsewhere in the embedded code.

However, as a stable high-throughput network connection cannot be assumed, storage capability is restricted to device-local storage. Furthermore, scalability aspects of FaaS and container techniques (e.g. running thousands of containers on a single machine) do not play a significant role here. Instead, the scenarios we identify above require running just a handful of isolated functions on top of the embedded OS. However, considering potentially large fleets of IoT devices, the scenario may nevertheless involve a large number of containers (but across a large number of devices).

In this paper, we focus primarily on the middleware embedded in the devices: the runtime permitting to host, run and isolate functions, on-demand, on heterogeneous low-power IoT devices deployed in the field, based on popular 32-bit microcontroller architectures (such as the ARM Cortex-M class, RISC-V or ESP32).

THREAT MODEL

When a client deploys functions on a device operational in the field, the embedded environment has to ensure these functions are sandboxed. In our threat model, we consider both malicious tenants which can deploy malicious code and malicious clients which can maliciously interact with deployed code [START_REF] Ren | Fine-grained isolation for scalable, dynamic, multi-tenant edge clouds[END_REF].

Malicious Tenant: The malicious tenant seeks to gain elevated permissions on the device it has already a set of permissions on. This tenant is already allowed to run code in the sandboxed environment, and the tenant might want to break free from the sandbox to either the host system or a different sandbox it doesn't have permissions for. While a tenant has to work within the permissions granted by the host service, it can make free use of the granted resources.

Malicious Client: The malicious client doesn't have any permissions for running sandboxed code on the device. The only access the malicious client has is access to networked endpoints exposed by the device, e.g. CoAP endpoints exposed by existing sandboxed environments. The malicious client seeks to gain any permission on the device to influence it or gain access to confidential data on the device. The malicious client could make use of an already vulnerable tenant function.

A number of attack vectors are considered in this work:

• Install and update time attacks: These attacks focus on modifying the application during the transport to the sandbox environment. This includes man-in-the-middle modifications to the applications.

• Privilege escalation to a different sandbox: This class of attacks focus on escaping the sandbox of the application to a different sandbox. The new sandbox could have different permissions.

• Privilege escalation to the operating system: This attack class attempts to escape the sandboxed environment altogether to the operating system.

• Resource exhaustion attacks: The devices considered here have very limited resources, both computational power and battery energy are limited. A denial of service vector can be to exhaust these resources.

Within the Femto-Container design we consider network attacks to exhaust resources on the system to be out of scope, this type of attack should be guarded against by the embedded operating system.

RELATED WORK

Typically, the fundamental building block for middleware embedded on devices allowing for generic function deployment and execution is a virtual machine runtime.

The vast majority of prior work on lightweight virtualization runtimes [START_REF] Morabito | Consolidate iot edge computing with lightweight virtualization[END_REF] does not target microcontrollers, but microprocessorclass computers. Recent examples include for instance AWS Firecracker [START_REF] Agache | Firecracker: lightweight virtualization for serverless applications[END_REF] for serverless computing, WebAssembly [START_REF] Haas | Bringing the web up to speed with WebAssembly[END_REF] for process isolation in Web browsers, or eBPF [START_REF] Mccanne | The BSD Packet Filter: A New Architecture for User-level Packet Capture[END_REF][START_REF] Fleming | A Thorough Introduction to eBPF[END_REF] for debug and inspection code inserted in the Linux kernel at run-time.

However, some ultra-lightweight virtualization approaches have been proposed for microcontrollers. For example, minimized Web-Assembly runtimes adapted to run on 32-bit microcontrollers were proposed, such as WAMR [START_REF]WebAssembly Micro Runtime (WAMR)[END_REF] and WASM3 [START_REF] Shymanskyy | WASM3: A high Performance WebAssembly Interpreter Written in C[END_REF]. RapidPatch [START_REF] He | Rapidpatch: firmware hotpatching for real-time embedded devices[END_REF] uses an eBPF runtime to provide a hotpatching framework for RTOS firmwares.

VM runtimes for microcontrollers include also earlier examples such as Mate [START_REF] Philip | Maté: a tiny virtual machine for sensor networks[END_REF] or Darjeeling [START_REF] Brouwers | Darjeeling, a feature-rich vm for the resource poor[END_REF], a subset of the Java VM, modified to use a 16 bit architecture, designed for 8-and 16-bit microcontrollers. JavaCard [START_REF][END_REF] also uses a small Java virtual machine tailored for cryptographic purposes, running on smart cards.

Recently, tiny scripted logic interpreters and runtimes have also been proposed to provide a basic virtualization environment. For instance, MicroPython [START_REF]MicroPython[END_REF] is a very popular scripted logic interpreter used on microcontrollers. Small Python runtimes are used on ESP8266 microcontrollers in prior work such as NanoLambda [START_REF] George | Nanolambda: implementing functions as a service at all resource scales for the internet of things[END_REF]. Small Javascript runtimes are used on Cortex-M microcontrollers in prior work such as RIOTjs [START_REF] Baccelli | Scripting Over-The-Air: Towards Containers on Low-end Devices in the Internet of Things[END_REF]. However, complementary mechanisms should however be used to guarantee mutual isolation between scripts (such as SecureJS [START_REF] Ko | Securejs compiler: portable memory isolation in javascript[END_REF]).

The most closely related work was published in [START_REF] Zandberg | Minimal virtual machines on iot microcontrollers: the case of berkeley packet filters with rbpf[END_REF] and in [START_REF] Yuan | End-to-end mechanized proof of an ebpf virtual machine for micro-controllers[END_REF]. In [START_REF] Zandberg | Minimal virtual machines on iot microcontrollers: the case of berkeley packet filters with rbpf[END_REF], authors provide rBPF, a port of the eBPF instruction set in order to host a (single) VM on a microcontroller. In contrast, we extend rBPF's instruction set architecture and VM core with an adequate embedded loading and execution environment, which caters for well-defined, event-driven, short lived and isolated (concurrent) execution of (multiple) functions to be deployed on-the-fly on a networked microcontroller. On the other hand, while [START_REF] Yuan | End-to-end mechanized proof of an ebpf virtual machine for micro-controllers[END_REF], concerns formal verification of the sole rBPF instruction interpreter, here we also verify the pre-flight instruction checker and we integrate both in our femto-container implementation -the performance of which we thoroughly evaluate on various microcontrollers. Our design and implementation are so small (a few hundreds lines of code) that formal verification was indeed realistic. Comparatively, software alternatives (WASM, MicroPython...) would require hundreds of thousands of lines of code, and magnitudes more lines of proof, all but voiding concrete perspectives of formal verification. Hardware alternatives (e.g. TrustZone [START_REF] Pinto | Demystifying Arm TrustZone: A Comprehensive Survey[END_REF]) are, to the best of our knowledge, not formally verified, and may require a software API to avoid unspecified hardware behaviours, hence faults.

To the best of our knowledge, our work provides the first formally verified middleware based on eBPF virtualization able to host multiple tiny runtime containers on a wide variety of heterogeneous low-power microcontrollers.

EMBEDDED RUNTIME ARCHITECTURE DESIGN

In this section, we introduce Femto-Containers, a new embedded runtime architecture tailored for constrained IoT devices, as described in the following.

Similarly to a FaaS runtime, Femto-Containers allow for the we deployment and execution of small logic modules. These modules, or functions, are hosted on top of a middleware offering isolation, abstraction and tight isolation with respect to the underlying OS and hardware. By combining isolation and hardware/OS abstraction, we retain the crucial properties of FaaS runtimes: code mobility and cyber-security. Differently from typical FaaS runtimes, however, Femto-Containers must be able to interact with specific hardware (e.g. sensor/actuators), and must drastically reduce the scope and the cost of virtualization to make do with IoT hardware constraints.

The Femto-Container architecture therefore relies on ultra-lightweight virtualization, as well as on a set of assumptions and features regarding an underlying RTOS, defined below.

Use of an RTOS with Multi-Threading. It is assumed that the RTOS supports real-time multi-threading with a scheduler. Each Femto-Container runs in a separate thread. Well-known operating systems in this space can provide for that, such as RIOT [START_REF] Baccelli | RIOT: an Open Source Operating System for Low-end Embedded Devices in the IoT[END_REF] or FreeR-TOS [START_REF] Barry | FreeRTOS, a FREE open source RTOS for small embedded real time systems[END_REF] and others [START_REF] Hahm | Operating Systems for Low-end Devices in the Internet of Things: a Survey[END_REF]. These can run on the bulk of commodity microcontroller hardware available. Note that RTOS facilities for scheduling enable simple controlling of how Femto-Containers interfere with other tasks in the embedded system.

No Assumptions on Microcontroller Hardware. To retain generality, we aim for a purely software-based isolation, which can also run on the least capable microcontrollers, without any assumptions on hardware architecture enhancements or security peripherals. If present, hardware-based isolation features could nevertheless be used to add layers of protection in-depth. For instance TrustZone software module isolation relies on enhanced Arm Cortex-M microcontroller architectures [START_REF] Pinto | Demystifying Arm TrustZone: A Comprehensive Survey[END_REF]. Other examples using hardware based protection mechanisms are TockOS [START_REF] Levy | Multiprogramming a 64kb computer safely and efficiently[END_REF] or Amulet [START_REF] Hardin | Application Memory Isolation on Ultra-Low-Power MCUs[END_REF], which rely on a hardware Memory Protection Unit (MPU) to isolate software modules.

Use of Ultra-Lightweight Virtualization. The virtual machine provides hardware agnosticism, and should therefore not rely on any specific hardware features or peripherals. This allows for running identical application code on heterogeneous hardware platforms. The virtual machine instances must have a low memory footprint, both in Flash and in RAM. This allows to run multiple VMs in parallel on the device. Note that, since we aim to virtualize less functionalities, the VM can in fact implement a reduced feature set. For instance, virtualized peripherals such as an interrupt controller are not required, and we give up the possibility of virtualizing a full OS. As exact virtualized hardware and peripherals is not a requirement, solutions around the interpretation of a scripting language are also suitable as target for Femto-Containers.

Use of OS Interfaces. A slim environment around the virtual machine (VM) exposes RTOS facilities to the VM. The container sandboxing a VM allows this VM to be independent of the underlying operating system, and provides the facilities as a generic interface to the VM. Simple contracts between container and RTOS can be used to define and limit the privileges of a container regarding its access to OS facilities. Note that such limitations must be enforced at run-time to safely allow 3rd party module reprogramming.

Isolation & Sandboxing through Virtualization. The OS and Femto-Containers must be mutually protected from malicious code, as described in section 3. This implies in particular that code running in the VM must not be able to access memory regions outside of what is granted via permissions. Here again, simple contracts can be used to define and limit memory and peripheral access of the code running in the Femto-Container. The strong isolation and security of the sandbox must prevent tenant escalation to the operating system and other tenants.

Slim Event-based Launchpad Execution Model. Femto-Containers are executed on-demand, when an event in the RTOS context calls for it. Femto-Container applications are rather short-lived and have a finite execution constraint. This execution model fits well with the characteristics of most low-power IoT software. To simplify containerization and enforce security-by-design, we mandate that Femto-Containers can only be attached and launch from predetermined launch pads, which are sprinkled throughout the RTOS firmware. Where applicable however, the result from the Femto-Container execution can modify the control flow in the firmware as defined in the launch pad.

Low-power Secure Runtime Update Primitives. Launching a new Femto-Container or modifying an existing Femto-Container can be done without modifying the RTOS firmware. However, updating the hooks themselves requires a firmware update. In our implementation, both types of updates use CoAP network transfer and software update metadata defined by SUIT [START_REF] Moran | A firmware update architecture for internet of things devices[END_REF] (CBOR, COSE) to secure updates end-to-end over network paths including low-power wireless segments [START_REF] Zandberg | Secure firmware updates for constrained iot devices using open standards: a reality check[END_REF]. Leveraging SUIT for these update payloads provides authentication, integrity checks and rollback options. Updating a Femto-Container application attached to a hook is done via a SUIT manifest. The exact hook to attach the new Femto-Container to is done by specifying the hook as a unique identifier (UUID) as a storage location in the SUIT manifest. A rapid develop-and-deploy cycle only requires a new SUIT manifest with the storage location specified every update. Sending this manifest to the device triggers the update of the hook after the new Femto-Container application is downloaded to the device and stored in the RAM. Using a secure update mechanism such as SUIT prevents a malicious client from intervening in the update and installation process of a Femto-Container application.

ULTRA-LIGHTWEIGHT VM MICRO-BENCHMARKS

In this section, we compare the performance of a proof of concept using RIOT [START_REF] Baccelli | RIOT: an Open Source Operating System for Low-end Embedded Devices in the IoT[END_REF] to extend with Femto-Container functionality, based on different ultra-lightweight isolation techniques: Python (MicroPython runtime), WebAssembly (WASM3 runtime), eBPF (rBPF runtime) and Javascript (RIOTjs runtime).

We run experiments using each virtualization candidate on an offthe-shelf IoT hardware platform representative of the landscape of modern 32-bit microcontroller architectures available: Arm Cortex-M4. Details of the benchmark setup are in Appendix A.

In the benchmarks we report on below, each implementation is loaded with a VM hosting logic performing a Fletcher32 checksum on a 360 B input string. We reason that this computing load roughly mimics the instruction complexity of intensive sensor data (pre-)processing on-board. Our benchmarks results are shown in Table 1 and Table 2. The startup time measures the time it takes for the runtime to load the application. This contains setup processing to parse the application or JIT compilation steps.

Runtime

Looking at size. While the size of applications are roughly comparable accross virtualization techniques (see Table 2), the memory required on the IoT device differs wildly. In particular, techniques based on script interpreters (RIOTjs and MicroPython) require the biggest dedicated ROM memory budget, above 100 KiB.

For comparison, the biggest ROM budget we measured requires 27 times more memory than the smallest budget. Similarly, RAM requirements vary a lot. Note that we could not determine with absolute precision the lower bound for script interpreters techniques, due to some flexibility given at compile time to set heap size in RAM. Nevertheless, our experiments show that the biggest RAM budget requires 140 times more RAM than the smallest budget. We remark that, as noted in prior work [START_REF] Zandberg | Minimal virtual machines on iot microcontrollers: the case of berkeley packet filters with rbpf[END_REF] the minimum required page size of 64 KiB to comply with the WebAssembly specification explains why WASM3 performs poorly in terms of RAM. One can envision enhancements where this requirement is relaxed. However the RAM budget would still be well above an order of magnitude more than the RAM budget we measured with rBPF.

Last but not least, let's give some perspective by comparison with a typical memory budget for the whole software embedded on the IoT device. As a reminder, in the class of devices we consider, a microcontroller memory capacity of 64kB in RAM and 256kB in Flash (ROM) is not uncommon. A typical OS footprint for this type of device is shown in the last row of Table 1. For such targets, according to our measurements, adding a VM can either incur a tremendous increase in total memory requirements (200% more ROM with MicroPython) or a negligible impact (8% more ROM with rBPF) as visualized in Figure 2.

Looking at speed. To no surprise, beyond size overhead, virtualization also has a cost in terms of execution speed. But here again, performance varies wildly depending on the virtualization technique. On one hand, solutions such as MicroPython and RIOTjs directly interpret the code snippet and execute it. On the other hand, solutions such as rBPF and WASM3 require a compilation step in between to convert from human readable code to machine readable.

Our measurements show that script interpreters incur an enormous penalty in execution speed. Compared to native code execution, script interpreters are a whooping 600 times slower. Compared to the same base (native execution) WASM is only 37 times slower, and rBPF 77 times slower.

One last aspect to consider is the startup time dedicated to preliminary pre-processing when loading new VM logic, before it can be executed (including steps such as code parsing and intermediate translation, various pre-flight checks etc.). Depending on the virtualization technique, this startup time varies almost 1000 foldfrom a few microseconds compared to a few milliseconds.

Considering VM architecture & security. WASM, MicroPython and RIOTjs each require some form of heap on which to allocate application variables. On the other hand, rBPF does not require a heap. With a view to accommodating several VMs concurrently, a heap-based architecture presents on the one hand some potential advantages in terms of memory (pooling) efficiency, but on the other hand some potential drawbacks in terms of security with mututal isolation of the VMs' memory between different tenants.

Furthermore, security guarantees call for a formally verified implementation of the hosting engine down the road. A typical approximation is: less lines of code (LoC) means much less effort to produce a verified implementation. For instance, the rBPF implementation is 1,5k LoC, while the WASM3 implementation is 10k LoC. The other implementations we considered in our pre-selection, RIOTjs and MicroPython, encompass significantly more LoC.

Choice of Virtualization

Our benchmarks indicate that in terms of memory overhead, startup time and LoC, Femto-Containers using eBPF virtualization is the most attractive, by far. We note that execution time with WebAssembly is 2x faster than with rBPF. However, we expect that a 2x factor in execution time will have no significant impact in practice for the use cases we target, such as small processing workloads. Since our priority is on memory footprint (recall our aim of ≈10% memory overhead for functionality containerization) we thus choose rBPF to flesh out our concept further.

FEMTO-CONTAINER RUNTIME IMPLEMENTATION

As proof of concept, we implemented the Femto-Container architecture, with functions hosted in the operating system RIOT and virtualization using an instruction set compatible with the eBPF instruction set. This implementation is open source (published in [START_REF]Femto-Containers RIOT Implementation[END_REF]). We detail below its main characteristics.

Simple Containerization. Simplified interfaces provide a uniform environment around the VM, independent of the RIOT operating system. Access from the Femto-Container to the required OS facilities is allowed through system calls to services provided by RIOT. These system calls can be used by the loaded applications via the eBPF native call instruction. Furthermore, the OS can share specific memory regions with the container.

Key-value store. In lieu of a file system, applications hosted in Femto-Containers can load and store simple values, by a numerical key reference, in a key-value store. This provides a mechanism for persistent storage, between application invocations. Interaction with this key-value store is implemented via a set of system calls, keeping it independent of the instruction set. By default, two keyvalue stores are provided by the OS. Use of RIOT Multi-Threading. Each Femto-Container application instance running is scheduled as a regular thread in RIOT. The native OS thread scheduling mechanism can simply execute concurrently and share resources amongst multiple Femto-Containers and other tasks, spread over different threads. A Femto-Containers instance requires minimal RAM: a small stack and the register set, but no heap. The host RTOS bears thus a very small overhead per Femto-Containers instance.

Figure 3 shows how Femto-Containers integrate into the operating system.An overview of how Femto-Containers integrate in the operating system is shown in Figure 3. It shows the flow within the operating system, with the Femto-Container triggered by an event in the operating system. The Femto-Container is started if it is present and gains access to it's own store and any bindings allowed by the operating system.

As the Femto-Container Instance does not virtualize its own set of peripherals, no interrupts or pseudo-hardware is available to the Femto-Container application. This also removes the option to interrupt the application flow inside a Femto-Container.

The hardware and peripherals available on the device are not accessible by the Femto-Containers instances. All interaction with hardware peripherals passes through the host RTOS via the system call interface.

Ultra-Lightweight Virtualisation using eBPF. Application code is virtualized using Femto-Containers, our enhancement of the rBPF virtual machine implementation. rBPF is again based on the Linux eBPF. The architectures of these virtual machines are similar enough that they all use the LLVM compiler with the eBPF target for compilation.

Register-based VM. The virtual machine operates on eleven registers of 64 bits wide. The last register (r10) is a read-only pointer to the beginning of a 512 B stack provided by the femto-container hosting engine. Interaction with the stack happens via load and store instructions. Instructions are divided into an 8 bit opcode, two 4 bit registers: source and destination, an 16 bit offset field and an 32 bit immediate value. Position-independent code is achieved by using the reference in r10 and the offset field in the instructions.

Jumptable & Interpreter. The interpreter parses instructions and executes them operating on the registers and stack. The machine itself is implemented as a computed jumptable, with the instruction opcodes as keys. During execution, the hosting engine iterates over the instruction opcodes in the application, and jumps directly to the instruction-specific code. This design keeps the interpreter itself small and fast.

Isolation & Sandboxing

To control the capabilities of Femto-Containers, and to protect the OS from memory access by malicious applications, a simple but effective memory protection system is used. By default each virtual machine instance only has access to its VM-specific registers and its stack.

Memory access checks at runtime. Allow lists can be configured (attached in the hosting engine) to explicitly allow a VM instance access to other memory regions. These memory regions can have individual flags for allowing read/write access. For example, a firewall-type trigger can grant read-only access to the network packet, allowing the virtual machine to inspect the packet, but not to modify it. As the memory instructions allow for calculated addresses based on register values, memory accesses are checked at runtime with the access lists against the resulting address, as show in Figure 4. Illegal access aborts execution. While this relies on properly configured allow lists, it prevents access to memory outside the sandbox by a malicious tenant.

Pre-flight instruction checks. A Femto-Container verifies the application before it is executed for the first time. These checks include checks on the individual instruction fields. For example, as there are only 11 registers, but space in the instruction for 16 registers, the register fields must be checked for out-of-bounds values. A special case here is register r10 which is read-only, and thus is not allowed in the destination field of the instructions.

The jump instructions are also checked to ensure that the destination of the jump is within the address space of the application code. As calculated jump destinations are not supported in the instruction set, the jump targets are known before executions and are checked during the pre-flight checks. During the execution of the application, the jump destinations no longer have to be verified and can be accepted as valid destinations. This prevents a tenant from jumping execution to the application code outside of the sandbox such as code from a different tenant or vulnerable code planted otherwise.

Finite execution is also enforced, by limiting both the total number of instructions 𝑁 𝑖 , and the number of branch instructions 𝑁 𝑏 that are allowed. In practice, this limits the total number of instructions executed to: 𝑁 𝑖 × 𝑁 𝑏 . This puts a limit on the computational resource exhausted by a single execution by putting a hard limit on the total number of instructions executed.

Hooks & Event-based Execution

The Femto-Container hosting engine instantiates and runs containers as triggered by events within the RTOS. Such events can be a network packet reception, sensor reading input or an operating system scheduling events for instance. Business logic applications can be implemented either by directly responding to sensor input or by attaching to a timer-based hook to fire periodically.

Simple hooks are pre-compiled into the RTOS firmware, providing a pre-determined set of pads from which Femto-Containers can be attached and launched. An example of a hook integrated in the firmware is shown in Listing 1. The firmware has to set up the context struct for the Femto-Containers after which it can call the hosting engine to execute the Femto-Container instances associated with the hook.

USE-CASE PROTOTYPING WITH FEMTO-CONTAINERS

In this section, we describe and demonstrate the programming model exposed by Femto-Containers. We use Femto-Containers to prototype the implementation of several use cases involving one or more functions (applications). Where multiple functions are involved, these are hosted concurrently on a single microcontroller. The goal of these functions is to match the scenarios we targeted initially in section 2.

In the prototype implementation we show below, we used C to code the applications hosted on Femto-Containers engine. However, any other target language supported by LLVM could be used instead such as C++ and Rust, for instance.

Programming Model

Femto-Containers follow an event-driven programming model. Applications hosted are only executed when triggered by events in the operating system. The applications specify the entry point and to which hooks they are to be attached inside the operating system.

The logic that can be deployed in Femto-Containers is limited following the eBPF architecture. For instance, asynchronous operation is not supported: there is no option to interrupt the control flow inside a Femto-Container application from outside the virtual machine. This is mainly caused by the simple nature of the architecture: neither interrupts nor indirect jumps are available. This trade-off reduces flexibility but increases the security for the host operating system.

Our current implementation is also limited by the fixed, small size of the stack (512 Bytes) dictated by the eBPF specification. More memory-consuming tasks would need special handling to provide additional memory. An enhanced implementation could however allow the application to request more stack from the RTOS, for example via the contracts, which would alleviate this issue. More computation-and memory-intensive tasks could also make use of additional system calls provided by the RTOS, which could execute generic primitives at native speed.

The Femto-Container hosting engine is designed to be fast enough to start applications on a hot code path without affecting significantly normal operating system execution times. Small applications can thus be inserted and execute without substantial overhead or slowdown for the RTOS. This way small debug or inspection applications can be inserted into the RTOS at any point as long as the application does not cause a deadline to be exceeded in the RTOS.

Kernel Debug Code Example

The first prototype we display consists in a single application, which intervenes on a hot code path: it is invoked by the scheduler of the OS. It keeps an updated count of each threads' activations. The logic hosted in the Femto-Container is shown in Listing 2. A small C struct is passed as context, which contains the previous running thread ID and the next running thread ID. The application maintains a value for every thread, incremented every time the thread is scheduled. External code can request these counters and provide debug feedback to the developer.

Networked Sensor Code Example

The second prototype we display adds two Femto-Containers from another tenant to the setup of the first prototype. Interaction between these two additional containers is achieved via a separate key-value store, as depicted in Figure 5. The logic hosted in the first Femto-Container, periodically triggered by the timer event, reads, processes and stores a sensor value. The code for this logic is shown in [START_REF]Femto-Containers sensor readout application[END_REF]. The second container's logic is triggered upon receiving a network packet (CoAP request), and returns the stored sensor value back to the requestor. The code for this logic is shown in [START_REF]Femto-Containers CoAP sensor value handler[END_REF].

In this toy example, the sensor value processing is a simple moving average, but more complex post-processing is possible instead, such as differential privacy or some federated learning logic, for instance. This example sketches both how multiple tenants can be accommodated, and how separating the concerns between different containers is achieved (between sensor value reading/processing on the one hand, and on the other hand the communication between the device and a remote requester).

FEMTO-CONTAINER FORMAL VERIFICATION

The critical components of Femto-Containers in terms of cybersecurity are the rBPF interpreter and the pre-flight instruction checker. Since the implementation is conveniently small (500 lines of C code for the interpreter and the checker), we aimed at producing a formally verified implementation of these components. We will refer to CertFC (for Certified Femto-Container) as the runtime which uses the formally verified interpreter and checker.

Targeted requirements formalization. The security guarantees we wish to provide Femto-Containers with are essentially memory and fault isolation. More precisely, we want to prove it impossible for CertFC to access a memory location out of its app's register memory or to execute an instruction leading to an undefined behavior, and consequently heading the VM and/or its host to crash. Providing these guarantees further strengthens the security needed with the threat model to prevent access to memory outside of the sandbox, in turn preventing unprivileged access to the operating system or other virtual machines.

Formal verification approach. We have used the Coq proof assistant to mechanically and exhaustively verify these requirements by employing the design workflow depicted in Figure 6: 1) First, we provide a proof model and a C-ready implementation that formalize (resp. optimize) the native, vanilla, C implementations of the rBPF verifier and virtual machine in RIOT. Proof and "C-ready" models are proved semantically equivalent in Coq.

2) The verification of expected safety and isolation properties is performed by the Coq proof assistant on the VM's proof model. It relies on the formalized isolation guarantees provided by a) the CompCert C memory model [START_REF] Leroy | Formal verification of a realistic compiler[END_REF] ii) the preflight runtime checks of the verifier, and iii) the defensive runtime checks of the virtual machine itself (for numerical and memory operations). 3) The verified C implementation is automatically extracted from the C-ready Coq model using the 𝜕𝑥 tool [START_REF] Jomaa | Proof-oriented design of a separation kernel with minimal trusted computing base[END_REF]. Based on a set of formalized translation rule from Coq to C, 𝜕𝑥 allows to craft a both reviewable and optimized C code from a functional Coq definition. 4) To ensure that the extracted C code refines the proof model, and hence satisfies the safety and isolation properties, the final simulation proof proceeds in two steps. First, a Com-pCert Clight model is extracted from the generated C code, using the VST-clightgen tool [START_REF] Appel | Program logics for certified compilers[END_REF]. Second, proving that Clight model to simulate the C-ready model using translation validation [START_REF] Pnueli | Translation validation[END_REF].

Formal verification details. The Coq models and proofs used to obtain CertFC are presented in [START_REF] Yuan | End-to-end mechanized proof of an ebpf virtual machine for micro-controllers[END_REF] and available from [START_REF]CertFC Artifact[END_REF].

PERFORMANCE EVALUATION

In this section we evaluate and compare the performance of Femto-Containers with rBPF and CertFC runtimes. The comparison is done on a number of low-power IoT hardware platforms: Cortex-M4, RISC-V and ESP32 based microcontrollers.

Hosting Engine Analysis

We benchmark the Femto-Container implementation on a number of aspects. First, we compare the footprint of the hosting engine on the embedded device. This shows the impact of adding Femto-Containers to the applications Second, we compare the execution time of a number of individual instructions.

To compare the impact of adding the Femto-Containers to an existing firmware, we compare the memory footprint of the implementations. In general, each Femto-Container needs memory to

• store the application bytecode;

• handle the virtual machine state and stack. The impact on the required flash on the firmware is shown in Figure 7 and Table 3 The different implementations of Femto-Containers are compared in Figure 8 against a set of eBPF instructions, showing that the rBPF extensions incur minimal overhead on the virtual machine and provide similar throughputs. Now, the performance of the formally verified CertFC is lagging behind the other implementations, revealing the trade off between the formally verified code and a natively optimized implementation. In this section we show the execution times of a number of Femto-Container applications. This shows the applicability of Femto-Containers in the different scenarios. we show the execution times in Figure 9.

The first example executes a Fletcher32 checksum over a data string of 360 B. It shows the time it takes for relative heavy processing within the Femto-Containers VM. Depending on the platform and the speed of the microcontroller it takes between 1.3 ms and 2.2 ms. For Femto-Containers the duration of this application is long.

The second example shown is the thread counter example previously shown in Listing 2. In normal operation it is inserted in the thread switch hook provided by the operating system, a hot path in the OS. As shown in the figure, adding this would increase the duration of a thread switch in the operating system by 10 µs to 27 µs. The impact on the operating system would not be negligible, but also not problematic during normal operation.

The last example shows the duration of the second stage of the networked sensor code example [START_REF]Femto-Containers CoAP sensor value handler[END_REF]. It depends heavily on system calls for formatting of the CoAP response, but still contains some processing inside the VM. It can be considered a representative example for business logic on the device. This example takes between 23 µs and 72 µs. For business logic programmed outside of the hot code path of the operating system itself, the overhead caused here by the VM is rather acceptable and doesn't impact the performance of the overall system.

Femto-Containers with Multiple Instances

Femto-Containers are optimized to run multiple containers on a single system in parallel. All state of an instance is kept local to the instance. Each new instance added takes 624 B of RAM to run, including the virtual machine stack. The other requirement is that the microcontroller must have a large enough storage for the all the application images.

We now measure the memory required to concurrently host multiple containers from multiple tenants on the same microcontroller, from the examples we described in section 8. As shown previously in Table 3, the minimal default memory footprint used by a Femto-Container amounts to 624 B, which is for storing the VM stack, housekeeping structs and information about memory regions. Furthermore, the key-value stores are also in RAM. In this case the total RAM used by the key value stores (and houskeeping) for different tenants was 340 B. Hence, the required RAM memory we measured so as to run the example with 3 containers and 2 tenants is 3.2 KiB. Beyond these examples, if we consider more containers hosting larger applications (e.g. ≈2000 B) an Arm Cortex-M4 microcontroller with 256 KiB RAM, the density of containers achievable would be of ≈100 instances, next to running the OS.

Different instances do not have access to each others resources by default. They are fully isolated and do not have access to each others memory, isolated by the memory protection mechanism. One way provided to communicate between the instances is the shared key-value store.

Multiple containers can be attached to the same launchpad hook inside the operating system. It depends on the hook how the return value from each instance is processed further. This allows for multiple tenants attaching to the same hook and process similar events.

Overhead Added by Hooks

One key question is how performance is affected by pre-provisioning launchpads (hooks) in the RTOS firmware. We measure in Table 4 the overhead caused by adding a hook to the RTOS workflow. This overhead amounts to ≈100 clock ticks on all the hardware we tested. Compared to the number of cycles needed for an average task in the operating system, this impact is low. Furthermore, this overhead is less than 10% of the number of cycles needed to execute the logic hosted in a Femto-Container. From this observation, we can conclude that, even if this hook is on a very hot code path (as for the Thread Counter example) the performance loss is tolerable. Conversely, the perspective of adding many hooks sprinkled in many places in the RTOS firmware is realistic without incurring significant performance loss.

DISCUSSION

Virtualization vs Power-Efficiency. Inherently, virtualization causes some execution overhead, due to interpretation of the code. Thus Femto-Containers increase power consumption for functionality executed within the VM, compared to native code execution. However, this drawback is mitigated by several other factors. First, the absolute power consumption overhead may be neglible, e.g. if the hosted logic is not performing long-lasting, heavy-duty tasks. Second, network transfer costs, power consumption and downtime are saved if software updates modify a Femto-Container instead of the full firmware.

Controlling Tenant Priviledges. Controlling and granting access to specific RTOS resources to different containers or tenants is a complex challenge. Our design includes a basic permission system based on preprovisionned hooks, system calls, and simple contracts between the hosting engine (on behalf of the OS) and a given container. Basically: the OS restricts the set of priviledges that can be granted, the container specifies the set of priviledges it requires, and the hosting engine grants the intersection of these sets. One limitation of our current simplified design is that there is only one fixed set of priviledges possible per hook. In case 2 tenants have different priviledges, a second hook must be made available. Additional mechanisms would be required to overcome this limiation and/or to enable dynamic priviledge levels.

Install Time vs Execution Time. As mentioned before, one limitation due to virtualization is the inherent slump in execution speed, compared to native code exection. One way to remove this overhead is to transpile the portable eBPF bytecode into native instruction code. This could be done in a single pass to convert the whole application into native instructions in an installation step. This can result into a speed-up at the cost of extra install-time overhead. To avoid the issues describe before on complicating the run-time security checks, this compilation into native code has to be done at run-time by the device deploying the code.

Fixed-vs Variable-length Instructions. Originally, eBPF scripts are optimized for fast execution on 64-bit platforms. Compared to other virtual machines such as Wasm, the resulting bytecode is relative large. In fact, most of the instructions have bit fields that are fixed at zero. A possible way to reduce the size of these scripts is to compress the instructions into a variable size instruction set, removing these fields from the instructions where possible. This would create a variable length instruction set based on the eBPF set. For example the immediate field is not used with half of the instructions and would reduce the instructions to 32 bits in size when removed.

CONCLUSION

In this paper we have introduced Femto-Containers, a new middleware runtime architecture we designed, which enables FaaS capabilities embedded on heterogeneous low-power IoT hardware.

Using Femto-Containers, authorized (3rd party) maintainers of IoT software can deploy and manage via the network mutually isolated software modules embedded on a microcontroller-based device. We provided an open source implementation of the Femto-Container runtime, which uses the eBPF instruction set ported to microcontrollers, as well as integration in a common low-power IoT operating system (RIOT). We formally verified a fault-isolation guarantee which ensures that RIOT is shielded from arbitrary logic loaded and executed in a Femto-Container -and such, without requiring any specific hardware-based memory isolation mechanism. We then demonstrated experimentally the performance of the Femto-Container runtime on the most common 32-bit microcontroller architectures: Arm Cortex-M, RISC-V, ESP32. We show that Femto-Containers significantly improve state of the art, by providing FaaS-like capabilities with strong security guarantees on such microcontrollers, while requiring negligible Flash and RAM memory overhead (less than 10%) compared to native execution.

APPENDIX A: BENCHMARK CONFIGURATION

Hardware -We carry out our measurements on popular, commercial, off-the-shelf IoT hardware, representative of the landscape of the modern 32-bit microcontroller architectures that are available. More precisely, we build and run the code on the following boards, all configured to run at 64 MHz:

• Arm Cortex-M: a Nordic nRF52840 Development Kit, using an Arm Cortex-M4 microcontroller with 256 KiB RAM, 1 MiB Flash, and a 2.4 GHz radio transceiver (BLE/802.15.4),

• ESP32: a WROOM-32 board, using an Espressif ESP32 module which provides two low-power Xtensa ® 32-bit LX6 microprocessors with integrated Wi-Fi and Bluetooth, 520 KiB RAM, 448 KiB ROM and 16 kB RTC SRAM.

• RISC-V: a Sipeed Longan Nano GD32VF103CBT6 Development Board, which provides a RISC-V 32-bit microcontroller with 32 KiB RAM and 128 KiB Flash.

Note that an open-access testbed such as IoT-Lab [START_REF] Adjih | FIT IoT-LAB: A Large Scale Open Experimental IoT Testbed[END_REF] also provides some of this hardware, for reproducibility.

Software -In all benchmarks, the embedded software platform (OS) hosting the Femto-Containers is RIOT [START_REF] Baccelli | RIOT: an Open Source Operating System for Low-end Embedded Devices in the IoT[END_REF]. As base, we took RIOT Release 2022.01, configured to be IoT-ready. More precisely, we configured RIOT to provide standard low-power networking connectivity, leveraging the board's IEEE 802.15.4 radio chip and a ressource-efficient IPv6-compliant network stack (6LoWPAN, UDP, CoAP), as well as providing secure software update capability, enabling the update of Femto-Containers over the low-power network, in compliance with SUIT [START_REF] Birkholz | CBOR-based Firmware Manifest Serialisation Format for the Software Updates for Internet of Things (SUIT) Manifest[END_REF] specifications (using CBOR, COSE, ed25519 signatures and SHA256 hashes as primitives).

Figure 1 :

 1 Figure 1: Container runtime use on IoT microcontrollers.

Figure 3 :

 3 Figure 3: Femto-Container RTOS integration.

Figure 4 :

 4 Figure 4: Interaction between memory instructions and the access lists.

Listing 1 :

 1 Example hook implementation. , & context , sizeof ( context ) , & result ) ;

1 Figure 5 :

 15 Figure 5: Event and value flow when hosting multiple containers from different tenants.

Figure 6 :

 6 Figure 6: CertFC Formal verification workflow.

Figure 8 :

 8 Figure 8: Time per instructions on the Cortex-M4 platform

  fig1: Fletcher32 checksumming algorithm application.

Figure 9 :

 9 Figure 9: Execution duration of different examples running on Femto-Containers.

Table 1 :

 1 Memory requirements for Femto-Container runtimes.

		ROM size RAM size
	WASM3 rBPF RIOTjs MicroPython	64 KiB 4.4 KiB 121 KiB 101 KiB	85 KiB 0.6 KiB 18 KiB 8.2 KiB
	Host OS (without VM)	52.5 KiB	16.3 KiB

Table 2 :

 2 Size and performance of fletcher32 logic hosted in different Femto-Container runtimes on Cortex-M4.

  The first key-value store is Flash memory distribution with different Femto-Containers. RIOT is configured with 6LoWPAN, CoAP, SUITcompliant OTA (totalling 53kBytes in Flash memory).local to the application, for values that are private to the VM accommodated in the container. The second key-value store is global, and can be accessed by all applications, used to communicate values between applications. An optional third intermediate-level of key-value store is possible to facilitate sharing data across a set of VMs from the same tenant, while isolating this set of VMs from other tenants' VMs.

	5%	11%	13%	5%	35%	13%	Crypto Network stack Kernel
	66%			30%	14%	8%	OTA module Femto-Container runtime
	fig1: RIOT with MicroPython Femto-Container (154kBytes).	fig2: RIOT with rBPF Femto-Container (57kBytes).
	Figure 2:

  Listing 2: Thread counter code.

	# include < stdint .h >
	# include " bpf / bpfapi / helpers . h "
	# define THREAD_START_KEY	0 x0
	typedef struct {
	uint64_t previous ; /* previous thread */
	uint64_t next ;	/* next thread */
	} sched_ctx_t ;
	int pid_log ( sched_ctx_t * ctx )
	{
	/* Zero pid means no next thread */
	if ( ctx -> next != 0) {
	uint32_t counter ;
	uint32_t thread_key = THREAD_START_KEY +
	ctx -> next ;
	bpf_fetch_global ( thread_key ,
		& counter ) ;
	counter ++;
	bpf_store_global ( thread_key ,
		counter ) ;
	}
	return 0;
	}

Table 3 :

 3 . In terms of required RAM for execution, Memory footprint of a Femto-Container hosting minimal logic on Arm Cortex-M4.

		3,500 4,000 4,500	rBPF Femto-Containers CertFC
		3,000
	Bytes	2,000 2,500
		1,500
		1,000
		500
		0
			C o r t e x -M 4	E S P 3 2	R IS C -V
	Figure 7: Flash requirement for the different implementa-
	tions and platforms
	both rBPF and Femto-Containers show comparable flash and RAM memory usage. In terms of Flash memory size, our measurements show that CertFC actually reduces the footprint by 55 % on Cortex-M4. The CertFC implementation requires slightly more memory, an increase of around 50 B per instance. This is caused by CertFC storing extra state of the virtual machine in the context struct and not on the thread stack.
				ROM size RAM size
			Femto-Containers rBPF CertFC	2992 B 3032 B 1378 B	624 B 620 B 672 B

Table 4 :

 4 Hook overhead in clock ticks for the thread switch example

		Empty Hook Hook with Application
	Cortex-M4 ESP32 RISC-V	109 83 106	1750 1163 754

ACKNOWLEDGEMENTS

The research leading to these results partly received funding from the RIOT-fp project, and from the TinyPART project (within the MESRI-BMBF German-French cybersecurity program under grant agreements no ANR-20-CYAL-0005 and 16KIS1395K). The paper reflects only the authors' views. MESRI and BMBF are not responsible for any use that may be made of the information it contains.