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.

The emergence of the Internet of Things (IoT) model featuring different types of wireless networks made of many different constrained devices conducts researchers to face new security challenges to protect these networks. Indeed, they need to build and evaluate dedicated monitoring tools and Intrusion Detection Systems (IDSs). To succeed in these goals, quality datasets including benign and under attack situations are necessary for all IoT protocols. However, if we consider for instance the smart-home sub-market dominated by Wi-Fi, Zigbee and BLE, only complete Wi-Fi datasets can easily be found today. To specifically overcome the lack of Zigbee datasets and contribute to the development of related IDSs, this paper presents ZBDS2023, a 10-day realistic Zigbee dataset made publicly available. Fully documented with metadata, it has been collected from a real populated smart home equipped with 10 recent Zigbee lighting devices. Some periods of capture are free of attack, allowing to build normality models, and some include various labelled attacks, enabling the evaluation of different intrusion detection strategies. Also, as an original second contribution, each emitted frame is captured by one to four demodulating passive probes distributed in the house. Besides providing redundancy concerning MAC layer data, the corresponding values of Received Signal Strength Indicator (RSSI) have also been made available. Being a physical feature, RSSI cannot be easily impersonated and as such, it is a priori a good candidate for participating in fingerprints feeding spoofing detection systems. Moreover, its extraction is uncostly and available in many wireless technologies. However, exploitation of RSSI time series is not trivial, especially in populated buildings. A third contribution using our dataset evaluates a naive attack detection system to serve as a baseline for future works.

The scheduler is a critical piece of software in real-time systems. A failure in the scheduler can have serious consequences; therefore, it is important to provide strong correctness guarantees for it. In this paper we propose a formal proof methodology that we apply to an Earliest Deadline First (EDF) scheduler. It consists first in proving the correctness of the election function algorithm and then lifting this proof up to the implementation through refinements. The proofs are formalized in the Coq proof assistant, ensuring that they are free of human errors and that all cases are considered. Our methodology is general enough to be applied to other schedulers or other types of system code. To the best of our knowledge, this is the first time that an implementation of EDF applicable to arbitrary sequences of jobs has been proven correct.

The Internet of Things (IoT) is everywhere around us. Smart communicating objects offer the digitalization of lives. Thus, IoT opens new opportunities in criminal investigations such as a protagonist or a witness to the event. Any investigation process involves four phases: firstly the identification of an incident and its evidence, secondly device collection and preservation, thirdly data examination and extraction and then finally data analysis and formalization.

We propose a deductive verification approach for proving partial-correctness and invariance properties on transition-system models. Regarding partial correctness, we generalise the recently introduced formalism of Reachability Logic, currently used as a language-parametric logic for programs, to transition systems. We propose a sound and relatively complete proof system for the resulting reachability logic. The soundness of the proof system is formally established in the Coq proof assistant, and the mechanised proof provides us with a Coq-certified Reachability-Logic prover for transition-system models. The relative completeness of the proof system, although theoretical in nature, also has a practical value, as it induces a proof strategy that is guaranteed to prove all valid formulas on a given transition system. The strategy reduces partial-correctness verification to invariance verification; for the latter we propose an incremental technique in order to deal with the case-explosion problem that affects it. All these techniques were instrumental in enabling us to prove, within reasonable time and effort limits, that the nontrivial algorithm implemented in security hypervisor that we designed in earlier work meets its expected functional requirements.

For security and safety reasons, it is essential to ensure memory isolation between processes. The memory manager is thus a critical part of the kernel of an operating system. It is common for kernels to ensure memory isolation through a piece of hardware called memory management unit (MMU). However an MMU by itself does not provide memory isolation. It is only a tool the kernel can use to ensure this property. In this paper we show how a proof assistant such as Coq can be used to model a hardware architecture with an MMU, and an abstract model of microkernel supporting preemptive scheduling and memory manager. We proceed by making formally explicit the consistency properties that must be preserved in order for memory isolation to be preserved.

Nowadays, the desire to embed more applications in systems as small as smart cards or sensors is growing. However, physical limitations of these systems, like very small main memory, and their cost of production make this very difficult to achieve. One solution is to execute code from a secondary memory, cheaper, denser, but slower, such as NAND Flash. Solutions based on Demand-Paging and using a cache in main memory, began to be proposed and implemented in the domain of mobile phones, but consume too much RAM yet, compared to what can provide a smart card. In this paper, we show that we can dramatically increase performance by reducing the size of pages in the cache. This solution then allows a more intelligent access to the NAND. We also show that our solution allows to use Demand-Paging within limits of smart cards memories, where a conventional approach, offering too low bandwidth, makes impossible code execution from this kind of secondary memory.

Requests scheduling in Web servers is a hot research topic. Many works aim at providing optimal algorithms according to various metrics. Most of these works are based on classical scheduling metrics, considering jobs completion times, but ignoring intermediate states. We claim that this choice conduces to the design of algorithm that do not efficiently share the system resources. Indeed, Web servers have some properties that make them different than the system considered in usual scheduling theory. The classical round-robin policy, used in most production Web servers, has intrinsic qualities: it shares equally the system resources and avoids any job starvation. We introduce a novel parameterizable algorithm proposing a compromise between the benefits of the round-robin and the policies that provide the best performances. Then, we discuss the appropriate choice of the parameter depending in the requirements and the context of the Web server.

This article presents a new way to deploy and customize embedded virtual machine based operating systems for very restrained devices. Due to the specificity of restrained embedded devices (large usage of read-only memory, very few writable memory available, …), these systems are typically deployed off-board, in a process called romization . However, current romization solutions do not allow a complete deployment to take place outside of the execution device: they are capable of converting system components and applications into their executable form, but are unable to perform any operation that would require the system to be running. This results in a good part of the deployment being performed by the target device, at the cost of longer startup times, bloat with code and data that are only executed once at startup, and suboptimal memory placement of data structures. In this article, we propose a new romization scheme that allows the system to be started within a virtual execution environment, and thus to be fully deployed off-board before being transferred to its real execution support. We then take advantage of all the information provided by the deployed state in order to analyze and customize it, resulting in a very low-footprint, custom-tailored embedded system. The Java platform is used as a support to implement our romization architecture and perform our experiments. For the evaluated set of embedded applications, we were able to obtain embedded systems which memory footprint was lower than their J2ME counterpart, while being based on a full-fledged J2SE environment.

In this paper, we show that Web protocols and technologies are good candidates to design the Internet of Things, through a user-centric architecture (the user simply has to use a standard Web browser). We detail how this Web of Things can handle typical embedded devices interaction needs. We discuss the technical feasibility of embedded Web servers, and, thanks to an analysis of the Web protocols, we propose new cross-layer solutions for efficient tiny embedded Web servers design. The problem of event notification for Web applications is also discussed. We finally present a prototype - named Smews - as a proof of concept of the Web of Things. Smews implements our proposals and has been embedded in tiny devices (smart cards, sensors and other embedded devices), with a requirement of only 200 bytes of volatile memory and 7 kilo-bytes of code. We show that it is significantly faster than other state of the art solutions. We made Smews source code publically available under an open-source license.

Embedded systems such as smart cards or sensors are now widespread, but are often closed systems, only accessed via dedicated terminals. A new trend consists in embedding Web servers in small devices, making both access and application development easier. In this paper, we propose a TCP performance model in the context of embedded Web servers, and we introduce a taxonomy of the contents possibly served by Web applications. The main idea of this paper is to adapt the communication stack behavior to application contents properties. We propose a strategies set fitting with each type of content. The model allows to evaluate the benefits of our strategies in terms of time and memory charge. By implementing a real use case on a smart card, we measure the benefits of our proposals and validate our model. Our prototype, called Smews, makes a gap with state of the art solutions both in terms of performance and memory charge.

Smart card platforms are migrating from restrictive proprietary environments to open multi-application infrastructures. Computing the worst case execution time of an embedded application while there is no way to make previous assumptions on the CPU configuration available on the smart card had to be faced differently. In this paper, an evaluation of a distributed WCET computation method is presented. A low-level analysis on an ARM7TDMI CPU core is also described. We explain how the global WCET of a dynamically loaded application is extracted. Experimental results show a small overestimation compared to the observed execution time for a PIN-based authentication applet. Hardware-dependent WCET computation can also take advantage of the typing information related to the intermediate language. Improvement in the performance evaluation is up to 81,22%.

Small devices have a specific hardware configuration. In particular, they usually include several types of memories (typically ROM, internal and external RAM, ROM, Flash memory) different in quantities and properties. We propose an object memory management where the placement of an object in a given generation is based on different properties. This approach is supported by a domain specific language allowing to write powerful and flexible placement policies. These placement policies completely describe the placement, in the different memories, of the objects handled by the virtual machine.

Using beam forming antennas and ULB modulations in ad hoc networks have been recently focused on, as they allow to drastically improve ad-hoc network performances. This new technological context implies revisiting common network algorithms. When considering an multi-sector antenna uncommon with an uncommon high switch delay, packets have to be efficiently scheduled on beams at the MAC layer level, in order to improve the network capacity. We consider two optimization criteria: the network throughput and the maximum delay of packets. This paper proposes and studies a MAC scheduler, FIFO TBW, efficiently reducing the overhead due to beam switching delays. We give a first approach to estimate the window duration parameter

In most current approaches to software security, security flaws are fixed only after they have been exploited. To increase user confidence in software products, the software industry needs more proactive and durable security solutions by addressing security requirements throughout the software system lifecycle, including requirements and design specification, testing, and maintenance phases. Appropriate security analysis techniques must be used for each of these phases. In this paper, we illustrate an integrated security analysis framework, which combines a quantitative design security analysis technique, with a static program analyzer, which tracks unsafe information flows. We illustrate the framework by presenting a case study based on medical information card

Pervasive computing is the next generation of computing environments. As a result more and more applications are dynamically deployed on a growing set of small safe devices. Applications delivered by different vendors may share code and data while they may not trust one another. We present an information flow analysis for full Java bytecode adapted for applications dedicated to embedded systems. Existing techniques are not well adapted to this domain and are often too complex. To ease embedded operations and reduce overhead, an external static analysis is performed initially, and the results are embedded as annotations within the code and certified at loading time. In contrast with other analysis techniques, our model supports dynamic class loading. We evaluated our model on a business case study involving an electronic wallet for air miles storage and management from the literature. We obtained the same results as the other papers but under more restrictive conditions related to inherent characteristics of embedded environments.