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

2 Citations (Scopus)

Abstract

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
PublisherSpringer
Pages502-515
Number of pages14
ISBN (Print)9783030034177
DOIs
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
http://www.isola-conference.org/isola2018/

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

Conference

Conference8th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, (ISoLA 2018)
Abbreviated titleISoLA2018
CountryCyprus
CityLimassol
Period5/11/189/11/18
Internet address

Fingerprint

Confidentiality
Information Flow
Flow control
Specifications
Control Policy
Flow Control
Application programs
Access control
Refining
Correctness
Specification
Tool Support
Access Control
Software
Computing
Policy

Cite this

Schaefer, I., Runge, T., Knüppel, A., Cleophas, L., Kourie, D., & Watson, B. W. (2018). Towards confidentiality-by-construction. In B. Steffen, & T. Margaria (Eds.), Leveraging Applications of Formal Methods, Verification and Validation. Modeling - 8th International Symposium, ISoLA 2018, Proceedings (pp. 502-515). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11244 LNCS). Springer. https://doi.org/10.1007/978-3-030-03418-4_30
Schaefer, Ina ; Runge, Tobias ; Knüppel, Alexander ; Cleophas, Loek ; Kourie, Derrick ; Watson, Bruce W. / Towards confidentiality-by-construction. Leveraging Applications of Formal Methods, Verification and Validation. Modeling - 8th International Symposium, ISoLA 2018, Proceedings. editor / Bernhard Steffen ; Tiziana Margaria. Springer, 2018. pp. 502-515 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{826a209dcafc4597826779a05dbd9d97,
title = "Towards confidentiality-by-construction",
abstract = "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.",
author = "Ina Schaefer and Tobias Runge and Alexander Kn{\"u}ppel and Loek Cleophas and Derrick Kourie and Watson, {Bruce W.}",
year = "2018",
month = "1",
day = "1",
doi = "10.1007/978-3-030-03418-4_30",
language = "English",
isbn = "9783030034177",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer",
pages = "502--515",
editor = "Bernhard Steffen and Tiziana Margaria",
booktitle = "Leveraging Applications of Formal Methods, Verification and Validation. Modeling - 8th International Symposium, ISoLA 2018, Proceedings",
address = "Germany",

}

Schaefer, I, Runge, T, Knüppel, A, Cleophas, L, Kourie, D & Watson, BW 2018, Towards confidentiality-by-construction. in B Steffen & T Margaria (eds), Leveraging Applications of Formal Methods, Verification and Validation. Modeling - 8th International Symposium, ISoLA 2018, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 11244 LNCS, Springer, pp. 502-515, 8th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, (ISoLA 2018), Limassol, Cyprus, 5/11/18. https://doi.org/10.1007/978-3-030-03418-4_30

Towards confidentiality-by-construction. / Schaefer, Ina; Runge, Tobias; Knüppel, Alexander; Cleophas, Loek; Kourie, Derrick; Watson, Bruce W.

Leveraging Applications of Formal Methods, Verification and Validation. Modeling - 8th International Symposium, ISoLA 2018, Proceedings. ed. / Bernhard Steffen; Tiziana Margaria. Springer, 2018. p. 502-515 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11244 LNCS).

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

TY - GEN

T1 - Towards confidentiality-by-construction

AU - Schaefer, Ina

AU - Runge, Tobias

AU - Knüppel, Alexander

AU - Cleophas, Loek

AU - Kourie, Derrick

AU - Watson, Bruce W.

PY - 2018/1/1

Y1 - 2018/1/1

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=85056479564&partnerID=8YFLogxK

U2 - 10.1007/978-3-030-03418-4_30

DO - 10.1007/978-3-030-03418-4_30

M3 - Conference contribution

AN - SCOPUS:85056479564

SN - 9783030034177

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 502

EP - 515

BT - Leveraging Applications of Formal Methods, Verification and Validation. Modeling - 8th International Symposium, ISoLA 2018, Proceedings

A2 - Steffen, Bernhard

A2 - Margaria, Tiziana

PB - Springer

ER -

Schaefer I, Runge T, Knüppel A, Cleophas L, Kourie D, Watson BW. Towards confidentiality-by-construction. In Steffen B, Margaria T, editors, Leveraging Applications of Formal Methods, Verification and Validation. Modeling - 8th International Symposium, ISoLA 2018, Proceedings. Springer. 2018. p. 502-515. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-030-03418-4_30