Re: [seL4] seL4 10.1.0 and camkes-3.6.0

Dear seL4 community, I’d like to clarify that Matt publicly taking the blame for creating a minor issue with the release was not necessary. We do not blame Matt for this and he shouldn’t blame himself. What happened was that our release process is imperfect, and the imperfection of the process ended up in a release where not all i's were dotted. This is in itself no surprise, as it is an informally specified process and thus must be expected to have flaws. One of them was triggered by a particular race condition. Far from blaming one of our hard-working and highly committed engineers, we take responsibility as a team, and we do not want to create any impression to the contrary. Of course, we are improving our processes. And of course we understand that they will still be imperfect, as they aren’t formally verified ;-) And please note that what went out may be absolutely fine, i.e. ATM we have no indication that the code is actually broken, only that a particular part of the proof is out of sync with the code. Quite likely it’s only the proof that will updating, but we’re still investigating. Gernot for Trustworthy Systems

On 8 Nov 2018, at 11:25, Matthew.Brecknell@data61.csiro.au wrote:

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 on behalf of Kent.Mcleod@data61.csiro.au Sent: Thursday, 8 November 2018 8:44 AM To: devel@sel4.systems 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 Devel@sel4.systems https://sel4.systems/lists/listinfo/devel

_______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel