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:

“The manifestation of poetry in external life is formal perfection. True sentiment grows within, and art must represent internal phenomena externally.”
—Franz Grillparzer (1791–1872)

“Great speeches have always had great soundbites. The problem now is that the young technicians who put together speeches are paying attention only to the soundbite, not to the text as a whole, not realizing that all great soundbites happen by accident, which is to say, all great soundbites are yielded up inevitably, as part of the natural expression of the text. They are part of the tapestry, they aren’t a little flower somebody sewed on.”
—Peggy Noonan (b. 1950)