This is orthogonal. But first, there are still buffer overflows, null pointer accesses & segmentation faults, etc. in the kernel happening. And this is a big pr

This is orthogonal. But first, there are still buffer overflows, null pointer accesses & segmentation faults, etc. in the kernel happening. And this is a big problem! But lets assume this is solved. Then a API can be checked for certain properties. You can specify what it means that something is read-only in an environment etc. And ensure that it is enforced by the operating system. As example: the verification of seL4 not only guarantees avoidance of classical security holes (buffer overflows etc.) but also certain non-interference properties.