Security Type Systems as Recursive Predicates
This work provides a more direct representation for security type systems, which is incremental for researchers in programming languages and security.
The paper tackles the problem of representing security type systems for language-based noninterference more directly as recursive predicates on programs, showing that their uniform syntactic criteria cover several previous type-system soundness results.
We show how security type systems from the literature of language-based noninterference can be represented more directly as predicates defined by structural recursion on the programs. In this context, we show how our uniform syntactic criteria from previous work cover several previous type-system soundness results.