On 21 Jan 2018, at 12:56, Baconicsynergy <baconicsynergy@protonmail.chmailto:baconicsynergy@protonmail.ch> wrote:

Now to my questions - how does the formal verification of seL4 compare with the Integrity-178B security guarantees? Also, how do two structurally compare with each other in terms of design principles and implementation?

To the best of my knowledge, Integrity-178B makes *no* guarantees. It has undergone security evaluation, including a degree of formal verification on a low-level *model* of the kernel. The correspondence between that model and the actual kernel code was established informally (code inspection etc). In other words, there is *not* guarantee that the properties proved apply to the actual implementation (although there is a strong informal argument that they do).

In addition, the formal-methods work, and the general security evaluation, was done on a particular PowerPC processor. AFAIK, nothing similar has been done on other processors, incl x86 and ARM.

This is based on information that is publicly available and represents the state of a number of years ago. It is possible that further work has been done in the meantime, but I have not heard about any such work.

In contrast, seL4 on ARM has a complete proof chain from isolation properties to a formal operational model of the kernel, to the C code, to the binary, for multiple architecture versions. The story is less complete on x86, although a further major verification step for x86 will be released in the near future.

Gernot