Declassification policies aim to guarantee trustedrelease of confidential information. The semantic securityconditions of declassification policies focus on differentdimensions. In order to prevent the special attacks aiming tocompromise the mechanisms of declassification, it isimportant for a declassification policy to combine differentdimensions. Moreover, current body of work on theenforcement of the declassification policy focuses on staticand flow-insensitive information-flow analysis, which isover-restrictive and imprecise. Dynamic and flow-sensitiveinformation flow analysis techniques offer distinctadvantages in permissiveness and precision. As a step inthese directions, this paper first presents a declassificationpolicy combining two dimensions, which control the amountand the location of confidential information releaserespectively, based on the security-typed language proposed.Then we presents an automaton-based monitoringmechanisms of the declassification policy. Abstractions ofevents occurring during the execution of a program are sentto the automaton as inputs, and the automaton uses theseinputs to track the information flows and controls theexecution of the program by forbidding or editing insecurecommands that violate the declassification policy.Additionally, we prove the monitoring mechanism proposedis sound.
展开▼
