CONTENTS 1 Introduction .................................................................................................................... 85 2 Motivation ...................................................................................................................... 85
3 Building Trustworthy Systems ......................................................................................... 87 |
3.1 |
Challenges ......................................................................................................................... 87 |
3.2 |
Solutions ........................................................................................................................... 88 |
3.2.1 |
A MicroKernel Foundation ................................................................................................ 89 |
3.2.2 |
A Secure Communications Software Framework .............................................................. 92 |
4 A Foundation for Building Trustworthy Systems .............................................................. 94 |
4.1 |
The Foundation Part 1 : TRENTOS – The Framework for a Secure OS .................................... 95 |
4.2 |
The Foundation Part 2 : A Software Framework for Certified Systems .................................. 95 |
4.3 |
Example Trustworthy Architectures ................................................................................... 97 |
4.3.1 |
Running in seL4 Trusted User Space .................................................................................. 97 |
4.3.2 |
seL4 as a Hypervisor .......................................................................................................... 98 |
5 Conclusion ...................................................................................................................... 99 6 Getting Started ............................................................................................................. 100 7 References .................................................................................................................... 101 8 Acknowledgements ....................................................................................................... 101
FIGURES
Figure 3-1 . High assurance stack . ................................................................................................................ 88 Figure 3-2 . Kernel design approaches : Monolithic and microkernel ( taken from seL4 white paper ). ....... 90 Figure 3-3 . A Typical CAmkES system architecture ( taken from seL4 white paper ). .................................. 91 Figure 3-4 . Microkernels provide process separation . ............................................................................... 92 Figure 3-5 . The DDS middleware operates between the platform and the application ............................. 93 Figure 4-1 . Infusion pump controller architecture . ..................................................................................... 97 Figure 4-2 . Example when running your applications directly on seL4 / CAmkES in trusted user space . .... 98 Figure 4-3 . Using seL4 as a hypervisor ......................................................................................................... 99
84 July 2022