Starting from a denotational semantics of imperative programs, the standard collecting semantics is defined as specifying the strongest program property. By successive Galois connection based abstractions, a type system that certifies secure information flows is designed as an abstract semantics approximating the collecting semantics of imperative programs. Security abstract analysis embodies the secure flow conditions of Denning’s lattice model (see [6]), giving rise to a type system which is similar to, but strictly more expressive than, the one proposed by Volpano et al. in [10]. This shows that types and type systems for control flow analysis can be viewed as abstract interpretations.