It sounds to me like your ideal situation could be implemented with the tools we already have at hand - it is just an issue of default settings and how the package maintainers set compilation and installation options. Unless you really wanna go hardcore and advocate for something that is impossible for users/developers to break, which would most likely require a formally verified microkernel [0] - at the very least.

[0] http://en.wikipedia.org/wiki/L4_microkernel_family#High_assu...