Formal methods emphasizes the need for a top-down approach when developing large reliable software systems. Refinements are
used to map step by step abstract algebraic specifications to executable specifications. Action refinements are used to add
detailed design information to abstract actions. Information flow control is used to specify and verify the admissible flow
of confidential information in a complex system. However, it is well-known that in general action refinement will not preserve
information flow properties which have been proved on an abstract level. In this paper we develop criteria ensuring that these
properties are inherited during action refinement. We adopt Mantel’s MAKS framework on possibilistic information flow control
to formulate security predicates but advance to configuration structures instead of trace event systems to cope with necessary
modeling of concurrency.
This work was supported by the German Federal Ministry of Education and Research (BMBF) and the German Research Foundation
(DFG).