OUR VISION: SECURE IT INSTEAD OF IT SECURITY
Sebastian Eckl, Senior Software Engineer at HENSOLDT Cyber
This blog post marks the second article in a series of six and will explain the idea of CAmkES, which is meant to ease systems development by providing an abstraction layer on top of the seL4® microkernel. For a better understanding, the architecture of the CAmkES framework is explained and the overall system interplay is described based on a small example
CAmkES – an abstraction layer on top of seL4
Despite all the microkernel-based benefits discussed in the previous blog article, implementing services directly on top of the seL4 microkernel API itself can be quite a challenging task. In order to allow for an easier access to the underlying concepts, various helper libraries have been developed on top to hide the low-level kernel mechanisms of seL4 and make the security features and the mechanisms (e.g. IPC, memory management) offered by the microkernel more usable. CAmkES (Component Architecture for microkernel-based Embedded Systems) extends this approach and provides “a software development and runtime framework for quickly and reliably building microkernel-based multiserver (operating) systems” [1]. The result is a layered component architecture for the separation of concerns, which allows for model-driven development.
The CAmkES Architecture
CAmkES consists of a clear set of building blocks, that allow for the development of statically configured embedded systems. First of all, it provides a dedicated language for describing the components, their respective interfaces and the composition of complete component-based systems. Furthermore, CAmkES offers tooling in order to process these descriptions, automatically translating them into C code as well as generating the respective proofs. The glue code will then be combined with programmer-provided component code in order to build a complete and bootable system image. All in all, this is neatly integrated into the existing seL4 environment and build system.
Figure 1: CAmkES building blocks, adapted from [2]
As depicted in figure 1, a typical CAmkES system consists of components (e.g. CompA) and their respective connections (e.g. RPC). Grouping all components and connections together forms a composition. Combined additionally with a dedicated configuration section, this finally represents a complete system (also called assembly). Hereby, components reflect seL4’s isolation feature and comprise (at least) one thread for execution, the respective address space (VSpace) as well as the respective storage for the required capabilities (CSpace). Regarding interaction, CAmkES basically provides three connection types, which internally map to a respective seL4 communication mechanism:
Providing a small CAmkES example
Figure 2 shows the graphical representation of a small CAmkES example, depicting a system that consists of two components, an UART (uart0) and an application (app). The components are able to communicate with each other via RPC (uart_io and io) and can exchange data through a dataport (uart_port and port).
Figure 2: a small CAmkES example, consisting of two components and their connections
As can be seen in listing 2, before being able to use the actual components, the two underlying component types UART and APP have to be described first. This is done with the help of the CAmkES Architecture Description Language (ADL). Both component types make use of a predefined RPC interface of the type interface_io. This interface is defined with the help of the CAmkES Interface Definition Language (IDL), as can be seen in listing 1. It contains two functions (write and read) that have to be implemented by the component type that will offer a respective service. In our case this is UART, as can be seen by the keyword provides. On the other side, APP wants to call these functions (as can be seen by the keyword uses), whereas it is also declared as an active component (keyword control). Apart from that, both component types contain a respective dataport connector.
Now, in order to create our example system, both component types have to be instantiated once (uart0 and app) and placed into the aforementioned composition and assembly constructs. In order to allow for communication between the two components at runtime, the two interfaces of each component have to be connected (rpc and shareMem) to each other according to their type (seL4RPCCall or seL4SharedData).
procedure interface_io {
void write(size_t len);
void read(size_t len);
};
Listing 1: RPC interface defined with the help of the CAmkES IDL
Component UART {
provides interface_io io;
dataport Buf port;
}
component APP {
control;
uses interface_io uart_io;
dataport Buf uart_port;
}
assembly {
composition {
component UART uart0;
component APP app;
connection seL4RPCCall rpc(from app.uart_io, to uart0.io);
connection seL4SharedData shareMem(from uart0.port, to app.uart_port);
}
}
Listing 2: Declaration and instantiation of two components (with the help of the CAmkES ADL) that communicate via RPC interface and exchange data based on shared memory
Once done, the basic system declaration is more or less complete. Nevertheless, a system developer still has to implement the required component logic with the help of the C programming language. Finally, CAmkES is able to generate a complete, platform-specific bootable system image.
CAmkES and TRENTOS® – providing the framework for a secure OS
With TRENTOS, HENSOLDT Cyber takes the next logical step – developing a novel secure embedded OS on top of the proven seL4 ecosystem. It alleviates the entry to the quite complex area of developing secure embedded systems by abstraction. Hereby, developers can fully focus on creating secure applications without having to worry about lower-level details and the underlying architecture.
CAmkES hereby provides the framework on top of seL4, which is used by TRENTOS to build the respective OS components and services (e.g. for storage or networking support).
Within TRENTOS, the application of CAmkES allows for a certain degree of flexibility. For supporting strong isolation, functionality can be provided separately in form of different CAmkES components that may be explicitly allowed to communicate with each other. In case specified performance requirements have to be satisfied, functionality may also be bundled within a library that is executed in just a single CAmkES component, therefore avoiding any communication overhead. Hence, the design of a TRENTOS system strongly depends on the given requirements. So, stay tuned for the upcoming blog posts, which will provide more insights on the TRENTOS architecture as well as the content of the respective SDK. If you are interested in more details regarding CAmkES itself, have a look at the CAmkES manual [3].
International Day of Families at HENSOLDT Cyber Interview with Markus Wolf, Sascha Fedderwitz, Emilia Fries We asked some of our colleagues a few questions on
How to mitigate hardware attacks? Written by Maja Malenko, Hardware Researcher at HENSOLDT Cyber In the final blog post of our hardware security trilogy, we
Is Hardware Reverse Engineering a Real Threat? Written by Maja Malenko, Hardware Researcher at HENSOLDT Cyber Today we are continuing the story of hardware security
Hardware Security: HENSOLDT Cyber’s MITHRIL Project Written by Maja Malenko, Hardware Researcher at HENSOLDT Cyber Creating secure hardware is a challenging task, especially in times
Successful ISO 9001:2015 certification We are pleased to announce that after eight months of hard work, preparation, and intensive teamwork, HENSOLDT Cyber has certified its
Hello Secure World – How to build and run your first secure TRENTOS® system Building on our first video session in which we took a
LEGAL:
CONTACT US:
FOLLOW US ON:
HEADQUARTER POSTAL ADDRESS:
OUR OFFICE IS LOCATED HERE: