seL4 for USB mass storage

Hi all,

My group is currently working on the DARPA TWISTED[0] program, where we are working
to develop an seL4-based verified secure boot for USB mass storage devices. I’m very new to
seL4, so I have some basic questions:

  1. Are there any other projects that have used seL4 in a USB device that we could use for reference?
  2. What is the process for interfacing with USB device-side PHYs on seL4? Are there existing drivers for this? Or is this typically handled in a Linux VM?
  3. Are there flash storage drivers for seL4? Or is a Linux VM used for this?
  4. Is it possible to run Linux on top of seL4 without hardware virt extensions (a la Xen PV)?

Thanks,
Connor

[0] Trust Worthy Information Storage Technology Enhanced Devices (TWISTED) | SBIR.gov