interfering

This Readme describes the mapping between structures in the paper and those in the coq development.

-- 4.1:Values, states and observations and 4.2:Policies correspond to the contents of Machine.v. Here policy states are initialized by a partial function, initPolicyState, reflecting a model in which the policy can statically reject programs that are inconsistent with the given program structures (removed for simplicity).

-- The trace-of operator corresponds to Machine.v:124, RunOf, and the MP trace version to Machine.v:129, MPRunOf.

-- pi_o is ObsTrace.v:542, ObsOfM and ObsOfMP.

-- The Coq development sometimes uses MTraceOf and MPTraceOf (Machine.v:111) to generate traces of machine states and MP states, respectively, without observations. Then observations can be generated by ObsTraceOf and ObsTraceOfM, (Machine.v:524) which rely on the determinism of step to reconstruct the observations from the trace.

-- Until is RunUpTo, formal.v:174, but some theorems use PrefixUpTo instead (Trace.v:72)

-- Observational similarity is ObsTraceEq', ObsTrace.v:382, which has an inductive form ObsTraceEq at ObsTrace.v:41. Observational prefix is at ObsTrace.v:236

-- The inductive relation FindCallMP finds the n-transitions and splits the trace at each one, generating a contour. formal.v:830

-- The unmatched return relation is at formal.v:4098

Properties

Properties are all in formal.v. Formalizations of the paper versions are at the end, line 4572, with a brief explanation of how they relate to the versions we've proven things about. All adjustments are primarily for the readability of the paper. Relevant properties are:

EagerStackIntegrityInd : 26 -- Inductive form of integrity

EagerStackIntegrityEnd : 77 -- Version of integrity that checks at the end

EagerStackConfidentialityOld : 102 -- based on MPTraceOf and ObsOfM, and contains the variation instead of having the variant trace as argument

EagerLSE : 854 -- this property essentially combines StackIntegrity and StackConfidentiality, along with EagerLSEWrap

StrongEagerStackConfidentiality : 203 -- the testing property

ObservableIntegrityOld : 3439 -- once again, based on MPTraceOf, changed to MPRunOf for the paper

ObservableConfidentialityOld : 3467 -- same

LazyLSE : 3539 : Top level property for Observable LSE

WellBracketedControlFlow : 4138 -- this corresponds pretty directly to what's in the paper