Statically checking confidentiality via dynamic labels


Share/Save/Bookmark

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.

[img]
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:
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

 

Repository Staff Only: item control page