Accelerating Time-to-Market
by DDS . The main benefit of using the CAmkES design pattern is that the developer gets verified interfaces “ for free ”. This may lead to a much quicker verification process .
This architecture has three key advantages :
1 . It avoids the need for a full-blown operating system , 2 . it reduces the power , memory , and CPU requirements for your system 3 . It significantly reduces the attack surface .
It also comes with three disadvantages
1 . Your applications need to be written in C 2 . The development environment is very limited 3 . There is extra work you need to do in your application to bootstrap your code .
While you can copy from examples , all of this code will still need to be reviewed and adapted to your needs . In particular , there will be quite a bit of seL4 configuration needed , allocation of memory , bootstrapping the standard C library , bootstrapping all the I / O , etc . While CAmkES simplifies these bootstrapping steps , another approach will be needed if you want to avoid the first two disadvantages . We discuss this next .
Figure 4-2 . Example when running your applications directly on seL4 / CAmkES in trusted user space .
The second architectural option reaps the benefits of seL4 while avoiding the development constraints imposed by seL4 ’ s trusted user space . Using this approach , seL4 can be used as a hypervisor ( see Figure 4-3 ). It provides separation guarantees to ensure that there is no unintentional information leakage between the VMs . While the Linux attack surface within each VM still exists , the isolation provided by seL4 will ensure that a failure in one VM will not bring down any other running VMs .
98 July 2022