[cap-talk] Wall banging (was: Bellizzomi - Capabilities and Shapiro's focus, Coyotos, etc.)

Toby Murray toby.murray at comlab.ox.ac.uk
Wed Nov 29 17:30:19 CST 2006


Thanks for taking this up David. I appreciate it.

On Wed, 2006-11-29 at 12:36 -0800, David Wagner wrote:
> Deterministic: A computational process whose behavior and output is a
> deterministic function of its inputs (and only the inputs explicitly
> provided, and not any other implicit values).
Right. Is the following function deterministic then?

bool timeIsEven(clock){
  return (clock.getTicks() % 2 == 0);
}

timeIsEven looks to be a completely deterministic function of its input
(clock) but I suspect it fails your definition and hence, I'm
misunderstanding what you mean. I suspect it might fail your definition
because its input is non-deterministic. Am I viewing things too closely
then? Is 'timeIsEven' nondet because given some 'clock' object who's
behaviour we cannot examine, we can't determine whether a call to
'timeIsEven' will return true or false.

If possible, could you point me at a paper that introduces these
definitions (and the context in which they live, since I think this
might be the disconnect) in a little more detail?

> 
> Deterministically replayable: A computational process that makes a record
> of every nondeterministic choice, sufficient so that given the (explicit)
> inputs and the non-determinism log you can replay the process and get
> the exact same behavior and output every time.  Note that deterministic
> processes are automatically deterministically replayable (d.r.); they are the
> trivial case where you never need to write anything to the log.
> 
> Transforming a program into d.r. form often makes implicit inputs
> more obvious.  For instance, if your behavior or output depends upon
> the time of day, random number sources, packets read from the input,
> scheduling decisions made by the OS, etc., then the act of rendering
> the program d.r. will usually make this fact apparent.
> 
> Non-interference is trickier.  I may write about this subject later,
> when I have more time, if there is interest.  But roughly speaking, if
> a LOW process is running on the same system as a HIGH process, and the
> LOW process cannot listen to covert channels, then the combination of
> the two processes forms a computational system that ought to satisfy the
> non-interference property (I think).

I had thought that non-interference was usually characterised by the LOW
processes's view of the system being identical whether the HIGH
processes were running or not. If LOW can't listen to covert channels
(and there's no overt channel between HIGH and LOW) then presumably
LOW's view of the world cannot be affected by HIGH so it ought to
satisfy n.i. Is this the sort of reasoning you had in mind with the
above?

>   Be warned, though: non-interference
> is too weak of a notion; a system can satisfy non-interference but still
> be subject to covert channels.
Presuming you're not referring to errors such as inadequate modelling of
a real-world system and such, could you provide an example of the above?
I'm certainly aware of non-interference properties that are "too weak"
because they pass processes who's refinements clearly do not satisfy
n.i., and hence may allow a real-world implementation to fail n.i.
(given that we view a real-world implementation as a "refinement" of the
model).

>   Hence the introduction of notions such
> as probabilistic non-interference.

> _______________________________________________
> cap-talk mailing list
> cap-talk at mail.eros-os.org
> http://www.eros-os.org/mailman/listinfo/cap-talk



More information about the cap-talk mailing list