Easy component-based system design with CAmkES

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:

  • remote procedure calls (RPCs) provide a synchronous communication, internally utilizing seL4’s IPC mechanism.
  • events in contrast represent an asynchronous communication that uses seL4’s notification mechanism.
  • dataports offer a bidirectional communication, suitable for exchanging large data between components via shared memory.

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]. 

READ MORE
Share on facebook
Share on linkedin
Share on email
Share on whatsapp
Share on twitter
Share on reddit

Leave a Reply

Your email address will not be published. Required fields are marked *