Statically checking confidentiality via dynamic labels

B.P.F. Jacobs, Wolter Pieters, M. Warnier

    Research output: Contribution to conferencePaperpeer-review

    10 Citations (Scopus)
    164 Downloads (Pure)


    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.
    Original languageUndefined
    Number of pages7
    Publication statusPublished - 2005
    EventWITS '05: 2005 workshop on Issues in the theory of security - Long Beach, CA
    Duration: 10 Jan 200511 Jan 2005


    WorkshopWITS '05: 2005 workshop on Issues in the theory of security
    Other10-11 Jan 2005


    • SCS-Cybersecurity
    • IR-65097
    • EWI-14062

    Cite this