We model the runtime as an ideal attested HTTP request-response functionality.
The functionality provides an authenticated and confidential HTTP service associated with an image identity, backed by canonical deployment state and evaluated relative to an admissible view of the external world.
Security is defined by simulation: every real execution must be computationally indistinguishable from an execution using only the ideal functionality.
Migration is modeled as a transition to an already-existing successor execution. The successor image is not supplied independently to the migration functionality; it is derived from the protected execution identified by the migration request.
The model is defined relative to two external abstractions:
G_att
G_world
G_att provides attested protected execution.
Each protected execution is associated with an image identity:
I
and an authenticated service endpoint:
E
Attestation establishes:
image I operates endpoint E
Communication with E takes place over an authenticated and confidential channel.
G_world represents external facts available to protected execution.
A view of the external world is denoted:
W
and may be used only if:
ValidView(W)
holds.
The contents of W and the relation ValidView are parameters of the environment in which the functionality is instantiated.
The protected channel exposes only:
L_HTTP(request, eid, |req|)
L_HTTP(response, eid, |resp|)
Request and response contents remain confidential.
Attestation output is public.
d deployment identifier
I image identity
eid service execution identifier
E authenticated endpoint
S_d canonical protected deployment state
mem volatile private execution state
Next_d authorized image-successor function
Gen deployment-state generation functionality
App HTTP application functionality
L_HTTP HTTP metadata leakage
For each deployment:
Next_d : Image -> Image | ⊥
If:
Next_d(I) = I'
then I' is the authorized successor of I.
The application is evaluated as:
(resp, mem') <- App(req, S, mem, W)
Let A be a PPT adversary, S a PPT simulator, and Z a PPT environment.
The real execution is denoted:
REAL(Pi_RT, A, Z ; G_att, G_world)
The ideal execution is denoted:
IDEAL(F_RT, S, Z ; G_world)
where:
F_RT = F_RT[Next, Gen, App, L_HTTP]
Pi_RT securely realizes F_RT if:
for every PPT adversary A,
there exists a PPT simulator S,
such that for every PPT environment Z,
REAL(Pi_RT, A, Z ; G_att, G_world)
~=c
IDEAL(F_RT, S, Z ; G_world)
where:
~=c
denotes computational indistinguishability.
Define:
F_RT[Next, Gen, App, L_HTTP]
with deployment state:
D[d] = {
active_image,
state
}
and service-execution state:
T[eid] = {
deployment,
image,
state,
memory,
endpoint,
status
}
where:
status ∈ {candidate, ready, halted}
For deployment d, define:
S_d = D[d].state
On:
GENESIS(d, I0, spec)
if D[d] already exists, return:
⊥
Otherwise:
S_d <- Gen(spec)
D[d] = {
active_image: I0,
state: S_d
}
Return:
ok
S_d is generated exactly once.
On:
BOOT(d, I)
if D[d] does not exist, return:
⊥
State recovery may return:
⊥
Otherwise recover exactly:
S_d := D[d].state
Generate:
eid <- fresh()
E <- fresh_endpoint()
mem <- 0
If:
I = D[d].active_image
set:
S := S_d
status := ready
Otherwise set:
S := ⊥
status := candidate
Store:
T[eid] = {
deployment: d,
image: I,
state: S,
memory: mem,
endpoint: E,
status: status
}
Return:
(eid, E)
A candidate execution exists and may attest its image identity, but does not possess the canonical deployment state and cannot serve application requests.
On:
ATTEST(eid, nonce)
if T[eid] does not exist, return:
⊥
If:
T[eid].status ∉ {candidate, ready}
return:
⊥
Otherwise let:
I := T[eid].image
E := T[eid].endpoint
and return an attestation for:
(I, E, nonce)
Successful verification establishes:
image I operates endpoint E
The nonce binds the attestation to the invocation that requested it.
On:
REQUEST(eid, req)
over the authenticated confidential endpoint associated with eid, if:
T[eid].status != ready
return:
⊥
Reveal:
L_HTTP(request, eid, |req|)
Obtain:
W <- G_world
If:
ValidView(W) = false
return:
⊥
Let:
S := T[eid].state
mem := T[eid].memory
Evaluate:
(resp, mem') <- App(req, S, mem, W)
Update:
T[eid].memory := mem'
Reveal:
L_HTTP(response, eid, |resp|)
Return:
resp
over the authenticated confidential channel.
On:
MIGRATE(d, eid_new)
if D[d] does not exist, return:
⊥
If T[eid_new] does not exist, return:
⊥
Require:
T[eid_new].deployment = d
T[eid_new].status = candidate
Otherwise return:
⊥
Let:
I_old := D[d].active_image
I_new := T[eid_new].image
Require:
Next_d(I_old) = I_new
Otherwise return:
⊥
Atomically update:
D[d].active_image := I_new
T[eid_new].state := S_d
T[eid_new].status := ready
while preserving:
D[d].state = S_d
Return:
ok
The successor identity is therefore derived from an existing protected execution rather than supplied independently by the migration caller.
The ideal functionality does not verify a Nitro attestation inside MIGRATE. It already knows the authenticated execution state T[eid_new]. In a real protocol, attestation is the mechanism used to establish the corresponding relation between a live successor execution and its image identity.
On:
HALT(eid)
if T[eid] does not exist, return:
⊥
Erase:
T[eid].state
T[eid].memory
and set:
T[eid].status := halted
The deployment state remains unchanged.
For every initialized deployment:
D[d].state = S_d
and:
GENESIS: ⊥ -> S_d
BOOT: S_d -> S_d
MIGRATE: S_d -> S_d
HALT: S_d -> S_d
There is no transition:
S_d -> S'_d
for:
S'_d != S_d
For every service execution:
T[eid].status = ready
and
T[eid].image = D[d].active_image
and
T[eid].deployment = d
=>
T[eid].state = D[d].state = S_d
For every candidate execution:
T[eid].status = candidate
=>
T[eid].state = ⊥
and therefore:
T[eid].status = candidate
=>
REQUEST(eid, req) = ⊥
A candidate may attest its image identity before receiving deployment state.
Verify(Attest(eid, nonce))
=>
T[eid].image operates T[eid].endpoint
RequestSuccess(eid, req)
=>
ValidView(W)
for the view W used by that request.
MigrateSuccess(d, eid_new)
=>
T[eid_new].deployment = d
and, immediately before migration:
T[eid_new].status = candidate
Let:
I_old = D[d].active_image
I_new = T[eid_new].image
immediately before migration.
Then:
MigrateSuccess(d, eid_new)
=>
Next_d(I_old) = I_new
and after migration:
D[d].active_image = I_new
T[eid_new].state = S_d
T[eid_new].status = ready
while:
state before migration
=
state after migration
=
S_d
Thus migration cannot authorize an image identity that is independent of the successor execution named by eid_new.
Because:
Next_d : Image -> Image | ⊥
is a function:
Next_d(I) = I1
and
Next_d(I) = I2
=>
I1 = I2
Hence the authorized image history has the form:
I0 -> I1 -> I2 -> ...
For every reachable state of an initialized deployment:
D[d] = {
active_image: I_k,
state: S_d
}
where I_k lies on the unique successor chain beginning at I0, and S_d is the canonical deployment state established by GENESIS.
Let:
Trace(F_RT)
denote the set of traces generated by repeated application of the transitions defined above from an initially empty state.
A trace:
τ = (e_1, e_2, ..., e_n)
is admissible iff every event e_i is produced by one of:
GENESIS
BOOT
ATTEST
REQUEST
MIGRATE
HALT
according to the corresponding transition rule, and every prefix of τ preserves the invariants in Section 6.7.
In particular, a successful migration to a new image requires a previously created candidate execution:
BOOT(d, I_new)
->
MIGRATE(d, eid_new)
where the eid_new returned by BOOT satisfies:
T[eid_new].image = I_new
and:
Next_d(I_old) = I_new
An ATTEST(eid_new, nonce) event may occur between BOOT and MIGRATE. In the real protocol, the corresponding attestation is the mechanism by which the predecessor verifies the successor execution and derives its image identity.
The ideal functionality induces executions only over:
τ ∈ Trace(F_RT)
No other execution trace is defined.