Felix Bräunling
email: manyfelix.braeunling@methodpark.de

Robert Hilbrich
email: robert.hilbrich@dlr.de

Simon Wegener
email: swegener@absint.com

Isabella Stilkerich
email: isabella.stilkerich@schaeffler.com

Daniel Kästner
email: kaestner@absint.com

* Felix

Using Generic Software Components for Safety-Critical Embedded Systems -An Engineering Framework

come   L'archive ouverte pluridisciplinaire

Introduction

Safety-critical embedded systems represent a special class of computerized control systems. The interplay of their software and hardware parts realizes complex functions, such as engine control or vehicular guidance. Undetected errors in the implementation of a function may jeopardize human lives, hence the additional attribute safety-critical. Implementing the necessary software correctly, satisfying all safety requirements and maximizing hardware resource utilization in a cost-sensitive and competitive market poses a significant challenge for established software engineering methods and tools.

A recent example for the increasing capabilities of microcontrollers are embedded multicore processors containing multiple and possibly heterogeneous execution units. In order to tap their potential and maximize resource utilization, software components have to be tightly integrated and optimized specifically for each hardware platform. This optimization step is referred to as adaptation and often conducted manually.

With more software components sharing common resources of a microcontroller, ensuring their isolation against undesired interferences is essential in order to maintain the reliability and safety of the system. Therefore, the adaptation needs to ensure isolation between tightly integrated software components. This can be achieved by controlling access to both memory and CPU time, thereby supporting error containment.

Problem Statement

Software engineering for safety-critical embedded systems is currently conducted in a "per-project" fashion. Depending on the setup of the system architecture in different projects, it may be necessary to distribute software components across a network of microcontrollers or to run them on different microcontroller derivatives. Unfortunately, due to the complexity and the lack of proper engineering tools, software components are often developed specifically to match the requirements of a particular project. They are allocated manually to the resources in the system's hardware architecture and adapted manually to make best use of the capabilities of the microcontrollers. Especially for safety-critical systems, ensuring an isolated execution of software components requires additional configuration and analysis steps which are specific to the microcontroller and thus often conducted manually as well.

While the "per-project" approach may be sufficient for a small number of projects, it still requires a lot of manual effort and reduces the reusability of software components. With more and more control functions in safety-critical devices being implemented in software, the need for reusability and adaptability for different hardware platforms increases, which renders the "per-project" approach no longer economically sustainable. The question arises, how software components for safety-critical embedded systems can be developed in a generic and reusable way, so that they can be used in multiple projects, but without reducing resource utilization or jeopardizing their isolation properties and memory safety.

General Approach

The authors argue that the level of reusability can be significantly improved with a model-based development of generic software components in combination with an automated adaptation toolkit to handle project-specific hardware properties and safety requirements.

In general, software components are concerned with the implementation of specific features of the system. By using abstraction layers, they can be developed in a platform agnostic manner and organized as a library of generic software components for later use in multiple projects. As a result of adopting a formalized and model-based development approach, these generic functions can be automatically tailored and adapted to the specific requirements of a project. In particular, this approach facilitates automated software deployment in combination with automated platform-specific code generation as well as automated configuration and validation of isolation properties. This "feature-based" software development is not entirely new [START_REF] Apel | An overview of feature-oriented software development[END_REF][START_REF] Berger | A study of variability models and languages in the systems software domain[END_REF]. However, the authors believe that the state of practice and the capabilities of available tools for this purpose have not yet reached the level of maturity needed for the development of multi-platform safety-critical embedded systems.

Contribution

In this paper, the authors present the results of the development of an engineering framework aiding system architects and software engineers. Software for embedded systems relies on mature development tools in order to cope with complexity and to satisfy all (safety) requirements. Therefore, the framework combines and extends the tools ASSIST, Astrée and cAMP. By providing interoperability between these tools and enhancing them with new functionality, the framework is able to automate the integration and tailoring of applications in safety-critical embedded systems (i.e., automated adaptation).

In its current state, the framework provides an early and significantly less error-prone evaluation of timing and memory-partitioning decisions at the system level, the software level and also the implementation level. Combining these tools as a framework allows to automatically adapt and integrate generic software components in order to create project-specific applications running on project-specific microcontrollers. Projectspecific topics, such as the properties of a particular microcontroller, as well as spatial and/or temporal isolation requirements are also taken into account. By taking advantage of code generation, the framework supports an automated development process, thus building the missing link between generic libraries of software components and project-specific applications.

Conceptual Overview

Figure 1 depicts the simplified workflow of our framework. It is based on the idea of a strictly top-down engineering approach combined with the correctness by construction methodology [START_REF] Chapman | Correctness by construction: a manifesto for high integrity software[END_REF] and supports the engineer by automating the synthesis and validation of crucial engineering artifacts.

Based on a model of the functional architecture, the systems engineer creates a model of the envisioned system architecture. This model contains a selection of generic software components from a library and a project-specific hardware platform. The feasibility of the chosen hardware platform with respect to the technical and safety-related requirements of the particular project can be automatically validated by constructing a deployment for the selected software components (see Section 6). If a valid deployment cannot be found, either the hardware platform or the selection of software components need to be modified. Then, sound semantic code analysis is applied to all software code to ensure sufficient isolation and memory protection, both of which are essential to ensure the correctness of the system (see Section 7). Finally, data and code of software components are automatically mapped to the isolation partitions of their microcontroller (see Section 8).

The essential parts of the framework are described in more detail in the next sections. However, this paper is not intended to provide a thorough and detailed description for each of the tools used in the framework. Instead it focuses on their contribution for an automated development process based on generic software components.

I4Copter

To illustrate our approach, we will use the I4Copter flight controller as an overarching example. The I4Copter is a research project developing a quadcopter as an example for hard real-time systems and control systems [START_REF] Ulbrich | I4Copter: An adaptable and modular quadrotor platform[END_REF][START_REF] Ulbrich | The I4Copter project -Research platform for embedded and safety-critical system software[END_REF]. While the quadcopter software was originally meant to be deployed to a single-core Infineon TriCore TC1796, we used the AURIX TC277 for this paper, which is a three-core automotive microcontroller. The control software of the I4Copter consists of six modules: a digital signal processor (DSP) for reading sensor and remote inputs, a two-stage controller, and three observers. All these modules are responsible for controlling the positioning of the quadcopter during take-off, flight and landing. Further details of the I4Copter and the targeted hardware will be given in the following sections to describe their relevance to the presented framework. The example system resembles control systems similar to those used in automotive chassis systems in complexity and size. The AURIX TC277 was selected because it is a widely used microcontroller in the automotive domain. It also provides heterogeneous memories and computation units which allow for a flexible and adaptive deployment of software based on

Platform Development

In order to develop application software components in a reusable and structured way, the state of practice in systems engineering [START_REF] Kossiakoff | Systems Engineering Principles and Practice[END_REF] recommends to start with a functional architecture. It is constructed as a result of a rigorous requirements engineering process and its relationship to other system views [START_REF] Pohl | Model-Based Engineering of Embedded Systems: The SPES 2020 Methodology[END_REF]. The functional architecture is tightly bound to the logical intentions and dependencies of the software applications. It is a special kind of abstraction and usually, it does not include details of the technical architecture.

The separation into a functional and a technical architecture allows for a separation of concerns between the problem domain and the variations of possible technical solutions. This approach allows to construct applications and infrastructure software independently, because implementations on both ends can be developed separately as long as they comply with the "contract" of the common interface.

In our case, this can be described by using the bridge pattern, which is depicted in Figure 2. The bridge pattern is intended to decouple the abstraction from its implementation [START_REF] Gamma | Design patterns: elements of reusable object-oriented software[END_REF]. A functional element describes an abstract function. A technical implementation on the other hand is a tangible implementation providing the functionality described by the functional element. The functional element does not need to know about the tangible implementation, thus the technical implementation can be replaced by other solutions as long as all project-specific requirements are met. Still, the functional and technical view are not fully independent of each other, because changes in either view may have significant effects on the other.

One example for a functional element in the I4Copter software is the filter used to reduce noise from sensor inputs. A technical implementation to provide the functionality could be an alpha-beta-filter, a running average filter or a Kalman filter. Their software modules must provide a common interface to make the filter implementations exchangeable. The choice of the filtering al-gorithm can be controlled by changing which module is linked during compile time into the application code.

In each project, it is the task of the systems engineer to select the suitable building blocks for each functional element, i.e., generic software components from a library as well as hardware components (microcontrollers), in order to create the system architecture model. Of course, the model needs to fulfill the requirements set forth in the functional architecture.

System Architecture

At the core of our approach is a system architecture model. There are several notations available to model a system architecture, for example SysML, UML, or AMALTHEA [START_REF] Höttger | APP4MC: Application platform project for multi-and many-core systems[END_REF], which allows to express safety-and timing-related requirements as well-defined first-class model elements.

Generally speaking, the system architecture model comprises of a description of the software components with their distinct resource requirements, a description of the available hardware resources, such as microcontrollers or memory, and also constraints, in particular safety requirements, that restrict the resource usage and allocation of software components.

Examples for safety requirements can be the need to detect sporadic hardware defects in the computation of a software component, heterogeneous hardware execution environments or the use of additional hardware for error correcting/detecting codes. These requirements translate to constraints on the system architecture and thus are limiting the solution space of the architecture. With the system architecture model being available, the mapping between software components and hardware resources is constructed in the next step. The construction needs to consider the capacities of all available resources, e.g., the size of flash memory. It must also ensure that the additional constraints (temporal and spatial isolation) are satisfied. This is achieved by constructing a feasible mapping and a static periodic schedule for all software components. Due to the complexity of the solution space and the importance of the correctness of the solution, this process is conducted in an automated fashion with the tool ASSIST [START_REF] Hilbrich | Experiences gained from modeling and solving large mapping problems during system design[END_REF]. The challenge of finding a correct mapping and a feasible static schedule is addressed by transformation of this problem into an equivalent constraint-satisfaction problem and the subsequent application of constraint programming [START_REF] Dechter | Constraint Processing[END_REF][START_REF] Apt | Principles of constraint programming[END_REF][START_REF] Rossi | Handbook of Constraint Programming[END_REF]. Similar approaches for safety-critical systems have been published [START_REF] Hilbrich | Model-based generation of static schedules for safety critical multi-core systems in the avionics domain[END_REF][START_REF] Schwitzer | Tackling the Complexity of Timing-Relevant Deployment Decisions in Multicore-Based Embedded Automotive Software Systems[END_REF]. Constraint programming refers to a set of techniques in operations research, discrete optimization, and artificial intelligence. These techniques assist in finding solutions for problems based on variables, which are affected by constraints (constraint-satisfaction problems). Each variable has a finite integer domain and every constraint defines valid or invalid solutions for a subset of these variables. Solutions for this problem class can be obtained by applying a combination of search techniques-including backtracking-and constraint propagation techniques for value elimination. ASSIST automates this process and hides the intricacies of a formal specification from the user by offering a user-friendly domain specific language to describe the mapping and scheduling problem. ASSIST is less detailed. Software tasks are considered to be "black boxes" with annotated resource requirements. ASSIST also aims to simplify the complexity of the scheduling problem, by constructing a scheduling for a single hyperperiod containing periodic executions of all tasks. Internally, ASSIST uses the CHOCO SOLVER [START_REF] Prud'homme | Choco Documentation[END_REF], which has been successfully applied in a wide variety of scheduling problems.

Figure 3 contains the specification of the hardware properties of the Infineon AURIX TC277 microcontroller. ASSIST allows to specify features, such as an FPU, as well as capacities, for example flash memory, to constrain the deployment process.

The specification of the software architecture is presented in Figure 4. It consists of six applications together with their tasks. For the sake of simplicity and readability of the example, each task only requires a certain amount of the processor time (called CoreUtilization in the specification). The core utilization is determined by the task's worst-case execution time (WCET) divided by the task's period. Safe upper bounds on the WCET can be calculated, e.g., by aiT WCET Analyzer [START_REF] Kästner | Reliability of WCET Analysis[END_REF] for timing-predictable processors such as the AURIX TC277. On non-timing-predictable multi-core processors, WCET estimates can be provided by hybrid WCET analyzers such as TimeWeaver [START_REF] Kästner | TimeWeaver: A Tool for Hybrid Worst-Case Execution Time Analysis[END_REF]. The task T2 EngineController shows how particular features of a processing core can be required by a task.

Figure 5 shows the dependencies between the different tasks which are present for a single period of the cyclic tasks of the I4Copter system. The tasks T4 HeightObserver and T5 AltitudeObserver could be run in parallel to exploit the resources of the TC277 multicore processor. ever, this does not constitute a hard constraint for the deployment synthesis, because a deployment of these tasks to the same core may still be feasible, but less desirable. Therefore, ASSIST needs to treat the information about the parallel execution of T4 HeightObserver and T5 AltitudeObserver as a hint for achieving an optimized solution. For this purpose, a task graph can be specified in ASSIST, which allows the tool to automatically determine which tasks could be run in parallel in order to derive the optimization hints for the deployment. The specification of the task graph for the example of this paper is contained in Figure 6.

In contrast to the "soft" optimization hints, there are also "hard" deployment constraints, such as safetyrelated constraints, which affect the feasibility and validity of the results. These constraints must be satisfied in order to obtain a valid deployment. For the example use case, two additional safety requirements are assumed to ensure reliability despite potentially harsh environmental conditions.

1. The tasks T6 DSP and T3 AttitudeObserver must not share the same core.

2. The tasks T6 DSP and T4 HeightOberserver must not share the same core.

Figure 7 shows how these requirements can be expressed as "hard" mapping constraints in ASSIST.

Based on the deployment specification described in the listings above, ASSIST was able to determine all valid deployment solutions. There are 208 different solutions, which were computed in about 250 ms on a regular desktop computer. In order to find the "best" solutions among the set of valid solutions, ASSIST allows to apply a set of metrics to each deployment. Those metrics allow to compute a score for each solution, which reflects the fulfillment of the optimization goals reflected in the metrics. Solutions with the highest scores are therefore assumed to be the "best" solutions. Most important is the achievement of parallel execution of tasks by the deployment. Therefore, solutions should be ranked higher, if parallel tasks in the task graph are indeed mapped to different cores. Furthermore, mapping solutions with a uniform core load are preferred over solutions with a heterogeneous load. Figure 8 shows the selection of these metrics in ASSIST. Setting the Weight of the Max parallelism metric to the value of two allows to express the importance of the first goal in comparison to the second optimization goal. The automated evaluation with the aforementioned metrics identified two solutions with the highest score, from which we selected one (see Figure 10).

As a last step, an AUTOSAR-OS configuration file is generated by ASSIST, which constitutes a central engineering artifact for the following steps in our engineering framework.

Static Analysis of OS Configuration and Source Code

This section addresses the prerequisites for an automated low-level deployment of code and data in order to provide the memory handling and memory protection.

AUTOSAR-OS System Model

AUTOSAR is a partnership between different automotive manufacturers to design a standard for an embedded automotive operating system. Currently there are two versions of the standard, the AUTOSAR Classic for static systems and AUTOSAR Adaptive for dynamic systems. In this paper we only refer to the AUTOSAR Classic family of operating systems. The AUTOSAR system model is depicted in Figure 9.

The system is structured around OS-Applications that are executed on one specific computing unit of the underlying hardware. OS-Applications manages instructions and data in memory as an execution environment for one or more tasks. The tasks themselves are schedulable execution units, each with its own data and stack segment. By using hardware-based memory access protection, such as a memory protection unit (MPU), the kernel memory can be spatially isolated from OS-Applications. The same mechanisms also allows for spatial isolation of OS-Applications from other OS-Applications, as well as of tasks inside of OS-Applications. This is indicated by the thick black lines in Figure 9 The static structure of an AUTOSAR system, consisting of the mapping of cores, OS-Applications, tasks and memory protection regions as well as schedules and timer events, is described in a configuration file. The so called ARXML files are written in an AUTOSARstandardized XML format. Based on this file operating systems implementing the AUTOSAR standard can generate operating system code reflecting the configuration described in the ARXML file. Such an ARXML file is the output of ASSIST, which in turn can then be used by Astrée for a semantic analysis of the operating system and the application code.

Ensuring Memory and Type Safety

Despite the successful deployment of all software components, memory and type safety need to be addressed in order to ensure spatial isolation between all tightly integrated software components. Memory safety in the scope of the C programming language is defined as the absence of memory accesses that trigger undefined behavior, as well as the absence of data races where shared variables are accessed by concurrent threads without proper synchronization. Although the C programming language itself does not ensure memory safety, a sound static analysis of the C source code is able to guarantee memory safety at the programming language level. In our framework we use the Astrée analyzer [START_REF] Kästner | Finding All Potential Runtime Errors and Data Races in Automotive Software[END_REF][START_REF] Miné | Taking Static Analysis to the Next Level: Proving the Absence of Run-Time Errors and Data Races with Astrée[END_REF]. Its main purpose is to report program defects caused by unspecified and undefined behaviors according to the C99 standard. The reported code defects include integer/floating-point division by zero, out-of-bounds array indexing, erroneous pointer manipulation and dereferencing (buffer overflows, null pointer dereferencing, dangling pointers, etc.), data races, lock/unlock problems, and deadlocks. To deal with concurrency defects, Astrée implements a low-level concurrent semantics [START_REF] Miné | Static analysis of run-time errors in embedded real-time parallel C programs[END_REF] which provides a scalable sound abstraction covering all possible thread interleavings. The analyzer takes task priorities into account and, for multicore systems, the mapping of tasks to applications and cores. Table 1 shows the relation between memory and type safety and the defects found by Astrée. Astrée is widely used in safety-critical systems, and provides the necessary tool qualification support, including Qualification Support Kits and Qualification Software Life Cycle Data reports.

The AUTOSAR-OS configuration file produced by ASSIST during the high-level deployment is parsed by Astrée to automatically generate a matching analysis configuration that models the asynchronous execution of the various tasks and ISRs. Astrée returns a list of potential code defects. An analysis resulting in zero alarms guarantees the absence of memory safety violations in the C source code. Since the C semantics assumes unlimited stack space, the source-level analysis needs to be complemented by a sound static stackusage analysis at the binary level to prove the absence of stack overflows [START_REF] Kästner | Proving the Absence of Stack Overflows[END_REF]. Moreover, using a formally verified compiler ensures that no memory safety defects are introduced by miscompilation [START_REF] Leroy | CompCert -A Formally Verified Optimizing Compiler[END_REF]. Together, these approaches are able to prevent software-induced memory corruption, hence establishing memory safety.

Besides reporting runtime errors and concurrency defects, Astrée also produces detailed data and control flow reports. Soundness provides a guarantee that neither control flow paths nor read or write accesses are missed, even in case of data or function pointer accesses, or task interference. Global data and control flow analysis gives a summary of variable accesses and function invocations throughout program execution. The reports also contain each effectively shared variable, the list of tasks accessing it, the application and the core to which the task has been assigned, and the types of the accesses (read, write, read/write). Indirect variable accesses via pointers as well as function pointer call targets are fully taken into account. Filtering allows determining the control and data flow per software component, thus supporting the analysis of data and control coupling as required by DO-178C. An excerpt from the data flow report for the example system is shown in Table 2. Note that Astrée detects data races for each of the shared variables in our example system, which is expected, because the code does not contain any synchronization mechanisms.

Memory Mapping

After the definition of the system, the deployment of all software components, and the analysis for memory safety, the next step constitutes the low-level mapping of all instructions and their data to the physical memories of the specific microcontroller. This step is also called binding.

Heterogeneous Memory

This task is especially important for multicore processors with heterogeneous memories, such as the AURIX TC277, in order to achieve good runtime behavior as well as spatial isolation for freedom from interference. The AURIX TC277 offers six core-coupled SRAMs for data (DSPR) and instructions (PSPR), a non-volatile flash memory (PMU) and a bus-accessed SRAM (LMU). It is possible to access any of the memories from any of the cores using the microcontroller's bus. However, read and write operations to the corecoupled SRAM take only one CPU cycle if they origi-nate from the coupled core, whereas memory accesses via the bus take more time. Moreover, accesses via the bus have less deterministic access times because of interference due to concurrent bus accesses. The flash memory is also equipped with error correction capabilities to ensure data integrity.

Data and Function Classes

At the same time, data and functions exhibit traits such as origin of access, type of access, frequency of access, and logical traits such as being constant or used for in-system calibration. The combination of these properties favors the binding of each data item or function to a different memory of the microcontroller. Data items and functions that exhibit similar traits can be grouped to variable and function classes, each with a set of preferred memories dictated by a binding policy. In the I4Copter example two orthogonal types of classification exists: task-wise and core-wise. Task-local data and functions are only accessed by a single task whereas task-global data is accessed by two or more tasks. Analogous to this, core-local data and functions are only accessed from a single core, while core-global data and functions are shared between different cores. Constant data items are grouped into different classes, as their read-only property makes them suitable for binding them to the flash memory and relying on core-coupled cache memories to reduce access times.

Binding Policy

Binding policies describe to which memory a particular data item or functions should be mapped, depending on both the properties exhibited by the available memories as well as the variable and function classes.

An example for such a policy is the mapping of task-local, core-local data to the core-coupled SRAM to achieve the fastest access time. Another policy is that task-global, core-global data is mapped to the corecoupled memory of the core from which most accesses are originating. As the capacity of these memories is finite, it needs to be decided which data and functions are bound first. This can be done by optimizing policies, ranging from a very simple one based on the total access frequency, using different weights for read and write operations, to complex optimization algorithms using either constraint solving problems or integer linear programming.

In the I4Copter example presented in this paper, data items are sorted by the total amount of reads and writes to these data items. The access frequencies are determined by taking the amount of read and writes reported by Astrée multiplied by the amount of task activations during one hyperperiod (9 ms) of the system. Data items with a higher count of total accesses are mapped first.

Automated Memory Mapping

Gathering the information about data and function traits, combining it into classes and then creating a mapping to hardware memories is not feasible if done manually in systems of arbitrary complexity. The cAMP tool addresses this problem by automatically generating a mapping of instructions and data to memories. For this, all available information from the previous development steps is used: deployment information from ASSIST by taking into account the deployment solution described in the generated ARXML file. Information about data and functions traits can be extracted from Astrée by taking into account the data flow report (see Table 2). Finally, also the requirements from the system specification such as task times, safety requirements and constraints are taken into account.

The information is aggregated within cAMP and used to generate a binding of data and functions to memories, as well as assigning MPU-enforced memory protection regions to each used section of memory. The binding is performed by following the binding policies for the selected hardware. The result of this process is a linker script that describes the memory mapping and exposes the sections needed to configure the system's MPU.

To reduce the amount of effort necessary to use the linker script, i.e., the assignment of individual variables and functions to the various memory sections, cAMP is able to interface with code generation tools to automatically include the necessary annotations in the generated code. In its current form, cAMP is able to interface with TargetLink, a widely used C code generator for Mat-Lab/Simulink.

The use of cAMP allows the automatic tailoring of applications to specific hardware and memory layouts by creating a reproducible binding process. Using code generation and platform-based development adds further benefits, such as automatic code adaption and reusable binding policies. The automatic binding of data and code results in a significant reduction of software development time, while being less error-prone than manual binding.

Related Work

The basic idea for our framework is inspired by KESO and program families presented by Parnas [START_REF] Parnas | On the design and development of program families[END_REF]. Parnas was one of the first to give thought to program families and software-product lines (SPL). He described the problem in the context of operating systems. Building on his ideas, later approaches examined the variability challenge in large software systems. For instance, Sincero et al. [START_REF] Sincero | Is the Linux kernel a software product line[END_REF] investigated the Linux kernel and treated it as an SPL through configuration analyses. Liebig et al. [START_REF] Liebig | An analysis of the variability in forty preprocessor-based software product lines[END_REF] looked at configurable software composed in C and explored ways to deal with the complexity induced through preprocessor directives. There are also solutions (e.g., [START_REF] Elsner | Variability in time -product line variability and evolution revisited[END_REF][START_REF] Siegmund | SPL Conqueror: Toward optimization of non-functional properties in software product lines[END_REF]), which use generative programming [START_REF] Czarnecki | Generative programming and active libraries[END_REF] to create program variants from configurability models. Another project that leverages the idea of program families is an operating-system construction kit called PURE [START_REF] Beuche | The PURE family of object-oriented operating systems for deeply embedded systems[END_REF]. The authors define a base set of reusable OS-infrastructure components (e.g., threads, scheduling, concurrency, interruptions or memory service) needed to build infrastructure services. For instance, light-weight threads that can be used to compose address spaces and processes. The authors employ a configuration-and code-generation-based framework to create operating-system variants. Different from these prior works, we allow to manipulate spatial and temporal isolation properties in an early design phase based on architecture-and code-analyzing techniques of reusable application parts that can also be developed using model-based techniques.

The KESO Java Virtual Machine [START_REF] Stilkerich | Tailor-made JVMs for statically configured embedded systems[END_REF] provides an isolation concept that is similar to the process concept found in general-purpose operating systems. KESO features a compiler, which is able to produce a virtual machine environment specialized for a particular application. Therefore, KESO adopts ideas from Parnas' approach. In the following, we describe the characteristics of KESO that are relevant for our work. Spatial isolation ensures that control flows are only able to access memory of data regions belonging to the protection zone (called domain) in the context of which the control flow is being executed. Therefore, each piece of data can be logically assigned to exactly one domain. In Java, type safety ensures that programs can only access memory regions to which they were given an explicit reference; the type of the reference also determines in which way a program can access the memory region pointed to by the reference. To achieve spatial isolation, the KESO compiler enforces that a reference value is never present in more than a single domain. Different from KESO, our applications are not developed in Java but using a model-based technique in which the generated C code is analyzed using abstract interpretation in order to cre-ate memory-safe C code. We extended Astrée to use information on the AUTOSAR OS threading model toamongst other things-be able to perform a flow-and context-sensitive analysis based on OS-Applications to build logical isolation zones that are enforced by memory protection hardware.

The article [START_REF] Pagano | A Model Based Safety Critical Flow for the AURIX Multi-core Platform[END_REF] addresses problems similar to those addressed by our work, but assumes a different communication model. In contrast to AUTOSAR, which uses shared memory for communication between task, their communication model is based on Kahn Process Networks, and the used operating system is based on a nonshared memory model. For spatial isolation, they rely solely on the use of the MPU to ensure dynamic fault containment. We, in contrast, use sound static analysis of the integrated source code to foster safety by construction and utilize the MPU as a safety net. Moreover, the high-level deployment is not part of their workflow but assumed as an input.

Conclusion

The authors present the results of a joint research and development project towards an engineering framework for using generic software components in safety-critical embedded systems. The framework combines several tools, so that generic software components can be adapted to a particular microcontroller and analyzed for memory integrity. Common starting point is a model of the system architecture comprising of a system specification and a functional architecture. Additional information about the target hardware (microcontroller family) and a library of generic software components is considered to be available as well. These specifications are passed through different engineering tools and code analyzers via common exchange formats.

In particular, the tool suite ASSIST allows to generate software allocations for the targeted hardware. By including timing constraints, it also allows to construct a static schedule, thus ensuring the feasibility of the system design. This results in an operating system configuration describing the spatial and temporal behavior of all software components.

In combination with the generated application software, the C sources are examined with Astrée. By removing memory and type defects found during the analysis, memory integrity can be ensured at the C code level. Furthermore, information about data and function access behavior is collected during the analysis step. In a final step, this information is used by cAMP to perform the low-level mapping of data and functions to physical memories and protection regions.

The final result comprises of annotated application code and a linker script describing the memory mapping, which is guaranteed to satisfy all project-specific safety requirements and to utilize the capabilities of the microcontroller. The final results as well as the intermediate work products can be found on GitHub [START_REF] Bräunling | Generic Software Tailoring Example[END_REF]. Us-ing this framework allows to adapt generic application software for safety-critical systems in an efficient and automated manner, so that software reusability can be achieved without reducing resource utilization or jeopardizing system safety.

Figure 2 :

 2 Figure 2: The relation between the functional elements and the technical implementation exhibits the bridge pattern.

Figure 4 :

 4 Figure 4: Applications and Tasks in ASSIST

Figure 5 :Figure 6 :Figure 7 :

 567 Figure 5: Task Dependency Graph

Figure 8 :

 8 Figure 8: Evaluation of Solutions

Figure 9 :

 9 Figure 9: AUTOSAR Isolation Schemes

Figure 10 :

 10 Figure 10: Deployment solution found by ASSIST

Table 1 :

 1 Mapping of Requirements of Type-and Memory Safety[START_REF] Aiken | Deconstructing process isolation[END_REF] to Astrée Alarm Types [1].

	Requirement	Alarm Type
	Operations only applied for	Invalid pointer comparison
	instances of correct type	Subtraction of invalid pointers
		Attempt to write to a constant
		Dereference of mis-aligned pointer
		Overflow of Integers or Float
		Invalid shift argument
		Use of uninitialized variables
		Division or modulo by zero
		Undefined integer modulo
		Invalid function calls
		Unsynchronized access to shared data
	Access only existing objects	Dereference of null or invalid pointer
		Pointer to invalid or null function
		Use of dangling pointer
		Arithmetics on invalid pointers
		Possible overflow upon dereference
	Access only inside object	Incorrect field dereference
	boundaries	Out-of-bound array access
		Dereference of mis-aligned pointer
		Possible overflow upon dereference

Table 2 :

 2 Excerpt from Astrée Data Flow Report

	Variable	Function	Access Process	Data Races Shared Class
	In_altCtr_AccZ_g_altObs_noiseVariance	TASK_T1_Controllers	write	T1 Controllers	no	no	process local
	In_altCtr_AccZ_g_altObs_processVariance TASK_T1_Controllers	write	T1 Controllers	no	no	process local
	Out_accX_g_dsp_noiseVariance	TASK_T3_AttitudeObserver read	T3 AttitudeObserver yes	yes	global
	Out_accX_g_dsp_noiseVariance	TASK_T6_DSP	write	T6 DSP	yes	yes	global
	Out_accX_g_dsp_processVariance	TASK_T3_AttitudeObserver read	T3 AttitudeObserver yes	yes	global
	Out_accX_g_dsp_processVariance	TASK_T6_DSP	write	T6 DSP	yes	yes	global
	Out_torqueX_NM_attCtr	TASK_T2_EngineController read	T2 EngineController yes	yes	core local
	Out_torqueX_NM_attCtr	STEP_AttitudeController	write	T1 Controllers	yes	yes	core local
	Out_torqueX_NM_engCtr	TASK_T3_AttitudeObserver read	T3 AttitudeObserver yes	yes	core local
	. . .	. . .	. . .	. . .	. . .	. . .	. . .

ACKNOWLEDGMENT

This work was funded within the project ARAMiS II by the German Federal Ministry for Education and Research with the funding ID 01IS16025 and by the Deutsche Forschungsgemeinschaft (DFG) within the AORTA project with funding ID SCHR 603/9-1. The responsibility for the content remains with the authors.

Data Data Data Code Code Code Code Task B Task C Task D Data Data Data Data Stack

In contrast to other approaches [START_REF] Rogovchenko | Composition and compositionality in a component model for autonomous robots[END_REF][START_REF] Rogovchenko | Handling hardware heterogeneity through rich interfaces in a component model for autonomous robotics[END_REF], which are based on the composition of components with rich interfaces, ASSIST works on a higher abstraction level and treats mapping and scheduling as separate steps in order to reduce the size of the problem in each step. For this purpose, the modeling of component properties in


Daniel Kästner

Laurent Mauborgne

Stephan Wilhelm

Christian Ferdinand

High-Precision Sound Analysis to Find Safety and Cybersecurity Defects

In recent years, security concerns have become more and more relevant for safety-critical systems. Many cybersecurity vulnerabilities are caused by runtime errors, hence sound static runtime error analysis contributes to meeting both safety and security goals. In addition, for cybersecurity goals, often sophisticated data and control flow analyses are needed, e.g., to track the effects of corrupted values, or determine dependence on potentially corrupted inputs. A sound analysis can guarantee that neither control flow paths nor read or write accesses are missed, even in case of data or function pointer accesses. To be feasible for industrial use, a static analyzer must be precise, i.e., produce few false alarms, and it must be user-configurable to allow analyzing specific data and control flow properties. It must also support efficient alarm investigation to minimize the manual effort needed to review the findings of the analyzer. In this article we give an overview of novel extensions of the sound static analyzer Astrée to minimize the false alarm rate, and to support advanced data and control flow analysis by taint analysis and analysisenhanced program slicing. We describe an application of Astrée's taint analysis framework to detect Spectre v1/1.1/SplitSpectre vulnerabilities. Astrée's program slicer can also be applied for alarm slicing, which can significantly reduce the manual effort of reviewing the analyzer findings. Practical experience is reported on industrial avionic and automotive applications.

Introduction

A failure of a safety-critical system may cause high costs or even endanger human beings. With the growing size of software-implemented functionality, preventing software-induced system failures becomes an increasingly important task. It becomes paramount when failoperational behavior is required, which is the case for systems providing highly automated driving capability.

One particularly dangerous class of errors are runtime errors due to undefined or unspecified behaviors of the programming language used. Examples are faulty pointer manipulations, numerical errors such as arithmetic overflows and division by zero, data races, and synchronization errors in concurrent software. Such er-rors can cause software crashes, invalidate separation mechanisms in mixed-criticality software, and are a frequent cause of errors in concurrent and multi-core applications. At the same time, these defects also constitute security vulnerabilities, and have been at the root of a multitude of cybersecurity attacks, in particular buffer overflows, dangling pointers, or race conditions [START_REF] Kästner | Detecting Safety-and Security-Relevant Programming Defects by Sound Static Analysis[END_REF].

In the past, security properties have mostly been relevant for non-embedded and/or non-safety-critical programs. Due to increasing connectivity requirements (cloud-based services, car-to-car communication, overthe-air updates, etc.), more and more security issues are rising in safety-critical software as well. Security exploits like the Jeep Cherokee hacks [START_REF] Wired | The jeep hackers are back to prove car hacking can get much worse[END_REF] which affect the safety of the system are becoming more and more frequent. Because of the increasingly pervasive monitoring of personal data including location data or health information, confidentiality breaches in embedded systems like mobile phones, automobiles, or airplanes have to be considered increasingly critical. Furthermore, data leakage might also have impacts on safety, e.g., if administrator or maintenance passwords are leaked.

Static code analysis has evolved to be a standard technique in the development process of safety-critical software. It can be applied to show compliance to coding guidelines, and to demonstrate the absence of critical programming errors, including runtime errors and data races. Abstract interpretation is a formal methodology for semantics-based static program analysis [START_REF] Cousot | Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF] which can be applied to demonstrate the absence of code defects due to undefined/unspecified behaviors, including runtime errors and data races. Abstract interpretation supports formal soundness proofs, i.e., it can be proven that -from the class of errors under analysis -no error is missed. Sound static analyzers provide full control and data coverage and allow conclusions to be drawn that are valid for all program runs with all inputs.

Safety-critical software is developed according to strict guidelines which effectively reduce the relevant subset of the programming language used and improve software verifiability. As an example dynamic memory allocation and recursion often are forbidden or used in a very limited way. By using formal techniques like abstract interpretation on such software, proving the absence of programming defects like runtime errors be-comes possible with very low false alarm rates: then, the corresponding safety risks and security vulnerabilities have been effectively eliminated. In addition, for cybersecurity -and for data safety [START_REF]Data Safety (Version 2.0)[END_REF] -, advanced data and control flow analyses are needed, e.g., to determine data and control coupling, to track the effects of corrupted values, or to determine dependence on potentially corrupted inputs. Here, a sound analysis can guarantee that neither control flow paths nor read or write accesses are missed, even when functions are called indirectly via function pointers, and data is accessed via pointers.

While soundness means that false negatives can be ruled out, the analyzer may still report false alarms. In general, if the false alarm rate of a (sound or unsound) analyzer is too high, the effort to review and classify the findings may be economically unsustainable. In this article we focus on the sound static analyzer Astrée for which the zero alarm goal has been an important design criterion [START_REF] Blanchet | A Static Analyzer for Large Safety-Critical Software[END_REF][START_REF] Kästner | Finding All Potential Runtime Errors and Data Races in Automotive Software[END_REF][START_REF] Kästner | Analyze This! Sound Static Analysis for Integration Verification of Large-Scale Automotive Software[END_REF] right from the start. The key idea is to be parameterizable with respect to its abstract domains: new domains can be added, and there is a global hierarchy in the implementation, which determines what kind of information each domain may access, and what level of abstraction they can use. As an example, we will give an overview of its most recent abstract domain, designed to automatically detects finite state machines and their state variables, which allows to disambiguate the different states and transitions by partitioning. Experimental results on real-life automotive and aerospace code show that embedded control software using finite state machines can be analyzed with close to zero false alarms, and that the improved precision can reduce analysis time.

The contribution of this article is to give an overview of the key mechanisms to enable precise and flexible sound static analysis for safety and cybersecurity properties, with the example of the analyzer Astrée.

The article is structured as follows: after a brief introduction of abstract interpretation in Sec. 2, we outline general design considerations for achieving high analysis precision in Sec. 3, give an overview of Astrée's novel finite state machine domain (Sec. 3.1) and summarize practical experience made on industrial software. To enable configurable deep data and control flow analyses (Sec. 4), Astrée has been equipped with a generic abstract domain for taint analysis, which is described in Sec. 4.1. It allows Astrée to perform normal code analysis, with its usual process-interleaving, interprocedural and memory layout precision, while carrying and computing taint information at the byte level. Any number of taint hues can be tracked by Astrée, and their combinations will be soundly abstracted. Based on this generic taint analysis framework we implemented an automatic detection of Spectre V1/V1.1/SplitSpectre vulnerabilities (cf. Sec. 4.2). To complement taint analysis, which is a forward analysis, Astrée also has been extended by a program slicer which performs backward analysis to identify the code parts and inputs relevant for a selected slicing criterion (cf. Sec. 4.3). While supporting analyzing safety-or security-oriented information flow in a program, it also allows for automatic alarm slicing, which improves usability of the analyzer. This is the subject of Sec. 5. Sec. 6 concludes.

Abstract Interpretation

The semantics of a programming language is a formal description of the behavior of programs. The most precise semantics is the so-called concrete semantics, describing closely the actual execution of the program on all possible inputs. Yet in general, the concrete semantics is not computable. Even under the assumption that the program terminates, it is too detailed to allow for efficient computations. Unsound analyzers may choose to reduce complexity by not taking certain program effects or certain execution scenarios into account. A sound analyzer is not allowed to do this; all potential program executions must be accounted for. Since in the concrete semantics this is too complex, the solution is to introduce a formal abstract semantics that approximates the concrete semantics of the program in a well-defined way and still is efficiently computable. This abstract semantics can be chosen as the basis for a static analysis. Compared to an analysis of the concrete semantics, the analysis result may be less precise but the computation may be significantly faster.

Abstract interpretation is a formal method for sound semantics-based static program analysis [START_REF] Cousot | Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF]. It supports formal correctness proofs: it can be proved that an analysis will terminate and that it is sound, i.e., that it computes an over-approximation of the concrete semantics. Imprecisions can occur, but it can be shown that they will always occur on the safe side.

The difference between syntactical, unsound semantical and sound semantical analysis can be illustrated with the example of division by 0. In the expression x/0 the division by zero can be detected syntactically, but not in the expression a/b. When an unsound analyzer does not report a division by zero in a/b it might still happen in scenarios not taken into account by the analyzer. When a sound analyzer does not report a division by zero in a/b, this is a proof that b can never be 0.

Minimizing False Alarms

Astrée [START_REF] Miné | Taking Static Analysis to the Next Level: Proving the Absence of Run-Time Errors and Data Races with Astrée[END_REF][9] uses abstractions to efficiently represent and manipulate over-approximations of program states. One simple example of abstraction used pervasively in Astrée is to consider only the bounds of a numeric variable, forgetting the exact set of possible values within these bounds. However, more complex abstractions can also be necessary, such as tracking linear relationships between numeric variables (which is useful for the precise analysis of loops).

As no single abstraction is enough to obtain suffi-ciently precise results, Astrée is actually built by combining a large set of efficient abstractions. Some of them, such as abstractions of digital filters -and now of finite state machines -, have been developed specifically to analyze control-command software as these constitute an important share of safety-critical embedded software. In addition to numeric properties, Astrée contains abstractions to reason about pointers, pointer arithmetic, structures, arrays (in a field-sensitive or field-insensitive way). Finally, to ensure precision, Astrée keeps a precise representation of the control flow, by performing a fully context-sensitive, flow-sensitive (and even partially path-sensitive) inter-procedural analysis. Combined, the available abstract domains enable a highly precise analysis with low false alarm rates.

To deal with concurrency defects, Astrée implements a sound low-level concurrent semantics [START_REF] Miné | Static analysis of run-time errors in embedded real-time parallel C programs[END_REF] which provides a scalable sound abstraction covering all possible thread interleavings. The interleaving semantics enables Astrée, in addition to the classes of runtime errors found in sequential programs, to report data races, and lock/unlock problems, i.e., inconsistent synchronization. The set of shared variables does not need to be specified by the user: Astrée assumes that every global variable can be shared, and discovers which ones are effectively shared, and on which ones there is a data race. After a data race, the analysis continues by considering the values stemming from all interleavings. Since Astrée is aware of all locks held for every program point in each concurrent thread, Astrée can also report all potential deadlocks.

Practical experience on avionics and automotive industry applications are given in [START_REF] Kästner | Finding All Potential Runtime Errors and Data Races in Automotive Software[END_REF][13] [START_REF] Kästner | Analyze This! Sound Static Analysis for Integration Verification of Large-Scale Automotive Software[END_REF]. They show that industry-sized programs of millions of lines of code can be analyzed in acceptable time with high precision for runtime errors and data races.

Analyzing Finite State Machines

One long-standing problem for static analyzers is the analysis of finite state machine implementations: as control flow is encoded in data values, the values of state variables must be very precisely known in order to determine the feasible control flow paths. Using legacy abstractions, such analyses were either very imprecise or very slow and memory demanding, sometimes both. Hence the required precision used not to be feasible, typically resulting in high false alarm rates.

Consider the code fragment in One major difficulty on this simple code, is to recognize that in state 3, the pointer p always points to the variable state. Using standard abstract domains, the analyzer cannot distinguish between individual iterations of the endless loop, it can only compute invariants which hold for any possible loop iteration. That means that the analyzer will (correctly) determine that at

G G 0 Ó Ó ! ! 1 ' ' 2 o o 3 G G 4
Figure 2: State machine the beginning of any iteration of the loop p being either uninitialized (invalid) or pointing to state. After executing the statements of case 0 the value of p did not change, but state can be in 1,2. After case 1, p points to state, and state must be 3. However, as the information at the beginning of the loop body is imprecise the analyzer cannot infer that when execution reaches case 3, it must have been in case 1 in the previous iteration. Therefore it cannot exclude that p may be invalid and will raise an alarm in line 17 (possibly invalid pointer dereference).

The FSM Domain

The FSM (finite state machine) domain allows us to map each relevant program variable to an own abstract value for every possible value of a state variable in a finite state machine. This works by partitioning the abstract value of the memory domain according to the state variable.

Let us first assume we already have a basic abstraction for sets of memory states, which we assume to be sound and terminating. Such an abstraction introduces an abstract domain that will be referred in the following as the underlying domain. We denote this domain D # , its maximal element, its approximation partial order, its join operator, and ∇ its widening operator (see Sec. 2). The meaning of an abstract element is described by the concretization function γ, such that for any abstract element a, γ(a) is the set of memory states represented by a. This is summarized by the following notation:

D # , , , , ∇ γ - → (P (M) , ⊆, ∪) (1)
In order to formally define the state machine abstract domain, we introduce the sets: L, of expressions of a program which are valid destinations of assignments (left-values), and V, of integer values. Our goal is to define a new abstraction where we can have a separate abstract value of the underlying domain (i.e. a set of memory states) for each integer value that the state variable may take. For reasons of efficiency this partitioning must not be applied in cases where it is not relevant (i.e. when we are outside the scope of a finite machine implementation), or unnecessarily costly. Then the state machine domain D #

A is defined as follows:

D # A := (V → D # ) × L ∪ D # × { } (2)
An abstract value of the state machine domain is either a value of the underlying abstract domain combined with to denote cases when we do not partition. Or it is a function f S : V → D # , called partitioning function, from integer values to abstract values in the underlying domain, combined with an expression l ∈ L that is currently partitioned. Here l is an lvalue of a state variable S, and the integer values in V are the values S can take. This allows us to have different abstract values in the underlying domain for each different value of S. As mentioned before, the underlying domain is the memory domain which keeps track of the values of all program variables. Hence we can separately keep track of the values of all variables for each possible value of the state variable.

Implementation

As mentioned above, Astrée combines a lot of abstract domains to achieve precision, parameterization and efficiency. There is a global hierarchy in the implementation, which determines what kind of information each domain may access, and what level of abstraction they can use.

The State Machine Domain builds on the Memory Layout Domain, which abstracts memory locations and pointer information, and associates memory locations to unique keys. All value domains only see the keys and compute sets of possible values for those keys. A dedicated helper value domain tracks which keys must be considered as state machine variables, and warns the State Machine Domain when such a variable is modified. Then, and only then, does the State Machine Domain trigger a call to trans, which is key to the efficient implementation for that domain.

While state machine state variables can be declared by an end-user using a simple directive (__ASTREE_states_track((v));), we always aim at the maximum automation of Astrée. In order to avoid this end-user declaration, we also have implemented automatic discovery of state machine state variables. It works in the following way:

• Identify integer variables used in switch statements

• keep those variables which are also assigned in at least one case of the switch, possibly following function calls

• keep only the switch statements appearing inside possibly infinite loops That heuristics captures some commonly generated state machines, and allows for a fully automatic and precise analysis of codes using this pattern. When the heuristics misses a state machine, the analysis will just miss the expected precision gain, which can still be achieved using directives. When the heuristics wrongly identifies a state machine, if the number of supposed states is small enough, the analysis will just be imprecise, and if the number of supposed states exceeds a built-in threshold, it will be rejected by the heuristics. Generalizing the heuristics to cover more complex patterns is subject of future work.

Applying the FSM Domain

The formal definition of the FSM Domain is given in [START_REF] Giet | Towards zero alarms in sound static analysis of finite state machines[END_REF]; here we will illustrate its operation with Fig. 3, which shows the analysis results of the working example of Fig. 1.

Let us call an abstract value of the underlying memory domain an environment. Using the heuristics described above, the analyzer automatically detects the finite state machine in the code and is aware that the variable state represents its states. Therefore it maintains a full partitioning of state which means that it keeps a separate environment for each possible value of state. The environment includes full information about the abstract value of all relevant program variables. In particular, this allows the analyzer to be aware of the fact that when state is 3 at the beginning of a loop iteration, p must point to state. Fig. 3 depicts this partitioning, i.e. the environments associated with every possible value of state at the beginning of the loop (A), immediately before the break statement in each switch case (B-E), and immediately before the return (F). More precisely, the tree structures of Fig. 3 represent the partitioning functions. For example, the tree shown at location (B) represents the abstract value d = ( f , state), where state is the state machine variable, and f a partitioning function such that f (1) is the abstract memory value (i.e. the environment) in which state is 1, p is invalid and E is true. f (2) is the abstract memory value in which state is 2, p is invalid and E is false. In [START_REF] Giet | Towards zero alarms in sound static analysis of finite state machines[END_REF] an detailed discussion of analysis results on several industrial examples is given. The largest benefit could be seen in an automotive control module implemented as hierarchal finite state machine composed of four sub-automata which comprises 348.530 lines of code. Without the FSM domain the analysis reports 45 alarms, needs 816 MB RAM and finishes in 24.5 minutes. With the FSM domain the analysis raises 4 alarms, finishes in 9 seconds, and consumes 424 MB RAM. The 41 alarms which are not reported any more have been confirmed as false alarms; the four remaining alarms can be considered justified. The reduction in analysis time and memory consumption is due to the fact that by applying the FSM domain the analyzer can eliminate many infeasible control flow paths that otherwise had to be taken into account.

In general, the required analysis time typically increases, and the observed increase depends on the number of combined states possible at a given program location during the run of the program. Also the memory needed for the analysis typically increases when we do an analysis with state partitioning. In the benchmarks under investigation in [START_REF] Giet | Towards zero alarms in sound static analysis of finite state machines[END_REF] the maximum observed increase in RAM usage is 40%.

Data and Control Flow Analysis

Safety standards such as DO-178C and ISO-26262 require to perform control and data flow analysis as a part of software unit or integration testing and in order to verify the software architectural design. Investigating control and data flow is also subject of the Data Safety guidance [START_REF]Data Safety (Version 2.0)[END_REF], and it is a prerequisite for analyzing confidentiality and integrity properties as a part of a secu-rity case. Technically, any semantics-based static analysis is able to provide information about data and control flow, since this is the basis of the actual program analysis. However, data and control flow analysis has many aspects, and for some of them, tailored analysis mechanisms are needed.

Global data and control flow analysis gives a summary of variable accesses and function invocations throughout program execution. It is the basis to determine the data and control coupling, as required by DO-178C.

In its standard data and control flow reports Astrée computes the number of read/write accesses for every global or static variable and lists the location of each access along with the function from which the access is made and the thread in which the function is executed. The control flow is described by listing all callers and callees for every C function along with the threads (and, if specified, the core) in which they can be run. Indirect variable accesses via pointers as well as function pointer call targets are fully taken into account. Filtering allows determining the control and data flow per software component. Astrée also provides a call graph visualization enhanced by data flow information, which can be interactively explored.

More sophisticated information can be provided by two dedicated analysis methods: taint analysis and program slicing. Taint analysis is a forward analysis and can answer questions about program parts affected by reading corrupted input values. Program slicing is a backward analysis which can answer questions about the program parts which might influence the value of a particular variable at a particular program point.

Taint Analysis

Astrée has been equipped with a generic abstract domain for taint analysis. It allows Astrée to perform normal code analysis, with its usual process-interleaving, interprocedural and memory layout precision, while carrying and computing taint information at the byte level. Any number of taint hues can be tracked by Astrée, and their combinations will be soundly abstracted.

Taint propagation can be formalized using a nonstandard semantics of programs, where an imaginary taint is associated to some input values. Considering a standard semantics using a successor relation between program states, and considering that a program state is a map from memory locations (variables, program counter, etc.) to values in V, the tainted semantics relates tainted states, which are maps from the same memory locations to V × {taint, notaint}, and such that if we project on V we get the same relation as with the standard semantics.

To define what happens to the taint part of the tainted value, one must define a taint policy. The taint policy specifies:

• Taint sources which are a subset of input values or variables such that in any state, the values associated with that input values or variables are always tainted.

• Taint propagation describes how the tainting gets propagated. Typical propagation is through assignment, but more complex propagation can take more control flow into account, and may not propagate the taint through all arithmetic or pointer operations.

• Taint cleaning is an alternative to taint propagation, describing all the operations that do not propagate the taint. In this case, all assignments not containing the taint cleaning will propagate the taint.

• Taint sinks is an optional set of memory locations. This has no semantical effect, except to specify conditions when an alarm should be emitted when verifying a program (an alarm must be emitted if a taint sink may become tainted for a given execution of the program).

Tainted input is specified through directives (__ASTREE_taint((var;hues))) attached to program locations. Such directives can precisely describe which variables, and which part of those variables, is to be tainted, with the given taint hues, each time this program location is reached.

Taint sink directives may be used to declare that some parts of some variables must be considered as taint sinks for a given set of taint hues. When a tainted value is assigned to a taint sink, then Astrée will emit a dedicated alarm, and remove the sinked hues, so that only the first occurrence has to be examined to fix potential issues with the security data flow.

The main intended use of taint analysis in Astrée is to expose potential vulnerabilities with respect to security policies or resilience mechanisms. Thanks to the intrinsic soundness of the approach, no tainting can be forgotten, and that without any bound on the number of iterations of loops, size of data or length of the call stack.

Detecting Spectre Vulnerabilities

Spectre/Meltdown attacks are transient instruction execution attacks, i.e., they exploit instructions which should not have an observable effect since they are speculatively executed [START_REF] Kocher | Spectre attacks: Exploiting speculative execution[END_REF] or have to be flushed because of an exception [START_REF] Lipp | Meltdown[END_REF]. They affect a wide range of target architectures. The Spectre v1, Spectre v1.1 and Split-Spectre attacks (Spectre-PHT) are based on speculative execution, in particular, on branch prediction on array bound index checks. Taint analysis is particularly well suited to help detecting these vulnerabilities.

The first condition of Spectre-PHT vulnerabilities is the ability to control a variable through user (or public) input. The data flow from the corresponding input locations can be approximated using tainting, so first tainting directives have to be introduced, using the directive ASTREE taint. Typically this just requires tainting the arguments of some specific input functions.

The second condition is that such data controlled by the attacker are compared to a bound, so that speculative execution can be exploited. The idea here is to use the facility for Astrée to deal with more than one taint hue, to distinguish between possibly controlled, and possibly controlled and tested to be smaller than a bound. Since it would be quite demanding to manually add tainting directives for that to the source code under analysis, we added inside Astrée an automatic detection of comparison with bounds, which automatically changes the taint from controlled to dangerous. Now the question is, how far in the code should variables stay dangerous? Speculative execution does not last forever, and in all known attacks so far, the memory access using dangerous variables must occur during speculative execution, which is one of the reasons why [START_REF] Wang | oo7: Low-overhead defense against spectre attacks via binary analysis[END_REF] introduced their speculative execution window. But we work on the source code level, and we aim at target architecture independence. One reasonable limit, though, is the length of the branches: when there is a test, there are two possible outcome, the branches, and when the control flow becomes the same whatever the outcome (the branches are merged) then the variable should not be considered dangerous anymore. The implementation challenge with that view is that tainting, by design, cannot be removed on joins. So, we came up with some non-standard use of the multi-hues tainting facilities offered by Astrée: we decided to taint public input with two hues (let us call them 1 and 2), and that flagging a memory location as dangerous consists in removing a hue (let us say it is hue 2). In that way, as long as the memory is tainted with only hue 1, it is considered dangerous, but as soon as we merge with a context where it is tainted with hue 1 and 2, it becomes merely controlled by the attacker again.

The third step is that the dangerous variable must be used to compute some memory address. Once again, we automatically discover in Astrée when a dangerous value is used to compute a memory location, and in that case, flag that address with a new taint hue. At each place where an address tainted with that hue is dereferenced, we emit a Spectre vulnerability alarm, and remove the tainting for that address, so that end-users can concentrate on the first occurrence, where they can, e.g., introduce fences that will anyway mitigate the vulnerability for all subsequent dereferences of the same address.

To illustrate the tainting algorithm we use the following example code shown in Figure 4: In that code, val is tainted with hues 1 and 2, to denote that it may be controlled by the attacker. The taint is propagated to argument x of the victim function, and when x is compared to the size of the array, the tainting is transformed into hue 1 (hue 2 is removed from the tainting of x). This means that x is considered dangerous after the test. Then when x is used to compute an offset of array1 before dereferencing, Astrée emits a Spectre vulnerability alarm.

A screen shot of a Spectre vulnerability alarm in Astrée is shown in Fig. 5. The taint hues derived for variables in the code are shown in the tool tips. This approach does not provide absolute safety from Spectre attacks. The first limitation is that tainting can only taint reachable code, and Spectre may be exploited on unreachable code (speculative execution may cause the execution of normally unreachable code). Note that Astrée displays unreachable code as parts of its normal output. If needed, the code can be made reachable to be covered by the analysis. Second, it targets a specific set of Spectre vulnerabilities, not all possible flavors of Spectre vulnerabilities. It embeds the Spectre detection into the runtime error analysis which is needed in safetycritical systems anyway, and reports vulnerabilities with The article [START_REF] Kästner | Detecting Spectre Vulnerabilities by Sound Static Analysis[END_REF] gives a detailed overview of Spectre attacks, Astrée's Spectre detection and its application to the PikeOS operating system. Astrée analyzes the whole code (400 000 LOC) in 2h30, using 17 GB of memory. During the analysis, Astrée does much more than warn about Spectre vulnerabilities, it also checks for compliance to coding rules, or warns about potential runtime errors. The precision is very high: Astrée only reports 68 locations with possible Spectre vulnerabilities, and manual inspection confirms that the false alarm rate is below 5%.

Further experiments were conducted on industrial avionics and automotive code. In the two cases described in the following we manually selected some global variables as taint sources since no information about actual user-controlled values was available to us. The first project is avionics software consisting of 2 million lines of preprocessed C code. It ran through in 2h43 (21 GB), compared to 2h36 without Spectre detection. The run with Spectre detection enabled found 113 possible vulnerabilities. The second project is an automotive application which consists of about 2.7 million lines of preprocessed C code. Without Spectre detection, it ran through in 1h42, and in 1h47 with Spectre detection enabled, and found 1271 vulnerabilities.

Program Slicing

The following definitions introduce the basic principles of static program slicing. Definition 1 (Slicing Criterion) Let P be a program. A slicing criterion in P is a tuple (s,V ) which consists of a statement s and a set of variables V from P Definition 2 (Slice) A slice S is a subprogram of P that exhibits the same behavior with respect to the slicing criterion (s,V ).

Computing minimal slices is an undecidable problem. However there are well-established algorithms for computing non-minimal, but still useful slices. A common approach is to compute a System Dependence Graph (SDG), which contains all data and control dependences of the program. Then a slice can be expressed as a reachability problem in this graph [START_REF] Horwitz | Interprocedural slicing using dependence graphs[END_REF]. The precision of the slice directly depends on the precision of the SDG. However, computing precise system dependency graphs is a non-trivial task since it requires deriving intricate program properties. These may include points-to information for variable and function pointers, code reachability, context information or possible variable values at certain program points. As an example, over-approximating the set of possible destinations of a pointer variable blows up the size of the system dependence graph as it may add false dependences to statements which contain variables that would otherwise not be included in the slice. This may cause a drastic transitive increase in the number of dependences and vertices.

Analysis-Enhanced Slicing

A first novel contribution of Astrée's program slicer is that it leverages the invariants computed by the main Astrée analysis. In the following, we denote this slicing method analysis-enhanced slicing. This slicer can produce sound and compact slices by exploiting pointsto and reachability information. Furthermore Astrée detects code which is guaranteed to be unreachable for any possible program execution. Ignoring such unreachable code fragments when constructing the system dependence graph further decreases its size. Hence, compared to slicing without leveraging Astrée invariants, a significant precision gain is achieved by reducing the amount of vertices and the amount of data-and control dependences in the system dependence graph. Another important advantage of analysis-enhanced slicing is its efficiency. While computing sound slices with standard static slicing requires lots of time and memory, those resources are significantly lower for analysis-enhanced slicing. This is due to the smaller size and smaller complexity of the computed system dependence graphs. This efficiency improvement makes it possible to compute slices for very large programs in feasible time.

A system dependence graph computed by our approach is a sound abstraction of the data-and control dependences of a computer program. This follows from the soundness of the Astrée core analysis. As a consequence, the resulting slices are also sound. The amount of precision gain depends on the precision of the exported invariants.

A detailed experimental survey of Astrée's analysisenhanced program slicer with programs from automotive and avionic industry is given in [START_REF] Kästner | Advanced Sound Static Analysis to Detect Safety-and Security-Relevant Programming Defects[END_REF]. It demonstrates that slicing can be applied to industry-size code with high precision and with feasible memory and compu-tation time requirements.

Alarm Slicing

A second novel contribution of Astrée's slicer is its ability to compute a slice for one specific analysis context. The main application for this is alarm slicing: the goal is to compute a slice for the root cause of an alarm. By helping developers to prove the alarm to be a false alarm, or to recognize that it represents a true defect, respectively, the manual effort of reviewing the findings of the analyzer can be significantly reduced.

Astrée exhibits potential safety or security defects in the form of alarm messages. These messages are context sensitive with respective to the sequence of function calls and control decisions that lead to the particular alarm. Fig. 6 displays an example of such a context.

[ call#main at astree.cfg:18.0-50. In order to compute precise slices for such alarm messages, the slicer has to take into account context information. The basic idea is simple: the critical situation for a division by zero alarm, which is reported for a given context, is precisely the context where the denominator becomes 0. Therefore we want to compute a partial slice for the variables used in the denominator, which only considers program paths leading to this particular context. Therefore, we augment the previously given definition of program slicing by call contexts.

Definition 3 (Call Context) We denote a call context a sequence of functions [ f 1 , f 2 , . . . , f n ] in P, such that for each i ∈ {1, . . . , n -1} it holds that f i calls f i+1 . Definition 4 (Context-Sensitive Slicing Criterion) A context-sensitive slicing criterion in P is a 3-tuple (s,V, [ f 1 , f 2 , . . . , f n ]) consisting of a statement s ∈ f n , s set of variables V and a call context [ f 1 , f 2 , . . . , f n ] of P. Definition 5 (Context-Sensitive Slice) Let (s,V, [ f 1 , f 2 , . . . , f n ]
) be a context-sensitive slicing criterion and S a slice of P with respect to (s,V ). A context-sensitive slice S c is a subprogram of S, which behaves the same in the call context [ f 1 , f 2 , . . . , f n ].

To compute context-sensitive slices we enhance the slicing algorithm given in [START_REF] Horwitz | Interprocedural slicing using dependence graphs[END_REF] with a description of call contexts (stacks). In each step of the reachability analysis we additionally check that the dependences under examination match the relevant stacks. Dependences which do not match are discarded. When following a dependency edge which represents a function call, the Figure 7: Alarm Slicing in Astrée topmost function is removed from the stack. This modification of the algorithm allows for context-sensitive slicing as defined above (considering exactly one call context), as well as context-insensitive slicing (considering all possible contexts). Thus it matches our definition of a context-sensitive slice which implies that for one program point a context-insensitive slice is identical with the union over all context-sensitive slices.

In our implementation, to ensure that only feasible call contexts are taken into account, and that calls-byreference can be dealt with in a sound way, the slicer imports the intermediate internal program representation of Astrée. I then derives all possible call contexts from this representation. The soundness of the call contexts is directly inferred by the soundness of the Astrée analysis, in the same way as the information which is reused in analysis-enhanced slicing. The notion of contextsensitive slicing can be naturally extended to cover multiple call contexts.

In contrast to context-insensitive slices, contextsensitive slices do not capture all possible behaviors of the original program which influence the slicing criterion. Instead, the behavior described by the slice is restricted to execution paths which are in accordance with the set of considered call contexts. Context-sensitive slices tend to be significantly smaller than contextones. The slicing modes presented in this section are relevant for demonstrating safety and security properties. Sound slices can be computed by contextinsensitive analysis-enhanced slicing. With these slices it is possible to show that certain parts of the code or certain input variables might influence or cannot influence a program section of interest. They yield a global overview of these properties for the entire program.

In contrast to that, context-sensitive analysisenhanced slicing, which only considers a subset of possible contexts, is more suitable for investigating the influence of a certain code section, e.g. a function, or a module, on the program location of the slicing criterion. Hence it is perfectly suited as a basis for automatic alarm slicing.

Automatic Slicing of Astrée Alarm Messages

The investigation of alarm messages which describe safety-or security issues of a computer program is an important task. In most cases defects only materialize in certain executions and thus dependent on call contexts and control decisions. Consequently, only these executions, and their respective contexts, are interesting for the alarm investigation. To simplify manual inspection each Astrée alarm is emitted in conjunction with problematic contexts. Unfortunately, even when utilizing the context information, alarm investigation is still a tedious and time consuming task. One main reason for this is the size of the code. Further, even with the additional information it is hard to identify which parts of the code are actually relevant for the issue under analysis.

Context-sensitive analysis-enhanced slicing is a natural approach to construct a more efficient workflow for alarm investigation. It can be configured to take into account the function call stack of the alarm context. On top of that, some of the other alarm context elements, in particular control decisions may be implicitly exploited with the imported analysis information, as described in Sec. 4.3. Hence, from the context menu of an alarm in the Astrée graphical user interface the computation of a slice for the alarm can be automatically triggered. In Fig. 7 this is displayed for the alarm and context of the example in Fig. 6. The Astrée program slicer then transforms the given context into a call context C by discarding all context entries that do not constitute function calls. Further, it determines the relevant set of program variables V that are part of the statement s for which the alarm is emitted. These steps yield the context-sensitive slicing criterion (s,V,C). By construction the resulting slice will behave the same as the original program for the examined context. Investigating that behavior is much more efficient, as the source code size is smaller and its content needs not to be filtered for relevance.

Conclusion

Sound static program analysis can be applied to demonstrate the absence of safety-relevant code defects, and of cybersecurity vulnerabilities. To make the application of such analyzers economically feasible, the false alarm rate must be low. Analyzing finite state machines at the C code level was a long-standing problem for static analyzers that typically lead to high false alarm rates. We illustrate a novel abstract domain which allows a highly precise analysis of finite state machines implemented in C programs. To support cybersecurity analyses, it is additionally necessary to support advanced data and control flow analyses, which allow to track the effect of value corruption in a forward and backward manner. We have developed a generic and user-parameterizable abstract domain for taint analysis and applied it to detect Spectre V1, V1.1 and SplitSpectre vulnerabilities. This is complemented by Astrée's novel program slicer, which supports precise backwards analysis by analysisenhanced slicing. It can also be applied for automatic alarm slicing, making it easier for developers to determine whether a given alarm is justified. Experimental results on real-life software confirm both the precision and the efficiency of our approach.

Fig 1 .

 1 It implements the state machine described in Fig 2 whose state is represented by variable state.

Figure 1 :

 1 Figure 1: Example C implementation of Fig. 2

Figure 3 :

 3 Figure 3: Analysis result with novel FSM domain

Figure 4 :

 4 Figure 4: Code excerpt with taint coloring.

Figure 5 :

 5 Figure 5: Astrée GUI showing Spectre vulnerability alarm

Figure 6 :

 6 Figure 6: Context-sensitive alarm message of Astrée.

Acknowledgment

This work was funded within the project PROFORMA by the German Federal Ministry for Education and Research with the funding ID 01IS17083A-C. The responsibility for the content remains with the authors.