- Announce - lists.sel4.systems

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

seL4 2.0.0
by Announcements about seL4 -- low volume list 30 Nov '15

30 Nov '15

The Trustworthy Systems Team at Data61 (formerly NICTA) is pleased to announce seL4 release 2.0.0 The new release cleans up a large backlog of improvements we have been working on for the last 18 months. It also marks the transition to more frequent and regular releases, to minimise the lag between internal and public versions. We have also switched our release process to semantic versioning, so it's easy to tell which seL4 releases are binary-compatible, source-compatible, or will require updates to user-level code. Specific changes are performance improvements to the IPC fastpath and scheduling, making seL4 even faster overall. All changes are formally verified for ARMv6 to full seL4 standard. There are also changes to terminology to eliminate confusion introduced by some object and system call naming in the past. For details please see the Release Notes posted on the developer mailing list. 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

Registration for devdays
by Announcements about seL4 -- low volume list 17 Sep '15

17 Sep '15

We had a few issues with the registration form, but these should now be resolved. https://sel4.systems/Community/Devdays/ for info and https://sel4.systems/Community/Devdays/register.pyl for registration. Peter C -- Dr Peter Chubb peter.chubb AT nicta.com.au http://www.ssrg.nicta.com.au Software Systems Research Group/NICTA

1 0

Second seL4 Developers Day, 8–9 Oct in Malibu
by Announcements about seL4 -- low volume list 16 Sep '15

16 Sep '15

Dear seL4 community, After the great success of our first Developers Day last month, our friends at DARPA are organising a second one, this time on the US West Coast, and open to the wider community (capacity limits apply, of course). The event is hosted by our friends at HRL Labs in Malibu, CA. For details and registration info, please check the seL4 web site: https://sel4.systems/Community/Devdays/ Hope to see some of you there! Gernot ________________________________ 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

seL4 Roadmap announced
by Announcements about seL4 -- low volume list 16 Sep '15

16 Sep '15

Dear seL4 community, Our development and verification roadmap is now published at https://sel4.systems/Info/Roadmap/ Gernot ________________________________ 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

So Long NICTA, Go DATA61!
by Announcements about seL4 low volume list 03 Sep '15

03 Sep '15

Dear seL4 community, This announcement is not strictly about seL4, but is highly relevant to it. NICTA has merged with the Digital Productivity business unit of CSIRO, Australia’s largest and oldest research organisation, and the only one spanning the whole range of science. The resulting entity is called DATA61: http://www.minister.industry.gov.au/ministers/macfarlane/media-releases/csi… You will see changes in branding, e-mail addresses etc in the coming weeks and months, as the NICTA brand is being replaced by DATA61. You will *not* see changes in our commitment to seL4, and its role as a foundation for building highly dependable systems. What used to be the Trustworthy Systems Team at NICTA will continue in DATA61, and its vision of fundamentally changing the way systems are engineered will not change. Our strategy will remain essentially the same (subject to a similar degree of evolution as over the past few years, to ensure maximal relevance and impact). Stay tuned for exciting announcements seL4 itself in the next few days. Gernot ________________________________ 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

New seL4 ports
by Announcements about seL4 low volume list 30 Mar '15

30 Mar '15

seL4 now runs on two more platforms: the TI AM355x Beaglebone Black (courtesy of Tim Newsham) and the Allwinner A20-based CubieTruck (courtesy Robbie Van Vossen). The BeagleBone port includes the userspace libraries; the CubieTruck port so far includes only the kernel. These are the two first community-supported ports --- we at NICTA reviewed the code before merging it, but otherwise have not touched it. As always, code is available on github, at https://github.com/seL4/ -- Dr Peter Chubb peter.chubb AT nicta.com.au http://www.ssrg.nicta.com.au Software Systems Research Group/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

DARPA funds building stuff on seL4
by Announcements about seL4 low volume list 18 Dec '14

18 Dec '14

DARPA has just issued a SBIR call titled "Secure Software Components Leveraging the seL4 Microkernel”, see https://www.dodsbir.net/sitis/display_topic.asp?Bookmark=45918 The SBIR program funds “small” enterprises (that’s <500 employees in US speak) that are majority US-owned. The program clearly aims at developing an ecosystem around seL4. In the past US company that won SBIR projects sub-contracted some of the work to NICTA, so there seems to be no problem in involving foreign entities as subcontractors. Gernot ________________________________ 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

seL4-based "RefOS" released
by Announcements about seL4 low volume list 04 Nov '14

04 Nov '14

Today we announce the release of the RefOS project. RefOS is an OS personality that runs on seL4. RefOS stands for "Reference OS", the aspirational goal of the project, which is to provide a reference OS personality for seL4. RefOS is a student project built as a case study to explore more dynamic virtual memory (VM) management systems than the typical static systems architected on separation kernels. When compared to statically allocated systems, a key difference (and complexity) of dynamic VM management is relaxing the assumption that virtual memory (and memory objects) are managed by a single task upon the microkernel (or by the microkernel itself). RefOS has a distributed VM framework inspired by the Sawmill VM framework [1], though differing in the centralisation of some core book-keeping into a single server (mainly fault forwarding and mapping authorisation). An additional goal of the project was to create tension between user-level and kernel-level VM primitives to enable ongoing kernel experimentation in the area of higher-level VM abstractions. The current functionality of RefOS consists of processes, an in-memory boot-image file server, and console support. Additionally, some games and test applications have been ported to the system. RefOS is available at https://github.com/seL4/refos-manifest under a "BSD 2-Clause" license. [1] Mohit Aron, Jochen Liedtke, Kevin Elphinstone, Yoonho Park, Trent Jaeger, and Luke Deller. 2001. The sawmill framework for virtual memory diversity. In Proceedings of the 6th Australasian conference on Computer systems architecture (ACSAC '01). IEEE Computer Society, Washington, DC, USA, 3-10. ________________________________ 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