Computability Classes for Enforcement Mechanisms

Goal: What are the bounds on what security policies we can enforce in
programs, however we choose to enforce them?

Three classes:
- static analysis
- execution monitors (EM)
- program rewriters

Definitions:

Static conditions
EM1 - EM4

Key results shown in Fig. 1:

- static analysis subsumed by other mechs (RW can't enforce the
  "unsatisfiable" policy, which is the one that rejects all PMs,
  because it would have nothing to return; but this is a useless
  policy, though of course very safe!)

- old characterization of EM policies too strong because
  - "interventions" I that a policy would make to halt execution
    cannot be excluded from the policy.  I.e., if halting the program
    is illegal, then the EM monitor can't halt the program in
    response!  In general, this implies that real EMs cannot implement
    the unsatisfiable policy, because their intervention is itself
    unsatisfiable!
  - lack of "benevolence"---summary is that an EM enforcer may not be
    able to rule out an execution before a bad thing happens.  E.g. it
    will eventually rule out all bad executions, but not all bad
    prefixes of those executions.  (But I don't understand why.)
  - turns out the EM policies that benevolent are also RW-enforceable
    policies.  This makes sense because it is essentially "in-lining"
    the actions of the detector in the execution of the program, which
    is what a rewriter would do.

- RW-enforceable stuff:
  - Some policies are not RW-enforceable.  Some RW-enforceable
    policies cannot be enforced by EM detectors (implied by above). 
  - Edit automata, which modify execution traces, are RW-enforceable.
  - The ability to enforce policies without deciding them is the key
    (i.e. sandboxing vs. segment matching), since the former may be
    easier than the latter.

Other results:

- Static analysis is the recursively-decidable properties (\Pi_0).
- EM policies are co-RE, and all co-RE policies are EM (Thm 2).
- If the equivalence relation on machines is recursively decidable,
  then policies that are RW-enforceable are statically enforceable.

Questions:

- If static properties subsumed by dynamic enforcers, why are they
  interesting?  Is this question well-formed?

  - assumption of <<.>> for execution traces

- What is a policy that is not statically-enforceable, but is EM, or
  RW enforceable?  What is one that is RW-enforceable but not EM?

- What does benevolence mean, intuitively?  What is the intuition
  behind the intersection of EM and RW being benevolent?

- What is the intuition behind the existence of RW-enforceable
  properties outside of coRE (i.e. outside those enforced by EMs?)
  This is the secret file policy.  Answer: we'd have to prove that

- Are there other enforcement mechanisms you can think of?  I.e. does
  this cover everything reasonable?

- What details are important that are being elided in this analysis?
  What changes might we like to make to better characterize possible
  policies?
  - decidability may not be a strict requirement for
    statically-enforceable properties.  In practice, many things
    terminate that are not decidable (polymorphic-recursive type
    inference, for example).  Still might be better than dynamic
    policy.
  - characterization of running time.

- How could we characterize a virus scanner in terms of an EM policy,
  with a detector (easier to define P(X)).

- What is benevolence all about?  I don't get it precisely.

----------------------------------------------------------------------

Complexity tutorial:

Given:
Language B is recursively decidable (\Pi_0)
Then:

Language A is RE iff     A = { x | \exists y. (x,y) \in B }  (\Sigma_0)
  Here, we can in finite time determine whether z is in A.  That is,
  we can iterate until we discover it in B.  Halting problem here: the
  x are programs, and y is their execution times.  Thus, the set A is
  the set of programs whose execution halts.

Language B is co-RE iff  A = { x | \forall y. (x,y) \in B }  (\Pi_1)
  Here, we can, in finite time, determine that z is not \in A.  That
  is, we can iterate through B until we find a counterexample.

We go up the hierarchy by adding more quantifiers.  E.g.
  A = { x | \forall y. \exists z. (x,y,z) \in B }

  This could be something like "the programs that halt on all inputs".