I know few real details of the Linux kernel or of SELinux, but what Brad criticizes in these comments, at least on the surface, seems completely correct.
To be precise, if SELinux is ever changed or if any part of what SELinux depends on working properly ever changes in behavior, then one has to redo the "proof". Maybe this proof redo will be easy for most changes that happen in practice, but maybe not.
In any case, what is the code that must be audited and proven correct for SELinux to work as intended? That would have to be identified and locked down so that any weaknesses could not be introduced by changing anything else. [Eg, if hacking some part of the kernel with the sole intention to compromise the system is done, then that should not affect the "SELinux promise" unless that part being hacked was included as being needed to be locked down.]
I suspect there are too many assumptions being taken by those that would say SELinux is bulletproof. Software is not hardware. Has the hardware and the hardware creation processes and tools been audited?
Now, in practice, it would be a long list to document all the (eg, hardware) assumptions needed for SELinux to work as well as, eg, we might believe is the alternative of isolating data on different machines "not connected" with each other.
Then again, have we proven how many vendors sell a solution where they prove all of their product's requisites? There is an awfully lot of physics that must be documented or at least the assumptions stated. And this says nothing about physics we can't know we don't know about. Truly I don't believe anything is "proven" unless you talk within a limited context. We don't need a degree in philosophy to keep finding potential shortcomings with any system claimed to be perfect.
In short, I think the assumptions should be stated, if not on the glossy brochures main pages, at least on a little comment somewhere. Then again, most people that would identify some of these issues would challenge any vendor claiming some system was provably perfect, in order to weed out the actual assumptions being made. Brad might be going too far and might be playing devil's advocate ad infinitum, perhaps picking on Linux or FOSS because he has allegiances elsewhere. [?]
From what I have heard, the vast majority of the US government or likely virtually 100.0% [note an implied margin or error] of all other institutions out there do not have such high requirements. In these case, a risk analysis would probably reveal weaker links than an SELinux. In these cases, some of the hidden assumptions might be known or else taken for granted no matter the vendor.
Now, let's move the spotlight to Brad completely to wrap up this comment. Does Brad know of any provably secure system, for example? Has his best choice (not counting SELinux) stated their assumptions fully? Could I get access to these assumptions and the proofs? [eg, to the full blueprints for how such a system could ever possibly behave (given its assumptions) with a full analysis of what was believed to be the pertinent physics? And some analysis of what would happen if any of the assumptions were found not to hold?]
Are we all putting things into perspective AND trying to be honest about assumptions, or is perhaps each side failing? When you talk proving security, only the most open of systems could ever honestly attempt to engage in that conversation. Does a system that is really open exist (at hardware, software,... all levels)? Does it even make sense to speak of proofs when referring to physical systems?