On Wed, 28 Jan 2015 14:50:40 -0800 Raoul Duke raould@gmail.com wrote:
Easier to keep the generator simple and let the compiler do the optimisations it already understands.
Based on things like the experiences of Tahoe LAFS with compiler optimizations vs. security - let alone plain bugs - I am scared if anybody uses any optimizations at all, especially for serious business. I have not researched the position se4L takes on this. Are the proofs about the before-optimization code, or do they consider the after-optimization assembly output?
I will note, just as an aside, that there is now a formally verified C compiler (CompCert) for which even optimizations are formally verified. (Roughly, the proof shows observational equivalence between the input and output of the compiler.)
There has also been work on formally verified LLVM optimizer stages (the VeLLVM project), which again showed observational equivalence between the input and output of the verified optimizers.
So, even if the current seL4 has to rely a bit on gcc being non-buggy, the situation need not remain that way forever.
Perry