diff --git a/Foundation/Summit/2024/abstracts2024.html b/Foundation/Summit/2024/abstracts2024.html index c1fa9318..4651f7f7 100644 --- a/Foundation/Summit/2024/abstracts2024.html +++ b/Foundation/Summit/2024/abstracts2024.html @@ -308,28 +308,25 @@


See this talk in the program -
+

- Securing ROS Systems with seL4 + Enhancing seL4’s C/C++ userspace memory safety using CHERI

Talk

- Presented by Nathan Studer, DornerWorks -

-

- 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, Capabilities Limited

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

-
See this talk in the program
+
See this talk in the program
+

- Enhancing seL4’s C/C++ userspace memory safety using CHERI + Securing ROS Systems with seL4

Talk

- Presented by Hesham Almatary, Capabilities Limited + Presented by Nathan Studer, DornerWorks

- 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. +

+

+ 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.

-
See this talk in the program
+
See this talk in the program