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?
thanks.
On 29.01.2015, at 09:50, 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?
Our current iteration of the binary verification uses "gcc -O1”, so after mild optimisations. For highest security requirements this would currently be the one to take.
For “normal" production builds and benchmarking we do use gcc -O2, which we have so far found reliable for seL4. We use a fairly easy to translate subset of C, and -O2 is the most frequently used code path of gcc, so we are reasonably confident that gcc works correctly in this case, but there is no proof, only tests and (some) inspection of the binary.
We think we're fairly close to changing this and have the binary verification apply to the gcc -O2 build, so the highest security scenarios will have the same performance benefits, but we’re not quite there yet.
Note that we don’t have crypto code or code with constant time execution requirements in the kernel. These are not the only things that can go wrong, of course, but they are the ones where compiler optimisations often will give you headaches. Timing analysis is done on the binary, after optimisation.
Cheers, Gerwin
________________________________
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
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
Hi Perry,
We did some previous work towards applying CompCert to seL4 [0]. The changes required to seL4 were not especially invasive and mostly cosmetic. The seL4 branch for this was not maintained because we decided translation validation was a more feasible route to take for discharging the compiler assumptions [1], but it would not be difficult to revive them. Along the way, we learned that GCC-generated code significantly outperformed code generated by CompCert and other compilers for the case of the seL4 code base. At the time, each successive CompCert release was closing the gap, so I would not be surprised if the results are more favourable today.
When talking about GCC (or any compiler) bugs, it's important to note that this only matters if they are triggered and affect output code. Someone with more authority may wish to contradict me, but I believe the translation validation strategy admits a buggy compiler as long as it produces correct code for the case in question. E.g. If we fed the seL4 source code into a random number generator that happened to produce a binary that could be shown to correspond to the source, you would still have a correctly compiled binary.
Cheers, Matt
[0]: http://www.ssrg.nicta.com.au/publications/nictaabstracts/Fernandez_KK_12.abs... [1]: http://ssrg.nicta.com.au/publications/nictaabstracts/Sewell_14.abstract.pml
On 30/01/15 12:48, Perry E. Metzger wrote:
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
________________________________
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
-
Gerwin Klein -
Matthew Fernandez -
Perry E. Metzger -
Raoul Duke