- Announce - lists.sel4.systems

TS seeking Proof Engineers and Research Scientist
by Announcements about seL4 -- low volume list 31 Oct '17

31 Oct '17

We are expanding our Trustworthy Systems team in Sydney! We are currently looking for three motivated people in formal methods: - 2 Proof Engineers (junior and senior) - 1 Research Scientist to join Trustworthy Systems at Data61 CSIRO. We are expanding because we have a new funded project exploring verified infrastructure on top of seL4, our formally verified OS microkernel. This project includes building trustworthy applications at user-level, using CakeML and the CAmkES component system. Anyone interested in building and verifying real systems is highly encouraged to apply! This round of applications closes 21 November 2017. More information at [1,2] (and attached). Many thanks, June & Gerwin [1] https://ts.data61.csiro.au/jobs/proof-engineers-2017.pml [2] https://ts.data61.csiro.au/jobs/research-scientist-2017.pml

1 0

Mailing lists will be down for maintenance tomorrow
by Announcements about seL4 -- low volume list 19 Oct '17

19 Oct '17

The devel and announce mailing lists, and their on-line archives, will be unavailable tomorrow morning from around 9am to 10am Australian Eastern Summer Time, to allow upgrading seL4 and the Linux VM runnning on top of it. eMails sent to the lists will be queued, rather than lost. Peter C -- Dr Peter Chubb Tel: +61 2 9490 5852 http://ts.data61.csiro.au/ Trustworthy Systems Group Data61 (formerly NICTA)

1 0

ARM Multicore Support released
by Announcements about seL4 -- low volume list 30 Jun '17

30 Jun '17

Dear seL4 community, Trustworthy Systems @Data61 is pleased to announce the release of seL4 Version 6.0.0. The main new features are: * multicore is now supported for ARMv7 (32-bit) * the FPU is now supported of ARMv7 (32-bit) Details are in the release notes: https://wiki.sel4.systems/seL4%206.0.0 Gernot on behalf of the Trustworthy Systems Team

1 0

New MCS Branch
by Announcements about seL4 -- low volume list 14 Jun '17

14 Jun '17

The Trustworthy Systems team is pleased to announce a new branch of seL4, which provides advanced support for real-time systems, including explicit support for mixed-criticality systems (MCS) for the x86, x64 and ARM v7/v8 architectures. Key features include: * the ability to limit CPU bandwidth consumed by a thread, as a way to prevent high-priority threads from monopolising the processor * a new scheduling-context mechanisms, which extends capability-based access control to the time resource * a principled mechanism for passing CPU allocation between cooperating threads, which provides accurate accounting of CPU time yet retains seL4’s trademark ultra-fast IPC performance * low-overhead support for standard real-time locking protocols, especially the immediate priority ceiling protocol (IPCP) * support for low-overhead user-level scheduler implementation, enabling alternative scheduling policies. This is the first (and largest) step towards a kernel API that provides full temporal integrity enforcement, and support for general MCS, without inhibiting existing use cases. The new version can faithfully emulate the scheduling behaviour of mainline seL4. Further (less dramatic) features will be rolled in over the next year or so. The MCS kernel’s API is formally specified and there is a verification roadmap, but we emphasise that, at present, this version is not fully formally verified and may contain bugs. Verification will take a while, and completion is subject to availability of funding. It is important to understand that the MCS kernel represents the future of seL4. We plan to switch over to this as our mainline API once formal verification is completed. Until that time, the present mainline kernel should be used were verification is important. Note that even without full verification, the MCS version of seL4 is already a highly-dependable OS, sharing the majority of its code base with the verified mainline kernel. Specifically we believe that it is the only OS with a high degree of robustness that truly supports MCS without such limitations as strict static temporal partitioning (which results in inherently low resource utilisation). For these reasons we strongly encourage any new developments to consider adopting the MCS kernel, especially where deployment is still years out (by which time hopefully verification has caught up). More detailed information is available from this posting to the developer list (and references therein): https://sel4.systems/pipermail/devel/2017-June/001470.html Gernot for the Trustworthy Systems Team

1 0

seL4 4.0.0
by Announcements about seL4 -- low volume list 21 Dec '16

21 Dec '16

The Trustworthy Systems at Data61 (formerly NICTA) is pleased to announce seL4 release 4.0.0. The new release contains a number of new features, most notably the following: - support for the x64 platform - support for VT-x on the multicore ia32 platform - robustness improvements for handling device registers - API simplifications The full list is available at https://wiki.sel4.systems/seL4%204.0.0 We are also pleased to announce the first post at the new seL4 blog at https://research.csiro.au/tsblog/introducing-device-untyped-memory-sel4 Stay tuned for further posts on and around seL4. 2016 was an exciting year for seL4 with a lot of new developments, and great contributions from the community. We think that 2017 will be even better, with VT-x support for x64 in the pipeline, multicore support for ARM maturing, and formal verification for the x64 and ARM-hyp platforms scheduled to come out in the first half of the year. We’d like to thank everybody on this list for their support and enthusiasm. There are more cool things to come! Enjoy!

1 0

First International seL4 Workshop
by Announcements about seL4 -- low volume list 08 Nov '16

08 Nov '16

Dear seL4 community, We’d like to invite you to participate in the inaugural seL4 Workshop. Given the growth in the community we are starting an annual seL4 workshop where we can come together to share and learn what is being done with seL4. Unlike the previous developers days, the focus is much more on what is happening with seL4 and what interesting things are being done using seL4 rather than a learning or tutorial event. We’d like participants to join and: - present what they are doing with seL4 - demonstrate seL4-based projects - give tutorials on aspects of seL4 or tools, libraries, environments for working with seL4 - show results or progress of verification work involving seL4 - discuss interesting challenges (and possible solutions) they’ve encountered when using seL4 - discuss visions for the future of seL4 and high-assurance systems This workshop will take place on Thursday December 15, 2016 (and may be extended to December 16th if there is enough demand) in Malibu, CA, USA. Note that you are welcome to attend even if you do not present anything. Please register participation at: https://sel4.systems/Community/Devdays/ Participation is free, and we may be able to provide students with financial assistance for travel. This workshop is sponsored by the Center for Secure and Resilient Systems at HRL Laboratories, LLC, and by Data61. Gernot for the Data61 Trustworthy Systems Team

1 0

Genode supports dynamic workloads on seL4
by Announcements about seL4 -- low volume list 02 Sep '16

02 Sep '16

Genode have released version 16.08 of the Genode OS Framework on seL4. This provides a rich and mature framework for building dynamic systems on seL4 and is a major contribution to the seL4 ecosystem. For details see the posting on the developer list: https://sel4.systems/pipermail/devel/2016-August/000967.html Gernot

1 0

Full virtualisation supported on ARM
by Announcements about seL4 -- low volume list 02 Jul '16

02 Jul '16

The Trustworthy Systems team at Data61 (formerly NICTA) is pleased to announce that full virtualisation support (via the ARM hypervisor extensions) is now available in the seL4 master branch. Verification of this functionality is in progress and expected to be completed in Q1/17. More details are in this announcement on the seL4 developers list: https://sel4.systems/pipermail/devel/2016-June/000874.html Gernot on behalf of the Trustworthy Systems team at Data61 ________________________________ 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.

1 0

Experimental mixed-criticality real-time support available
by Announcements about seL4 -- low volume list 03 Jun '16

03 Jun '16

Dear seL4 community, The long-rumoured enhanced real-time support for seL4 is available for evaluation, released as a branch of the mainline kernel. While still considered “experimental”, the model and implementation are actually quite mature, and we don’t expect massive changes. It is already being deployed in a number of experimental systems, especially under the DARPA HACMS program. We will soon start migrating the new features into the mainstream kernel, and it will eventually be verified like the rest of the kernel. A high-level summary of the new features are: - a periodic thread model that provides temporal isolation via time budgets - capability-contolled allocation of CPU resources - mechanisms to enable proper accounting of time consumed by a server on behalf of clients - support for mixed-criticality real-time systems, where criticality is orthogonal to priority More details are in this announcement on the seL4 developers list and in resources linked from that: https://sel4.systems/pipermail/devel/2016-June/000831.html Gernot on behalf of the Trustworthy Systems team at Data61 (formerly NICTA). ________________________________ 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.

1 0

CAmkES 2.0.0
by Announcements about seL4 -- low volume list 06 Jan '16

06 Jan '16

The Trustworthy Systems Team at Data61 (formerly NICTA) is pleased to announce CAmkES release 2.0.0 The new release updates CAmkES to be compatible with seL4 version 2.0.0. It also marks the transition to more frequent and regular releases, as well as switching our release process to semantic versioning, so it's easy to tell which CAmkES releases are source-compatible, or will require updates to user-level code, and also with which seL4 versions they will be compatible. You can find it at: https://github.com/seL4/camkes-tool/tree/2.0.0 And a manifest for the 2.0.0 compatible versions of the CAmkES test and example apps: https://github.com/seL4/camkes-manifest/blob/master/default-2.0.x.xml Enjoy! ________________________________ 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.

1 0