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.abstract.pml
[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 <[email protected]>
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.
_______________________________________________
Devel mailing list
[email protected]
https://sel4.systems/lists/listinfo/devel
