WASM Interpreter for Safety - Requirements

The interpreter shall be resumable

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.

The interpreter shall be executable on bare-metal environments

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.

The interpreter shall yield back control flow eventually

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.

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

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

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.

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

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

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

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

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

The interpreter shall be stackless

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

The interpreter shall be implemented in no_std Rust

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

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

The interpreter shall support fuel bounded execution

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

The interpreter state shall be de-/serializable

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.

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

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.

The interpreter may depend on the libm crate version 0.2.8

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.

The interpreter shall compile on Rust 1.76.0 and later versions

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

The interpreter shall implement means for instrumentation

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

The instrumentation shall enable the measurement of statement coverage

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

The instrumentation shall enable the measurement of decision coverage

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

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

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

The interpreter shall support the generation of certification evidence