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.

Formal verification isn't as limited as you suggest. The original use of formal verification for security in high-assurance security was analysis of security kernels for OS's showing that every state the system could be in was secure or fail-safe. Early attempts like UCLA Secure UNIX showed UNIX was impossible to secure because the API's inherently leaked and/or gave attackers opportunities. That's why high-assurance projects abandoned them in favor of security kernels with user-mode version of UNIX isolating those apps from others. Or did entirely new architectures. Mainstream IT and INFOSEC ignored these lessons with most of the failures you've seen resulting. They still argue even though one model worked consistently and one they build on didn't. ;)

Here's a summary of security kernel approach:

http://www.cse.psu.edu/~trj1/cse443-s12/docs/ch6.pdf

Unfortunately, the secure UNIX papers are paywalled. Here's another high-assurance project with sections illustrating issues with UNIX API and changes they had to make. That's back when it had dozens of sys calls.

http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.93....

After a while, the formal verification people got the tools working well enough to prove absence of certain types of problems in code itself rather than an abstract model of it. So, now you see them showing absence of buffer overflows, etc. There's also tools to do similar stuff for assembly and hardware languages. I saw one proof that went down to the gates. Capabilities gradually expanded from system-level properties to lowest-level properties.

> But I think that is not really the big problem we have.

It is a really big problem and it needs to be solved. Did you miss this recent news?

http://www.theregister.co.uk/2016/10/21/linux_privilege_esca...