In the previous article, I introduced single-chip systems and operating systems based on single-chip kernels. In this article, I will continue to introduce the security analysis of operating systems based on microkernels.
Android Operating System
On August 22, 2017, Google officially released the final version of Android 8.0, officially named: Android Oreo.
On December 5, 2017, Google officially released the final version of Android 8.1, which is currently the latest version of the Android operating system.
According to developers, versions after Android 8.0 include a large number of new information security mechanisms. The key security features in this operating system are designed to mitigate vulnerabilities and reduce the attack surface to the greatest extent, including the use of the principle of least privilege, and significant changes in API design and architecture. The specifics are as follows:
1. Intelligent protection for authorized applications;
2. Advanced validation during application and operating system updates to prevent common types of attacks, including the implementation of database rollback mechanisms;
3. Built-in support for HSM (Hardware Security Module);
4. The application sandbox of seccomp filters (which restricts the ability of applications to make system calls) and the WebView component are isolated. Android’s seccomp filters block certain system calls, such as swapon/swapoff (which have been involved in some security attacks) and critical control system calls (which do not affect applications);
5. Support for a set of encryption profiles (different profiles use different key sets);
6. Built-in support for two-factor authentication using physical keys;
7. Adoption of complex application paths, so applications can no longer be found in their original static locations. Instead, applications are installed in new locations each time and must make special calls to the system to access the applications;
8. Stopped supporting outdated and vulnerable protocols and algorithms, such as SSL v3.0;
Undoubtedly, these are necessary and useful measures that significantly increase the difficulty for attackers to exploit vulnerabilities and gain root access.
However, as we all know, Android is based on the Linux kernel, so we should not forget the vulnerabilities of the Linux system itself. New vulnerabilities are continuously discovered in Android, a significant portion of which can execute arbitrary code.
Microkernel Operating Systems
In summary, a possible solution is to use a microkernel system architecture. A microkernel is a streamlined version of the kernel that provides core operating system functions, designed to increase portability in a small memory space and provide a modular design, allowing users to install different interfaces such as DOS, Workplace OS, Workplace UNIX, etc. New operating systems from IBM, Microsoft, the Open Software Foundation (OSF), and the UNIX System Laboratories (USL) have all adopted the advantages of this research achievement. In short, a microkernel only provides the basic functionalities of process management and the minimum set of hardware abstractions. Most of the work is done with the help of dedicated user processes that do not run in the kernel’s address space. This significantly reduces the attack surface of kernel services, and the operating system’s kernel can be rigorously verified using formal verification methods (thanks to the very small number of code libraries). For more information on verification and how it differs from general verification, please refer to the article written by Ekaterina Rudina.
From the perspective of information security, the security advantages of microkernel system architecture have already been demonstrated, such as the separation kernel method and the use of MILS system architecture. Currently, there is a significant emergence of different types of microkernel operating systems in the market, such as QNX, INTEGRITY RTOS, Genode, L4-based microkernel operating systems, and other derivative versions.
QNX: The QNX operating system is a distributed real-time operating system developed by QSSL (QNX Software System Ltd.) in Canada. This operating system can run in hardware environments based on Intel X86, Pentium, etc., as well as on hardware environments based on PowerPC, MIPS, etc. The QNX operating system complies with basic POSIX standards and real-time standards, making its applications easy to port.
INTEGRITY RTOS: INTEGRITY is a secure, royalty-free real-time operating system developed by Green Hills Software. Because it does not have to consider compatibility issues that existed since the 1980s, INTEGRITY applies the latest RTOS technologies from the design stage and includes unprecedented reliability, availability, and serviceability needed for telecommunications, defense, networking, and medical device industry applications. INTEGRITY RTOS is the first operating system certified according to the “POSIX: IEEE and Open Group Certification” program and the latest IEEE 1003.1-2003 system interface product standards. INTEGRITY uses hardware-based memory protection mechanisms to isolate and protect kernel and user tasks, preventing misoperations and malicious attacks. The object-oriented design allows strict access control and verification of data, communication, independent components, and systems. It strictly follows verifiable resource requests to allow embedded system designers to ensure resource availability. The F-16 and F-22 fighter jets use the Integrity real-time operating system, and NASA’s Space Technology 5 (ST5) mission also used the Integrity real-time operating system.
Here, I would like to briefly introduce the L4 microkernel, which is the result of the evolution of microkernel operating systems to date. Today, L4 is essentially the practical standard in the development of microkernel operating systems.
L4 Microkernel
In recent years, the L4 microkernel has gained increasing attention. The initial development of the L4 microkernel was merely to prove that creating a microkernel suitable for practical general-purpose operating systems is feasible. This attempt can be considered quite successful, and there is now a whole set of research and commercial projects utilizing L4. Currently, the L4 microkernel has been ported to a large number of hardware platforms. It is important to note that L4-based solutions support operations in hard real-time mode. Hard real-time systems refer to operating systems that can complete real-time tasks within specified deadlines (even under the worst processing loads).
Among the currently supported microkernel implementations, there are the following versions:
1. seL4: The first formally verified microkernel, which is still under active development;
2. Codezero: A commercial application version of the K4 microkernel. The source code of the kernel is available under the GPLv3 license, while the source code of additional modules and libraries is closed and requires commercial licensing for operation;
3. OC: A version developed by Dresden University of Technology and developed under the GPLv2 license, which requires commercial licensing to use;
For the operating systems listed above, you can use different virtualization solutions. Other L4-based virtualization solutions worth mentioning include OKL4, NOVA, and PikeOS operating systems.
The L4 series microkernels have also been used in the following operating systems:
1. Genode;
2. TUD:OS: An operating system developed by Dresden University of Technology based on L4Re, which is a framework for L4-based solutions.
3. CAamkES: A framework based on the L4 microkernel developed by the Trustworthy Systems Research Group of Data61.
4. L4Linux: A system based on the L4 series kernel that has ported the Linux operating system. In this implementation of L4, Linux serves as a user-mode service that runs alongside other L4 applications (including real-time components). The current version of the Linux kernel has reached 4.14, supporting x86 and ARM hardware platforms.
From a security perspective, the seL4 kernel is the most important version in the L4 series.
The microkernel seL4 implements the object-capability model and has undergone formal verification, which means the properties of the operating system can be guaranteed under specific concepts and assumptions, enhancing the protection mechanisms of the overall solution. However, if the input assumptions are incorrect, problems may arise. For example, during the verification process of seL4, a significant flaw in the formal model is that it excludes the possibility of several processes executing simultaneously; you can envision a situation where a single-processor system experiences blocking interrupts.
The object-capability model provides detailed control over system behavior, but it cannot be used to describe all security properties. There are many other security models whose properties cannot be expressed based on the object-capability model. For example, security properties may depend on system states, considering time relationships, etc. To describe these properties, additional mechanisms must be added to the security solution, and in such cases, the advantages of seL4 may be lost.
KasperskyOS uses many ideas from seL4, but it also allows the use of the Kaspersky Security System (KSS) as part of the KasperskyOS architecture to describe any security properties.
Hybrid Operating Systems
Hybrid kernels combine the attributes of monolithic and microkernel system architectures. The architecture of operating systems based on hybrid kernels is essentially an improved microkernel that allows operating system modules to execute in kernel space to accelerate operations.
Operating systems using hybrid kernels have already emerged in the market, with the main idea of developing them being to attempt to utilize the advantages of microkernel architecture while retaining as much well-tested monolithic code as possible. However, even in hybrid operating systems, information security issues remain unresolved, as the attack surface is still large.
Why Current Operating Systems Cannot Meet the Requirements of Embedded Systems
Many traditional operating systems were initially developed without considering security, and adding security features later brings many problems, such as the original functional mechanisms stopping to work and compatibility issues arising. However, for various reasons, developers cannot completely redesign these architectures, so they can only patch them and add some security-related attributes. There are many examples of such solutions, including QNX, Linux, and FreeBSD.
Only those operating systems that consider information security during the system’s development can ensure genuine security mechanisms without affecting various operational functions. Operating systems designed with security in mind include seL4, INTEGRITY RTOS, MUEN RTOS, KasperskyOS, etc.
KasperskyOS Introduction
KasperskyOS is a system built from scratch by Kaspersky Lab, officially released in February 2017. It is not based on any existing operating system, such as Linux, and the development process took 14 years. According to Kaspersky Lab, KasperskyOS is not designed for home PCs, but rather to protect industrial systems and embedded devices (IoT) from network attacks executed by third parties or malicious code.
The emergence of KasperskyOS is due to the fact that some popular operating systems did not consider security too much during their design, especially for emerging IoT. Therefore, rather than patching existing systems, it is simpler and safer to create a new system from scratch.
According to Kaspersky Lab’s estimates, KasperskyOS is nearly impossible to hack because the built-in security system can control application operations and system modules. For an attacker to crack the digital signature of a device running KasperskyOS, a quantum computer would be required.
KasperskyOS uses a microkernel architecture, where the microkernel system tools divide the system into security domains or “entities” in KasperskyOS terminology. All communication between security domains (inter-process communication, IPC) is executed and controlled by the microkernel, and no communication is allowed to bypass the microkernel.
All communication is classified, and the interfaces of entities are described using IDL (Interface Definition Language), and only this interface can be used for IPC, which is a significant difference between KasperskyOS and most other operating systems.
The microkernel of KasperskyOS runs in conjunction with the Kaspersky Security System (KSS), which is a subsystem for computing security judgments. For each IPC, the KasperskyOS microkernel requests a security judgment from KSS, which serves as the basis for allowing or blocking that specific IPC. For security judgment calculations, not only the facts and types of communication must be considered, but also the system’s topology, the environment in which communication occurs, and the allocation policies described within a formal security framework.
KSS supports a wide range of formal security models, such as Domain Type Enforcement (DTE); Object Capability model; RBAC (Role-Based Access Control), which simply means a user has several roles, and each role has several permissions, thus forming a “user-role-permission” authorization model, various temporal logic dialects, etc. These new models can be added as needed.
This provides developers with a flexible tool to describe security policies at a highly detailed level as needed. Security policies are defined in high-level languages, greatly simplifying the verification of solutions according to specified requirements. This also makes it possible to conduct formal verification of the described properties.
As solutions become increasingly complex, the addition of different protocols, algorithms, functions, etc., cannot guarantee that there are no vulnerabilities. Special measures must be taken to ensure that these vulnerabilities cannot be exploited or that their exploitation will not lead to adverse consequences. Such protective measures should include process isolation, limiting access to resources, attack detection systems, and countermeasures. In this case, security properties must be guaranteed by the trusted components of the system, namely the operating system kernel, security features, and specific types of protection for subsystems, such as password protection.
Meanwhile, there is a need to define relevant security policies in an increasingly detailed manner. Such a situation arises when the ability to refine policies reaches its limits. For example, policies based on the Capability model can allow or deny access to a certain resource. In this case, the required security properties are considered functional requirements and are implemented in the solution code along with other functionalities. This leads to a gradual increase in the amount of code that needs to be controlled, making ensuring its verifiability an increasingly challenging task. Therefore, the solution becomes insecure once again.
However, with the help of KasperskyOS and KSS, detailed descriptions of security properties can be provided as needed, and by decomposing solutions, a limited set of individual modules can be selected that contain the required minimum functional requirements for verification. In this way, these modules can be viewed as independent, and verification also becomes easier.
KasperskyOS can generate the code library responsible for implementing the security policies of the solution in KSS and formally verify it, making it trustworthy in this sense. This addresses the issue of uncontrolled growth of the code library, which is the source of security.
Since the definition of security properties is independent of functional logic, developers can build a security system for their solutions without considering the implementation details of specific components.
The functionalities described by KasperskyOS make it possible to develop a completely secure solution, as follows:
1. Threat analysis and threat modeling;
2. Developing a formal security policy to address the threats described in step 1;
3. Decomposing the solution into security domains and defining IPC interfaces based on the data obtained in step 2;
4. Executing the solution based on the data obtained in step 3 and implementing a security policy consistent with the results obtained in step 2;
This ensures the main advantage of KasperskyOS, which is the ability to build complex systems to meet specific information security characteristics.
KasperskyOS supports virtualization with the help of the Kaspersky Security Management (KSH) application, which can implement security policies related to virtual machine access control with internal resources alongside KSS. KSH is a lightweight solution, making its code library verifiable, which also means it can be considered part of a trusted platform. Even in the absence of cross-domain interactions, the Kaspersky hypervisor can apply KSS’s security judgments to its internal processes. This capability of KasperskyOS has not been seen in any other virtualization solution, which can only set rules to define how specific virtual machines interact with other isolated components of the system.
Conclusion
In the era of the Internet of Things, network security issues surrounding connected devices are becoming increasingly important. Researchers at Kaspersky Lab believe that the security of the operating system determines the overall network security level of the entire embedded system. Unfortunately, during the development of traditional operating systems, information security issues have not been adequately considered. Nearly half of the operating systems mentioned above have unresolved information security issues or have been addressed unsatisfactorily.
I hope this article can make developers of embedded system operating systems pay more attention to network security issues and help users choose suitable and reliable operating systems for their projects.
