Skip to content

Commit

Permalink
auto-deployed
Browse files Browse the repository at this point in the history
  • Loading branch information
@seL4-ci
seL4-ci committed Oct 15, 2024
1 parent 9f5fe31 commit a9871a7
Show file tree
Hide file tree
Showing 3 changed files with 152 additions and 152 deletions.
26 changes: 13 additions & 13 deletions Foundation/Summit/2024/abstracts2024.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -308,28 +308,25 @@ <h4 class="summit-abstract-title">

<br><a href="program#p-running-certified">See this talk in the program</a></div>

<div class="summit-abstract" id="a-securing-ros"><!--<title>Summit abstract</title>-->
<div class="summit-abstract" id="a-cheri-morello"><!--<title>Summit abstract</title>-->
<!--
Copyright 2024, seL4 summit authors (see abstracts)
SPDX-License-Identifier: CC-BY-SA-4.0
-->
<h4 class="summit-abstract-title">
Securing ROS Systems with seL4
Enhancing seL4’s C/C++ userspace memory safety using CHERI
</h4>
<p class="summit-abstract-type">
Talk
</p>
<p class="summit-abstract-author">
Presented by Nathan Studer, <span class="summit-abstract-affiliation">DornerWorks</span>
</p>
<p>
ROS (Robotic Operating System), a modular componentized architecture for robot applications, has made it possible to quickly develop and deploy systems utilizing autonomous or human guided robots. Focusing on ease of use and portability, ROS has enabled a community of developers to create autonomy solutions that were previously restricted to well-funded companies. However, ROS depends on many services included in a full Linux distribution to function properly. Beyond the Operating System itself, these distributions contain many unvetted software packages, which when used in high assurance environments, such as factory automation, could present an unacceptable amount of overhead and potential vulnerabilities.
Presented by Hesham Almatary, <span class="summit-abstract-affiliation">Capabilities Limited</span>
</p>
<p>
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.
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.
</p>

<br><a href="program#p-securing-ros">See this talk in the program</a></div>
<br><a href="program#p-cheri-morello">See this talk in the program</a></div>

<div class="summit-abstract" id="a-experience-developing"><!--<title>Summit abstract</title>-->
<!--
Expand Down Expand Up @@ -722,25 +719,28 @@ <h4 class="summit-abstract-title">
</p>
<br><a href="program#p-software-defined">See this talk in the program</a></div>

<div class="summit-abstract" id="a-cheri-morello"><!--<title>Summit abstract</title>-->
<div class="summit-abstract" id="a-securing-ros"><!--<title>Summit abstract</title>-->
<!--
Copyright 2024, seL4 summit authors (see abstracts)
SPDX-License-Identifier: CC-BY-SA-4.0
-->
<h4 class="summit-abstract-title">
Enhancing seL4’s C/C++ userspace memory safety using CHERI
Securing ROS Systems with seL4
</h4>
<p class="summit-abstract-type">
Talk
</p>
<p class="summit-abstract-author">
Presented by Hesham Almatary, <span class="summit-abstract-affiliation">Capabilities Limited</span>
Presented by Nathan Studer, <span class="summit-abstract-affiliation">DornerWorks</span>
</p>
<p>
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.
ROS (Robotic Operating System), a modular componentized architecture for robot applications, has made it possible to quickly develop and deploy systems utilizing autonomous or human guided robots. Focusing on ease of use and portability, ROS has enabled a community of developers to create autonomy solutions that were previously restricted to well-funded companies. However, ROS depends on many services included in a full Linux distribution to function properly. Beyond the Operating System itself, these distributions contain many unvetted software packages, which when used in high assurance environments, such as factory automation, could present an unacceptable amount of overhead and potential vulnerabilities.
</p>
<p>
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.
</p>

<br><a href="program#p-cheri-morello">See this talk in the program</a></div>
<br><a href="program#p-securing-ros">See this talk in the program</a></div>

<div class="summit-abstract" id="a-hardware-support"><!--<title>Summit abstract</title>-->
<!--
Expand Down
14 changes: 7 additions & 7 deletions Foundation/Summit/2024/program.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -206,11 +206,11 @@ <h4>Summit</h4>
<tr>
<td class="break" colspan="4">Break</td>
</tr>
<tr id="p-securing-ros">
<tr id="p-cheri-morello">
<td>15:30 - 16:00</td>
<td>Talk</td>
<td><a href="abstracts2024.html#a-securing-ros">Securing ROS Systems with seL4</a><br><span class="summit-abstract-presenter">Nathan Studer, Alex Pavey, Zach Clark</span>, <span class="summit-abstract-affiliation">DornerWorks</span>, <span class="summit-abstract-presenter">Dariusz Mikulski, Cristian Balas, Yale Empie</span>,
<span class="summit-abstract-affiliation">US Army - Ground Vehicle Robotics</span>
<td><a href="abstracts2024.html#a-cheri-morello">Enhancing seL4’s C/C++ userspace memory safety using CHERI</a><br><span class="summit-abstract-presenter">Hesham Almatary</span>,
<span class="summit-abstract-affiliation">Capabilities Limited</span>
</td>
<td class="summit_chair" rowspan="5">Gernot Heiser</td>
</tr>
Expand Down Expand Up @@ -266,7 +266,7 @@ <h4>Summit</h4>
<td><a href="abstracts2024.html#a-first-steps">First steps towards verification of user-space systems</a><br><span class="summit-abstract-presenter">Matthew Brecknell</span>,
<span class="summit-abstract-affiliation">Kry10</span>
</td>
<td class="summit_chair" rowspan="5">Gerwin Klein</td>
<td class="summit_chair" rowspan="5">Darren Cofer</td>
</tr>
<tr id="p-generating-trustworthy">
<td>11:00 - 11:30</td>
Expand Down Expand Up @@ -395,11 +395,11 @@ <h4>Summit</h4>
<tr>
<td class="break" colspan="4">Break</td>
</tr>
<tr id="p-cheri-morello">
<tr id="p-securing-ros">
<td>10:30 - 11:00</td>
<td>Talk</td>
<td><a href="abstracts2024.html#a-cheri-morello">Enhancing seL4’s C/C++ userspace memory safety using CHERI</a><br><span class="summit-abstract-presenter">Hesham Almatary</span>,
<span class="summit-abstract-affiliation">Capabilities Limited</span>
<td><a href="abstracts2024.html#a-securing-ros">Securing ROS Systems with seL4</a><br><span class="summit-abstract-presenter">Nathan Studer, Alex Pavey, Zach Clark</span>, <span class="summit-abstract-affiliation">DornerWorks</span>, <span class="summit-abstract-presenter">Dariusz Mikulski, Cristian Balas, Yale Empie</span>,
<span class="summit-abstract-affiliation">US Army - Ground Vehicle Robotics</span>
</td>
<td class="summit_chair" rowspan="4">Lucy Parker</td>
</tr>
Expand Down
Loading

0 comments on commit a9871a7

Please sign in to comment.