Preserving Information Flow Properties of CSP Specifications under Refinement


Complex computer systems are developed iteratively, starting with an 
abstract, non-deterministic specification of the intended high-level 
behavior of the system. In each subsequent iteration, the system’s 
behavior needs to be concretized by ruling out certain alternatives 
for the behavior, which is called refinement. In general, information 
flow properties such as the Perfect Security Property are not preserved 
under refinement, making the proof process tedious and time-consuming.

In "Preserving Information Flow Properties under Refinement" by Heiko 
Mantel security-preserving refinement operators were presented as a 
solution to this problem. Applying the operators to a secure system 
yields a refined system which is guaranteed to preserve the security 
property. In "Preserving Information Flow Properties under Refinement" 
systems are represented by state event systems, which has the advantage 
that the theory is independent of any particular specification language. 
However, specifying a system as a state event system is very tedious. 
Higher-level specification languages (like CSP) are usually preferred.

Therefore, the goal of this thesis is to construct security-preserving 
refinement operators for CSP specifications to support iterative 
development of secure systems in CSP. Applying the operators to these 
inputs should yield a secure refinement of the original CSP 
specification.