Towards an Integrated Vehicle Management System in DriveOS

Modern automotive systems feature dozens of electronic control units (ECUs) for chassis, body and powertrain functions. These systems are costly and inflexible to upgrade, requiring ever increasing numbers of ECUs to support new features such as advanced driver assistance (ADAS), autonomous technologies, and infotainment. To counter these challenges, we propose DriveOS, a safe, secure, extensible, and timing-predictable system for modern vehicle management in a centralized platform. DriveOS is based on a separation kernel, where timing and safety-critical ECU functions are implemented in a real-time OS (RTOS) alongside non-critical software in Linux or Android. The system enforces the separation, or partitioning, of both software and hardware among different OSes. DriveOS runs on a relatively low-cost embedded PC-class platform, supporting multiple cores and hardware virtualization capabilities. Instrument cluster, in-vehicle infotainment and advanced driver assistance system services are implemented in a Yocto Linux guest, which communicates with critical real-time services via secure shared memory. The RTOS manages a real-time controller area network (CAN) interface that is inaccessible to Linux services except via well-defined and legitimate communication channels. In this work, we integrate three Qt-based services written for Yocto Linux, running in parallel with a real-time longitudinal controller task and multiple CAN bus concentrators, for vehicular sensor data processing and actuation. We demonstrate the benefits and performance of DriveOS with a hardware-in-the-loop CARLA simulation using a real car dataset.

A Survey on Formal Verification of Separation Kernels

Introduction: In developing safety and security critical systems, separation kernel acts as a primary foundation, which provides spatial as well as temporal separation. Separation kernel offers highly assured partitions to the applications hosted on the fundamentally critical systems and can also control the flow of information between them. The industries, as well as academia, have developed several separation kernels that have been broadly applied in critical systems like military/defense secured applications, avionics/aerospace intelligent systems, healthcare units that deal with human lives and in many more areas. The increasing popularity of separation kernels demands the formal verification that assures the correctness of the functionalities in it. Further, formal verification of separation kernels has become mandatory by the security/safety certification authorities. Conclusion: This paper first presents the concept of separation kernel, and then it discusses the functionalities, design, and properties of it. The classification and analysis of the formal languages are being presented in this paper that has been used for writing the specifications of separation kernel and verifying it. The paper is an attempt towards the classification of formal languages being used for the verification of several separation kernels.

Formal Specification and Verification of Data Separation for Muen Separation Kernel

Introduction: Development of integrated mixed-criticality systems is becoming increasingly popular for application-specific systems, which needs separation mechanism for available onboard resources and the processors equipped with hardware virtualization. Hardware virtualization allow the partitions to physical resources, which include processor cores, memory, and I/O devices, among guest virtual machines (VMs). For building mixed criticality computing environment, traditional virtual machine systems are inappropriate because they use hypervisors to schedule separate VMs on physical processor cores. In this article, we discuss the design of an environment for mixed-criticality systems: The Muen an x86/64 separation kernel for high assurance. The Muen Separation Kernel is an Open Source microkernel which has no runtime errors at the source code level. The Muen separation kernel has been designed precisely to encounter the challenging requirements of high-assurance systems built on the Intel x86/64 platform. Muen is under active development, and none of the kernel properties of it has been verified yet. In this paper, we present a novel work of verifying one of the kernel properties formally. Method: The CTL used in NuSMV is a first-order modal along with data-depended processes and regular formulas. CTL is a branching-time logic, meaning that its model of time is a tree-like structure in which the future is not determined; there are different paths in the future, any one of which might be an actual path that is realized . This section shows the verification of all the requirements mentioned in section 3. In NuSMV tool the command used for verification of the formulas written in CTL is checkctlspec -p ”CTL-expression”. The nearest quantifier binds each occurrence of a variable in the scope of the bound variable, which has the same name and the same number of arguments. Result: Formal methods have been applied to various projects for specification and verification purpose. Some of them are the SCOMP , SeaView , LOCK,and Multinet Gateway projects. The TLS was written formally. Several mappings were done between the TLS and the SCOMP code: Informal English language to TLS, TLS to actual code , and TLS to pseudo-code. The authors present an ACL2 model for a generic separation kernel also known as GWV approach. Conclusion: We consider the formal verification of data separation property which is one of the crucial modules to achieve the separation functionality. The verification of the data separation manager is carried out on the design level using the NuSMV tool. Furthermore, we present the complete model of the data separation unit along with its code written in the NuSMV modelling language. Finally, we have converted the non-functional requirements into the formal logic, which then has verified the model formally.

Security Requirements Engineering in Safety-Critical Railway Signalling Networks

Securing a safety-critical system is a challenging task, because safety requirements have to be considered alongside security controls. We report on our experience to develop a security architecture for railway signalling systems starting from the bare safety-critical system that requires protection. We use a threat-based approach to determine security risk acceptance criteria and derive security requirements. We discuss the executed process and make suggestions for improvements. Based on the security requirements, we develop a security architecture. The architecture is based on a hardware platform that provides the resources required for safety as well as security applications and is able to run these applications of mixed-criticality (safety-critical applications and other applications run on the same device). To achieve this, we apply the MILS approach, a separation-based high-assurance security architecture to simplify the safety case and security case of our approach. We describe the assurance requirements of the separation kernel subcomponent, which represents the key component of the MILS architecture. We further discuss the security measures of our architecture that are included to protect the safety-critical application from cyberattacks.

Software Separation in Measuring Instruments through Security Concepts and Separation Kernels

<p class="Abstract">In the age of the Internet of Things and Industry 4.0, more and more embedded systems are connected through open networks, which also concerns measuring instruments under legal control (e.g. smart meters). Therefore, cyber-security for measuring instruments is becoming increasingly important. In this paper, possibilities to design secure measuring software running on general-purpose operating systems are analyzed according to legal requirements set up by European Directives, e.g., the Measuring Instruments Directive (2014/32/EU), which define the mandatory security level. Technical interpretations for the security concepts described in this paper are derived from these legal requirements with the aim to provide manufacturers the architectural guidance to construct systems which easily pass a conformity assessment at a Notified Body. In this paper security concepts, i.e., SELinux, AppArmor and Mandatory Integrity Control (MIC) are being described, which are based on Mandatory Access Control (MAC) strategies. Additionally, high-security methodologies and concepts, e.g., MILS and security kernels, are highlighted. In the examples given, software separation, which enhances overall security, is achieved by using SELinux mechanisms in the modules (virtual machines) atop a separation kernel.</p>