Towards confidentiality-by-construction

Ina Schaefer, Tobias Runge, Alexander Knüppel, Loek Cleophas, Derrick Kourie, Bruce W. Watson

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

    4 Citations (Scopus)


    Guaranteeing that information processed in computing systems remains confidential is vital for many software applications. To this end, language-based security mechanisms enforce fine-grained access control policies for program variables to prevent secret information from leaking through unauthorized access. However, approaches for language-based security by information flow control mostly work post-hoc, classifying programs into whether they comply with information flow policies or not after the program has been constructed. Means for constructing programs that satisfy given information flow control policies are still missing. Following the correctness-by-construction approach, we propose a development method for specifying information flow policies first and constructing programs satisfying these policies subsequently. We replace functional pre- and postcondition specifications with confidentiality properties and define rules to derive new confidentiality specifications for each refining program construct. We discuss possible extensions including initial ideas for tool support. Applying correctness-by-construction techniques to confidentiality properties constitutes a first step towards security-by-construction.

    Original languageEnglish
    Title of host publicationLeveraging Applications of Formal Methods, Verification and Validation. Modeling - 8th International Symposium, ISoLA 2018, Proceedings
    EditorsBernhard Steffen, Tiziana Margaria
    Number of pages14
    ISBN (Print)9783030034177
    Publication statusPublished - 1 Jan 2018
    Event8th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, (ISoLA 2018) - Limassol, Cyprus
    Duration: 5 Nov 20189 Nov 2018

    Publication series

    NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
    Volume11244 LNCS
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349


    Conference8th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, (ISoLA 2018)
    Abbreviated titleISoLA2018
    Internet address


    Dive into the research topics of 'Towards confidentiality-by-construction'. Together they form a unique fingerprint.

    Cite this