Universal VM - Exploring the design space

[void4]

Described here #5
tl;dr: A VM for running untrusted mobile code

• untrusted: processes are limited by resource constraints set by parent virtual machine
• mobile: processes are persistent and platform independent, runtimes can be suspended and fully serialized, then resumed on another machine

Syntax

Semantics

Determinism is required in order to compare runtimes and their results across different machines. The runtime format (code+data+state) should therefore be deterministic. Each runtime -> runtime' transition has to be unique. The execution "worldline" therefore represents the repeated evaluation of the same (partial) function.

http:https://canonical.org/~kragen/memory-models/

Runtime (and not only result determinism) is desirable because it allows for persistence and resumption of processes even on other machines in addition to computation markets.

Memory layout and semantics of change

• abstract vs implicit vs explicit

In any case, a specific runtime state has to map to a unique serialized memory layout and vice versa. They may be the same.

The problem of economic value

It may be cheaper to replace sequences of instructions to make execution cheaper, to the point that specific instructions may remain unused.

Furthermore, each instruction may have a different value depending on the hardware it executes on.

A computation market would not only have to consider these differences, but also other (objective/subjective/source relative, trusted/untrusted) properties such as the bandwidth of collaborating nodes. There may have to be a notion of performance expectation to assure liveness and correctness properties, efficiency and high quality of service.

Control over resources

Namespaces

Messages

Access control

Capabilities
Revoking access

Resources internal to the process

Runtime and memory

Control policies are easier to implement if the system under consideration is predictable. But a deterministic system is predictable only to some extent. Instruction-level determinism may still leave the runtime unspecified or highly inconsistent: consider for example a multiplication operation with two variable sized operands (e.g. BigInts). A (static) type system might alleviate this, but runtime limitation systems based on instruction count can only allow adequate timing control if execution intervals are small.

A language based on timing interrupts might not be able to guarantee liveness if operations are too time intensive and thus have to consider externalities such as hardware as well.

It might be necessary to reconcile these realities with the formal theories of process calculi and temporal logics to allow for a better analysis of runtime properties.

Recursive self hosted child processes

Detaching

Resources external to the process

Remote resources

Can remote resources be internal?

Outsourcing tasks

Contract/decision/optimisation theory might shed some light on the specific circumstances that make outsourcing tasks to external agents sensible.

Ensuring confidentiality

Homomorphic computation is not yet efficient enough.

Verifying results

Syntactic/Structural verification
Semantic verification

Locus of execution:
Own machines
Social trust networks

• comparing results across orthogonal or reversely incentivized agents
• security-deposits with trusted third party verifiers