Accelerating Time-to-Market
CAmkES consists of a clear set of building blocks . Its primary purpose is to support the development of statically configured embedded systems . Therefore , CAmkES provides a dedicated language used to describe the components and their respective interfaces , as well as the composition of complete component-based systems . It also offers tooling support for processing these descriptions and automatically translating them into C code . In addition , respective proofs are generated . The resulting glue code is combined with programmer-provided component code , leading to the creation of a complete and bootable system image . The overall setup is then neatly integrated into the existing seL4 environment and build system .
Figure
3-3 . A Typical CAmkES system architecture ( taken from seL4 white paper ).
As can be seen in Figure 3-3 , a typical CAmkES system consists of components ( e . g . Component A ) and their respective connections ( e . g . RPC ). When grouping all components and connections together , a composition is formed . If combined with a respective configuration section , a complete system ( also called assembly ) can be provided . The components hereby reflect seL4 ’ s isolation feature and comprise ( at least ) one thread for execution , an associated address space and required storage for associated capabilities . To enable interaction between components , CAmkES provides three basic connection types . Internally , they are mapped to a respective seL4 communication mechanism :
1 . remote procedure calls ( RPCs ): synchronous communication , reusing seL4 ’ s IPC mechanism
2 . events : asynchronous communication , reusing seL4 ’ s notification mechanism
3 . dataports : bidirectional communication , suitable for exchanging large data between components via shared memory ( size is constrained by available physical memory ).
CAmkES and seL4 represent the latest technology advancements in secure microkernels and together comprise the “ safety RTOS ” shown in Figure 3-1 .
Although seL4 and CAmkES provide rudimentary communications paths between processes that can be used for both on and offboard communications , all application-level code required to
Journal of Innovation 91