Roadmap

[CharlyCst]

Roadmap

The goal of this issue is to keep track of the various directions the project is pursuing:

• Trusted Boot
• Formal Verification
• Multi-core Support
• Virtual Machines
• Risc-V
• Tyche API & Drivers

Trusted Boot

• We can boot on a real laptop.
• We have a good understanding of what Trusted Boot implies for single core.
• We can emulate basic GETSEC instructions.

Formal Verification

• We investigated Serval (assembly-level verification).
  • We can use it with Rust.
  • Hard to use in practice (hard to write and understand specs, requires Racket).
  • Has the finite interface constraint.
  • Can not create function contract (i.e. end-to-end verification of functions without re-use of proved invariant).
• We started investigating Creusot (source-level verification).
  • Can be used to annotate Rust code out of the box.
  • Support for higher level constructs.
  • Required to write Why3 proofs, not clear to me how easy it is in practice.

Multi-code Support

• We can wake up other cores and switch to protected long mode.
• We can setup a proper environment (stack, GDT/IDT) for other cores.

Virtual Machines

We need to start investigating.

Risc-V

• We can jump into Rust code from OpenSBI and print from there.

Tyche API & Drivers

• We have a first version of the API that supports creating and managing regions.
• We can create and destroy enclaves using a driver in the guest Linux.