Possibilistic Information Flow Control in MAKS and Action Refinement

Abstract. Formal methods emphasizes the need for a top-down approach when developing large reliable software systems. Refinements are map step by step abstract algebraic specifications to executable specifications. Action refinements are used to add detailed design inforo 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.

• Type: Conference
• Year: 2006
• Where: ETRICS
• Authors: Dieter Hutter
• Keywords: Abstract Algebraic Specifications, Action Refinement, ETRICS 2006, Information Flow Control, Security Privacy