An Information Flow Tool for Gypsy

The Gypsy language is seeing increasing use as a tool for designing, specifying, and sometimes implementing computer systems intended for certification at the A1 level by the Department of Defense Computer Security Center. One of the criteria for A1 certification is a formal proof that the information flows within the design conform to a policy defined by formal security model. Despite the fact that it is possible to state such models in Gypsy and to prove some properties of programs with respect to a model, a flow analysis tool within the Gypsy environment would appear to be useful. The Gypsy Verification Environment, GVE, contains the basis for such tool in the form of a flow analyzer used to detect unused variables during optimization. In the discussion below, we will describe a simple information flow analyzer based upon this analysis.