Non Interference

Here is an assortment of thoughts on non-interference. This more or less tracks the history of our thought process on a definition of reactive non-interference in the presence of non-determinism. I will clean this up at some point:

-Indirect interference - solved using high/low sets (application of Reactive Non-interference) -What about dynamic list of components? - other work assumes static set of components. solved using function from comp to bool - we had two potential solutions to this problem (ask Valentin/see email) - Valentin’s solution not obvious at first. We thought about asymmetric labeling. We thought about Don’s idea of proving that “correct” labeling of one trace implies same set of high components in the other trace. -Spawn is output to spawned component - this was not obvious at first, but Don pointed it out. -What about non-determinism? - first we thought about making spawn and call inputs. Do we make them inputs from high or low? If high, then we permit to many systems because spawns and calls are correlated with state. If low, then we exclude too many systems. Two standard solutions: 1.) (More common TODO : refs) - consider two input traces with same high inputs. Then the two sets of reachable traces with those inputs are the same. This has two problems. First if the Reach predicate is too loose (consider limit where Reach accepts any trace) then any system satisfies non-interference. Second, if we make Reach as tight as possible, then this excludes systems which interfere through the outside world but not through the kernel. We want the user to be able to check that components do not interfere through the kernel even if they may interfere through the outside world. 2.) (Only found in one paper TODO : ref) - Suppose world is a deterministic function of the inputs and the trace up to that point (essentially our spawn and call axioms). Allow the user to restrict this function so that when a high component calls it, it must be a deterministic function of the history of calls only (for example). In general allow the user to filter the trace based on who is calling the function and on what arguments. This may require passing the calling component to the function. One might want to say that wget for some domain is a deterministic function of previous calls to that domain. Or one might say that wget does not depend at all only history. Or that it depends only on high calls to wget. Lots of flexibility. We need to prove that there are not weird consequences of this definition. For example, if you don’t pass the calling component to the call function, and you restrict high calls to be a function of only previous high calls and low calls to be a function of only previous low calls, then call becomes a function of only the string passed in. This is weird. -Syntatic check of non-interference - this could be useful for proof search, but not useful as a definition. We partition the variables into high and low and partition the components into high and low. Make sure that handlers for high components don’t read low variables and make sure that handlers for low components don’t send to high components and don’t write to high variables. -Communication graph - there is no interference from A to B if there is no path in communication graph from A to B. But how do we compute the communication graph? This is very subtle and not suitable for a definition. Maybe suitable for proof search. For example, components can interfere indirectly through state variables.