diff --git a/PR_417/About/Performance/index.html b/PR_417/About/Performance/index.html index 210d6a1a..5633ab4b 100644 --- a/PR_417/About/Performance/index.html +++ b/PR_417/About/Performance/index.html @@ -113,40 +113,40 @@

Performance

32 A9/i.MX6/Sabre 1.0 GHz - 582 + 586 (14) 317 - (2) - 338 - (6) - 837 - (12) + (3) + 343 + (7) + 830 + (11) x86_64 64 i7-4770/Haswell 3.4 GHz - 1533 - (265) - 576 - (12) - 590 - (12) - 1319 - (74) + 1560 + (270) + 573 + (10) + 587 + (13) + 1323 + (70) x86_64 64 i7-6700/Skylake (without meltdown mitigation) 3.4 GHz - 1276 - (206) + 1311 + (205) 382 (3) - 381 + 387 (3) - 752 - (82) + 753 + (83) Armv8a 64 @@ -154,25 +154,25 @@

Performance

1.9 GHz 664 (30) - 406 - (11) - 415 - (1) - 926 + 422 + (10) + 417 (6) + 894 + (4) RV64IMAC 64 U54-MC/SiFive Freedom U540/Hifive 1.5 GHz - 963 - (66) - 491 - (100) - 659 - (93) - 1345 - (46) + 985 + (90) + 468 + (12) + 627 + (16) + 1347 + (63)

MCS

@@ -191,66 +191,66 @@

MCS

32 A9/i.MX6/Sabre 1.0 GHz - 800 + 802 (18) 324 (2) - 364 - (2) - 1189 - (12) + 363 + (3) + 1197 + (13) x86_64 64 i7-4770/Haswell 3.4 GHz - 1988 - (428) - 586 + 2007 + (430) + 585 + (12) + 602 (13) - 605 - (11) 1590 - (8) + (5) x86_64 64 i7-6700/Skylake (without meltdown mitigation) 3.4 GHz - 1665 - (332) - 382 + 1648 + (358) + 380 (3) - 406 - (5) - 1039 - (6) + 407 + (4) + 1057 + (14) Armv8a 64 A57/Tx1/Jetson 1.9 GHz - 754 - (26) - 415 - (7) - 434 + 759 + (27) + 419 + (9) + 428 + (8) + 1017 (4) - 977 - (14) RV64IMAC 64 U54-MC/SiFive Freedom U540/Hifive 1.5 GHz - 2927 - (132) - 686 - (43) - 894 - (93) - 3856 - (150) + 2939 + (137) + 675 + (18) + 910 + (118) + 3841 + (138)

Compilation Details

@@ -349,7 +349,7 @@

MCS

Source Code

-

This page was generated on 2024-10-25 for sel4bench-manifest 8c799e7c.

+

This page was generated on 2024-11-11 for sel4bench-manifest 7e2229f3.

@@ -357,35 +357,56 @@

Source Code

- mastodon icon - youtube icon - linkedin icon + +mastodon icon +youtube icon +linkedin icon +

- Copyright © 2024 seL4 Project a Series of LF Projects, LLC.
- seL4 is a trademark of LF Projects, LLC.
- For trademark usage guidelines, privacy and cookie policies, - and other applicable policies, as well as terms and conditions - governing this web site, please see - www.lfprojects.org - and the trademark guidelines. + + +Copyright © 2024 seL4 Project a Series of LF Projects, LLC.
+seL4 is a trademark of LF Projects, LLC.
+For trademark usage guidelines, privacy and cookie policies, +and other applicable policies, as well as terms and conditions +governing this web site, please see +www.lfprojects.org +and the trademark guidelines. +
diff --git a/PR_417/About/index.html b/PR_417/About/index.html index bd12e774..2accd367 100644 --- a/PR_417/About/index.html +++ b/PR_417/About/index.html @@ -191,35 +191,56 @@

- mastodon icon - youtube icon - linkedin icon + +mastodon icon +youtube icon +linkedin icon +

- Copyright © 2024 seL4 Project a Series of LF Projects, LLC.
- seL4 is a trademark of LF Projects, LLC.
- For trademark usage guidelines, privacy and cookie policies, - and other applicable policies, as well as terms and conditions - governing this web site, please see - www.lfprojects.org - and the trademark guidelines. + + +Copyright © 2024 seL4 Project a Series of LF Projects, LLC.
+seL4 is a trademark of LF Projects, LLC.
+For trademark usage guidelines, privacy and cookie policies, +and other applicable policies, as well as terms and conditions +governing this web site, please see +www.lfprojects.org +and the trademark guidelines. +
diff --git a/PR_417/Contribute/index.html b/PR_417/Contribute/index.html index f4d217a4..6ced2136 100644 --- a/PR_417/Contribute/index.html +++ b/PR_417/Contribute/index.html @@ -133,35 +133,56 @@

Community Support Contributions

- mastodon icon - youtube icon - linkedin icon + +mastodon icon +youtube icon +linkedin icon +

- Copyright © 2024 seL4 Project a Series of LF Projects, LLC.
- seL4 is a trademark of LF Projects, LLC.
- For trademark usage guidelines, privacy and cookie policies, - and other applicable policies, as well as terms and conditions - governing this web site, please see - www.lfprojects.org - and the trademark guidelines. + + +Copyright © 2024 seL4 Project a Series of LF Projects, LLC.
+seL4 is a trademark of LF Projects, LLC.
+For trademark usage guidelines, privacy and cookie policies, +and other applicable policies, as well as terms and conditions +governing this web site, please see +www.lfprojects.org +and the trademark guidelines. +
diff --git a/PR_417/Foundation/Board/Minutes/241009-minutes-unconfirmed.pdf b/PR_417/Foundation/Board/Minutes/241009-minutes-unconfirmed.pdf new file mode 100644 index 00000000..2bad89dd Binary files /dev/null and b/PR_417/Foundation/Board/Minutes/241009-minutes-unconfirmed.pdf differ diff --git a/PR_417/Foundation/Board/Minutes/index.html b/PR_417/Foundation/Board/Minutes/index.html index e59a734f..eb0c7229 100644 --- a/PR_417/Foundation/Board/Minutes/index.html +++ b/PR_417/Foundation/Board/Minutes/index.html @@ -137,13 +137,13 @@

Confirmed Minutes

- +
@@ -152,35 +152,56 @@

Confirmed Minutes

- mastodon icon - youtube icon - linkedin icon + +mastodon icon +youtube icon +linkedin icon +

- Copyright © 2024 seL4 Project a Series of LF Projects, LLC.
- seL4 is a trademark of LF Projects, LLC.
- For trademark usage guidelines, privacy and cookie policies, - and other applicable policies, as well as terms and conditions - governing this web site, please see - www.lfprojects.org - and the trademark guidelines. + + +Copyright © 2024 seL4 Project a Series of LF Projects, LLC.
+seL4 is a trademark of LF Projects, LLC.
+For trademark usage guidelines, privacy and cookie policies, +and other applicable policies, as well as terms and conditions +governing this web site, please see +www.lfprojects.org +and the trademark guidelines. +
diff --git a/PR_417/Foundation/Board/index.html b/PR_417/Foundation/Board/index.html index 7315443c..8e690a15 100644 --- a/PR_417/Foundation/Board/index.html +++ b/PR_417/Foundation/Board/index.html @@ -353,35 +353,56 @@

Marketing Committee

- mastodon icon - youtube icon - linkedin icon + +mastodon icon +youtube icon +linkedin icon +

- Copyright © 2024 seL4 Project a Series of LF Projects, LLC.
- seL4 is a trademark of LF Projects, LLC.
- For trademark usage guidelines, privacy and cookie policies, - and other applicable policies, as well as terms and conditions - governing this web site, please see - www.lfprojects.org - and the trademark guidelines. + + +Copyright © 2024 seL4 Project a Series of LF Projects, LLC.
+seL4 is a trademark of LF Projects, LLC.
+For trademark usage guidelines, privacy and cookie policies, +and other applicable policies, as well as terms and conditions +governing this web site, please see +www.lfprojects.org +and the trademark guidelines. +
diff --git a/PR_417/Foundation/Contact/index.html b/PR_417/Foundation/Contact/index.html index 4c108e23..93c405f0 100644 --- a/PR_417/Foundation/Contact/index.html +++ b/PR_417/Foundation/Contact/index.html @@ -110,35 +110,56 @@

- mastodon icon - youtube icon - linkedin icon + +mastodon icon +youtube icon +linkedin icon +

- Copyright © 2024 seL4 Project a Series of LF Projects, LLC.
- seL4 is a trademark of LF Projects, LLC.
- For trademark usage guidelines, privacy and cookie policies, - and other applicable policies, as well as terms and conditions - governing this web site, please see - www.lfprojects.org - and the trademark guidelines. + + +Copyright © 2024 seL4 Project a Series of LF Projects, LLC.
+seL4 is a trademark of LF Projects, LLC.
+For trademark usage guidelines, privacy and cookie policies, +and other applicable policies, as well as terms and conditions +governing this web site, please see +www.lfprojects.org +and the trademark guidelines. +
diff --git a/PR_417/Foundation/Governance/index.html b/PR_417/Foundation/Governance/index.html index eb36b50c..82e2e53e 100644 --- a/PR_417/Foundation/Governance/index.html +++ b/PR_417/Foundation/Governance/index.html @@ -177,35 +177,56 @@

- mastodon icon - youtube icon - linkedin icon + +mastodon icon +youtube icon +linkedin icon +

- Copyright © 2024 seL4 Project a Series of LF Projects, LLC.
- seL4 is a trademark of LF Projects, LLC.
- For trademark usage guidelines, privacy and cookie policies, - and other applicable policies, as well as terms and conditions - governing this web site, please see - www.lfprojects.org - and the trademark guidelines. + + +Copyright © 2024 seL4 Project a Series of LF Projects, LLC.
+seL4 is a trademark of LF Projects, LLC.
+For trademark usage guidelines, privacy and cookie policies, +and other applicable policies, as well as terms and conditions +governing this web site, please see +www.lfprojects.org +and the trademark guidelines. +
diff --git a/PR_417/Foundation/Jobs/index.html b/PR_417/Foundation/Jobs/index.html index bae1f0e4..ed4bf651 100644 --- a/PR_417/Foundation/Jobs/index.html +++ b/PR_417/Foundation/Jobs/index.html @@ -402,35 +402,56 @@

- mastodon icon - youtube icon - linkedin icon + +mastodon icon +youtube icon +linkedin icon +

- Copyright © 2024 seL4 Project a Series of LF Projects, LLC.
- seL4 is a trademark of LF Projects, LLC.
- For trademark usage guidelines, privacy and cookie policies, - and other applicable policies, as well as terms and conditions - governing this web site, please see - www.lfprojects.org - and the trademark guidelines. + + +Copyright © 2024 seL4 Project a Series of LF Projects, LLC.
+seL4 is a trademark of LF Projects, LLC.
+For trademark usage guidelines, privacy and cookie policies, +and other applicable policies, as well as terms and conditions +governing this web site, please see +www.lfprojects.org +and the trademark guidelines. +
diff --git a/PR_417/Foundation/Join/index.html b/PR_417/Foundation/Join/index.html index 1105b5cf..e56dbe3a 100644 --- a/PR_417/Foundation/Join/index.html +++ b/PR_417/Foundation/Join/index.html @@ -272,35 +272,56 @@

Universities and public-sector

- mastodon icon - youtube icon - linkedin icon + +mastodon icon +youtube icon +linkedin icon +

- Copyright © 2024 seL4 Project a Series of LF Projects, LLC.
- seL4 is a trademark of LF Projects, LLC.
- For trademark usage guidelines, privacy and cookie policies, - and other applicable policies, as well as terms and conditions - governing this web site, please see - www.lfprojects.org - and the trademark guidelines. + + +Copyright © 2024 seL4 Project a Series of LF Projects, LLC.
+seL4 is a trademark of LF Projects, LLC.
+For trademark usage guidelines, privacy and cookie policies, +and other applicable policies, as well as terms and conditions +governing this web site, please see +www.lfprojects.org +and the trademark guidelines. +
diff --git a/PR_417/Foundation/Membership/LOGOS/rtx.svg b/PR_417/Foundation/Membership/LOGOS/rtx.svg new file mode 100644 index 00000000..f8daeb01 --- /dev/null +++ b/PR_417/Foundation/Membership/LOGOS/rtx.svg @@ -0,0 +1,47 @@ + + + + diff --git a/PR_417/Foundation/Membership/index.html b/PR_417/Foundation/Membership/index.html index dea58de8..5aa039cf 100644 --- a/PR_417/Foundation/Membership/index.html +++ b/PR_417/Foundation/Membership/index.html @@ -236,11 +236,11 @@

General Members

- Raytheon logo + Raytheon logo
- Raytheon Technologies + RTX Corporation
@@ -360,35 +360,56 @@

Associate Members

- mastodon icon - youtube icon - linkedin icon + +mastodon icon +youtube icon +linkedin icon +

- Copyright © 2024 seL4 Project a Series of LF Projects, LLC.
- seL4 is a trademark of LF Projects, LLC.
- For trademark usage guidelines, privacy and cookie policies, - and other applicable policies, as well as terms and conditions - governing this web site, please see - www.lfprojects.org - and the trademark guidelines. + + +Copyright © 2024 seL4 Project a Series of LF Projects, LLC.
+seL4 is a trademark of LF Projects, LLC.
+For trademark usage guidelines, privacy and cookie policies, +and other applicable policies, as well as terms and conditions +governing this web site, please see +www.lfprojects.org +and the trademark guidelines. +
diff --git a/PR_417/Foundation/Services/cog.html b/PR_417/Foundation/Services/cog.html index ab2e18a9..d2fce329 100644 --- a/PR_417/Foundation/Services/cog.html +++ b/PR_417/Foundation/Services/cog.html @@ -174,35 +174,56 @@

Cog Systems Services

- mastodon icon - youtube icon - linkedin icon + +mastodon icon +youtube icon +linkedin icon +

- Copyright © 2024 seL4 Project a Series of LF Projects, LLC.
- seL4 is a trademark of LF Projects, LLC.
- For trademark usage guidelines, privacy and cookie policies, - and other applicable policies, as well as terms and conditions - governing this web site, please see - www.lfprojects.org - and the trademark guidelines. + + +Copyright © 2024 seL4 Project a Series of LF Projects, LLC.
+seL4 is a trademark of LF Projects, LLC.
+For trademark usage guidelines, privacy and cookie policies, +and other applicable policies, as well as terms and conditions +governing this web site, please see +www.lfprojects.org +and the trademark guidelines. +
diff --git a/PR_417/Foundation/Services/dornerworks.html b/PR_417/Foundation/Services/dornerworks.html index 7dc69ff5..39d7a62b 100644 --- a/PR_417/Foundation/Services/dornerworks.html +++ b/PR_417/Foundation/Services/dornerworks.html @@ -184,35 +184,56 @@

Contact

- mastodon icon - youtube icon - linkedin icon + +mastodon icon +youtube icon +linkedin icon +

- Copyright © 2024 seL4 Project a Series of LF Projects, LLC.
- seL4 is a trademark of LF Projects, LLC.
- For trademark usage guidelines, privacy and cookie policies, - and other applicable policies, as well as terms and conditions - governing this web site, please see - www.lfprojects.org - and the trademark guidelines. + + +Copyright © 2024 seL4 Project a Series of LF Projects, LLC.
+seL4 is a trademark of LF Projects, LLC.
+For trademark usage guidelines, privacy and cookie policies, +and other applicable policies, as well as terms and conditions +governing this web site, please see +www.lfprojects.org +and the trademark guidelines. +
diff --git a/PR_417/Foundation/Services/endorsement.html b/PR_417/Foundation/Services/endorsement.html index 9049ac8d..aa7ca5e6 100644 --- a/PR_417/Foundation/Services/endorsement.html +++ b/PR_417/Foundation/Services/endorsement.html @@ -289,35 +289,56 @@

Products

- mastodon icon - youtube icon - linkedin icon + +mastodon icon +youtube icon +linkedin icon +

- Copyright © 2024 seL4 Project a Series of LF Projects, LLC.
- seL4 is a trademark of LF Projects, LLC.
- For trademark usage guidelines, privacy and cookie policies, - and other applicable policies, as well as terms and conditions - governing this web site, please see - www.lfprojects.org - and the trademark guidelines. + + +Copyright © 2024 seL4 Project a Series of LF Projects, LLC.
+seL4 is a trademark of LF Projects, LLC.
+For trademark usage guidelines, privacy and cookie policies, +and other applicable policies, as well as terms and conditions +governing this web site, please see +www.lfprojects.org +and the trademark guidelines. +
diff --git a/PR_417/Foundation/Services/hc.html b/PR_417/Foundation/Services/hc.html index d04902f0..5411a414 100644 --- a/PR_417/Foundation/Services/hc.html +++ b/PR_417/Foundation/Services/hc.html @@ -248,35 +248,56 @@

Industries

- mastodon icon - youtube icon - linkedin icon + +mastodon icon +youtube icon +linkedin icon +

- Copyright © 2024 seL4 Project a Series of LF Projects, LLC.
- seL4 is a trademark of LF Projects, LLC.
- For trademark usage guidelines, privacy and cookie policies, - and other applicable policies, as well as terms and conditions - governing this web site, please see - www.lfprojects.org - and the trademark guidelines. + + +Copyright © 2024 seL4 Project a Series of LF Projects, LLC.
+seL4 is a trademark of LF Projects, LLC.
+For trademark usage guidelines, privacy and cookie policies, +and other applicable policies, as well as terms and conditions +governing this web site, please see +www.lfprojects.org +and the trademark guidelines. +
diff --git a/PR_417/Foundation/Services/index.html b/PR_417/Foundation/Services/index.html index bec764bc..77e3a257 100644 --- a/PR_417/Foundation/Services/index.html +++ b/PR_417/Foundation/Services/index.html @@ -428,35 +428,56 @@

Products

- mastodon icon - youtube icon - linkedin icon + +mastodon icon +youtube icon +linkedin icon +

- Copyright © 2024 seL4 Project a Series of LF Projects, LLC.
- seL4 is a trademark of LF Projects, LLC.
- For trademark usage guidelines, privacy and cookie policies, - and other applicable policies, as well as terms and conditions - governing this web site, please see - www.lfprojects.org - and the trademark guidelines. + + +Copyright © 2024 seL4 Project a Series of LF Projects, LLC.
+seL4 is a trademark of LF Projects, LLC.
+For trademark usage guidelines, privacy and cookie policies, +and other applicable policies, as well as terms and conditions +governing this web site, please see +www.lfprojects.org +and the trademark guidelines. +
diff --git a/PR_417/Foundation/Summit/2022/abstracts2022.html b/PR_417/Foundation/Summit/2022/abstracts2022.html index b08270f3..2be7e9e3 100644 --- a/PR_417/Foundation/Summit/2022/abstracts2022.html +++ b/PR_417/Foundation/Summit/2022/abstracts2022.html @@ -1060,35 +1060,56 @@

- mastodon icon - youtube icon - linkedin icon + +mastodon icon +youtube icon +linkedin icon +

- Copyright © 2024 seL4 Project a Series of LF Projects, LLC.
- seL4 is a trademark of LF Projects, LLC.
- For trademark usage guidelines, privacy and cookie policies, - and other applicable policies, as well as terms and conditions - governing this web site, please see - www.lfprojects.org - and the trademark guidelines. + + +Copyright © 2024 seL4 Project a Series of LF Projects, LLC.
+seL4 is a trademark of LF Projects, LLC.
+For trademark usage guidelines, privacy and cookie policies, +and other applicable policies, as well as terms and conditions +governing this web site, please see +www.lfprojects.org +and the trademark guidelines. +
diff --git a/PR_417/Foundation/Summit/2022/bids.html b/PR_417/Foundation/Summit/2022/bids.html index 2a1576a0..5f1e3602 100644 --- a/PR_417/Foundation/Summit/2022/bids.html +++ b/PR_417/Foundation/Summit/2022/bids.html @@ -128,35 +128,56 @@

- mastodon icon - youtube icon - linkedin icon + +mastodon icon +youtube icon +linkedin icon +

- Copyright © 2024 seL4 Project a Series of LF Projects, LLC.
- seL4 is a trademark of LF Projects, LLC.
- For trademark usage guidelines, privacy and cookie policies, - and other applicable policies, as well as terms and conditions - governing this web site, please see - www.lfprojects.org - and the trademark guidelines. + + +Copyright © 2024 seL4 Project a Series of LF Projects, LLC.
+seL4 is a trademark of LF Projects, LLC.
+For trademark usage guidelines, privacy and cookie policies, +and other applicable policies, as well as terms and conditions +governing this web site, please see +www.lfprojects.org +and the trademark guidelines. +
diff --git a/PR_417/Foundation/Summit/2022/cfp.html b/PR_417/Foundation/Summit/2022/cfp.html index 01ecf841..c0a1f8cd 100644 --- a/PR_417/Foundation/Summit/2022/cfp.html +++ b/PR_417/Foundation/Summit/2022/cfp.html @@ -322,35 +322,56 @@

- mastodon icon - youtube icon - linkedin icon + +mastodon icon +youtube icon +linkedin icon +

- Copyright © 2024 seL4 Project a Series of LF Projects, LLC.
- seL4 is a trademark of LF Projects, LLC.
- For trademark usage guidelines, privacy and cookie policies, - and other applicable policies, as well as terms and conditions - governing this web site, please see - www.lfprojects.org - and the trademark guidelines. + + +Copyright © 2024 seL4 Project a Series of LF Projects, LLC.
+seL4 is a trademark of LF Projects, LLC.
+For trademark usage guidelines, privacy and cookie policies, +and other applicable policies, as well as terms and conditions +governing this web site, please see +www.lfprojects.org +and the trademark guidelines. +
diff --git a/PR_417/Foundation/Summit/2022/index.html b/PR_417/Foundation/Summit/2022/index.html index d444ef15..da8b16ac 100644 --- a/PR_417/Foundation/Summit/2022/index.html +++ b/PR_417/Foundation/Summit/2022/index.html @@ -565,35 +565,56 @@

- mastodon icon - youtube icon - linkedin icon + +mastodon icon +youtube icon +linkedin icon +

- Copyright © 2024 seL4 Project a Series of LF Projects, LLC.
- seL4 is a trademark of LF Projects, LLC.
- For trademark usage guidelines, privacy and cookie policies, - and other applicable policies, as well as terms and conditions - governing this web site, please see - www.lfprojects.org - and the trademark guidelines. + + +Copyright © 2024 seL4 Project a Series of LF Projects, LLC.
+seL4 is a trademark of LF Projects, LLC.
+For trademark usage guidelines, privacy and cookie policies, +and other applicable policies, as well as terms and conditions +governing this web site, please see +www.lfprojects.org +and the trademark guidelines. +
diff --git a/PR_417/Foundation/Summit/2022/principles.html b/PR_417/Foundation/Summit/2022/principles.html index be488802..b7d68f3a 100644 --- a/PR_417/Foundation/Summit/2022/principles.html +++ b/PR_417/Foundation/Summit/2022/principles.html @@ -119,35 +119,56 @@

- mastodon icon - youtube icon - linkedin icon + +mastodon icon +youtube icon +linkedin icon +

- Copyright © 2024 seL4 Project a Series of LF Projects, LLC.
- seL4 is a trademark of LF Projects, LLC.
- For trademark usage guidelines, privacy and cookie policies, - and other applicable policies, as well as terms and conditions - governing this web site, please see - www.lfprojects.org - and the trademark guidelines. + + +Copyright © 2024 seL4 Project a Series of LF Projects, LLC.
+seL4 is a trademark of LF Projects, LLC.
+For trademark usage guidelines, privacy and cookie policies, +and other applicable policies, as well as terms and conditions +governing this web site, please see +www.lfprojects.org +and the trademark guidelines. +
diff --git a/PR_417/Foundation/Summit/2022/program.html b/PR_417/Foundation/Summit/2022/program.html index 39457c40..5f98a4ab 100644 --- a/PR_417/Foundation/Summit/2022/program.html +++ b/PR_417/Foundation/Summit/2022/program.html @@ -606,35 +606,56 @@

- mastodon icon - youtube icon - linkedin icon + +mastodon icon +youtube icon +linkedin icon +

- Copyright © 2024 seL4 Project a Series of LF Projects, LLC.
- seL4 is a trademark of LF Projects, LLC.
- For trademark usage guidelines, privacy and cookie policies, - and other applicable policies, as well as terms and conditions - governing this web site, please see - www.lfprojects.org - and the trademark guidelines. + + +Copyright © 2024 seL4 Project a Series of LF Projects, LLC.
+seL4 is a trademark of LF Projects, LLC.
+For trademark usage guidelines, privacy and cookie policies, +and other applicable policies, as well as terms and conditions +governing this web site, please see +www.lfprojects.org +and the trademark guidelines. +
diff --git a/PR_417/Foundation/Summit/2023/abstracts2023.html b/PR_417/Foundation/Summit/2023/abstracts2023.html index 870a55ed..06f8899e 100644 --- a/PR_417/Foundation/Summit/2023/abstracts2023.html +++ b/PR_417/Foundation/Summit/2023/abstracts2023.html @@ -1110,35 +1110,56 @@

- mastodon icon - youtube icon - linkedin icon + +mastodon icon +youtube icon +linkedin icon +

- Copyright © 2024 seL4 Project a Series of LF Projects, LLC.
- seL4 is a trademark of LF Projects, LLC.
- For trademark usage guidelines, privacy and cookie policies, - and other applicable policies, as well as terms and conditions - governing this web site, please see - www.lfprojects.org - and the trademark guidelines. + + +Copyright © 2024 seL4 Project a Series of LF Projects, LLC.
+seL4 is a trademark of LF Projects, LLC.
+For trademark usage guidelines, privacy and cookie policies, +and other applicable policies, as well as terms and conditions +governing this web site, please see +www.lfprojects.org +and the trademark guidelines. +
diff --git a/PR_417/Foundation/Summit/2023/cfp.html b/PR_417/Foundation/Summit/2023/cfp.html index d867887c..692b6197 100644 --- a/PR_417/Foundation/Summit/2023/cfp.html +++ b/PR_417/Foundation/Summit/2023/cfp.html @@ -299,35 +299,56 @@

- mastodon icon - youtube icon - linkedin icon + +mastodon icon +youtube icon +linkedin icon +

- Copyright © 2024 seL4 Project a Series of LF Projects, LLC.
- seL4 is a trademark of LF Projects, LLC.
- For trademark usage guidelines, privacy and cookie policies, - and other applicable policies, as well as terms and conditions - governing this web site, please see - www.lfprojects.org - and the trademark guidelines. + + +Copyright © 2024 seL4 Project a Series of LF Projects, LLC.
+seL4 is a trademark of LF Projects, LLC.
+For trademark usage guidelines, privacy and cookie policies, +and other applicable policies, as well as terms and conditions +governing this web site, please see +www.lfprojects.org +and the trademark guidelines. +
diff --git a/PR_417/Foundation/Summit/2023/index.html b/PR_417/Foundation/Summit/2023/index.html index 82167fdd..deb2a172 100644 --- a/PR_417/Foundation/Summit/2023/index.html +++ b/PR_417/Foundation/Summit/2023/index.html @@ -566,35 +566,56 @@

- mastodon icon - youtube icon - linkedin icon + +mastodon icon +youtube icon +linkedin icon +

- Copyright © 2024 seL4 Project a Series of LF Projects, LLC.
- seL4 is a trademark of LF Projects, LLC.
- For trademark usage guidelines, privacy and cookie policies, - and other applicable policies, as well as terms and conditions - governing this web site, please see - www.lfprojects.org - and the trademark guidelines. + + +Copyright © 2024 seL4 Project a Series of LF Projects, LLC.
+seL4 is a trademark of LF Projects, LLC.
+For trademark usage guidelines, privacy and cookie policies, +and other applicable policies, as well as terms and conditions +governing this web site, please see +www.lfprojects.org +and the trademark guidelines. +
diff --git a/PR_417/Foundation/Summit/2023/program.html b/PR_417/Foundation/Summit/2023/program.html index 0c2e4710..20f1cfe7 100644 --- a/PR_417/Foundation/Summit/2023/program.html +++ b/PR_417/Foundation/Summit/2023/program.html @@ -598,35 +598,56 @@

- mastodon icon - youtube icon - linkedin icon + +mastodon icon +youtube icon +linkedin icon +

- Copyright © 2024 seL4 Project a Series of LF Projects, LLC.
- seL4 is a trademark of LF Projects, LLC.
- For trademark usage guidelines, privacy and cookie policies, - and other applicable policies, as well as terms and conditions - governing this web site, please see - www.lfprojects.org - and the trademark guidelines. + + +Copyright © 2024 seL4 Project a Series of LF Projects, LLC.
+seL4 is a trademark of LF Projects, LLC.
+For trademark usage guidelines, privacy and cookie policies, +and other applicable policies, as well as terms and conditions +governing this web site, please see +www.lfprojects.org +and the trademark guidelines. +
diff --git a/PR_417/Foundation/Summit/2023/submit.html b/PR_417/Foundation/Summit/2023/submit.html index 6397a753..f2ff17e2 100644 --- a/PR_417/Foundation/Summit/2023/submit.html +++ b/PR_417/Foundation/Summit/2023/submit.html @@ -123,35 +123,56 @@

- mastodon icon - youtube icon - linkedin icon + +mastodon icon +youtube icon +linkedin icon +

- Copyright © 2024 seL4 Project a Series of LF Projects, LLC.
- seL4 is a trademark of LF Projects, LLC.
- For trademark usage guidelines, privacy and cookie policies, - and other applicable policies, as well as terms and conditions - governing this web site, please see - www.lfprojects.org - and the trademark guidelines. + + +Copyright © 2024 seL4 Project a Series of LF Projects, LLC.
+seL4 is a trademark of LF Projects, LLC.
+For trademark usage guidelines, privacy and cookie policies, +and other applicable policies, as well as terms and conditions +governing this web site, please see +www.lfprojects.org +and the trademark guidelines. +
diff --git a/PR_417/Foundation/Summit/2024/abstracts2024.html b/PR_417/Foundation/Summit/2024/abstracts2024.html index 4b1f643d..6ad5fc6e 100644 --- a/PR_417/Foundation/Summit/2024/abstracts2024.html +++ b/PR_417/Foundation/Summit/2024/abstracts2024.html @@ -133,6 +133,8 @@

presentation will provide an overview of the PROVERS program objectives, the INSPECTA workflow to be developed, and the assurance evidence to be produced.

+ YouTube icon   + slides icon
See this talk in the program
@@ -158,6 +160,8 @@

We will further report on where the verification of the seL4 extensions for mixed-criticality systems (MCS) is at, and share our plans for DARPA's PROVERS program where, as part of the INSPECTA team, we are aiming at increasing verification automation and scope while reducing the reliance on formal methods experts.

+ YouTube icon   + slides icon
See this talk in the program

@@ -184,6 +188,8 @@

We will report on our progress in building such a framework, with the aim to maximise the reuse of existing proofs. We will also present how starting with a static multikernel design is the fastest path to providing the community with an seL4 kernel that allows utilisation of multiple processor cores, opening the path to building multicore seL4-based systems that come with a formal proof of correctness.

+ YouTube icon   + slides icon
See this talk in the program

@@ -209,6 +215,7 @@

(1) https://neutrality.ch/

+ YouTube icon  
See this talk in the program

@@ -235,6 +242,8 @@

In the talk I will explain the principles of Lions OS and its design, looking at concrete examples. I will present performance data that show that the approach can work and provide an overview of our current work on verification. This will be complemented by Ivan Velickovic’s talk covering Lions OS from a developer’s point of view, and Rob Sison’s and Courtney Darville’s talks on verifying Lions OS.

+ YouTube icon   + slides icon
See this talk in the program

@@ -261,6 +270,8 @@

We will dive into what it is like to use LionsOS by showcasing the tooling and surrounding infrastructure that has been created for developing a LionsOS-based system. This will cover topics such as I/O, virtualisation, debugging, profiling, as well as how to put all these pieces together.

+ YouTube icon   + slides icon
See this talk in the program

@@ -284,6 +295,8 @@

The Secure Multiserver Operating System (SMOS) project aims to create a secure, dynamic OS framework on top of seL4. Our goal is to enable the development of systems as dynamic as mainstream operating systems like Linux, that allow you to, for example, download and run arbitrary executables, while leveraging the security properties of seL4 to ensure that a global security policy is always correctly upheld. This talk will focus on the key principles behind the design of SMOS, the progress we have made on its implementation, and an overview of some of the challenges we have encountered, both in development and in correctly enforcing a variety of arbitrary, often complex security policies at runtime.

+ YouTube icon   + slides icon
See this talk in the program

@@ -304,6 +317,8 @@

Upstream hypervisor support has expanded in recent years to support additional configurations on x86, ARM, and RISC-V. Every upstream example simply runs Linux, which is an excellent use case for highly functional, general purpose computing platforms, however there are other guest Operating Systems that solve different use cases. Running seL4 in Hypervisor mode allows for the untrusted code in Linux to be sandboxed and isolated from trusted components in the system. What if the guest Operating System was fully trusted? Deos is a DO-178C DAL A certified RTOS for Avionics Applications, an area seL4 has struggled to break into. DornerWorks expanded seL4 Hypervisor support to run Deos under the CAmkES VM. This presentation will overview the changes that needed to be made to support a certifiable RTOS guest, how a Hypervisor effects the safety certification considerations of Deos, and the next steps needed to create a certifiable system with seL4.

+ YouTube icon   + slides icon
See this talk in the program

@@ -324,6 +339,8 @@

seL4 currently provides, formally verified, memory safety guarantees in the kernel and isolation guarantees between seL4's userspace tasks, but there is no safety within a single seL4 task or protection domain itself (e.g., VMs or single-address-space servers such as rumprun). According to a recent Microsoft study, memory safety vulnerabilities account for 70% of all software vulnerabilities. CHERI is a capability-based hardware-software architecture aiming to address memory-safety and software compartmentalisation issues. The goal of this project is to have a complete memory-safe C/C++ seL4-based software stack using CHERI on Morello, without having to re-write the existing seL4 C/C++ userspace libraries (currently over 250 KLoC, using sloc tool) from scratch or formally verify them. This talk will describe the progress of CHERIfying the existing seL4's userspace in order to have complete (spatial) memory and pointer safety.

+ YouTube icon   + slides icon
See this talk in the program

@@ -347,6 +364,8 @@

In this talk, we report on our experience developing, testing, and characterizing the performance of our implementation using the seL4 ecosystem. We have containerized our development environment to simplify building our application and to support users with differing platforms. In addition to relying on automated theorem prover assistants and model checkers, we have written many unit and integration tests to help write correct software. Using a network benchmark, we show that our solution exhibits competitive, if not superior, performance characteristics both in terms of average behavior and variance.

+ YouTube icon   + slides icon
See this talk in the program

@@ -367,6 +386,8 @@

This talk presents an experience report on migrating seL4-based systems from the CAmkES VMM to the Microkit VMM. Microkit is a simple framework and SDK created to enable more efficient designs and lower the barrier to entry to seL4. The presentation will compare and contrast MicroKit with CAmkES and highlight a few reasons to start using Microkit. In addition, it will examine how MicroKit can make learning and developing seL4-based systems easier and breakdown roadblocks encountered by new users when porting to a new platform. Finally, we will present our gap analysis between the two VMMs and highlight what still needs to be addressed so users can start developing real-world products.

+ YouTube icon   + slides icon
See this talk in the program

@@ -389,6 +410,8 @@

The seL4 Foundation is home to the ecosystem of software, developers and adopters for safety- and security-critical systems based on seL4. It was formed in April 2020 as a neutral and community-based organisation that ensures long-term, independent support for seL4 and its ecosystem, and fosters strong community participation and ownership in the ecosystem. It raises funds for continuing and accelerating development, facilitates interoperability, standardisation and sharing of cost for the benefit of all. Its aim is to ensure that seL4 is not only the world’s best secure operating-system technology, but is readily deployable and supported by a diverse and stable ecosystem of services and products.

+ YouTube icon   + slides icon
See this talk in the program

@@ -418,6 +441,8 @@

In this talk, we present our initial experiments with concurent user-space verification. We use the Iris separation logic framework to build an abstract model of a simple system in which components interact using shared memory and notifications, and we prove a simple correctness property. We explain the limitations of this experiment, and how we plan to address them in our next steps.

+ YouTube icon   + slides icon
See this talk in the program

@@ -441,6 +466,8 @@

We present Efeu, a framework that allows us to specify both the host-side driverand the peripherals. The specifications are composed of layers, which enableefficient modeling of different devices (including those with quirks). Theentire system is then model-checked using SPIN to ensure interoperability. Fromthat, Efeu generates trustworthy drivers in software and hardware. The softwareimplementations target seL4, but could also address other operating systems.Furthermore, when I2C communication speed or CPU usage is a concern, Efeu allowsgenerating hybrid hardware/software drivers, where the hardware part can bematerialized on programmable hardware such as Field Programmable Gate Arrays(FPGAs). We evaluated Efeu-generated I2C stacks on a Zynq MPSoC and show thatmodel-checking the whole system and generating the full stack is not onlypractical but that the resulting implementations can saturate the I2C bus andachieve competitive performance with off-the-shelf solutions.

+ YouTube icon   + slides icon
See this talk in the program

@@ -467,6 +494,8 @@

Using formal methods, and in particular model checking, vastly improves the development process of signalling protocols, since the tool can verify for deadlock freedom whilst also producing detailed traces (interleavings of executions) when a deadlock is found. This talk details how the model checker SPIN was used to develop and analyse sDDF signalling protocols, ultimately resulting in a verified protocol that reduces the number of unnecessary signals by 47% when compared to unconditionally signalling.

+ YouTube icon   + slides icon
See this talk in the program

@@ -487,6 +516,8 @@

The development and maintenance of Rust support in seL4 userspace has been an official seL4 Foundation project since last year’s summit. This project’s scope includes libraries for interacting with the seL4 API, higher-level libraries for use in seL4 userspace (e.g. support for asynchronous programming and integration with the seL4 Device Driver Framework), Rust language runtimes for root tasks and Microkit protection domains, modular building blocks for custom seL4 userspace Rust language runtimes, a CapDL system initializer implementation, and an easy-to-use kernel loader. The past year has seen the expansion and refinement of this project’s library offerings, the release of relevant educational materials, and further integration with the rest of the seL4 software ecosystem. In this talk, we will cover progress since last year’s summit, demonstrate how to leverage this work in your own systems, and share our vision and goals for the path ahead.

+ YouTube icon   + slides icon
See this talk in the program

@@ -510,6 +541,8 @@

We present the design of the language and its verified compiler, as well as demonstrating its usability, performance and current limitations through case studies of device drivers and related systems components for an seL4-based operating system.

+ YouTube icon   + slides icon
See this talk in the program

@@ -524,7 +557,7 @@

Talk

- Presented by Ihor Kuz, Kry10 + Presented by Ihor Kuz, Kry10 and Lance Joneckis, Idaho National Laboratory

When a digital system is undergoing cyber attack or is failing in some way, it is often necessary to take action different from its usual operating mode. These alternative modes of operation are called Reserve Modes. @@ -536,6 +569,8 @@

This presentation introduces Assured Reserve Modes on the seL4-based Kry10 OS. Assured Reserve Modes are a mechanism for providing reserved modes that successfully address the above challenges - implementing reserved mode functionality and providing assurance that they work correctly. We explain the concept of reserve modes and provide examples of reserve modes and their benefits, present the Assured Reserve Mode design and implementation, and discuss how to provide the assurance that they require.

+ YouTube icon   + slides icon
See this talk in the program

@@ -550,7 +585,7 @@

Talk

- Presented by Ihor Kuz, Kry10 + Presented by Ihor Kuz, Kry10 and Lance Joneckis, Idaho National Laboratory

Assured Reserve Modes are a mechanism that we’ve developed for the seL4-based Kry10 OS that allows a system to switch between pre-configured operating modes at runtime in response to security, safety, and other routine operational events. In this presentation we show the operation of assured reserve modes in action. @@ -562,6 +597,8 @@

This presentation is a companion to the Assured Reserve Modes presentation that describes the assured reserve mode model and mechanism itself.

+ YouTube icon   + slides icon
See this talk in the program

@@ -585,6 +622,8 @@

Deploying containers on embedded systems is not necessarily new and has been demonstrated across various embedded Linux deployments. At Kry10 we recognise the value of using containers and see the conveniences it can bring to a developers workflow and the capabilities it provides for developing update-able and maintainable systems. We've implemented first-class container support in Kry10 OS that allows developers to define and package native and VM-based applications. In this talk, I'll present the design and implementation behind our seL4-based container support. I'll step through how container builds are used to package and deploy different types of applications on Kry10 OS, starting from simple native applications, and as the needs and runtime requirements of the application grow, moving onto more complex microVM-style applications.

+ YouTube icon   + slides icon
See this talk in the program

@@ -608,6 +647,8 @@

We present empirical data on the CPU, memory, and I/O performance impacts of having a seL4 TEE on a PolarFire RISC-V platform and run different TEE services performance measurements. The insights into performance nuances, such as the minimal overhead introduced by the seL4 TEE and its operational efficiency in handling cryptographic tasks, solidify the practical benefits of our architecture. Furthermore, we outline ongoing advancements and future directions in enhancing the seL4-based TEE.

+ YouTube icon   + slides icon
See this talk in the program

@@ -628,6 +669,8 @@

A formally-verified microkernel is a great start, and an OS needs more than a microkernel. Over the past years, we have been building a vehicle operating system and toolsets based on seL4 from scratch. It is very challenging, especially when dependability is the top priority. In this talk, we would like to share our experiences along the journey, with an emphasis on the following topics: (1) POSIX or not, that is not a question. To leverage the existing code base and 3rd party libraries, a layered approach is adopted: The system has a core system call layer and a POSIX layer based on the core layer. System components use the core layer. Applications and 3rd party libraries use the POSIX interfaces. (2) Tooling is especially important for development efficiency and system usability. System status monitoring and comprehensive logging are critical since we rely on them to analyze issues remotely. Additionally, a building and integration tool is specifically designed to manage the building and releasing process of the OS and applications. (3) Resource management needs more thoughts. Seasoned system developers are surprised by another form of resource leakage: capability slot leakage. Access control to resources that are not managed by the kernel directly through capabilities also deserves some discussion. (4) Product-level maturity is paramount. We wish that the major OS components could be verified, but at least for now, realistically, various levels of testing are used to stabilize and mature the new OS.

+ YouTube icon   + slides icon
See this talk in the program

@@ -650,6 +693,8 @@

We transition our entire suite of contributions from CAmkES to Microkit. A greater range of USB device classes are now supported. A simple native HDMI driver is introduced. And we leverage sDDF and VMM, in permitting the secure routing of a selected physical USB device into a guest host. While our primary focus has been the Avnet MaaXBoard, many of these contributions would be readily portable to other platforms. More generally, as our focus on seL4 infrastructure reaches a conclusion, we describe our journey with seL4 thus far, summarising our overall contributions and experiences.

+ YouTube icon   + slides icon
See this talk in the program

@@ -673,6 +718,8 @@

At the 2020 seL4 Summit, Cog Systems presented this effort as a case study in applying seL4 to a product commercialization effort. Since then, the project has experienced multiple and varied challenges, and has not yet been completed. At the 2023 Summit we gave a follow-up presentation detailing the progress, setbacks, and lessons learned of the past few years. Now, in the 2024 continuation of the series, Cog Systems will provide an update and share some of the technical, logistical, and financial challenges we encountered while building a commercial smartphone product with seL4.

+ YouTube icon   + slides icon
See this talk in the program

@@ -696,6 +743,8 @@

This talk introduces you to the seL4-nix-utils, a collection of Nix expressions to compile but also ease integration and project bring-up with seL4. After a brief introduction to the mechanism behind Nix, we outline the provided Nix expressions and their use-cases. The talk closes with a list of remaining pain-points and a reference to a hands-on you may try after the talk.

+ YouTube icon   + slides icon
See this talk in the program

@@ -715,6 +764,8 @@

The automotive industry is rapidly evolving, with software-defined vehicles (SDVs) at the forefront of this transformation. At NIO, we are leveraging the seL4 microkernel to redefine vehicle architecture, ensuring robust safety, reliability, and performance. This presentation will explore the vision behind integrating seL4 into our SDV platform. We will share the journey of delivering the seL4-based SkyOS-M within the ONVO vehicle on our latest NT3 platform, highlight the significant impact this integration has had on our vehicle design and functionality, and outline our future roadmap beyond the current launch.

+ YouTube icon   + slides icon
See this talk in the program

@@ -738,6 +789,8 @@

Even in less critical environments, a compromised robot could surreptitiously spy on an end user or subtly/overtly cause harm to the environment in which it operates. While securing such systems with seL4 seems like an obvious solution, the lack of support for common software APIs and middleware presents a significant hurdle. Once this is overcome wider adoption of seL4 and more resilient robotic systems would be enabled. This presentation will show how the cyber-retrofit approach is being used to enable secure autonomous operation of an x86 based ground vehicle, how this approach is being extended to enable native seL4 ROS applications, and the barriers to further system hardening.

+ YouTube icon   + slides icon
See this talk in the program

@@ -761,6 +814,8 @@

At the 2022 seL4 summit, we presented the custom RISC-V fence.t instruction to temporally partition on-core processor state in CVA6, a simple in-order RV64GC processor. This year’s talk will propose a minimal ISA extension that enables hybrid spatial and temporal partitioning of a complete system-on-chip comprising complex out-of-order CPUs, last-level caches, and DRAMs, making system-wide microarchitectural state a first-class resource that can be managed by the OS. We will highlight hardware design implications in different system components and present preliminary experimental results detailing the efficacy and performance overheads of the proposed solution based on extended hardware systems running seL4.

+ YouTube icon   + slides icon
See this talk in the program

@@ -781,6 +836,8 @@

This talk will give an overview of the status of ongoing and planned research and development at Trustworthy Systems to expand the scope of proofs about seL4-based operating systems in two directions: (1) downwards, to prove that the seL4 kernel implements time protection correctly at the abstract and C specification levels, and (2) upwards, to prove functional specifications of seL4's system calls and on that basis carry out SMT-based automated deductive verification of the user-level seL4 Microkit and Lions OS service components built on top of it. Here I will lay out the research and engineering challenges facing us on both these fronts and the planned subprojects for which we seek talented PhD students, postdocs and engineers to tackle them.

+ YouTube icon   + slides icon
See this talk in the program

@@ -804,6 +861,8 @@

We are building Kirsch, a new OS that solves this problem by embracing and formally capturing the heterogeneity and multiple trust domains of modern hardware. To this end, Kirsch formally models what each hardware context can access using a decoding net representation of the platform (Link "Putting out the hardware dumpster fire", https://doi.org/10.1145/3593856.3595903), which induces a trust relationship between contexts. This trust relationship is the basis for reasoning about isolation, protection and authorization in the system. An seL4 instance can run from, and manage, a region of RAM which is explicitly isolated from untrusted contexts in the system, by using the trust an access information we formally derived. Kirsch thus recovers the power of the seL4 correctness proofs, and we can finally use the seL4 kernel to run truly isolated processes and virtual machines.

+ YouTube icon   + slides icon
See this talk in the program

@@ -813,35 +872,56 @@

- mastodon icon - youtube icon - linkedin icon + +mastodon icon +youtube icon +linkedin icon +

- Copyright © 2024 seL4 Project a Series of LF Projects, LLC.
- seL4 is a trademark of LF Projects, LLC.
- For trademark usage guidelines, privacy and cookie policies, - and other applicable policies, as well as terms and conditions - governing this web site, please see - www.lfprojects.org - and the trademark guidelines. + + +Copyright © 2024 seL4 Project a Series of LF Projects, LLC.
+seL4 is a trademark of LF Projects, LLC.
+For trademark usage guidelines, privacy and cookie policies, +and other applicable policies, as well as terms and conditions +governing this web site, please see +www.lfprojects.org +and the trademark guidelines. +
diff --git a/PR_417/Foundation/Summit/2024/cfp.html b/PR_417/Foundation/Summit/2024/cfp.html index 1dd577f6..bb18ee74 100644 --- a/PR_417/Foundation/Summit/2024/cfp.html +++ b/PR_417/Foundation/Summit/2024/cfp.html @@ -313,35 +313,56 @@

- mastodon icon - youtube icon - linkedin icon + +mastodon icon +youtube icon +linkedin icon +

- Copyright © 2024 seL4 Project a Series of LF Projects, LLC.
- seL4 is a trademark of LF Projects, LLC.
- For trademark usage guidelines, privacy and cookie policies, - and other applicable policies, as well as terms and conditions - governing this web site, please see - www.lfprojects.org - and the trademark guidelines. + + +Copyright © 2024 seL4 Project a Series of LF Projects, LLC.
+seL4 is a trademark of LF Projects, LLC.
+For trademark usage guidelines, privacy and cookie policies, +and other applicable policies, as well as terms and conditions +governing this web site, please see +www.lfprojects.org +and the trademark guidelines. +
diff --git a/PR_417/Foundation/Summit/2024/index.html b/PR_417/Foundation/Summit/2024/index.html index 2dde9034..54352204 100644 --- a/PR_417/Foundation/Summit/2024/index.html +++ b/PR_417/Foundation/Summit/2024/index.html @@ -108,9 +108,9 @@

  • Registration
  • Location & Venue
  • Submissions and Call for Presentations
    • -
  • Program & Abstracts
    • +
  • Program, Abstracts, Slides and Videos
  • Keynote Speakers
    • -
  • Latest news: Panel Session
    • +
  • Panel Session
  • Training day @ UNSW
  • Social Activities
  • Program Committee
    • @@ -200,11 +200,7 @@

    Program & Abstracts

    - Check out the summit Program and Abstracts for our list of speakers and presentations. -

    -

    -

    - See the Schedule on LF Events. + Videos of the seL4 summit 2024 are available on the seL4 YouTube channel! Links and slides can be found on the summit Program and Abstracts pages. Thanks to all the speakers for making the seL4 summit 2024 a great success!

    @@ -672,35 +668,56 @@

    - mastodon icon - youtube icon - linkedin icon + +mastodon icon +youtube icon +linkedin icon +

    - Copyright © 2024 seL4 Project a Series of LF Projects, LLC.
    - seL4 is a trademark of LF Projects, LLC.
    - For trademark usage guidelines, privacy and cookie policies, - and other applicable policies, as well as terms and conditions - governing this web site, please see - www.lfprojects.org - and the trademark guidelines. + + +Copyright © 2024 seL4 Project a Series of LF Projects, LLC.
    +seL4 is a trademark of LF Projects, LLC.
    +For trademark usage guidelines, privacy and cookie policies, +and other applicable policies, as well as terms and conditions +governing this web site, please see +www.lfprojects.org +and the trademark guidelines. +
    diff --git a/PR_417/Foundation/Summit/2024/program.html b/PR_417/Foundation/Summit/2024/program.html index 9ae8a72d..9128cf70 100644 --- a/PR_417/Foundation/Summit/2024/program.html +++ b/PR_417/Foundation/Summit/2024/program.html @@ -118,16 +118,18 @@

    Social activities

    Summit

    - + - + + + @@ -136,16 +138,20 @@

    Summit

    + + - + - + + @@ -154,23 +160,19 @@

    Summit

    + + + + - - - - - - - - + @@ -178,6 +180,8 @@

    Summit

    + + @@ -186,6 +190,8 @@

    Summit

    + + @@ -193,6 +199,8 @@

    Summit

    + + @@ -200,9 +208,11 @@

    Summit

    + + - + @@ -210,6 +220,8 @@

    Summit

    + + @@ -218,6 +230,8 @@

    Summit

    + + @@ -225,38 +239,47 @@

    Summit

    + + + + + + - + - + - + - + + - + @@ -264,6 +287,8 @@

    Summit

    + + @@ -272,6 +297,8 @@

    Summit

    + + @@ -279,6 +306,8 @@

    Summit

    + + @@ -286,6 +315,8 @@

    Summit

    + + @@ -293,23 +324,20 @@

    Summit

    + + - - - - - - - - - + + + + @@ -318,6 +346,8 @@

    Summit

    + + @@ -325,6 +355,8 @@

    Summit

    + + @@ -332,9 +364,11 @@

    Summit

    + + - + @@ -342,6 +376,8 @@

    Summit

    + + @@ -350,6 +386,8 @@

    Summit

    + + @@ -357,6 +395,8 @@

    Summit

    + + @@ -364,15 +404,17 @@

    Summit

    + + - + - + - + @@ -381,17 +423,20 @@

    Summit

    + + - + + + - + @@ -399,6 +444,8 @@

    Summit

    + + @@ -406,6 +453,8 @@

    Summit

    + + @@ -413,6 +462,8 @@

    Summit

    + + @@ -420,41 +471,44 @@

    Summit

    + + - - - - - - - - - + + + + - + + + - + + + + + @@ -462,9 +516,11 @@

    Summit

    + + - + @@ -472,6 +528,8 @@

    Summit

    + + @@ -479,6 +537,8 @@

    Summit

    + +
    Day 1 15 October 2024Day 1 15 October 2024
    Session chair
    9:00 - 9:10 Announcements WelcomeYouTube iconslides icon Ihor Kuz
    Industrial Scale Proof Engineering for Critical Trustworthy Applications (INSPECTA)
    Darren Cofer, Collins Aerospace     		YouTube iconslides icon
    BreakBreak
    10:30 - 11:00 TalkseL4 Verification: Status and Plans
    Gerwin Klein, June Andronick, Rafal Kolanski, Gerwin Klein, Corey Lewis, Michael McInerney, +     		seL4 Verification: Status and Plans
    Gerwin Klein, June Andronick, Rafal Kolanski, Corey Lewis, Michael McInerney, Proofcraft     		YouTube iconslides icon Matthew Brecknell
    seL4 multikernel roadmap and concurrency verification
    Gerwin Klein, Corey Lewis, Proofcraft     		YouTube iconslides icon
    11:30 - 12:00 Talk The Neutrality Atoll Hypervisor and the seL4 Multikernel
    David Cock, Mathieu Mirmont, Stevens Le Blond, Neutrality -     		YouTube icon
    LunchLunch
    13:30 - 13:45 Lions OS: Secure, fast, adaptable!
    Gernot Heiser, UNSW Sydney     		YouTube iconslides icon Everton de Matos
    In and Around Lions OS
    Ivan Velickovic, UNSW Sydney     		YouTube iconslides icon
    14:15 - 14:30 The Secure Multiserver Operating System Framework
    Alwin Joshy, Kevin Elphinstone, Gernot Heiser, Craig McLaughlin, UNSW Sydney     		YouTube iconslides icon
    14:30 - 15:00 Running Certified Operating Systems under the seL4 Hypervisor
    Chris Guikema, DornerWorks     		YouTube iconslides icon
    BreakBreak
    15:30 - 16:00 Enhancing seL4’s C/C++ userspace memory safety using CHERI
    Hesham Almatary, Capabilities Limited     		YouTube iconslides icon Gernot Heiser
    Experience Developing Code for the seL4 Environment
    Caitlyn Wilde, Wyeth Greenlaw Rollins, Alain Kägi, Lewis & Clark College     		YouTube iconslides icon
    16:15 - 16:30 Transitioning from CAmkES VMM to MicroKit VMM
    Leigha VanderKlok, DornerWorks     		YouTube iconslides icon
    16:30 - 16:45 Update seL4 Foundation Update
    June Andronick, - seL4 Foundation + seL4 Foundation    		YouTube iconslides icon
    16:45 - 17:00 Gold sponsor Real world needs and applications of seL4
    Boyd Multerer, - Kry10 + Kry10    		YouTube iconslides icon
    Cocktail reception @ Verandah Public 18:00Cocktail reception @ Verandah Public 18:00
    Day 2 16 October 2024Day 2 16 October 2024
    Session chair
    9:00 - 10:00 Panel
    - +     		seL4 Anniversary Panel Session +
    Moderated by Nick Spinale, + Colias Group, LLC     		YouTube iconslides icon Nick Spinale
    BreakBreak
    10:30 - 11:00 First steps towards verification of user-space systems
    Matthew Brecknell, Kry10     		YouTube iconslides icon Darren Cofer
    Generating Trustworthy Hardware/Software I2C Drivers for Board Management Controllers
    Daniel Schwyn, Zikai Liu, Timothy Roscoe, ETH Zurich     		YouTube iconslides icon
    11:30 - 11:45 Using Model Checking to Develop and Verify Inter-Component Signalling Protocols
    Courtney Darville, UNSW Sydney     		YouTube iconslides icon
    11:45 - 12:00 Rust Support in seL4 Userspace: Overview and Update
    Nick Spinale, Colias Group, LLC     		YouTube iconslides icon
    12:00 - 12:15 Pancake: a language for verified systems programming
    Miki Tanaka, Johannes Åman Pohjola, Gernot Heiser UNSW Sydney     		YouTube iconslides icon
    Lunch
    Lunch
    13:45 - 14:15 Talk Assured Reserve Modes
    Ihor Kuz, Kry10, Lance Joneckis, Idaho National Laboratory     		YouTube iconslides icon Robbie VanVossen
    Assured Reserve Modes in Action
    Ihor Kuz, Kry10, Lance Joneckis, Idaho National Laboratory     		YouTube iconslides icon
    14:30 - 14:45 Supporting container applications on Kry10 OS
    Alison Felizzi, Kry10     		YouTube iconslides icon
    14:45 - 15:00 Exploring an seL4-based Trusted Execution Environment in a RISC-V Platform
    Everton de Matos, TII     		YouTube iconslides icon
    BreakBreak
    15:30 - 16:00 Bridging Academia and Industry
    Yanyan Shen, Dhammika Elkaduwe, NIO     		YouTube iconslides icon June Andronick
    seL4 Infrastructure: USB and Beyond
    Bill Ellis, James Nevell, Stephen Williams, Josh Felmeden, Daniel Storer, Tom Harvey, Capgemini     		YouTube iconslides icon
    16:30 - 16:45 Building a Commercial Virtualized Mobile Device with seL4 – Part 3
    Jason Sebranek, Cog Systems, Inc.     		YouTube iconslides icon
    16:45 - 17:00 Doing Nix for seL4: Towards more Infrastructure-as-Code
    Wanja Zaeske, Deutsches Zentrum für Luft- und Raumfahrt (DLR)     		YouTube iconslides icon
    Dinner @ The Butler 18:00Dinner @ The Butler 18:00
    Day 3 17 October 2024Day 3 17 October 2024
    Session chair
    seL4 in Software-Defined Vehicles: Vision, Roadmap, and Impact at NIO
    Ning Qu, NIO     		YouTube iconslides icon Ihor Kuz
    9:50 - 10:00 Announcements
    - -     		Announcements
    June Andronick, + seL4 Foundation    		YouTube icon
    BreakBreak
    10:30 - 11:00 Securing ROS Systems with seL4
    Nathan Studer, Alex Pavey, Zach Clark, DornerWorks, Dariusz Mikulski, Cristian Balas, Yale Empie, US Army - Ground Vehicle Robotics     		YouTube iconslides icon Lucy Parker
    Talk Hardware Support for Time Protection
    Nils Wistoff, ETH Zurich, Gernot Heiser, UNSW Sydney, Luca Benini, ETH Zurich & University of Bologna     		YouTube iconslides icon
    11:15 - 11:45 Verification Status of Time Protection and Microkit-based OS Services
    Robert Sison, UNSW Sydney     		YouTube iconslides icon
    11:45 - 12:15 seL4 as a CPU Driver for an OS for Real Computers
    Roman Meier, Zikai Liu, Ben Fiedler, Timothy Roscoe, ETH Zurich     		YouTube iconslides icon
    Lunch
    Lunch
    13:30 - 13:45 Plenary Discussion, BoF Teasers Ihor Kuz/Nick Spinale
    14:00 - 15:00 Plenary BoFs
    BreakBreak
    15:30 - 16:30 Plenary BoFs Ihor Kuz/Nick Spinale
    16:30 - 16:45 Plenary Report from BoFs + Discussion
    16:45 - 17:00
    Day 4 18 October 2024 Training day @ UNSW Day 4 18 October 2024 Training day @ UNSW 
    10:00 - 12:30 Using LionsOS
    Ivan Velickovic, UNSW Sydney
    14:00 - 16:30 Using Rust in seL4 Userspace
    Nick Spinale, Colias Group, LLC

    @@ -489,35 +549,56 @@

    Summit

    - mastodon icon - youtube icon - linkedin icon + +mastodon icon +youtube icon +linkedin icon +

    - Copyright © 2024 seL4 Project a Series of LF Projects, LLC.
    - seL4 is a trademark of LF Projects, LLC.
    - For trademark usage guidelines, privacy and cookie policies, - and other applicable policies, as well as terms and conditions - governing this web site, please see - www.lfprojects.org - and the trademark guidelines. + + +Copyright © 2024 seL4 Project a Series of LF Projects, LLC.
    +seL4 is a trademark of LF Projects, LLC.
    +For trademark usage guidelines, privacy and cookie policies, +and other applicable policies, as well as terms and conditions +governing this web site, please see +www.lfprojects.org +and the trademark guidelines. +
    diff --git a/PR_417/Foundation/Summit/2024/slides/assured-reserve.pdf b/PR_417/Foundation/Summit/2024/slides/assured-reserve.pdf new file mode 100644 index 00000000..2fe4ed8d Binary files /dev/null and b/PR_417/Foundation/Summit/2024/slides/assured-reserve.pdf differ diff --git a/PR_417/Foundation/Summit/2024/slides/bridging-academia.pdf b/PR_417/Foundation/Summit/2024/slides/bridging-academia.pdf new file mode 100644 index 00000000..acdff6fd Binary files /dev/null and b/PR_417/Foundation/Summit/2024/slides/bridging-academia.pdf differ diff --git a/PR_417/Foundation/Summit/2024/slides/building-commercial.pdf b/PR_417/Foundation/Summit/2024/slides/building-commercial.pdf new file mode 100644 index 00000000..0efd1fb4 Binary files /dev/null and b/PR_417/Foundation/Summit/2024/slides/building-commercial.pdf differ diff --git a/PR_417/Foundation/Summit/2024/slides/camkes-to-microkit.pdf b/PR_417/Foundation/Summit/2024/slides/camkes-to-microkit.pdf new file mode 100644 index 00000000..0c506bbc Binary files /dev/null and b/PR_417/Foundation/Summit/2024/slides/camkes-to-microkit.pdf differ diff --git a/PR_417/Foundation/Summit/2024/slides/cheri-morello.pdf b/PR_417/Foundation/Summit/2024/slides/cheri-morello.pdf new file mode 100644 index 00000000..861ab44e Binary files /dev/null and b/PR_417/Foundation/Summit/2024/slides/cheri-morello.pdf differ diff --git a/PR_417/Foundation/Summit/2024/slides/cpu-driver.pdf b/PR_417/Foundation/Summit/2024/slides/cpu-driver.pdf new file mode 100644 index 00000000..5fb2fa47 Binary files /dev/null and b/PR_417/Foundation/Summit/2024/slides/cpu-driver.pdf differ diff --git a/PR_417/Foundation/Summit/2024/slides/doing-nix.pdf b/PR_417/Foundation/Summit/2024/slides/doing-nix.pdf new file mode 100644 index 00000000..f1718dac Binary files /dev/null and b/PR_417/Foundation/Summit/2024/slides/doing-nix.pdf differ diff --git a/PR_417/Foundation/Summit/2024/slides/experience-developing.pdf b/PR_417/Foundation/Summit/2024/slides/experience-developing.pdf new file mode 100644 index 00000000..6f46c37c Binary files /dev/null and b/PR_417/Foundation/Summit/2024/slides/experience-developing.pdf differ diff --git a/PR_417/Foundation/Summit/2024/slides/exploring-sel4.pdf b/PR_417/Foundation/Summit/2024/slides/exploring-sel4.pdf new file mode 100644 index 00000000..a7b7ab11 Binary files /dev/null and b/PR_417/Foundation/Summit/2024/slides/exploring-sel4.pdf differ diff --git a/PR_417/Foundation/Summit/2024/slides/first-steps.pdf b/PR_417/Foundation/Summit/2024/slides/first-steps.pdf new file mode 100644 index 00000000..f3daf4fd Binary files /dev/null and b/PR_417/Foundation/Summit/2024/slides/first-steps.pdf differ diff --git a/PR_417/Foundation/Summit/2024/slides/foundation-update.pdf b/PR_417/Foundation/Summit/2024/slides/foundation-update.pdf new file mode 100644 index 00000000..db54ec4b Binary files /dev/null and b/PR_417/Foundation/Summit/2024/slides/foundation-update.pdf differ diff --git a/PR_417/Foundation/Summit/2024/slides/generating-trustworthy.pdf b/PR_417/Foundation/Summit/2024/slides/generating-trustworthy.pdf new file mode 100644 index 00000000..d257a384 Binary files /dev/null and b/PR_417/Foundation/Summit/2024/slides/generating-trustworthy.pdf differ diff --git a/PR_417/Foundation/Summit/2024/slides/hardware-support.pdf b/PR_417/Foundation/Summit/2024/slides/hardware-support.pdf new file mode 100644 index 00000000..7818f71a Binary files /dev/null and b/PR_417/Foundation/Summit/2024/slides/hardware-support.pdf differ diff --git a/PR_417/Foundation/Summit/2024/slides/inspecta.pdf b/PR_417/Foundation/Summit/2024/slides/inspecta.pdf new file mode 100644 index 00000000..b31fb52d Binary files /dev/null and b/PR_417/Foundation/Summit/2024/slides/inspecta.pdf differ diff --git a/PR_417/Foundation/Summit/2024/slides/lions-os-practise.pdf b/PR_417/Foundation/Summit/2024/slides/lions-os-practise.pdf new file mode 100644 index 00000000..3bc8b763 Binary files /dev/null and b/PR_417/Foundation/Summit/2024/slides/lions-os-practise.pdf differ diff --git a/PR_417/Foundation/Summit/2024/slides/lions-os.pdf b/PR_417/Foundation/Summit/2024/slides/lions-os.pdf new file mode 100644 index 00000000..ab96a265 Binary files /dev/null and b/PR_417/Foundation/Summit/2024/slides/lions-os.pdf differ diff --git a/PR_417/Foundation/Summit/2024/slides/multikernel-roadmap.pdf b/PR_417/Foundation/Summit/2024/slides/multikernel-roadmap.pdf new file mode 100644 index 00000000..df119538 Binary files /dev/null and b/PR_417/Foundation/Summit/2024/slides/multikernel-roadmap.pdf differ diff --git a/PR_417/Foundation/Summit/2024/slides/pancake.pdf b/PR_417/Foundation/Summit/2024/slides/pancake.pdf new file mode 100644 index 00000000..c1f94ca1 Binary files /dev/null and b/PR_417/Foundation/Summit/2024/slides/pancake.pdf differ diff --git a/PR_417/Foundation/Summit/2024/slides/panel.pdf b/PR_417/Foundation/Summit/2024/slides/panel.pdf new file mode 100644 index 00000000..34dc61bf Binary files /dev/null and b/PR_417/Foundation/Summit/2024/slides/panel.pdf differ diff --git a/PR_417/Foundation/Summit/2024/slides/real-world.pdf b/PR_417/Foundation/Summit/2024/slides/real-world.pdf new file mode 100644 index 00000000..d7479fba Binary files /dev/null and b/PR_417/Foundation/Summit/2024/slides/real-world.pdf differ diff --git a/PR_417/Foundation/Summit/2024/slides/running-certified.pdf b/PR_417/Foundation/Summit/2024/slides/running-certified.pdf new file mode 100644 index 00000000..74229c90 Binary files /dev/null and b/PR_417/Foundation/Summit/2024/slides/running-certified.pdf differ diff --git a/PR_417/Foundation/Summit/2024/slides/rust-support.pdf b/PR_417/Foundation/Summit/2024/slides/rust-support.pdf new file mode 100644 index 00000000..cef3e435 Binary files /dev/null and b/PR_417/Foundation/Summit/2024/slides/rust-support.pdf differ diff --git a/PR_417/Foundation/Summit/2024/slides/secure-multiserver.pdf b/PR_417/Foundation/Summit/2024/slides/secure-multiserver.pdf new file mode 100644 index 00000000..bb172c17 Binary files /dev/null and b/PR_417/Foundation/Summit/2024/slides/secure-multiserver.pdf differ diff --git a/PR_417/Foundation/Summit/2024/slides/securing-ros.pdf b/PR_417/Foundation/Summit/2024/slides/securing-ros.pdf new file mode 100644 index 00000000..2c779ef4 Binary files /dev/null and b/PR_417/Foundation/Summit/2024/slides/securing-ros.pdf differ diff --git a/PR_417/Foundation/Summit/2024/slides/sel4-infrastructure.pdf b/PR_417/Foundation/Summit/2024/slides/sel4-infrastructure.pdf new file mode 100644 index 00000000..18c2c3ee Binary files /dev/null and b/PR_417/Foundation/Summit/2024/slides/sel4-infrastructure.pdf differ diff --git a/PR_417/Foundation/Summit/2024/slides/sel4-verification.pdf b/PR_417/Foundation/Summit/2024/slides/sel4-verification.pdf new file mode 100644 index 00000000..67764543 Binary files /dev/null and b/PR_417/Foundation/Summit/2024/slides/sel4-verification.pdf differ diff --git a/PR_417/Foundation/Summit/2024/slides/software-defined.pdf b/PR_417/Foundation/Summit/2024/slides/software-defined.pdf new file mode 100644 index 00000000..663c97c9 Binary files /dev/null and b/PR_417/Foundation/Summit/2024/slides/software-defined.pdf differ diff --git a/PR_417/Foundation/Summit/2024/slides/supporting-container.pdf b/PR_417/Foundation/Summit/2024/slides/supporting-container.pdf new file mode 100644 index 00000000..f62fad2b Binary files /dev/null and b/PR_417/Foundation/Summit/2024/slides/supporting-container.pdf differ diff --git a/PR_417/Foundation/Summit/2024/slides/using-model.pdf b/PR_417/Foundation/Summit/2024/slides/using-model.pdf new file mode 100644 index 00000000..07b40f7d Binary files /dev/null and b/PR_417/Foundation/Summit/2024/slides/using-model.pdf differ diff --git a/PR_417/Foundation/Summit/2024/slides/verification-status.pdf b/PR_417/Foundation/Summit/2024/slides/verification-status.pdf new file mode 100644 index 00000000..4b0346dd Binary files /dev/null and b/PR_417/Foundation/Summit/2024/slides/verification-status.pdf differ diff --git a/PR_417/Foundation/Summit/2024/slides/welcome.pdf b/PR_417/Foundation/Summit/2024/slides/welcome.pdf new file mode 100644 index 00000000..51c45c97 Binary files /dev/null and b/PR_417/Foundation/Summit/2024/slides/welcome.pdf differ diff --git a/PR_417/Foundation/Summit/2024/social-activities.html b/PR_417/Foundation/Summit/2024/social-activities.html index 43d46b91..04854b3e 100644 --- a/PR_417/Foundation/Summit/2024/social-activities.html +++ b/PR_417/Foundation/Summit/2024/social-activities.html @@ -334,35 +334,56 @@

    A guided tour of the Maritime Museum

    - mastodon icon - youtube icon - linkedin icon + +mastodon icon +youtube icon +linkedin icon +

    - Copyright © 2024 seL4 Project a Series of LF Projects, LLC.
    - seL4 is a trademark of LF Projects, LLC.
    - For trademark usage guidelines, privacy and cookie policies, - and other applicable policies, as well as terms and conditions - governing this web site, please see - www.lfprojects.org - and the trademark guidelines. + + +Copyright © 2024 seL4 Project a Series of LF Projects, LLC.
    +seL4 is a trademark of LF Projects, LLC.
    +For trademark usage guidelines, privacy and cookie policies, +and other applicable policies, as well as terms and conditions +governing this web site, please see +www.lfprojects.org +and the trademark guidelines. +
    diff --git a/PR_417/Foundation/Summit/2024/submit.html b/PR_417/Foundation/Summit/2024/submit.html index c0d06d99..c5a9c439 100644 --- a/PR_417/Foundation/Summit/2024/submit.html +++ b/PR_417/Foundation/Summit/2024/submit.html @@ -125,35 +125,56 @@

    - mastodon icon - youtube icon - linkedin icon + +mastodon icon +youtube icon +linkedin icon +

    - Copyright © 2024 seL4 Project a Series of LF Projects, LLC.
    - seL4 is a trademark of LF Projects, LLC.
    - For trademark usage guidelines, privacy and cookie policies, - and other applicable policies, as well as terms and conditions - governing this web site, please see - www.lfprojects.org - and the trademark guidelines. + + +Copyright © 2024 seL4 Project a Series of LF Projects, LLC.
    +seL4 is a trademark of LF Projects, LLC.
    +For trademark usage guidelines, privacy and cookie policies, +and other applicable policies, as well as terms and conditions +governing this web site, please see +www.lfprojects.org +and the trademark guidelines. +
    diff --git a/PR_417/Foundation/Summit/index.html b/PR_417/Foundation/Summit/index.html index 92b49b8a..5a7bc1ed 100644 --- a/PR_417/Foundation/Summit/index.html +++ b/PR_417/Foundation/Summit/index.html @@ -116,35 +116,56 @@

    - mastodon icon - youtube icon - linkedin icon + +mastodon icon +youtube icon +linkedin icon +

    - Copyright © 2024 seL4 Project a Series of LF Projects, LLC.
    - seL4 is a trademark of LF Projects, LLC.
    - For trademark usage guidelines, privacy and cookie policies, - and other applicable policies, as well as terms and conditions - governing this web site, please see - www.lfprojects.org - and the trademark guidelines. + + +Copyright © 2024 seL4 Project a Series of LF Projects, LLC.
    +seL4 is a trademark of LF Projects, LLC.
    +For trademark usage guidelines, privacy and cookie policies, +and other applicable policies, as well as terms and conditions +governing this web site, please see +www.lfprojects.org +and the trademark guidelines. +
    diff --git a/PR_417/Foundation/Support/index.html b/PR_417/Foundation/Support/index.html index 24954c73..22542803 100644 --- a/PR_417/Foundation/Support/index.html +++ b/PR_417/Foundation/Support/index.html @@ -158,35 +158,56 @@

    - mastodon icon - youtube icon - linkedin icon + +mastodon icon +youtube icon +linkedin icon +

    - Copyright © 2024 seL4 Project a Series of LF Projects, LLC.
    - seL4 is a trademark of LF Projects, LLC.
    - For trademark usage guidelines, privacy and cookie policies, - and other applicable policies, as well as terms and conditions - governing this web site, please see - www.lfprojects.org - and the trademark guidelines. + + +Copyright © 2024 seL4 Project a Series of LF Projects, LLC.
    +seL4 is a trademark of LF Projects, LLC.
    +For trademark usage guidelines, privacy and cookie policies, +and other applicable policies, as well as terms and conditions +governing this web site, please see +www.lfprojects.org +and the trademark guidelines. +
    diff --git a/PR_417/Foundation/TSC/index.html b/PR_417/Foundation/TSC/index.html index 79556ad2..efd324cc 100644 --- a/PR_417/Foundation/TSC/index.html +++ b/PR_417/Foundation/TSC/index.html @@ -260,35 +260,56 @@

    Joining the TSC

    - mastodon icon - youtube icon - linkedin icon + +mastodon icon +youtube icon +linkedin icon +

    - Copyright © 2024 seL4 Project a Series of LF Projects, LLC.
    - seL4 is a trademark of LF Projects, LLC.
    - For trademark usage guidelines, privacy and cookie policies, - and other applicable policies, as well as terms and conditions - governing this web site, please see - www.lfprojects.org - and the trademark guidelines. + + +Copyright © 2024 seL4 Project a Series of LF Projects, LLC.
    +seL4 is a trademark of LF Projects, LLC.
    +For trademark usage guidelines, privacy and cookie policies, +and other applicable policies, as well as terms and conditions +governing this web site, please see +www.lfprojects.org +and the trademark guidelines. +
    diff --git a/PR_417/Foundation/Trademark/index.html b/PR_417/Foundation/Trademark/index.html index a172c5ab..4e54e9ec 100644 --- a/PR_417/Foundation/Trademark/index.html +++ b/PR_417/Foundation/Trademark/index.html @@ -296,35 +296,56 @@

    Updates

    - mastodon icon - youtube icon - linkedin icon + +mastodon icon +youtube icon +linkedin icon +

    - Copyright © 2024 seL4 Project a Series of LF Projects, LLC.
    - seL4 is a trademark of LF Projects, LLC.
    - For trademark usage guidelines, privacy and cookie policies, - and other applicable policies, as well as terms and conditions - governing this web site, please see - www.lfprojects.org - and the trademark guidelines. + + +Copyright © 2024 seL4 Project a Series of LF Projects, LLC.
    +seL4 is a trademark of LF Projects, LLC.
    +For trademark usage guidelines, privacy and cookie policies, +and other applicable policies, as well as terms and conditions +governing this web site, please see +www.lfprojects.org +and the trademark guidelines. +
    diff --git a/PR_417/Foundation/Trademark/logo.html b/PR_417/Foundation/Trademark/logo.html index db7d059b..39d55af4 100644 --- a/PR_417/Foundation/Trademark/logo.html +++ b/PR_417/Foundation/Trademark/logo.html @@ -119,35 +119,56 @@

    - mastodon icon - youtube icon - linkedin icon + +mastodon icon +youtube icon +linkedin icon +

    - Copyright © 2024 seL4 Project a Series of LF Projects, LLC.
    - seL4 is a trademark of LF Projects, LLC.
    - For trademark usage guidelines, privacy and cookie policies, - and other applicable policies, as well as terms and conditions - governing this web site, please see - www.lfprojects.org - and the trademark guidelines. + + +Copyright © 2024 seL4 Project a Series of LF Projects, LLC.
    +seL4 is a trademark of LF Projects, LLC.
    +For trademark usage guidelines, privacy and cookie policies, +and other applicable policies, as well as terms and conditions +governing this web site, please see +www.lfprojects.org +and the trademark guidelines. +
    diff --git a/PR_417/Foundation/index.html b/PR_417/Foundation/index.html index 57330501..7ba79e34 100644 --- a/PR_417/Foundation/index.html +++ b/PR_417/Foundation/index.html @@ -181,35 +181,56 @@

    - mastodon icon - youtube icon - linkedin icon + +mastodon icon +youtube icon +linkedin icon +

    - Copyright © 2024 seL4 Project a Series of LF Projects, LLC.
    - seL4 is a trademark of LF Projects, LLC.
    - For trademark usage guidelines, privacy and cookie policies, - and other applicable policies, as well as terms and conditions - governing this web site, please see - www.lfprojects.org - and the trademark guidelines. + + +Copyright © 2024 seL4 Project a Series of LF Projects, LLC.
    +seL4 is a trademark of LF Projects, LLC.
    +For trademark usage guidelines, privacy and cookie policies, +and other applicable policies, as well as terms and conditions +governing this web site, please see +www.lfprojects.org +and the trademark guidelines. +
    diff --git a/PR_417/Info/FAQ/proof.html b/PR_417/Info/FAQ/proof.html index 0df55065..ce5dc5c3 100644 --- a/PR_417/Info/FAQ/proof.html +++ b/PR_417/Info/FAQ/proof.html @@ -412,35 +412,56 @@

    - mastodon icon - youtube icon - linkedin icon + +mastodon icon +youtube icon +linkedin icon +

    - Copyright © 2024 seL4 Project a Series of LF Projects, LLC.
    - seL4 is a trademark of LF Projects, LLC.
    - For trademark usage guidelines, privacy and cookie policies, - and other applicable policies, as well as terms and conditions - governing this web site, please see - www.lfprojects.org - and the trademark guidelines. + + +Copyright © 2024 seL4 Project a Series of LF Projects, LLC.
    +seL4 is a trademark of LF Projects, LLC.
    +For trademark usage guidelines, privacy and cookie policies, +and other applicable policies, as well as terms and conditions +governing this web site, please see +www.lfprojects.org +and the trademark guidelines. +
    diff --git a/PR_417/Info/Website/index.html b/PR_417/Info/Website/index.html index f360a69c..b214ce7d 100644 --- a/PR_417/Info/Website/index.html +++ b/PR_417/Info/Website/index.html @@ -141,35 +141,56 @@

    - mastodon icon - youtube icon - linkedin icon + +mastodon icon +youtube icon +linkedin icon +

    - Copyright © 2024 seL4 Project a Series of LF Projects, LLC.
    - seL4 is a trademark of LF Projects, LLC.
    - For trademark usage guidelines, privacy and cookie policies, - and other applicable policies, as well as terms and conditions - governing this web site, please see - www.lfprojects.org - and the trademark guidelines. + + +Copyright © 2024 seL4 Project a Series of LF Projects, LLC.
    +seL4 is a trademark of LF Projects, LLC.
    +For trademark usage guidelines, privacy and cookie policies, +and other applicable policies, as well as terms and conditions +governing this web site, please see +www.lfprojects.org +and the trademark guidelines. +
    diff --git a/PR_417/Info/index.html b/PR_417/Info/index.html index 7e942fd4..a2feef83 100644 --- a/PR_417/Info/index.html +++ b/PR_417/Info/index.html @@ -139,35 +139,56 @@

    - mastodon icon - youtube icon - linkedin icon + +mastodon icon +youtube icon +linkedin icon +

    - Copyright © 2024 seL4 Project a Series of LF Projects, LLC.
    - seL4 is a trademark of LF Projects, LLC.
    - For trademark usage guidelines, privacy and cookie policies, - and other applicable policies, as well as terms and conditions - governing this web site, please see - www.lfprojects.org - and the trademark guidelines. + + +Copyright © 2024 seL4 Project a Series of LF Projects, LLC.
    +seL4 is a trademark of LF Projects, LLC.
    +For trademark usage guidelines, privacy and cookie policies, +and other applicable policies, as well as terms and conditions +governing this web site, please see +www.lfprojects.org +and the trademark guidelines. +
    diff --git a/PR_417/Info/more-research.html b/PR_417/Info/more-research.html index ad0799ed..41d6f363 100644 --- a/PR_417/Info/more-research.html +++ b/PR_417/Info/more-research.html @@ -259,35 +259,56 @@

    - mastodon icon - youtube icon - linkedin icon + +mastodon icon +youtube icon +linkedin icon +

    - Copyright © 2024 seL4 Project a Series of LF Projects, LLC.
    - seL4 is a trademark of LF Projects, LLC.
    - For trademark usage guidelines, privacy and cookie policies, - and other applicable policies, as well as terms and conditions - governing this web site, please see - www.lfprojects.org - and the trademark guidelines. + + +Copyright © 2024 seL4 Project a Series of LF Projects, LLC.
    +seL4 is a trademark of LF Projects, LLC.
    +For trademark usage guidelines, privacy and cookie policies, +and other applicable policies, as well as terms and conditions +governing this web site, please see +www.lfprojects.org +and the trademark guidelines. +
    diff --git a/PR_417/Learn/index.html b/PR_417/Learn/index.html index 76ab1e32..6c520780 100644 --- a/PR_417/Learn/index.html +++ b/PR_417/Learn/index.html @@ -194,35 +194,56 @@

    Courses

    - mastodon icon - youtube icon - linkedin icon + +mastodon icon +youtube icon +linkedin icon +

    - Copyright © 2024 seL4 Project a Series of LF Projects, LLC.
    - seL4 is a trademark of LF Projects, LLC.
    - For trademark usage guidelines, privacy and cookie policies, - and other applicable policies, as well as terms and conditions - governing this web site, please see - www.lfprojects.org - and the trademark guidelines. + + +Copyright © 2024 seL4 Project a Series of LF Projects, LLC.
    +seL4 is a trademark of LF Projects, LLC.
    +For trademark usage guidelines, privacy and cookie policies, +and other applicable policies, as well as terms and conditions +governing this web site, please see +www.lfprojects.org +and the trademark guidelines. +
    diff --git a/PR_417/Use/index.html b/PR_417/Use/index.html index 4438a84b..b544949d 100644 --- a/PR_417/Use/index.html +++ b/PR_417/Use/index.html @@ -178,35 +178,56 @@

    - mastodon icon - youtube icon - linkedin icon + +mastodon icon +youtube icon +linkedin icon +

    - Copyright © 2024 seL4 Project a Series of LF Projects, LLC.
    - seL4 is a trademark of LF Projects, LLC.
    - For trademark usage guidelines, privacy and cookie policies, - and other applicable policies, as well as terms and conditions - governing this web site, please see - www.lfprojects.org - and the trademark guidelines. + + +Copyright © 2024 seL4 Project a Series of LF Projects, LLC.
    +seL4 is a trademark of LF Projects, LLC.
    +For trademark usage guidelines, privacy and cookie policies, +and other applicable policies, as well as terms and conditions +governing this web site, please see +www.lfprojects.org +and the trademark guidelines. +
    diff --git a/PR_417/contact/index.html b/PR_417/contact/index.html index 2c83f677..81b3ef31 100644 --- a/PR_417/contact/index.html +++ b/PR_417/contact/index.html @@ -172,35 +172,56 @@

    Website Issues

    - mastodon icon - youtube icon - linkedin icon + +mastodon icon +youtube icon +linkedin icon +

    - Copyright © 2024 seL4 Project a Series of LF Projects, LLC.
    - seL4 is a trademark of LF Projects, LLC.
    - For trademark usage guidelines, privacy and cookie policies, - and other applicable policies, as well as terms and conditions - governing this web site, please see - www.lfprojects.org - and the trademark guidelines. + + +Copyright © 2024 seL4 Project a Series of LF Projects, LLC.
    +seL4 is a trademark of LF Projects, LLC.
    +For trademark usage guidelines, privacy and cookie policies, +and other applicable policies, as well as terms and conditions +governing this web site, please see +www.lfprojects.org +and the trademark guidelines. +
    diff --git a/PR_417/css/sel4.css b/PR_417/css/sel4.css index 6ae498ad..e8468121 100644 --- a/PR_417/css/sel4.css +++ b/PR_417/css/sel4.css @@ -558,6 +558,11 @@ font-weight:bold; } + /* yellow background for TBD tasks (used during development) */ + .tbd { + background-color: yellow; + } + .emph { color:#668B37; /* greenDark */ } diff --git a/PR_417/index.html b/PR_417/index.html index 3c804188..12d4039c 100644 --- a/PR_417/index.html +++ b/PR_417/index.html @@ -102,19 +102,19 @@