Chrystel Gaber

Despite growing efforts and encouraging successes in recent decades, fully formally verified projects are still rare in the industrial landscape. The industry often lacks the tools and methodologies to efficiently scale the proof development process. In this work, we give a comprehensible overview of the proof development process for proof developers and project managers. The goal is to support proof developers by rationalizing the proof development process, which currently relies heavily on their intuition and expertise, and by facilitating communication with the management line. To this end, we concentrate on the aspect of proof manufacturing and highlight the most significant sources of proof effort. We propose means to mitigate the latter through proof practices (proof structuring, proof strategies, and proof planning), proof metrics, and tools. Our approach is project-agnostic, independent of specific proof expertise, and computed estimations do not assume prior similar developments. We evaluate our guidelines using a separation kernel undergoing formal verification, driving the proof process in an optimised way. Feedback from a project manager unfamiliar with proof development confirms the benefits of detailed planning of the proof development steps, clear progress communication to the hierarchy line, and alignment with established practices in the software industry.

Microservices architecture has become an increasingly common approach for building complex software systems. With the distributed nature of microservices, multiple actors can contribute to a service, hence affecting the dynamics of the environment and making the management of liabilities and trust more challenging. Service-Level Agreements (SLAs) are critical in that regard and any SLA violation or breach can result in significant financial damages. One major challenge is the lack of indicators to handle the liability and trust in such architectures. To address this issue, in this paper we propose a liability and trust analysis framework, namely the LASM Analysis Service (LAS), for multi-actor dynamic microservices that employs Machine Learning (ML) techniques.

Transitioning edge and cloud computing in 5G networks towards service-based architecture increases their complexity as they become even more dynamic and intertwine more actors or delegation levels. In this paper, we demonstrate the Liability-aware security manager Analysis Service (LAS), a framework that uses machine learning techniques to compute liability and trust indicators for service-based architectures such as cloud microservices. Based on the commitments of Service Providers (SPs) and real-time observations collected by a Root Cause Analysis (RCA) tool GRALAF, the LAS computes three categories of liability and trust indicators, specifically, a Commitment Trust Score, Financial Exposure, and Commitment Trends.

This article presents a hardware-based memory isolation solution for constrained devices. Existing solutions target high-end embedded systems (typically ARM Cortex-A with a Memory Management Unit, MMU) such as seL4 or Pip (formally verified kernels) or target low-end devices such as ACES, MINION, TrustLite, EwoK but with limited flexibility by proposing a single level of isolation. Our approach consists in adapting Pip to inherit its flexibility (multiple levels of isolation) but using the Memory Protection Unit (MPU) instead of the MMU since the MPU is commonly available on constrained embedded systems (typically ARMv7 Cortex-M4 or ARMv8 Cortex-M33 and similar devices). This paper describes our design of Pip-MPU (Pip's variant based on the MPU) and the rationale behind our choices. We validate our proposal with an implementation on an nRF52840 development kit and we perform various evaluations such as memory footprint, CPU cycles and energy consumption. We demonstrate that although our prototyped Pip-MPU causes a 16% overhead on both performance and energy consumption, it can reduce the attack surface of the accessible application memory from 100% down to 2% and the privileged operations by 99%. Pip-MPU takes less than 10 kB of Flash (6 kB for its core components) and 550 B of RAM.

This paper first introduces a possible evolution of secure personal identification devices, based on RFID technology in the mobiles phones (NFC). Given the characteristics of the mobile phone market, this trend could grow quickly and importantly. This paper considers the possible impact of this evolution in term of privacy, focusing on a typical and important case: payment transactions. This paper sticks to the general approach and role of “card payment system”. Yet, it demonstrates that it is possible to improve some of the privacy characteristics of this kind of application. It also outlines the way payment protocol should be designed in order to reach this goal.