Non-interference, may testing, and compositionality

Steve Schneider, Royal Holloway, University of London

This talk uses CSP to introduce a characterisation of non-interference in terms of the deductions that may be made about high level processes by low level tests. May testing yields classic noninference, and has a concise formulation in CSP. It is preserved by a wide range of CSP composition operators, and thus also composes under the operators traditionally studied with non-interference. The CSP characterisation of may non-interference permits some attractive compositionality proofs. The talk also discusses the current state of ongoing work to strengthen the characterisation of non-interference using timed CSP. This approach incorporates the treatment of refusal testing information within the context of more detailed may testing.