Non-interference (security) - Formal Expression

Formal Expression

Let be a memory configuration, and let and be the projection of the memory to the low and high parts, respectively. Let be the function that compares the low parts of the memory configurations, i.e., iff . Let be the execution of the program starting with memory configuration and terminating with the memory configuration .

The definition of non-interference for a deterministic program is the following:

$\begin{array}{rrl}\forall M_1, M_2 :\; & M_1\ {=_L}\ M_2 & \land\\ & (P,M_1) \rightarrow^* M_1^\prime & \land\\ &(P,M_2) \rightarrow^* M_2^\prime &\Rightarrow\\ &M_1^\prime\ {=_L}\ M_2^\prime\end{array}$

Read more about this topic: Non-interference (security)

Famous quotes containing the words formal and/or expression:

“There must be a profound recognition that parents are the first teachers and that education begins before formal schooling and is deeply rooted in the values, traditions, and norms of family and culture.”
—Sara Lawrence Lightfoot (20th century)

“A work of art is an abstract or epitome of the world. It is the result or expression of nature, in miniature. For, although the works of nature are innumerable and all different, the result or the expression of them all is similar and single.”
—Ralph Waldo Emerson (1803–1882)