3 ms·
Except that making changes can actually invalidate the proof that were made. At least it matters in the sense that Apple should have made an arrangement so the
by suavesito 3y ago
Except that making changes can actually invalidate the proof that were made. At least it matters in the sense that Apple should have made an arrangement so the things added didn't invalidate the correctness.
- tptacek 3y agoThat's not really how any of this works. The formally verified kernel of the operating system gives you some assurance that your primitives are reliable (unlike on, say, Linux, where you're always a kernel reference tracking bug away from an LPE). But the "application" code you build on top of L4 doesn't "inherit" that formal verification; it's just code, with code bugs. If you formally verify your own code, it's verified, but otherwise you still own your own bugs. For what it's worth, I'm not sure Apple publishes which variant of L4 it runs on, and there are many of them. The whole formal verification conversation here might be moot.
- monocasa 3y ago> I'm not sure Apple publishes which variant of L4 it runs on The SEPOS kernel is an apparently derived from a fork of L4-embedded they used in Darbat (a fork of XNU to run on top of L4). Not formally verified unless Apple internally has done so.
- suavesito 3y agoAbsolutely, the problem I'm referring to is if Apple changed the kernel and not only built an application on top of it. I don't know, but maybe Apple just built an application on top, which seems sensible.