> I've read in several places that basebands now widely use the OKL4 microvisor,[1] based on the formally verified (fwiw) seL4 microkernel, and are much more se

> I've read in several places that basebands now widely use the OKL4 microvisor,[1] based on the formally verified (fwiw) seL4 microkernel, and are much more secure than before. Does anyone know more about this? > > [1] https://gdmissionsystems.com/cyber/products/trusted-computing-cross-domain/microvisor-products/ https://gdmissionsystems.com/cyber/products/trusted-computin... Surely baseband processors are not based on seL4, since it currently has no realtime support (though it is in development: https://wiki.sel4.systems/seL4%200.0.1-rt-dev https://wiki.sel4.systems/seL4%200.0.1-rt-dev). OKL4 is based on a kernel of the L4 family (source: https://en.wikipedia.org/wiki/L4_microkernel_family#Commercial_deployment https://en.wikipedia.org/wiki/L4_microkernel_family#Commerci...): > https://en.wikipedia.org/wiki/L4_microkernel_family https://en.wikipedia.org/wiki/L4_microkernel_family seL4 is another kernel of this family that has been formally verified.