TS News

News

seL4 is verified on RISC-V
2020-06-09 – Trustworthy Systems is extremely pleased to announce that we have completed the functional correctness proof of seL4 on the RV64 ISA. Congratulations to our awesome Proof Engineering Team on achieving this major milestone for seL4! And many thanks to HENSOLDT Cyber for making it possible. We now have the refinement proof from the seL4 formal spec to the C implementation, putting RV64 on the same level as x64 in terms of seL4 verification. The binary verification, which extends this refinement to the binary code of the kernel is progressing, stay tuned for more news on that in the foreseeable future. You can find more details about the verification of seL4 on RISC-V on Gernot's blog

seL4 is verified on RISC-V

2020-06-09 – Trustworthy Systems is extremely pleased to announce that we have completed the functional correctness proof of seL4 on the RV64 ISA. Congratulations to our awesome Proof Engineering Team on achieving this major milestone for seL4! And many thanks to HENSOLDT Cyber for making it possible.

We now have the refinement proof from the seL4 formal spec to the C implementation, putting RV64 on the same level as x64 in terms of seL4 verification. The binary verification, which extends this refinement to the binary code of the kernel is progressing, stay tuned for more news on that in the foreseeable future.

You can find more details about the verification of seL4 on RISC-V on Gernot's blog

seL4 teaching videos available
2020-06-02 – Yet another contribution of UNSW Sydney to the seL4 community: This year Gernot Heiser is making the seL4-related videos from his UNSW Advanced Operating Systems class freely available. You’ll find them at the UNSW CSeLearning COMP9242 YouTube channel. At present there are the first two modules, which provide some background on microkernels and seL4, and discuss the seL4 API. More material will show up over the next two months. The complete course material, including all lecture slides, the project spec and code, are available, as always, from the COMP9042 web site.

seL4 teaching videos available

2020-06-02 – Yet another contribution of UNSW Sydney to the seL4 community: This year Gernot Heiser is making the seL4-related videos from his UNSW Advanced Operating Systems class freely available. You’ll find them at the UNSW CSeLearning COMP9242 YouTube channel.

At present there are the first two modules, which provide some background on microkernels and seL4, and discuss the seL4 API. More material will show up over the next two months.

The complete course material, including all lecture slides, the project spec and code, are available, as always, from the COMP9042 web site.

Announcing the seL4 Foundation whitepaper: "The seL4 Microkernel – An Introduction"
2020-05-25 This white paper provides an introduction to and overview of seL4. We explain what seL4 is (and is not) and explore its defining features. We explain what makes seL4 uniquely qualified as the operating-system kernel of choice for security- and safety- critical systems, and generally embedded and cyber-physical systems. In particular, we explain seL4’s assurance story, its security- and safety-relevant features, and its benchmark-setting performance. We also discuss typical usage scenarios, including incremental cyber retrofit of legacy systems. You can download it at https://sel4.systems/About/

Announcing the seL4 Foundation whitepaper: "The seL4 Microkernel – An Introduction"

2020-05-25 This white paper provides an introduction to and overview of seL4. We explain what seL4 is (and is not) and explore its defining features. We explain what makes seL4 uniquely qualified as the operating-system kernel of choice for security- and safety- critical systems, and generally embedded and cyber-physical systems. In particular, we explain seL4’s assurance story, its security- and safety-relevant features, and its benchmark-setting performance. We also discuss typical usage scenarios, including incremental cyber retrofit of legacy systems.

You can download it at https://sel4.systems/About/

The seL4 Foundation has launched
2020-04-07 We have taken an exciting step to expand the seL4 community, by setting up the seL4 Foundation. It forms an open, transparent and neutral organisation tasked with growing the seL4 ecosystem. It brings together developers of the seL4 kernel, developers of seL4-based components and frameworks, and those adopting seL4 in real-world systems. Its focus is on coordinating, directing and standardising development of the seL4 ecosystem in order to reduce barriers to adoption, raising funds for accelerating development, and ensuring clarity of verification claims. You can learn more by visiting the seL4 Foundation section of our newly revamped sel4.systems website, or reading Gernot's announcement blog.

The seL4 Foundation has launched

2020-04-07 We have taken an exciting step to expand the seL4 community, by setting up the seL4 Foundation. It forms an open, transparent and neutral organisation tasked with growing the seL4 ecosystem. It brings together developers of the seL4 kernel, developers of seL4-based components and frameworks, and those adopting seL4 in real-world systems. Its focus is on coordinating, directing and standardising development of the seL4 ecosystem in order to reduce barriers to adoption, raising funds for accelerating development, and ensuring clarity of verification claims.

You can learn more by visiting the seL4 Foundation section of our newly revamped sel4.systems website, or reading Gernot's announcement blog.

TS wins ACM SIGOPS Hall of Fame Award
2019-11-07 We have won the ACM Special Interest Group in Operating Systems (SIGOPS) Hall of Fame Award for our paper: seL4: Formal Verification of an OS Kernel published at the 2009 ACM SIGOPS Symposium on Operating Systems Principles (SOSP). This award recognises "the most influential Operating Systems papers that were published at least ten years in the past." The citation notes that "the work has become the basis for a large amount of subsequent work in provably correct systems.”. Congratulations! See more detail here.

TS wins ACM SIGOPS Hall of Fame Award

2019-11-07 We have won the ACM Special Interest Group in Operating Systems (SIGOPS) Hall of Fame Award for our paper:

seL4: Formal Verification of an OS Kernel published at the 2009 ACM SIGOPS Symposium on Operating Systems Principles (SOSP).

This award recognises "the most influential Operating Systems papers that were published at least ten years in the past." The citation notes that "the work has become the basis for a large amount of subsequent work in provably correct systems.”.

Congratulations!

See more detail here.

Show older articles