Module 9 - Usefulness of Compositionality Result - Definition: Globally Sound Use of Modes

AlexanderF
BASIC-Programmierer
BASIC-Programmierer
Beiträge: 140
Registriert: 2. Mai 2010 17:55

Module 9 - Usefulness of Compositionality Result - Definition: Globally Sound Use of Modes

Beitrag von AlexanderF » 6. Feb 2018 16:18

The theorem on slide 22 ensures SIFUM-security for a multithreaded program where all threads are SIFUM-secure,
if for every state, the global configuration pairing all single threads with the initial mode mods_0 state ensures a sound use of modes.

A global configuration ensures a sound use of modes if it ensures a globally sound use of modes
and each local configuration associated to the pairs of statement and mode state in the global configuration ensures a locally sound use of modes (cf. Definition, slide 20).

A global configuration ensures a globally sound use of modes if EACH mode state tuple reachable from it has compatible modes (cf. Definition, slide 17).

let S :=
// acq(asm-nowrite, debug) // debug := 0;
...
// rel(asm-nowrite, debug) // skip
like defined on slide 29.

If I understand correct, the global configuration
<(S, mds_0),(y := x, mds_0), sigma>
does not ensure a globally sound use of modes (for any state sigma),
because the second thread does not guarantee that it does not use the variable debug.

But now let S' :=
// acq(guar-nowrite, debug) // y := x;

Do I see right that also
<(S, mds_0),(S', mds_0), sigma>
does NOT ensure a globally sound use of modes (for any state sigma),
because there is a mode state tuple (mds_1, mds_2) reachable from this global configuration (namely when the first thread performs a step first),
where debug is in mds_1(asm-nowrite) but debug is not in mds_2(guar-nowrite) (i.e. the first thread assumes nowrite but the second does not yet guarantee it)
and hence the mode state tuple does not have compatible modes.

Thus do I conclude right that according to the definition of "ensures a globally sound use of modes" (with the quantification over all reachable state tuples), no multithreaded program that assumes a noread or a nowrite somewhere,
with more then one thread (maybe except for threads where the statement is stop and hence are not further executable), can ensure a globally sound use of modes,
and hence the theorem (slide 22) is not applicable to ensure SIFUM security for those multithreaded programs?

best regards,
Alexander

Zurück zu „Archiv“