We propose a new notion of declassification policy called linear declassification. Linear declassification controls not only which functions may be applied to declassify high-security values, but also how often the declassification functions may be applied. We present a linear type system which guarantees that well-typed programs never violate linear declassification policies. To state a formal security property guaranteed by the linear declassification, we also introduce linear relaxed non-interference as an extension of Li and Zdancewic's relaxed non-interference. An application of the linear relaxed non-interference to quantitative information flow analysis is also discussed.
展开▼
