News
SysV: notes on confidentiality preserving refinement
Written on 12.12.2021 11:36 by Hamed Nemati
Some notes on confidentiality preserving refinement stated in the following theorem:
where means "T_impl simulates T_spec" and it is define as follows:
Regarding the simulation relation used in the confidentiality preserving refinement part of the lecture, please note the direction of the simulation property, that is "T_impl simulates T_spec". This is in opposite direction of the simulation property we normally use to prove the functional correctness of systems. The specific direction that we used here guarantees that all permitted behaviour of the systems (modeled by the specification) are also behaviour of the implementation model.
Moreover, to rule out the problem stated in slide 39 (slide 44 in lecture notes) we used an additional constraint (stated as "all behaviours of T_impl are possible behaviors of T_spec" in the final Theorem) to make sure that there cannot be an implementation trace for which there is no corresponding specification trace. Please note that, in the supplementary paper this constraint is denoted as .
These two conditions together help us to prove the theorem above and thus conclude that implementation does not leak more secret than the specification.
In the simulation relation definition the condition "" guarantees that initial states of the two transitions are related by the property