Preserving Information Flow Properties under Refinement

In a stepwise development process, it is essential thatsystem properties that have been already investigated insome phase need not be re-investigated in later phases. Informal developments, this corresponds to the requirementthat properties are preserved under refinement. While safetyand liveness properties are indeed preserved under moststandard forms of refinement, it is well known that this is,in general, not true for information flow properties, a largeand useful class of security properties. In this article, wepropose a collection of refinement operators as a solutionto this problem. We prove that these operators preserve informationflow as well as other system properties. Thus,information flow properties become compatible with stepwisedevelopment. Moreover, we show that our operatorsare an optimal solution