Model-checking Secure Information Flow for Multi-Threaded Programs

Marieke Huisman, Henri-Charles Blondeel

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    5 Citations (Scopus)
    104 Downloads (Pure)


    This paper shows how secure information flow properties of multi-threaded programs can be verified by model checking in a precise and efficient way, by using the idea of self-composition. It discusses two properties that aim to capture secure information flow for multi-threaded programs, and it shows how these properties can be char- acterised in modal μ-calculus. For this characterisation, a self-composed model of the program is constructed. More precisely, this is a model that contains two copies of the labelled transition system induced by the program, so that the program is executed in parallel with itself. The self- composed model allows to compare two program executions in a single temporal formula that characterises a secure information flow property. Both the formula and model are translated into the input language for the Concurrency Workbench model checker. We discuss this encoding, and use it for some practical experiments on several simple examples.
    Original languageUndefined
    Title of host publicationProceedings of the Joint Workshop on Theory of Security and Applications, TOSCA 2011
    EditorsS. Mödersheim, C. Palamadessi
    Place of PublicationBerlin
    Number of pages18
    ISBN (Print)978-3-642-27374-2
    Publication statusPublished - Mar 2011
    EventJoint Workshop on Theory of Security and Applications, TOSCA 2011 - Saarbruecken, Germany
    Duration: 31 Mar 20111 Apr 2011

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer Verlag
    ISSN (Print)0302-9743


    WorkshopJoint Workshop on Theory of Security and Applications, TOSCA 2011
    Other31 March - 1 April 2011


    • METIS-277679
    • EWI-20260
    • IR-77615

    Cite this