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 |