The fundamental issue is that, IMhO, security classification needs to be attached to the data at the lowest level -- OS level is simply to coarse. Take for example an encrypted channel. At the OS level the channel is treated opaquely whereas at the programming language level, after decryption the authenticated data can be assigned both a different level of secrecy and trust, and it can be data dependent. Strong type systems can ensure that secret data is never accidentally leaked, nor untrusted data used in a trusted context. (For a real-life simple subset of this, see tperl).
It may be possible to build such a system on top of seL4, but seL4 isn't sufficient.
I do intend on working on this eventually. Incidentally, D. J. Bernstein recently shared a similar complaint about the state of security - the models we use have practically not advanced since the 1950es.
