A Graded Modal Approach to Relaxed Semantic Declassification

In this paper we present Declassification Core Calculus (DeCC), a graded modal type theory for relaxed semantic declassification, a declassification criterion inspired from Delimited Release and Relaxed Noninterference. We build upon Dependency Core Calculus (DCC) that already has a graded monad for classification of information. DeCC inherits DCC's graded monad, but adds a new modality for the purpose of declassification. We build a logical relation model describing both the unary and relational semantics of the types including the two graded modalities, and use this model to prove the soundness of DeCC. We describe how our new modality interacts with DCC's graded monad via distributive laws, and also describe the conditions under which our new modality forms a comonad. This work has been mechanised in the HOL4 theorem prover.