Abstract:
We address the issue of declassification in a language-based
security approach. We introduce, in a Core ML-like language with
concurrent threads, a declassification mechanism that takes the form
of a local flow policy declaration. The computation in the scope of
such a declaration is allowed to implement information flow according
to the local policy. This dynamic view of information flow policies is
supported by a concrete presentation of the security lattice, where
the confidentiality levels are sets of principals, similar to access
control lists. To take into account declassification, and more
generally dynamic flow policies, we introduce a generalization of
non-interference, that we call the non-disclosure policy,
and we design a type and effect system for our language that enforces
this policy.