| Abstract Declassification with Cryptographic Functions in a Security-Typed Language (2008) | |||||||||||||||
Abstract | |||||||||||||||
| Security-typed languages are powerful tools for provably enforcing noninterference. Real computing systems, however, often intentionally violate noninterference by deliberately releasing (or declassifying) sensitive information. These systems frequently trust cryptographic functions to achieve declassification while still maintaining confidentiality. We introduce the notion of trusted functions that implicitly act as declassifiers within a security-typed language. Proofs of the new language’s soundness and its enforcement of a weakened form of noninterference are given. Additionally, we implement trusted functions used for declassification in the Jif language. This represents a step forward in making security-typed languages more practical for use in real systems. 1 | |||||||||||||||
Publication details | |||||||||||||||
| |||||||||||||||