A Formal Connection between Security Automata and JML Annotations

Marieke Huisman, A. Tamalet

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

    4 Citations (Scopus)


    Security automata are a convenient way to describe security policies. Their typical use is to monitor the execution of an application, and to interrupt it as soon as the security policy is violated. However, run-time adherence checking is not always convenient. Instead, we aim at developing a technique to verify adherence to a security policy statically. To do this, we consider a security automaton as specification, and we generate JML annotations that inline the monitor~--~as a specification~--~into the application. We describe this translation and prove preservation of program behaviour, i.e., if monitoring does not reveal a security violation, the generated annotations are respected by the program. The correctness proofs are formalised using the PVS theorem prover. This reveals several subtleties to be considered in the definition of the translation algorithm and in the program requirements.
    Original languageUndefined
    Title of host publicationFundamental Approaches to Software Engineering
    EditorsM. Checkik, M. Wirsing
    Place of PublicationBerlin
    Number of pages15
    ISBN (Print)978-3-642-00592-3
    Publication statusPublished - 2009
    Event12th International Conference on Fundamental Approaches to Software Engineering, FASE 2009 - York, United Kingdom
    Duration: 22 Mar 200929 Mar 2009

    Publication series

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


    Conference12th International Conference on Fundamental Approaches to Software Engineering, FASE 2009
    Abbreviated titleFASE 2009
    Country/TerritoryUnited Kingdom


    • EWI-15336
    • IR-62803
    • METIS-263839

    Cite this