Share this link via
Or copy link
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.
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.
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.
There are several challenges in implementing reserve modes in systems. The first challenge is developing a mechanism for defining and loading all modes into a system at boot time and enabling alternative modes as necessary. The second challenge is making these changes without affecting or disturbing parts of the system not involved in the reserve modes. The final and hardest challenge is being able to perform such system level changes with assurance that the reserve modes will be enabled as required and operate as expected, without modification.
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.
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.
We present the Kry10 OS design and implementation of assured reserve modes, demonstrating their application to a representaive industrial control system (based on the Fischertechnik Training Factory 4.0). The system is exposed to security and safety incidents, which it will detect and then switch into appropriate reserve modes in order to mitigate, resolve, or contain the problem.
This presentation is a companion to the Assured Reserve Modes presentation that describes the assured reserve mode model and mechanism itself.