Statically checking confidentiality via dynamic labels

This paper presents a new approach for verifying confidenfor programs, based on abstract interpretation. The framework is formally developed and proved correct in the theorem prover PVS. We use dynamic labeling functions actly interpret a simple programming language via modification of security levels of variables. Our approach is sound and compositional and results in an algorithm for statically checking confidentiality.

• Type: Conference
• Year: 2005
• Where: POPL
• Authors: Bart Jacobs, Wolter Pieters, Martijn Warnier
• Keywords: Dynamic Labeling Functions, POPL 2005, Programming Languages, Simple Programming Language, Theorem Prover Pvs