Copland

Semantics, languages and tools for layered attestation

Home
Publications
Documentation
Software
Blog

Assumption file for Example 17

Assume adversary avoids detection at our main measurement event. By using the label, in the antecedent, we do not need to know the event number in the compiled Copland phrase.

l(E) = msp(us, E1, M, us, exts)
 => phi(us, exts, E).

Assumptions about system dependencies.
Comment these out to consider unaccounted-for dependencies.

depends(P, C, ks, av) => P = ks & C = ker. 
depends(P, C, us, bmon) => false.
depends(P, C, us, bser) => false.
depends(P, C, us, extmgr) => P = us & C = bser.
depends(P, C, hv, kim) => false.
depends(P, C, hv, avm) => false. 

Axiom ruling out corruption of “deep” components. In this case any component in the place hv is considered deep.
Leave uncommented if you wish to exclude models with deep corruptions.

l(E) = cor(hv, M) => false.

Axiom ruling out “recent” corruptions in which components might be corrupted during attestation. Recent is defined here as occurring after any measurement event.
Leave uncommented if you wish to exclude models with recent corruptions.

prec(E, E2) & l(E2) = cor(P,C) & ms_evt(E)
 => false. 

Injectivity of names.

kim = avm => false.
kim = ker => false.
kim = av => false.
kim = bmon => false.
kim = bser => false.
kim = extmgr => false.
kim = exts => false.
avm = ker => false.
avm = av => false.
avm = bmon => false.
avm = bser => false.
avm = extmgr => false.
avm = exts => false.
ker = av => false.
ker = bmon => false.
ker = bser => false.
ker = extmgr => false.
ker = exts => false.
av = bmon => false.
av = bser => false.
av = extmgr => false.
av = exts => false.
bmon = bser => false.
bmon = extmgr => false.
bmon = exts => false.
bser = extmgr => false.
bser = exts => false.
extmgr = exts => false.