Search

Formal method tools are used in the initial stages of the software development cycle and have advanced to deal with the design difficulties related to ensuring strong cybersecurity and reliability in high-assurance systems. Operating system kernels are the security keystone of most computer systems. Their continuous advances require formal verification that guarantees the accuracy of their functionalities. As the world’s first microkernel to be proven mathematically secure and functionally correct, seL4 has been adopted for use in a range of critical systems, including defense, aerospace, and financial services applications. In spite of the great effort of the seL4 team to present a comprehensive formal verification of the kernels, there are some security aspects of verification that suffer from a limited scope. From an outsider’s perspective, this paper aims to evaluate if seL4 formal verification is adequate to address security requirements and surveys the recent state of the art for seL4 microkernels.

Virtualization plays an essential role in providing security to computational systems by isolating execution environments. Many software solutions, called hypervisors, have been proposed to provide virtualization capabilities. However, only a few were designed for being deployed at the edge of the network in devices with fewer computation resources when compared with servers in the Cloud. Among the few lightweight software that can play the hypervisor role, seL4 stands out by providing a small Trusted Computing Base and formally verified components, enhancing its security. Despite today being more than a decade with seL4 microkernel technology, its existing userland and tools are still scarce and not very mature. Over the last few years, the main effort has been to increase the maturity of the kernel itself, and not the tools and applications that can be hosted on top. Therefore, it currently lacks proper support for a full-featured userland Virtual Machine Monitor, and the existing one is quite fragmented. This article discusses the potential directions to a standard VMM by presenting our view of design principles and the feature set needed. This article does not intend to define a standard VMM, we intend to instigate this discussion through the seL4 community. [ABSTRACT FROM AUTHOR]

IPC (Inter-Process Communication) is a widely used operating system (OS) technique that allows one process to invoke the services of other processes. The IPC participants may share the same OS (internal IPC) or use a separate OS (external IPC). Even though a long line of researches has optimized the performance of IPC, it is still a major factor of the run-time overhead of IPC-intensive applications. Furthermore, there is no one-size-fits-all solution for both internal and external IPC. This paper presents SkyBridge, a general communication technique designed and optimized for both types of IPC. SkyBridge requires no involvement of the privileged software (the kernel or the hypervisor) and enables a process to directly switch to the virtual address space of the target process, regardless of whether they are running on the same OS or not. We have implemented SkyBridge on two microkernels (seL4 and Google Zircon) as well as an open-source serverless hypervisor (Firecracker). The evaluation results show that SkyBridge improves the latency of internal IPC and external IPC by up to 19.6x and 1265.7x, respectively. [ABSTRACT FROM AUTHOR]

IPC (inter-process communication) is a critical mechanism for modern OSes, including not only microkernels such as seL4, QNX, and Fuchsia where system functionalities are deployed in user-level processes, but also monolithic kernels like Android where apps frequently communicate with plenty of user-level services. However, existing IPC mechanisms still suffer from long latency. Previous software optimizations of IPC usually cannot bypass the kernel that is responsible for domain switching and message copying/remapping across different address spaces; hardware solutions such as tagged memory or capability replace page tables for isolation, but usually require non-trivial modification to existing software stack to adapt to the new hardware primitives. In this article, we propose a hardware-assisted OS primitive, XPC (Cross Process Call), for effi- cient and secure synchronous IPC. XPC enables direct switch between IPC caller and callee without trapping into the kernel and supports secure message passing across multiple processes without copying. We have implemented a prototype of XPC based on the ARM AArch64 with Gem5 simulator and RISC-V architecture with FPGA boards. The evaluation shows that XPC can reduce IPC call latency from 664 to 21 cycles, 14x-123x improvement on Android Binder (ARM), and improve the performance of real-world applications on microkernels by 1.6x on Sqlite3. [ABSTRACT FROM AUTHOR]

Virtualization techniques continue to evolve at rapid speed and have now come to find its application in embedded and mobile computing devices. Virtualization improves the utilization of system resources effectively and also enhances security by providing isolated environments to run untrusted applications. There are various approaches to virtualization of embedded systems, from among them, we have chosen microkernel-based virtualization for our analysis due to its low memory requirements and advantages in terms of security. The microkernel selected for our work is the L4/Fiasco microkernel. Most of the modern CPUs consist of Performance Monitoring Unit (PMUs), which have a set of hardware counters that can be configured to monitor events. These hardware performance counters in the PMU block is not accessible from a microkernel-based virtualization environment. Access to PMU from a virtual environment would facilitate profiling with better accuracy and reduced overheads. To get this realized we propose a method to access the hardware performance counters from a microkernel-based virtualization environment. We have used this implementation to analyze the performance of applications in a microkernel-based virtual environment and to compare its performance in a non-virtual environment.

We approach the problem of implementing mixed-datatype support within the general matrix multiplication (gemm) operation of the BLAS-like Library Instantiation Software framework, whereby each matrix operand A, B, and C may be stored as single- or double-precision real or complex values. Another factor of complexity, whereby the matrix product and accumulation are allowed to take place in a precision different from the storage precisions of either A or B, is also discussed. We first break the problem into orthogonal dimensions, considering the mixing of domains separately from mixing precisions. Support for all combinations of matrix operands stored in either the real or complex domain is mapped out by enumerating the cases and describing an implementation approach for each. Supporting all combinations of storage and computation precisions is handled by typecasting the matrices at key stages of the computation—during packing and/or accumulation, as needed. Several optional optimizations are also documented. Performance results gathered on a 56-core Marvell ThunderX2 and a 52-core Intel Xeon Platinum demonstrate that high performance is mostly preserved, with modest slowdowns incurred from unavoidable typecast instructions. The mixed-datatype implementation confirms that combinatorial intractability is avoided, with the framework relying on only two assembly microkernels to implement 128 datatype combinations. [ABSTRACT FROM AUTHOR]

Progress in the production technology of microprocessors significantly increased reliability and performance of the computer systems hardware. It cannot be told about the corresponding characteristics of the software and its basis – the operating system (OS). Some achievements of program engineering are more modest in this field. Both directions of OS improvement (increasing of productivity and reliability) are connected with the development of effective structures of these systems. OS functional complexity leads to the multiplicity of the structure, which is further enhanced by the specialization of the operating system depending on scope of computer system (complex scientific calculations, real time, information retrieval systems, systems of the automated and automatic control, etc.) The functional complexity of the OS leads to the complexity of its architecture, which is further enhanced by the specialization of the operating system, depending on the computer system application area (complex scientific calculations, real-time, information retrieval systems, automated and automatic control systems, etc.). That fact led to variety of modern OS. It is possible to estimate reliability of different OS structures only as results of long-term field experiment or simulation modeling. However it is most often unacceptable because of time and funds expenses for carrying out such research. This survey attempts to evaluate the reliability of two main OS architectures: large multi-layered modular core and a multiserver (client-server) system. Represented by continuous Markov chains which are explored in the stationary mode on the basis of transition from systems of the differential equations of Kolmogorov to system of the linear algebraic equations, models of these systems are developed.

Almost all efforts to optimize high-performance matrix-matrix multiplication have been focused on the case where matrices contain real elements. The community's collective assumption appears to have been that the techniques and methods developed for the real domain carry over directly to the complex domain. As a result, implementors have mostly overlooked a class of methods that compute complex matrix multiplication using only real matrix products. This is the second in a series of articles that investigate these so-called induced methods. In the previous article, we found that algorithms based on the more generally applicable of the two methods--the 4M method--lead to implementations that, for various reasons, often underperform their real domain counterparts. To overcome these limitations, we derive a superior 1M method for expressing complex matrix multiplication, one which addresses virtually all of the shortcomings inherent in 4M. Implementations are developed within the BLIS framework, and testing on microarchitectures by three vendors confirms that the 1M method yields performance that is generally competitive with solutions based on conventionally implemented complex kernels, sometimes even outperforming vendor libraries. [ABSTRACT FROM AUTHOR]

This article introduces the Spunky microkernel project recently presented at the 10th Ada Developer Room at FOSDEM 2020 [3]. The Spunky project aims for providing a kernel for the Genode OS framework written in Ada that may subsequently be transferred to SPARK to enable automated proving of fundamental kernel aspects. [ABSTRACT FROM AUTHOR]

Since most of the system services of the microkernel run in user space, the user process needs to request these services through the kernel's communication mechanism. Therefore, the frequency and amount of IPC (inter-process communication) in the microkernel is much higher than those in the monolithic kernel, causing the performance of the microkernel to be poor. In this paper, two exchange-based IPC algorithms are proposed to optimize the communication algorithm based on the replication mode, which is commonly used in the microkernel. One is based on the exchange of physical pages of MMU (memory management unit), and the other is based on the exchange of segment base addresses of MMU. These two exchange algorithms can achieve efficient transmission while keeping the independent address space to ensure the correctness and security of the transmitted data, greatly improving the efficiency of communication in the microkernel. [ABSTRACT FROM AUTHOR]

This paper proposes an operating system architecture for unmanned aerial vehicle (UAV), which is secure against root exploit, resilient to connection loss resulting in the control loss, and able to utilize common applications used in Linux. The Linux-based UAVs are exposed to root exploit. On the other hand, the microkernel-based UAVs are not able to use the common applications utilized in Linux, even though which is secure against root exploit. For this reason, the proposed architecture uses a virtualized microkernel on the Linux operating system to isolate communication roles and prevent root exploit. As a result, the suggested Operating system is secure against root exploit and is able to utilize the common applications at the same time. [ABSTRACT FROM AUTHOR]

Industrial security situation is increasingly serious; operating system security is an important basis for the entire information security. In the industrial security systems, industrial control terminal at the operating system level, lack of a comprehensive security system, unable to adapt to the security situation under the new situation. To effectively solve the above problems, self-controlled safety technology operating system research was critical needed. In the industrial operating system security, operating system security kernel integrity is an important guarantee. Based on NARIsecOS, this paper proposed kernel integrity protection program, and part of the work carried out formal verification. Secure operating system can bring the following goodness: 1) Trojan virus immunity, and against hacker attacks; 2) Greatly reduce the zero-day vulnerabilities; 3) Decentralized management, effectively circumvent a dominant right; 4) Enhance industrial endpoint security protection. [ABSTRACT FROM AUTHOR]

The current development trend of Internet of Things (IoT) aims for a tighter integration of mobile and stationary devices via various networks. This includes communication of vehicles to roadside infrastructure (V2I), as well as intelligent sensors / actors in Logistics and smart home environments.

Embedded systems show the tendency of becoming more and more connected. This fact combined with the trend towards the Internet of Things, from which measuring instruments are not immune (e.g., smart meters), lets one assume that security in measuring instruments will inevitably play an important role soon. Additionally, measuring instruments have adopted general-purpose operating systems to offer the user a broader functionality that is not necessarily restricted towards measurement alone. In this paper, a flexible software system architecture is presented that addresses these challenges within the framework of essential requirements laid down in the Measuring Instruments Directive of the European Union. This system architecture tries to eliminate the risks general-purpose operating systems have by wrapping them, together with dedicated applications, in secure sandboxes, while supervising the communication between the essential parts and the outside world.

Trusted Execution Environment is an execution environment that resides in connected devices and ensures that sensitive data are stored, processed, and protected isolated from general-purpose OS such as Android. The TrustZone TEE solution can achieve a medium protection level with comparatively low cost, so it is widely used. However, related researches show that the TrustZone TEE solution has security defects; for example, hardware isolation provided by TrustZone is insufficient. In this paper, we propose a security enhancement scheme based on TEE. According to the existing problems in the TrustZone TEE scheme, a corresponding protection mechanism is established to fully enhance the reliability of connected devices. In our scheme, TEE is used alongside other security technology such as secure elements and microkernel and kernel real-time protection to provide multi-layered defense mechanisms. In our scheme, we introduce a security element as the root of trust (ROT) of connected devices. The secure element is used to store sensitive data such as the first-stage bootloader, various secret keys, and the certificate of the second-stage bootloader. The secure element is also used to execute sensitive operations such as encryption and decryption. [ABSTRACT FROM AUTHOR]

Virtualization has been deployed as a key enabling technology for coping with the ever growing complexity and heterogeneity of modern computing systems. However, on its own, classical virtualization is a poor match for modern endpoint embedded system requirements such as safety, security and real-time, which are our main target. Microkernel-based approaches to virtualization have been shown to bridge the gap between traditional and embedded virtualization. This notwithstanding, existent microkernel-based solutions follow a highly para-virtualized approach, which inherently requires a significant software engineering effort to adapt guest operating systems (OSes) to run as userland components. In this paper, we present mRTZVisor as a new TrustZone-assisted hypervisor that distinguishes itself from state-of-the-art TrustZone solutions by implementing a microkernel-like architecture while following an object-oriented approach. Contrarily to existing microkernel-based solutions, mRTZVisor is able to run nearly unmodified guest OSes, while, contrarily to existing TrustZone-assisted solutions, it provides a high degree of functionality and configurability, placing strong emphasis on the real-time support. Our hypervisor was deployed and evaluated on a Xilinx Zynq-based platform. Experiments demonstrate that the hypervisor presents a small trusted computing base size (approximately 60KB), and a performance overhead of less than 2% for a 10 ms guest-switching rate. [ABSTRACT FROM AUTHOR]

This paper presents a microkernel architecture for constraint programming organized around a small number of core functionalities and minimal interfaces. The architecture contrasts with the monolithic nature of many implementations. With this design, variables, domains and constraints all remain external to the microkernel which isolates the propagation logic and event protocols from the modeling constructions. The Objective-CP search blends the control primitives of the host language with search combinators in a completely transparent and fully compositional way, delivering a natural search procedure in which one can use native constructions and tools such as debuggers. Empirical results indicate that the software engineering benefits are not incompatible with runtime efficiency. [ABSTRACT FROM AUTHOR]

In this paper a software model called Resource Loading Manager (RLM) for Location Based Services (LBS) is designed using Free and Open Source Software (FOSS). Geographical Information System (GIS) always play an integral role in information systems, but it comes with technology problem, such as low efficiency ,less flexible, no redundancy of existing GIS application configuration which have high entry cost. The aim of this paper is to presents a lightweight, efficient and scalable microkernel plug-in geospatial information application system and its implementation method for GIS in microkernel design and practice. Through the RLM efficient allocation of geographic information resources and security management could be achieved. Using existing cloud computing technology, GIS of spatial public service will impact the ordinary way of life, bring enormous business opportunities. [ABSTRACT FROM AUTHOR]

Verified microkernels such as seL4 provide trustworthy foundations for safety- and security-critical systems. However, their full potential remains unrealized due, in part, to the lack of application development environments that help engineers integrate the microkernel's configuration and hosting of application code with modeling, analysis, and verification tools that address broader aspects of the development lifecycle. This paper presents a model-driven tool chain for the seL4 microkernel based on the open source High Assurance Modeling and Rapid engineering (HAMR) code generation framework for the Architecture and Analysis Definition Language (AADL). We describe how the semantics of AADL communication and threading can be realized in terms of the access primitives and strong spatial and temporal partitioning mechanisms provided by seL4. For AADL users, seL4 provides a high-assurance platform with formally verified enforcement of component boundaries and communication pathways. For seL4 users, AADL provides high-level abstractions for developing seL4 applications, along with an ecosystem of system engineering and analysis tools. We illustrate the framework by applying a model-based development environment for increasing resiliency against cyber attacks to an unmanned aircraft flight control system. [ABSTRACT FROM AUTHOR]

Microkernel-based operating systems provide high level of protection due to the strong isolation of components, small size of Trusted Computing Base and execution of drivers in user space. At the same time, such systems are vulnerable to a stack overflow attacks, because these attacks exploit the hardware features of the platform, such as shared memory space for data and code. Modern architectures, such as AMD64 and ARM, provide opportunities to counteract attacks at the hardware level by disallowing memory allocation for storing executable stack and heap, but this protection mechanism requires additional support from the operating system. This paper presents memory management, program execution model and IPC mechanism of microkernel Fiasco.OC and environment L4Re from nonexecution memory support point of view.