This paper presents a new approach for verifying confidentiality for programs, based on abstract interpretation. The framework is formally developed and proved correct in the theorem prover PVS. We use dynamic labeling functions to abstractly 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.
|Number of pages||7|
|Publication status||Published - 2005|
|Event||WITS '05: 2005 workshop on Issues in the theory of security - Long Beach, CA|
Duration: 10 Jan 2005 → 11 Jan 2005
|Workshop||WITS '05: 2005 workshop on Issues in the theory of security|
|Period||10/01/05 → 11/01/05|
|Other||10-11 Jan 2005|