Disclaimer: I've never compiled sel4 nor executed sel4 and, at this point, am just a
follower of this mailing list (with tentative plans to use sel4 "someday")
Regarding the issue that was fixed here, my first thought was "why did the compiler
not complain?". My next thought was "maybe sel4 doesn't enable all warnings
in their builds or they ignore the warnings!" But surely a kernel that focuses on
security would enable all compiler warnings and fix them immediately as they are
Turns out it doesn't matter what sel4 builds are doing, the gcc compiler has a bug
that prevents warnings for several of these common "might be used uninitialized"
cases. See here:
It also appears this bug will not be fixed! An alternative for some projects, though maybe
not sel4, is to *also* compile their code with clang, which does catch these uninitialized
cases. If sel4 can use clang to catch these types of mistakes earlier, in a compiler
warning, it might save a lengthy validation procedure to catch the error (if it gets
caught at all).
Just thought folks might be interested in this gcc bug -- I certainly wasn't aware of
From: Devel <devel-bounces(a)sel4.systems> On Behalf Of
Sent: Thursday, November 8, 2018 7:22 PM
Subject: Re: [seL4] seL4 10.1.0 and camkes-3.6.0
Now that the fix for this issue has made it through our integration pipeline, I can
explain what happened, since some of you might be interested. The fix is here:
At line 56, the target variable was originally declared uninitialised.
If the loop at lines 57 to 64 executes at least once, then the variable is initialised at
line 58. But if the loop does not execute, then the variable would remain uninitialised
when it is used at line 65. This would be the case if infer_cpu_gic_id was ever called
with nirqs <= 0.
This is *not* a problem in the released kernel, becuase infer_cpu_gic_id is only ever
called once in dist_init, with 32 <= nirqs <= 1024.
However, the binary translation validation test that failed does not do the
inter-procedural analysis that would be necessary to realise this.
When looking at infer_cpu_gic_id, the analysis allows nirqs to take any value. It
considers that the loop might not execute, and therefore target might be uninitialised
when it is used at line 65. The dataflow model that is produced by the analysis cannot
model such undefined behaviour, and so the test fails. With the fix, the variable is never
uninitialised, so the analysis does not run into this problem.
In summary, the fix you see here keeps our proofs happy, but it does not increase the
safety of the kernel. This function, as it is actually used, was already safe.
In terms of our development process, this kind of failure in the binary translation
validation is quite rare and difficult to predict. And since our proofs take quite a long
time to run, we don't always insist that our kernel developers run the proofs for
changes in boot code, which is currently unverified except for binary translation
validation. We accept that these failures will occasionally happen, and we deal with them
when they do. The functions dist_init and infer_cpu_gic_id are boot-only code, so this was
one of those rare failures.
Of course, we should insist on running all the tests for versions we intend to formally
release, and we will for future releases.
From: Brecknell, Matthew (Data61, Kensington NSW)
Sent: Thursday, 8 November 2018 11:25 AM
Cc: Mcleod, Kent (Data61, Kensington NSW)
Subject: Re: seL4 10.1.0 and camkes-3.6.0
Due to an oversight on my part, seL4 10.1.0 was released without passing the full
verification test suite.
We have no reason to believe that there is any problem in the verified parts of this seL4
The test that failed is part of the binary translation validation, which produces a
dataflow graph from the Isabelle/HOL model of the C code, and then attempts to
automatically prove a refinement relation between the C and that dataflow graph. The
failure occurred in boot code, which in any case is currently not verified. The failure
does not mean that there is any problem with the C code. Most likely, it just means that
some new code uses some C idiom which is currently not handled by the automatic
All other components of the verification test suite pass, including security proofs and
functional correctness proofs for the Isabelle/HOL model of the C code.
Nevertheless, we intend to rectify this failure as soon as possible, and we'll make
further announcements when we understand what happened.
I want to reiterate that this was entirely my fault, and was not at all Kent's
From: Devel <devel-bounces(a)sel4.systems> on behalf of Kent.Mcleod(a)data61.csiro.au
Sent: Thursday, 8 November 2018 8:44 AM
Subject: [seL4] seL4 10.1.0 and camkes-3.6.0
See an online copy of the release notes at:
10.1.0 2018-11-07: SOURCE COMPATIBLE
* structures in the boot info are not declared 'packed'
- these were previously packed (in the GCC attribute sense)
- some field lengths are tweaked to avoid padding
- this is a source-compatible change
* ARM platforms can now set the trigger of an IRQ Handler capability
- seL4_IRQControl_GetTrigger allows users to obtain an IRQ Handler capability
and set the trigger (edge or level) in the interrupt controller.
* Initial support for NVIDIA Jetson TX2 (ARMv8a, Cortex A57)
* AARCH64 support added for raspberry pi 3 platform.
* Code generation now use jinja2 instead of tempita.
* AARCH32 HYP support added for running multiple ARM VMs
* AARCH32 HYP VCPU registers updated.
* A new invocation for setting TLSBase on all platforms.
* Kbuild/Kconfig/Makefile build system removed.
Using seL4 version 10.1.0
* AARCH64 is now supported.
* CakeML components are now supported.
* Added `query` type to Camkes ADL to allow for querying plugins for component
* Components can now make dtb queries to parse device information from dts files.
* Component definitions for serial and timer added on exynos5422, exynos5410, pc99.
* Preliminary support for Isabelle verification of generated capDL.
- See cdl-refine-tests/README for more information
* Simplify and refactor the alignment and section linking policy for generated Camkes
* Dataports are now required to declare their size in the ADL.
* Templates now use seL4_IRQHandler instead of seL4_IRQControl, which is consistent with
the seL4 API.
- This change is BREAKING.
* Remove Kbuild based build system.
* Remove caches that optimised the Kbuild build system, which are not required with the
new Cmake build system.
* Added virtqueue infrastructure to libsel4camkes, which allows virtio style queues
## Upgrade Notes
* Any dataport definitions that did not specify a size must be updated to use a size.
* Any template that used seL4_IRQControl must be updated to use seL4_IRQHandler.
* Projects must now use the new Cmake based build system.
Devel mailing list
Devel mailing list