Security Type Systems as Recursive Predicates

TL;DR

This paper presents a method to represent security type systems as recursive predicates, providing a unified framework that encompasses various existing soundness results in language-based noninterference.

Contribution

It introduces a uniform syntactic criterion that captures multiple security type system soundness proofs through recursive predicates.

Findings

Unified recursive predicate framework for security type systems

Coverage of several existing soundness results

Simplification of security type system analysis

Abstract

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.