Nontransitive Policies Transpiled
by Mohammad M. Ahmadpanah, Aslan Askarov, Andrei Sabelfeld.
In Proceedings of the 6th IEEE European Symposium on Security and Privacy (EuroS&P), September 2021.
Nontransitive Noninterference (NTNI) and Nontransitive Types (NTT)
are a new security condition and enforcement for policies which,
in contrast to Denning's classical lattice model, assume no
transitivity of the underlying flow relation.
Nontransitive
security policies are a natural fit for coarse-grained information-flow
control where labels are specified at module rather than variable
level of granularity.
While the nontransitive and transitive policies
pursue different goals and have different intuitions, this paper
demonstrates that nontransitive noninterference can in fact be reduced to classical transitive
noninterference.
We develop a
lattice encoding that
establishes a precise relation between NTNI and classical noninterference.
Our results make it possible to clearly position the new
NTNI characterization
with respect to the large body of work on noninterference.
Further, we devise a lightweight program transformation
that leverages standard
flow-sensitive information-flow analyses to enforce nontransitive
policies.
We demonstrate several immediate benefits of our approach,
both theoretical and practical. First,
we improve the
permissiveness over (while retaining the soundness of) the nonstandard NTT
enforcement.
Second, our results naturally
generalize to a language with intermediate inputs and outputs.
Finally, we demonstrate the practical benefits
by utilizing state-of-the-art flow-sensitive tool JOANA
to enforce nontransitive policies for Java programs.
[Paper] [Proofs] [Source code and case studies] [Presentation]