Modular deductive verification is a powerful technique capable to show that each function in a program satisfies its contract. However, function contracts do not provide a global view of which high-level (e.g. security-related) properties of a whole software module are actually established, making it very difficult to assess them. To address this issue, this paper proposes a new specification mechanism, called meta-properties. A meta-property can be seen as an enhanced global invariant specified for a set of functions, and capable to express predicates on values of variables, as well as memory related conditions (such as separation) and read or write access constraints. We also propose an automatic transformation technique translating meta-properties into usual contracts and assertions, that can be proved by traditional deductive verification tools. This technique has been implemented as a Frama-C plugin called MetAcsl and successfully applied to specify and prove safety- and security-related meta-properties in two illustrative case studies.

A common way to specify software properties is to associate a contract to each function, allowing the use of various techniques to assess (e.g. to prove or to test) that the implementation is valid with respect to these contracts. However, in practice, high-level properties are not always easily expressible through function contracts. Furthermore, such properties may span across multiple functions, making the specification task tedious, and its assessment difficult and error-prone, especially on large code bases. To address these issues, we propose a new specification mechanism called meta-properties. Meta-properties are enhanced global invariants specified for a set of functions, capable of expressing predicates on values of variables as well as memory related conditions (such as separation) and read or write access constraints. This paper gives a detailed presentation of meta-properties and their support in a dedicated Frama-C plugin MetAcsl, and shows that they are automatically amenable to both deductive verification and testing. This is demonstrated by applying these techniques on two illustrative case studies.

Spécifier et vérifier des exigences de haut niveau sur des programmes importants : application à la sécurité des programmes C: La spécification et la vérification d’exigences haut niveau (comme des propriétés de sécurité, telles que l’intégrité des données ou la confidentialité) reste un défi pour l’industrie, alors que les cahiers des charges en sont remplis. Cette thèse présente un cadre formel pour les exprimer appelé les meta-propriétés, décrites pour un langage de programmation abstrait, et centrées sur les propriétés liées aux manipulations de la mémoire et les invariants globaux. Ce cadre formel est appliqué au langage C avec HILARE, une extension d’ACSL, qui permet la spécification d’exigences haut niveau sur des programmes C de grande taille avec facilité. Des techniques de vérification pour HILARE, basées sur la génération d’assertions locales et la réutilisation des analyseurs de Frama-C existants, sont présentées et implantées dans le greffon MetAcsl pour Frama-C. Une méthodologie pour l’évaluation des propriétés de grands programmes est détaillée, articulant les méta-propriétés, les techniques de vérification et les particularités du C. Cette méthodologie est illustrée par un cas d’étude complexe : le bootloader de Wookey, un périphérique de stockage chiffré. Enfin, nous explorons une autre manière de vérifier une exigence de haut niveau en la déduisant à partir d’autres, via un système formel prouvé en Why3 et intégré dans MetAcsl.

Recent improvements in hardware and software have enabled a paradigm shift in satellite computing, moving from purpose-built satellites running a single application to platforms capable of executing and even receiving new workloads on orbit. This evolution has allowed image processing to migrate from ground stations to single- or multi-node satellite clusters, with only processed results transmitted, significantly reducing end-to-end latency. This paper proposes ORCHIDE, an orchestration solution built on cloud-native technologies such as Kubernetes and Argo, purpose built for space edge computing. A key capability of ORCHIDE is its support for unikernels—minimal, single-application virtual machines—alongside containers. Compared to traditional containerized deployments, unikernels substantially reduce CPU and memory footprint, achieve short boot times, and produce smaller binary images. ORCHIDE further enables unikernel workloads to leverage heterogeneous accelerator hardware, including FPGAs, through a dedicated accelerator management library. We describe the system architecture, the scheduling model, and the minimum target hardware required for deployment. Three clusters of varying topology were used to evaluate ORCHIDE, demonstrating that it operates effectively on both single- and multi-node heterogeneous configurations. Preliminary results show the ORCHIDE platform being able to run in heterogeneous and single-node environments with as low as 4 cores and 8 GB of memory, offering potential users the flexibility to compose satellite hardware to best match their mission requirements.