Existing Platforms and Capabilities
Trusted ST
Platforms and Capabilities with Formal Methods based Evidence of Trust
Organization | Architecture | HW Platform | Software Stack | Capabilities | Maturity/Availability |
Trusted ST | ARM | Xilinx Ultrascale+ MPSoC/ZCU-102 | Agile resilient embedded systems (ARES) stack–VMM, guest OS & apps, security services (monitor, policy, recovery) | Security servicesUAV swarmCrypto librariesDDS | Relevant simulation-based flight testing
Available for capability demonstration
Government-off-the-shelf
Not turnkey for end user |
Trusted ST | ARM | Raspberry Pi-4 | Basic seL4 porting without VMM support done by Trusted ST | seL4 testing | Benchtop test
Available for capability demonstration
Government-off-the-shelf
Not turnkey for end user |
Trusted ST | ARM | GE Aviation M-100 mission computer | ARES software stack + GE Aviation flight management software | Security servicesCrypto libraries | Fixed-wing flight tests using mission-relevant scenarios and realistic attacks
Available for capability demonstration
Government-off-the-shelf
Not turnkey solution |
Trusted ST | ARM | GE Aviation M-series mission computer | ARES software stack + GE Aviation flight management software | Security servicesUAV swarmCrypto librariesDDS | Relevant simulation-based flight testing
Available for capability demonstration
Government-off-the-shelf
Not turnkey for end user |
Trusted ST | ARM - Morello | ARM Morello System | ARES software stack + GE Aviation flight management software | Security services with CHERI UAV swarmCrypto librariesDDS | Workflow integrationRelevant simulation-based flight testing – in progress
Available for capability demonstration
Government-off-the-shelf
Not turnkey for end user |
Trusted ST | x86 | NUVO -7000 | ARES software stack + GE Aviation flight management software | Security servicesIDS (e.g., Snort) | Benchtop testingAvailable for capability demonstration
Government-off-the-shelf
Not turnkey for end user |
Trusted ST | RISC-V | PolarFire Icicle SoCQEMU | ARES software stack with VMM | Security servicesJust-In-Time execution | Benchtop testingAvailable for capability demonstration
Government-off-the-shelf
Not turnkey for end user |
*This software is a modification of seL4®, not seL4 itself, and has not been formally verified by the seL4 Foundation https://sel4.systems/Foundation/ or their authorized agents. Versions of the official seL4 code, some configurations of which have been formally verified by them, are freely available from their repository at https://github.com/seL4/seL4 and their open source release is gratefully acknowledged.
DornerWorks
Supported seL4-based Platforms and Capabilities – March 2024
Organization | Architecture | HW Platform | Software Stack | Capabilities | Maturity/Availability |
DornerWorks | ARM | Collins Aerospace VPM | seL4 software stack – DornerWorks VMM, guest OS & apps, Cyber resiliency component, VM Container support (DevSecOps) | Cyber resilienceSecure BootNIDS, MulticoreGuests: Deos, VxWorks7, Linux, RTEMS, FreeRTOS, 64 or 32-bit High-performance inter-VM communication | Demonstrated on fieldable hardware for SBIR
Available for capability demonstration
Government-off-the-shelf
Turnkey |
DornerWorks | ARM | DornerWorks ARM North Atlantic Industries (NAI) 68ARM2 (AMD Ultrascale+ MPSoC Based) | seL4 software stack – DornerWorks VMM, guest OS & apps, Cyber resiliency component, VM Container support (DevSecOps) | Cyber resilienceSecure BootNIDS, MulticoreGuests: Deos, VxWorks7, Linux, RTEMS, FreeRTOS, 64 or 32-bit High-performance inter-VM communication | Demonstrated on fieldable hardware
Available for capability demonstration
Government-off-the-shelf
Turnkey |
DornerWorks | ARM | UEI Zynq(AMD Ultrascale+ MPSoC Based) | seL4 software stack – DornerWorks VMM, guest OS & apps, Health Monitor Framework | MulticoreGuests: Linux, PREEMPT_RT Linux | Demonstrated on fieldable hardware Available for capability demonstration Government-off-the-shelf Turnkey |
DornerWorks | ARM | AMD/Xilinx Ultrascale+ MPSoC:ZCU102Ultra96v2GenesysZUZCU208 | seL4 software stack – DornerWorks VMM, guest OS & apps, Cyber resiliency component, VM Container support (DevSecOps) | Cyber resilienceSecure BootNIDS, MulticoreGuests: Deos, VxWorks7, Linux, RTEMS, FreeRTOS, 64 or 32-bit High-performance inter-VM communication | Demonstrated on Lab hardware Available for capability demonstration Government-off-the-shelf Turnkey |
DornerWorks | ARM | Nvidia TX2 developer kitNvidia TX2-NX SOM on Jetson Nano kit | seL4 software stack – DornerWorks VMM, guest OS & apps | MulticoreGuests: LinuxGPU, Camera, Display pass-through | Demonstrated on Lab hardware Available for capability demonstration Government-off-the-shelf Turnkey |
DornerWorks | ARM | AMD Versal:VCK190 (AI Core) | seL4 software stack – DornerWorks VMM, guest OS & apps | MulticoreGuests: Linux, RTEMS, FreeRTOS | Demonstrated on Lab hardware Available for capability demonstration Government-off-the-shelf Turnkey |
DornerWorks | x86 | NUVO-7000 | seL4 software stack – DornerWorks VMM, guest OS & apps | Multicore64-bit guests: Standard Linux, Ubuntu 20i210 network driver and bridge component | Demonstrated on fieldable hardware
Available for capability demonstration
Government-off-the-shelf
Not Turnkey |
DornerWorks | x86 | Versalogic Blackbird | seL4 software stack – DornerWorks VMM, guest OS & apps | Multicore64-bit guests: Standard Linux, RedHat, Cent OSi210 network 1553 Passthrough | Demonstrated on fieldable hardware Available for capability demonstration Government-off-the-shelf Not Turnkey |
DornerWorks | x86 | DellOptiPlex Micro 7020 | seL4 software stack – DornerWorks VMM, guest OS & apps | Multicore64-bit guests: Standard Linux, Rocky, Ubuntu 20i210 network driver and bridge component | Demonstrated on Lab hardware Available for capability demonstration Government-off-the-shelf Not Turnkey |
DornerWorks | RISC-V | Microchip PolarFire SoC Icicle Kit | seL4 software stack without VMM | Demonstrated on Lab hardware Available for capability demonstration Government-off-the-shelf Not Turnkey | |
DornerWorks | RISC-V | Rocket-Chip (Soft-core) | seL4 software stack with VMM | Soft-core with virtualization extensions | Demonstrated on Lab hardware Available for capability demonstration Government-off-the-shelf Not Turnkey |
*This software is a modification of seL4®, not seL4 itself, and has not been formally verified by the seL4 Foundation https://sel4.systems/Foundation/ or their authorized agents. Versions of the official seL4 code, some configurations of which have been formally verified by them, are freely available from their repository at https://github.com/seL4/seL4 and their open source release is gratefully acknowledged.