The Generic Unwinding Theorem for CSP Noninterference Security

The classical definition of noninterference security for a deterministic state machine with outputs requires to consider the outputs produced by machine actions after any trace, i.e. any indefinitely long sequence of actions, of the machine. In order to render the verification of the security of such a machine more straightforward, there is a need of some sufficient condition for security such that just individual actions, rather than unbounded sequences of actions, have to be considered. By extending previous results applying to transitive noninterference policies, Rushby has proven an unwinding theorem that provides a sufficient condition of this kind in the general case of a possibly intransitive policy. This condition has to be satisfied by a generic function mapping security domains into equivalence relations over machine states. An analogous problem arises for CSP noninterference security, whose definition requires to consider any possible future, i.e. any indefinitely lon...

• Type: Journal
• Year: 2015
• Where: AFP
• Authors: Pasquale Noce
• Keywords: AFP 2015, Formal Methods