Untitled Project
WASM Interpreter for Safety - Requirements
1. Functional Requirements
1.1. Resumable UID: REQ-1 child relations: STATEMENT:

The interpreter shall be resumable

RATIONALE:

Operation with fuel or other implementations of bounded run-time requires that the interpreter can be halted. Conversely, later on the interpreter may be resumed, as if it was not halted in the first place.

  • 1.6.1. Stackless UID: REQ-2 parent relations: STATEMENT:

    The interpreter shall be stackless

    RATIONALE:

    A stackless interpreter is one that does not use function calls in the host environment to implement function calls inside the interpreter. Instead, the stack of the interpreted bytecode is stored in a traditional data structure (such as a Vec<u8>). Interpretation can be interrupted between any two virtual instructions of the bytecode, and crucially so resumed from there.

    Further information: https://kyju.org/blog/piccolo-a-stackless-lua-interpreter/#a-stackless-interpreter-design

1.2. Baremetal UID: REQ-3 child relations: STATEMENT:

The interpreter shall be executable on bare-metal environments

RATIONALE:

No reliance on any specific functionality from the provided execution environment is acceptable, as the interpreter shall be ready for embedding to any environment that Rust can compile for.

  • 1.6.2. no_std UID: REQ-4 parent relations: STATEMENT:

    The interpreter shall be implemented in no_std Rust

    RATIONALE:

    Only relying on the functionality that is provided by no_std enables execution on bare environments where operating system is available.

    COMMENT:

    Reliance on alloc is allowable, as an allocator can be implemented without further reliance on the execution environment.

1.3. Bounded execution UID: REQ-5 child relations: STATEMENT:

The interpreter shall yield back control flow eventually

RATIONALE:

A user shall be able to call the interpreter with a bound, expecting a result in a finite amount of time or bytecode operations. Even if the bytecode itself does never finish execution (i.e. due to a infinite loop), the interpreter shall yield eventually, by pausing the bytecode execution.

COMMENT:

It is not acceptable to constraint the interpreter to only those bytecode instances for which the halting-problem is solvable.

  • 1.6.3. Fuel UID: REQ-6 parent relations: STATEMENT:

    The interpreter shall support fuel bounded execution

    RATIONALE:

    Fuel is a mechanism to limit the amount of bytecode operations conducted when calling the interpreter. Each bytecode instruction is associated with a specific amount of fuel consumed when executing it. The interpreter is provided a finite amount of fuel, that is deplete during execution, until the amount of fuel is insufficient to conduct further bytecode operations. At this point, the interpreter yields back the control flow. Later on, the execution may be resumed.

    Further information: https://docs.rs/wasmtime/latest/wasmtime/struct.Config.html#method.consume_fuel

1.4. Migrateable UID: REQ-12 child relations: STATEMENT:

The interpreter state shall be able to halt on one computer and continue execution on another

RATIONALE:

This enables various workflows in deployments of multiple computers. For load-balancing or redundancy purposes, running applications can be migrated to other computers without disruption.

  • 1.6.4. De-/Serializable UID: REQ-13 parent relations: STATEMENT:

    The interpreter state shall be de-/serializable

    RATIONALE:

    If the interpreter state can be serialized to and deserialized from a canonical representation, migration to other computers as well as check-point/lock-step like execution become simple to implement.

1.5. No Dependencies UID: REQ-14 child relations: STATEMENT:

No dependencies but those explicitly allowed by a requirement shall be used

RATIONALE:

Dependencies have to forego the full V&V process as well, which quickly adds enormous work.

COMMENT:

This requirement constraints the usage and introduction of normal dependencies, but not Dev Dependencies [1] and not Build Dependencies [2] .

[1]https://doc.rust-lang.org/cargo/reference/specifying-dependencies.html#development-dependencies
[2]https://doc.rust-lang.org/cargo/reference/specifying-dependencies.html#build-dependencies
COMMENT:

Exceptions to this, i.e. allowed dependencies, must refer to this requirement as their parent.

COMMENT:

All requirements that allow a dependency must specify the exact version of the dependency (at least major, minor and patch release)

  • 1.6.5. Allow log dependency UID: REQ-15 parent relations: STATEMENT:

    The interpreter shall have an optional dependency on the log crate version 0.4.22

    RATIONALE:

    Logging is an essential tool to make a system observable, and aid in debugging. Bespoke crate is widely used in the Rust ecosystem and can be attached to any (or no) logging backend. Using conditional compilation, all of the log crate's footprint in the WASM interpreter (foremost the debug, error, info, trace and warn macro) can be expanded to empty statements to avoid any run-time impact when opting out of the dependency on log.

  • 1.6.6. Allow libm dependency UID: REQ-16 parent relations: STATEMENT:

    The interpreter may depend on the libm crate version 0.2.8

    RATIONALE:

    Rust does not expose all floating point operations in a bare-metal (as in no_std) target, as to not introduce any dependency on the C standard library's libm (respective PR: https://github.com/rust-lang/rust/pull/27823). However, we identified at least the following operations to be required for WASM interpretation while unavailable in no_std:

    • abs
    • ceil
    • floor
    • trunc
    • round
    • sqrt
    • copysign

    In order use these operations, having the libm crate as dependencies of the WASM interpreter is an acceptable trade-off.

1.6. Low-Level Functional Requirements
  • 1.1. Resumable UID: REQ-1 child relations: STATEMENT:

    The interpreter shall be resumable

    RATIONALE:

    Operation with fuel or other implementations of bounded run-time requires that the interpreter can be halted. Conversely, later on the interpreter may be resumed, as if it was not halted in the first place.

1.6.1. Stackless UID: REQ-2 parent relations: STATEMENT:

The interpreter shall be stackless

RATIONALE:

A stackless interpreter is one that does not use function calls in the host environment to implement function calls inside the interpreter. Instead, the stack of the interpreted bytecode is stored in a traditional data structure (such as a Vec<u8>). Interpretation can be interrupted between any two virtual instructions of the bytecode, and crucially so resumed from there.

Further information: https://kyju.org/blog/piccolo-a-stackless-lua-interpreter/#a-stackless-interpreter-design

  • 1.2. Baremetal UID: REQ-3 child relations: STATEMENT:

    The interpreter shall be executable on bare-metal environments

    RATIONALE:

    No reliance on any specific functionality from the provided execution environment is acceptable, as the interpreter shall be ready for embedding to any environment that Rust can compile for.

1.6.2. no_std UID: REQ-4 parent relations: STATEMENT:

The interpreter shall be implemented in no_std Rust

RATIONALE:

Only relying on the functionality that is provided by no_std enables execution on bare environments where operating system is available.

COMMENT:

Reliance on alloc is allowable, as an allocator can be implemented without further reliance on the execution environment.

  • 1.3. Bounded execution UID: REQ-5 child relations: STATEMENT:

    The interpreter shall yield back control flow eventually

    RATIONALE:

    A user shall be able to call the interpreter with a bound, expecting a result in a finite amount of time or bytecode operations. Even if the bytecode itself does never finish execution (i.e. due to a infinite loop), the interpreter shall yield eventually, by pausing the bytecode execution.

    COMMENT:

    It is not acceptable to constraint the interpreter to only those bytecode instances for which the halting-problem is solvable.

1.6.3. Fuel UID: REQ-6 parent relations: STATEMENT:

The interpreter shall support fuel bounded execution

RATIONALE:

Fuel is a mechanism to limit the amount of bytecode operations conducted when calling the interpreter. Each bytecode instruction is associated with a specific amount of fuel consumed when executing it. The interpreter is provided a finite amount of fuel, that is deplete during execution, until the amount of fuel is insufficient to conduct further bytecode operations. At this point, the interpreter yields back the control flow. Later on, the execution may be resumed.

Further information: https://docs.rs/wasmtime/latest/wasmtime/struct.Config.html#method.consume_fuel

  • 1.4. Migrateable UID: REQ-12 child relations: STATEMENT:

    The interpreter state shall be able to halt on one computer and continue execution on another

    RATIONALE:

    This enables various workflows in deployments of multiple computers. For load-balancing or redundancy purposes, running applications can be migrated to other computers without disruption.

1.6.4. De-/Serializable UID: REQ-13 parent relations: STATEMENT:

The interpreter state shall be de-/serializable

RATIONALE:

If the interpreter state can be serialized to and deserialized from a canonical representation, migration to other computers as well as check-point/lock-step like execution become simple to implement.

1.6.5. Allow log dependency UID: REQ-15 parent relations: STATEMENT:

The interpreter shall have an optional dependency on the log crate version 0.4.22

RATIONALE:

Logging is an essential tool to make a system observable, and aid in debugging. Bespoke crate is widely used in the Rust ecosystem and can be attached to any (or no) logging backend. Using conditional compilation, all of the log crate's footprint in the WASM interpreter (foremost the debug, error, info, trace and warn macro) can be expanded to empty statements to avoid any run-time impact when opting out of the dependency on log.

1.6.6. Allow libm dependency UID: REQ-16 parent relations: STATEMENT:

The interpreter may depend on the libm crate version 0.2.8

RATIONALE:

Rust does not expose all floating point operations in a bare-metal (as in no_std) target, as to not introduce any dependency on the C standard library's libm (respective PR: https://github.com/rust-lang/rust/pull/27823). However, we identified at least the following operations to be required for WASM interpretation while unavailable in no_std:

  • abs
  • ceil
  • floor
  • trunc
  • round
  • sqrt
  • copysign

In order use these operations, having the libm crate as dependencies of the WASM interpreter is an acceptable trade-off.

1.6.7. Minimum Supported Rust Version (MSRV) UID: REQ-17 STATEMENT:

The interpreter shall compile on Rust 1.76.0 and later versions

RATIONALE:

An MSRV should be clearly stated to specify which toolchain is acceptable.

2. Observability Requirements
2.1. Instrumentation UID: REQ-7 child relations: STATEMENT:

The interpreter shall implement means for instrumentation

RATIONALE:

Instrumentation is needed to generate evidence for certification. Instrumentation eases debugging. Instrumentation enables elaborate run-time monitoring.

  • 2.2.1. Statement Coverage UID: REQ-8 parent relations: STATEMENT:

    The instrumentation shall enable the measurement of statement coverage

    RATIONALE:

    Statement coverage is required by DO-178C starting at DAL-C (6.4.4.c)

  • 2.2.2. Decision Coverage UID: REQ-9 parent relations: STATEMENT:

    The instrumentation shall enable the measurement of decision coverage

    RATIONALE:

    Decision coverage is required by DO-178C starting at DAL-B (6.4.4.c)

  • 2.2.3. Modified Condition/Decision Coverage UID: REQ-10 parent relations: STATEMENT:

    The instrumentation shall enable the measurement of modified condition/decision coverage

    RATIONALE:

    Modified condition/decision coverage is required by DO-178C starting at DAL-A (6.4.4.c)

2.2. Low-Level Observability Requirements
2.2.1. Statement Coverage UID: REQ-8 parent relations: STATEMENT:

The instrumentation shall enable the measurement of statement coverage

RATIONALE:

Statement coverage is required by DO-178C starting at DAL-C (6.4.4.c)

2.2.2. Decision Coverage UID: REQ-9 parent relations: STATEMENT:

The instrumentation shall enable the measurement of decision coverage

RATIONALE:

Decision coverage is required by DO-178C starting at DAL-B (6.4.4.c)

2.2.3. Modified Condition/Decision Coverage UID: REQ-10 parent relations: STATEMENT:

The instrumentation shall enable the measurement of modified condition/decision coverage

RATIONALE:

Modified condition/decision coverage is required by DO-178C starting at DAL-A (6.4.4.c)

2.2.4. Certification Evidence UID: REQ-11 child relations: STATEMENT:

The interpreter shall support the generation of certification evidence

  • 2.2.1. Statement Coverage UID: REQ-8 parent relations: STATEMENT:

    The instrumentation shall enable the measurement of statement coverage

    RATIONALE:

    Statement coverage is required by DO-178C starting at DAL-C (6.4.4.c)

  • 2.2.2. Decision Coverage UID: REQ-9 parent relations: STATEMENT:

    The instrumentation shall enable the measurement of decision coverage

    RATIONALE:

    Decision coverage is required by DO-178C starting at DAL-B (6.4.4.c)

  • 2.2.3. Modified Condition/Decision Coverage UID: REQ-10 parent relations: STATEMENT:

    The instrumentation shall enable the measurement of modified condition/decision coverage

    RATIONALE:

    Modified condition/decision coverage is required by DO-178C starting at DAL-A (6.4.4.c)