Statically checking confidentiality via dynamic labels

Jacobs, B.P.F. and Pieters, W. and Warnier, M. (2005) Statically checking confidentiality via dynamic labels. In: WITS '05: Proceedings of the 2005 workshop on Issues in the theory of security, 10-11 Jan 2005, Long Beach, CA.

Preview

PDF
168Kb

Abstract:	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.
Item Type:	Conference or Workshop Item
Faculty:	Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:	Distributed and Embedded Systems (DIES)
Link to this item:	http://purl.utwente.nl/publications/65097
Official URL:	http://doi.acm.org/10.1145/1045405.1045411
Export this item as:	BibTeX EndNote HTML Citation Reference Manager

Show download statistics for this publication

Repository Staff Only: item control page