| Summary: | Language-based information flow methods offer a principled way to enforce
strong security properties, but enforcing noninterference is too inflexible for
realistic applications. Security-typed languages have therefore introduced
declassification mechanisms for relaxing confidentiality policies, and
endorsement mechanisms for relaxing integrity policies. However, a continuing
challenge has been to define what security is guaranteed when such mechanisms
are used. This paper presents a new semantic framework for expressing security
policies for declassification and endorsement in a language-based setting. The
key insight is that security can be characterized in terms of the influence
that declassification and endorsement allow to the attacker. The new framework
introduces two notions of security to describe the influence of the attacker.
Attacker control defines what the attacker is able to learn from observable
effects of this code; attacker impact captures the attacker's influence on
trusted locations. This approach yields novel security conditions for checked
endorsements and robust integrity. The framework is flexible enough to recover
and to improve on the previously introduced notions of robustness and qualified
robustness. Further, the new security conditions can be soundly enforced by a
security type system. The applicability and enforcement of the new policies is
illustrated through various examples, including data sanitization and
authentication.
|
|---|