Skip to content

Commit

Permalink
deploy: seL4/website@60a03e5
Browse files Browse the repository at this point in the history
  • Loading branch information
@lsf37
lsf37 committed Jul 29, 2024
1 parent c67f0fd commit a5c3f09
Show file tree
Hide file tree
Showing 2 changed files with 199 additions and 264 deletions.
199 changes: 67 additions & 132 deletions PR_381/news/2020.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -125,31 +125,15 @@ <h1>
09 Nov 2020: seL4 12.0.0 release
</div>
<div>
<a href="https://sel4.systems"><img src="/website_pr_hosting/PR_381/images/seL4.svg" style="width:20%;" class="news-img" alt="seL4 logo"></a>
<p>Announcing the releases of seL4, CAmkES and CapDL under the seL4 Foundation.
Below you can find links to release notes with updates to other supporting
projects to come before the end of the year. Versioned Releases:</p>

<p>
<a href="https://sel4.systems">
<img src="../images/seL4.svg" style="width:30%; padding-left:1em; float:right" alt="seL4" />
</a>

Announcing the releases of seL4, CAmkES and CapDL under the seL4
Foundation. Below you can find links to release notes with updates
to other supporting projects to come before the end of the year.

Versioned Releases:
</p>
<ul>
<li>
seL4 12.0.0 ~ <a
href="https://docs.sel4.systems/releases/sel4/12.0.0">https://docs.sel4.systems/releases/sel4/12.0.0</a>
</li>
<li>
CAmkES 3.9.0 ~ <a
href="https://docs.sel4.systems/releases/camkes/camkes-3.9.0">https://docs.sel4.systems/releases/camkes/camkes-3.9.0</a>
</li>
<li>
CapDL 0.2.0 ~ <a
href="https://docs.sel4.systems/releases/capdl/0.2.0">https://docs.sel4.systems/releases/capdl/0.2.0</a>
</li>
<li>seL4 12.0.0 ~ <a href="https://docs.sel4.systems/releases/sel4/12.0.0">https://docs.sel4.systems/releases/sel4/12.0.0</a></li>
<li>CAmkES 3.9.0 ~ <a href="https://docs.sel4.systems/releases/camkes/camkes-3.9.0">https://docs.sel4.systems/releases/camkes/camkes-3.9.0</a></li>
<li>CapDL 0.2.0 ~ <a href="https://docs.sel4.systems/releases/capdl/0.2.0">https://docs.sel4.systems/releases/capdl/0.2.0</a></li>
</ul>

</div>
Expand Down Expand Up @@ -178,23 +162,15 @@ <h1>
22 Jul 2020: Adventium Labs joins the seL4 Foundation!
</div>
<div>

<p>
<a href="https://www.adventiumlabs.com">
<img src="../Foundation/Membership/LOGOS/adventium-labs.svg" style="width:40%; padding-left:1em; float:right"
alt="Adventium Labs logo" />
</a>

We're happy to announce the newest member of the seL4 Foundation:
Minneapolis-based company <a href="https://www.adventiumlabs.com">Adventium Labs</a>.

Adventium Labs develops solutions for safe and secure software-intensive
complex systems, with specialties in separation architectures, model-based
system engineering, and mathematical analysis technologies. They are
leveraging these capabilities to extend seL4 into safety and security critical
industries, including medical devices, defense and commercial avionics, and
industrial control.
</p>
<a href="https://www.adventiumlabs.com"><img src="/website_pr_hosting/PR_381/Foundation/Membership/LOGOS/adventium-labs.svg" style="width:30%;" class="news-img" alt="Adventium Labs logo"></a>
<p>We’re happy to announce the newest member of the seL4 Foundation:
Minneapolis-based company <a href="https://www.adventiumlabs.com">Adventium Labs</a>.
Adventium Labs develops solutions for safe and secure software-intensive complex
systems, with specialties in separation architectures, model-based system
engineering, and mathematical analysis technologies. They are leveraging these
capabilities to extend seL4 into safety and security critical industries,
including medical devices, defense and commercial avionics, and industrial
control.</p>

</div>
<div class="news-finish"></div>
Expand All @@ -204,32 +180,20 @@ <h1>
09 Jun 2020: Functional correctness proof of seL4 RISC-V
</div>
<div>
<a href="https://riscv.org"><img src="/website_pr_hosting/PR_381/Foundation/Membership/LOGOS/RISC-V.svg" style="width:20%;" class="news-img" alt="RISC-V logo"></a>
<p>RISC-V (RV64) is the third ISA with verified seL4. The functional correctness
proof of seL4 on the RV64 ISA has completed. Congratulations to the awesome
Proof Engineering Team of the Trustworthy Systems group on achieving this major
milestone for seL4! And many thanks to HENSOLDT Cyber for making it possible.</p>

<p>
<a href="https://riscv.org">
<img src="../Foundation/Membership/LOGOS/RISC-V.svg" style="width: 15%; padding-left:10px; float:right"
alt="RISC-V logo" />
</a>

RISC-V (RV64) is the third ISA with verified seL4. The functional
correctness proof of seL4 on the RV64 ISA has
completed. Congratulations to the awesome Proof Engineering Team of
the Trustworthy Systems group on achieving this major milestone for
seL4! And many thanks to HENSOLDT Cyber for making it possible.
</p>

<p>
What we have now is 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.
</p>
<p>What we have now is 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.</p>

<p>
More on this in this <a href="https://microkerneldude.wordpress.com/2020/06/09/sel4-is-verified-on-risc-v/">blog
post</a>.
</p>
<p>More on this in this <a href="https://microkerneldude.wordpress.com/2020/06/09/sel4-is-verified-on-risc-v/">blog
post</a>.</p>

</div>
<div class="news-finish"></div>
Expand All @@ -239,33 +203,20 @@ <h1>
02 Jun 2020: UNSW seL4 teaching videos available
</div>
<div>
<a href="https://www.unsw.edu.au"><img src="/website_pr_hosting/PR_381/Foundation/Membership/LOGOS/UNSW.svg" style="width:20%;" class="news-img" alt="UNSW logo"></a>
Yet another contribution of [UNSW Sydney](https://www.unsw.edu.au) 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](https://www.youtube.com/playlist?list=PLbSaCpDlfd6qLbEsKquVo3--0gwYBmrUV).

<p>
<a href="https://www.unsw.edu.au">
<img src="../Foundation/Membership/LOGOS/UNSW.svg" style="width: 15%; padding-left:10px; float:right"
alt="UNSW logo" >
</a>

Yet another contribution of <a href="https://www.unsw.edu.au">UNSW
Sydney</a> 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 <a href="https://www.youtube.com/playlist?list=PLbSaCpDlfd6qLbEsKquVo3--0gwYBmrUV">UNSW
CSeLearning COMP9242 YouTube channel</a>.
</p>

<p>
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.
</p>
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.

<p>
The complete course material, including all lecture slides, the
project spec and code, are available, as always, from the <a
href="https://www.cse.unsw.edu.au/~cs9242/current/">COMP9042 web
site</a>.
</p>
The complete course material, including all lecture slides, the project spec and
code, are available, as always, from the [COMP9042 web
site](https://www.cse.unsw.edu.au/~cs9242/current/).

</div>
<div class="news-finish"></div>
Expand Down Expand Up @@ -303,27 +254,14 @@ <h1>
09 May 2020: Breakaway Consulting joins the seL4 Foundation!
</div>
<div>

<p>

<a href="https://brkawy.com">
<img src="../Foundation/Membership/LOGOS/Brkawy.png" style="width:40%; padding-left:1em; float:right"
alt="Breakaway logo">
</a>

We're happy to announce the first new member since the launch of
the seL4 Foundation: Sydney-based company <a href="https://brkawy.com">Breakaway Consulting</a>.

Through Founder and Managing Director Ben Leslie, Breakaway comes
with 20 years of experience in L4 microkernels and systems based on
various L4 kernels. Prior to founding Breakaway, Ben was a student
with what is now the TS Group, and then VP Engineering of Open
Kernel Labs.

Breakaway offers consulting services on architecture, design and
implementation of seL4-based systems.

</p>
<a href="https://brkawy.com"><img src="/website_pr_hosting/PR_381/Foundation/Membership/LOGOS/Brkawy.png" style="width:30%;" class="news-img" alt="Breakaway logo"></a>
<p>We’re happy to announce the first new member since the launch of the seL4
Foundation: Sydney-based company <a href="https://brkawy.com">Breakaway Consulting</a>.
Through Founder and Managing Director Ben Leslie, Breakaway comes with 20 years
of experience in L4 microkernels and systems based on various L4 kernels. Prior
to founding Breakaway, Ben was a student with what is now the TS Group, and then
VP Engineering of Open Kernel Labs. Breakaway offers consulting services on
architecture, design and implementation of seL4-based systems.</p>

</div>
<div class="news-finish"></div>
Expand All @@ -333,37 +271,34 @@ <h1>
07 Apr 2020: Launch of the seL4 Foundation
</div>
<div>

<img src="/website_pr_hosting/PR_381/images/mosaic.jpg" style="width:30%;" class="news-img" alt="seL4 Foundation launch">
<p>
<img src="../images/mosaic.jpg" style="width:30%; padding-left:1em; float:right" alt="seL4 foundation launch" />

The <a href="https://trustworthy.systems">Trustworthy Systems
group</a> is excited to announce the creation of the <a href="../Foundation/">seL4 Foundation</a>. Its aim is to
provide a
neutral and independent organisation to ensure the longevity of
seL4, and grow its ecosystem of adopters and contributors.
The <a href="https://trustworthy.systems">Trustworthy Systems group</a> is
excited to announce the creation of the <a href="../Foundation/">seL4
Foundation</a>. Its aim is to provide a neutral and independent organisation
to ensure the longevity of seL4, and grow its ecosystem of adopters and
contributors.

It has a <a href="../Foundation/Board/">high-profile Board</a>
consisting of Gernot Heiser (Chair), June Andronick, Gerwin Klein,
John Launchbury, Sascha Kegreiß, Daniel Potts.
consisting of Gernot Heiser (Chair), June Andronick, Gerwin Klein, John
Launchbury, Sascha Kegreiß, Daniel Potts.

It already has a number of members, including major adopters
HENSOLDT Cyber and Ghost Systems, and providers of services for
seL4, Cog Systems and DornerWorks. Please check the <a href="../Foundation/Membership/">membership page</a> for
details and
how to join.
It already has a number of members, including major adopters HENSOLDT Cyber
and Ghost Systems, and providers of services for seL4, Cog Systems and
DornerWorks. Please check the <a href="../Foundation/Membership/">membership
page</a> for details and how to join.

The seL4 Foundation is set up under the Linux Foundation, which
provides a mature and well-known framework.
The seL4 Foundation is set up under the Linux Foundation, which provides a
mature and well-known framework.
</p>

<p>
More information on the <a
href="https://microkerneldude.wordpress.com/2020/04/07/the-sel4-foundation-what-and-why/">Blog
post</a> about "The seL4 Foundation &mdash; What and Why", and in
the press releases from <a
href="https://www.linuxfoundation.org/press/press-release/sel4-microkernel-optimized-for-security-gets-support-of-linux-foundation">the
Linux Foundation</a>.
href="https://microkerneldude.wordpress.com/2020/04/07/the-sel4-foundation-what-and-why/">Blog
post</a> about "The seL4 Foundation &mdash; What and Why", and in the press
releases from <a
href="https://www.linuxfoundation.org/press/press-release/sel4-microkernel-optimized-for-security-gets-support-of-linux-foundation">the
Linux Foundation</a>.
</p>
</div>
<div class="news-finish"></div>
Expand Down
Loading

0 comments on commit a5c3f09

Please sign in to comment.