Skip to content

Reduce/eliminate unsafe code in the shims #560

@jstarks

Description

@jstarks

In order to make useful safety claims about LiteBox as a whole, I think we need to better layer our use of unsafe across the LiteBox stack. Considering the four layers:

  • Platform code requires lots of unsafe, since it is integrating with OS primitives that the Rust borrow checker and even Verus cannot easily reason about.
  • Runner code's use of unsafe depends on how well the associated platform manages to provide safe methods on top of the unsafe code.
  • litebox code requires unsafe to implement mutexes and other low-level data structures... but this type of code is probably formally verifiable via Verus.
  • Shim code should require no unsafe code--it should be built on top of abstractions provided by litebox.

This issue is most concerned with shim code. We should drive all uses of unsafe out of the shims and into litebox.

The biggest offender is user-mode memory access. We will need to consider #505 as part of this.

Metadata

Metadata

Assignees

No one assigned

    Labels

    layer-shimFocusing on one or more shims / "north" of LiteBox itself

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions