Hi, Today I created a few pull-requests on seL4 repos to build x86-64 with clang: - https://github.com/seL4/seL4/pull/105 - https://github.com/seL4/musllibc/pull/4 - https://github.com/seL4/seL4_tools/pull/19 /Jonas
‐‐‐‐‐‐‐ Original Message ‐‐‐‐‐‐‐ On Wednesday, November 14, 2018 5:28 PM, <[email protected]> wrote: > Message: 3 > Date: Wed, 14 Nov 2018 16:28:17 +0000 > From: Andy Helten [email protected] > To: "[email protected]" > [email protected], "[email protected]" > > <[email protected]> > > > Subject: Re: [seL4] seL4 10.1.0 and camkes-3.6.0 > Message-ID: > dm6pr17mb2314d1ef141dd6dd6a4779be92...@dm6pr17mb2314.namprd17.prod.outlook.com > > Content-Type: text/plain; charset="utf-8" > > 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 introduced. > > 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: > > https://gcc.gnu.org/bugzilla/show_bug.cgi?id=18501 > > 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 it. > > Andy > > -----Original Message----- > From: Devel [email protected] On Behalf Of > [email protected] > Sent: Thursday, November 8, 2018 7:22 PM > To: [email protected] > Subject: Re: [seL4] seL4 10.1.0 and camkes-3.6.0 > > Hi, > > 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: > > https://github.com/seL4/seL4/commit/d12bb374ab47d2b13f438969d2eb5dde1021af84 > > 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. > > Best regards, > Matt > > From: Brecknell, Matthew (Data61, Kensington NSW) > Sent: Thursday, 8 November 2018 11:25 AM > To: [email protected] > Cc: Mcleod, Kent (Data61, Kensington NSW) > Subject: Re: seL4 10.1.0 and camkes-3.6.0 > > Hi, > > 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 version. > > 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 translation process. > > 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 fault. > > Best regards, > Matt > > From: Devel [email protected] on behalf of > [email protected] [email protected] > Sent: Thursday, 8 November 2018 8:44 AM > To: [email protected] > Subject: [seL4] seL4 10.1.0 and camkes-3.6.0 > > See an online copy of the release notes at: > https://docs.sel4.systems/sel4_release/seL4_10.1.0 > https://docs.sel4.systems/camkes_release/Camkes_3.6.0 > > 10.1.0 2018-11-07: SOURCE COMPATIBLE > > Changes > > -------- > > - 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. > - seL4_TCB_SetTLSBase > - Kbuild/Kconfig/Makefile build system removed. > > camkes-3.6.0 2018-11-07 > Using seL4 version 10.1.0 > > Changes > > -------- > > - AARCH64 is now supported. > - CakeML components are now supported. > - Added `query` type to Camkes ADL to allow for querying plugins for > component configuration values. > - 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 binaries. > - 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 between components. > > > 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 > [email protected] > https://sel4.systems/lists/listinfo/devel > > Devel mailing list > [email protected] > https://sel4.systems/lists/listinfo/devel > > -------------------------------------------------------------------------------- > > Subject: Digest Footer > > Devel mailing list > [email protected] > https://sel4.systems/lists/listinfo/devel > > > --------------------------------------------------------------------------------- > > End of Devel Digest, Vol 54, Issue 12 _______________________________________________ Devel mailing list [email protected] https://sel4.systems/lists/listinfo/devel
