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 language | English |
|---|---|
| Title of host publication | Leveraging Applications of Formal Methods, Verification and Validation. Modeling - 8th International Symposium, ISoLA 2018, Proceedings |
| Editors | Bernhard Steffen, Tiziana Margaria |
| Publisher | Springer |
| Pages | 502-515 |
| Number of pages | 14 |
| ISBN (Print) | 9783030034177 |
| DOIs | |
| Publication status | Published - 1 Jan 2018 |
| Event | 8th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, (ISoLA 2018) - Limassol, Cyprus Duration: 5 Nov 2018 → 9 Nov 2018 http://www.isola-conference.org/isola2018/ |
Publication series
| Name | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
|---|---|
| Volume | 11244 LNCS |
| ISSN (Print) | 0302-9743 |
| ISSN (Electronic) | 1611-3349 |
Conference
| Conference | 8th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, (ISoLA 2018) |
|---|---|
| Abbreviated title | ISoLA2018 |
| Country | Cyprus |
| City | Limassol |
| Period | 5/11/18 → 9/11/18 |
| Internet address |
Fingerprint
Cite this
}
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 proceeding › Conference contribution › Academic › peer-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 -