Statically checking confidentiality via dynamic labels

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

    Research output: Contribution to conferencePaperAcademicpeer-review

    9 Citations (Scopus)
    59 Downloads (Pure)

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

    Workshop

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

    Keywords

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

    Cite this