This talk concentrates on the preservation of information confidentiality by potentially malicious and/or buggy applications. Building on the technology of programming languages (such as programming-language semantics, type-based analysis, and program transformation) we develop a series of security policies and enforcement mechanisms for sequential, concurrent, and distributed programs that allow for modeling and statically analyzing information flow in a given program. The soundness of our security analyses guarantees the absence of insecure information flows. This means that if a program passes the analysis then it may not compromise confidentiality during the execution. We show that our approach is capable of detecting timing and probabilistic covert channels, i.e., the attacker is prevented from learning sensitive information by making timing and stochastic observations about secure programs.
Joint work with David Sands and Heiko Mantel.
| Iliano Cervesato |