- Announce - lists.sel4.systems

seL4 Training and ARMv8 virtualization release
by Announcements about seL4 -- low volume list 19 Jan '19

19 Jan '19

All, We at DornerWorks wanted to let the seL4 community know about some seL4 training opportunities that we will be providing on behalf of the seL4 Center of Excellence (CoE). First, we will be providing an introductory webinar that provides an overview and explains the basics of seL4. Webinar: Intro to seL4 Thursday, February 7 11 a.m. EST Register Now: https://dornerworks.clickmeeting.com/intro-to-sel4/register Second, a more advanced two day training will take place on March 7th. This is a paid training that will provide information on seL4, libraries, CAmkES, the proof, and supported platforms. The training will also have hands-on labs that will include configuring CAmkES applications, debugging seL4 applications with GDB, and writing an HTTP server application to serve as a real life example. You can see more information and sign up here: https://www.sae.org/learn/content/c1874/ Finally, we wanted to let people know about our release of our ARMv8 virtualization feature. We recently received approval to release these features to the public. We have a press release providing additional details, a link to the code, and user instructions: https://dornerworks.com/news/new-commits-to-open-source-sel4. Currently, the release is on the DornerWorks github and based on an earlier version of seL4 and its libraries. We are working with Data61 to update to the latest versions and then mainline into the Data61 repositories. This may take some time as we integrate our ARMv8 virtualization code with Data61's ARMv8 virtualization code. Cheers, Robbie VanVossen DornerWorks, Ltd.

1 0

seL4 with proof on x64
by Announcements about seL4 -- low volume list 30 Jul '18

30 Jul '18

Dear seL4 community, it’s my pleasure to announce that even more proofs have become available for seL4. In particular, the Intel x64 version of seL4 now has a functional correctness proof from abstract specification down to the C code. This brings the number of architecture configurations seL4 is verified for up to three (ARMv7, ARMv7 with hypervisor extensions, Intel x64) with a fourth one (RISC-V) in progress. The x64 functional correctness proof does not yet include the fast path, VT-x, or VT-d extensions, nor binary verification or the security proofs we have for ARM, but functional correctness is the core part for all of these other properties and is in itself a big step forward for reliability of the x64 code base. As usual, the proofs and code for seL4 are available on https://github.com/seL4/l4v and https://github.com/seL4/seL4. Enjoy! Gerwin for the Trustworthy Systems Team

1 0

seL4 supports RISC-V
by Announcements about seL4 -- low volume list 18 Apr '18

18 Apr '18

Dear seL4 community, We are extremely pleased to announce that seL4 now supports the RISC-V architecture, making it the third seL4 architecture besides ARM and x86. This is a major step in the seL4 story. For details see https://sel4.systems/pipermail/devel/2018-April/001928.html Gernot for the Trustworthy Systems Team

1 0

Paper describing temporal integrity / MCS scheduling support
by Announcements about seL4 -- low volume list 16 Mar '18

16 Mar '18

A new peer-reviewed paper is now available that describes the motivation, design, implementation and evaluation of our support for temporal integrity enforcement, as required for mixed-criticality systems (MCS). We believe this makes seL4 the first real-world OS with temporal integrity enforcement that goes beyond the simplistic, and highly inefficient, strict time-and-space partitioning (TSP) approach. Furthermore, CPU access is now controlled by capabilities, just like access to spatial resources, resulting in a consistent approach to resource control that we believe is also unique, and will support formal reasoning about temporal system properties. The new model is still in a branch, separate to mainline, until verification is complete, at which time it will supersede the present mainline version. Verification is in progress and should be completed sometime next year (but no guarantees yet). Compared to the earlier announcement (http://sel4.systems/pipermail/announce/2017/000017.html) the model has matured and is now fairly stable, we anticipate no major changes. The paper will appear at next month’s EuroSys conference and is available from https://ts.data61.csiro.au/publications/csiroabstracts/Lyons_MAH_18.abstrac… Gernot for the Trustworthy Systems team

1 0

US seL4 Center of Excellence
by Announcements about seL4 -- low volume list 09 Mar '18

09 Mar '18

We’re pleased to announce that DARPA, in conjunction with Intelligent Automation Inc. and DornerWorks, has created a seL4 Center of Excellence (CoE). The CoE will serve as a USA-based clearing house and ecosystem hub for seL4-related development efforts in the USA. For further information, please contact: Nick Evancich nevancich(a)i-a-i.com Gernot

1 0

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