Hacker Newsnew | past | comments | ask | show | jobs | submitlogin

Based on what I've read from more authoritative sources (or is the author an authority in this area?), this information is outdated:

> It can be safely assumed that this baseband is highly insecure. It is closed source and probably not audited at all. My understanding is that the genesis of modern baseband firmware is a development effort for GSM basebands dating back to the 1990s during which the importance of secure software development practices were not apparent. In other words, and my understanding is that this is borne out by research, this firmware tends to be extremely insecure and probably has numerous remote code execution vulnerabilities.

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



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

OKL4 is based on a kernel of the L4 family (source: https://en.wikipedia.org/wiki/L4_microkernel_family#Commerci...):

> https://en.wikipedia.org/wiki/L4_microkernel_family

seL4 is another kernel of this family that has been formally verified.




Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: