TY - GEN
T1 - Information Flow Control-by-Construction for an Object-Oriented Language
AU - Runge, Tobias
AU - Kittelmann, Alexander
AU - Servetto, Marco
AU - Potanin, Alex
AU - Schaefer, Ina
N1 - Publisher Copyright:
© 2022, The Author(s), under exclusive license to Springer Nature Switzerland AG.
PY - 2022/10/1
Y1 - 2022/10/1
N2 - In security-critical software applications, confidential information must be prevented from leaking to unauthorized sinks. Static analysis techniques are widespread to enforce a secure information flow by checking a program after construction. A drawback of these systems is that incomplete programs during construction cannot be checked properly. The user is not guided to a secure program by most systems. We introduce IFbCOO, an approach that guides users incrementally to a secure implementation by using refinement rules. In each refinement step, confidentiality or integrity (or both) is guaranteed alongside the functional correctness of the program, such that insecure programs are declined by construction. In this work, we formalize IFbCOO and prove soundness of the refinement rules. We implement IFbCOO in the tool CorC and conduct a feasibility study by successfully implementing case studies.
AB - In security-critical software applications, confidential information must be prevented from leaking to unauthorized sinks. Static analysis techniques are widespread to enforce a secure information flow by checking a program after construction. A drawback of these systems is that incomplete programs during construction cannot be checked properly. The user is not guided to a secure program by most systems. We introduce IFbCOO, an approach that guides users incrementally to a secure implementation by using refinement rules. In each refinement step, confidentiality or integrity (or both) is guaranteed alongside the functional correctness of the program, such that insecure programs are declined by construction. In this work, we formalize IFbCOO and prove soundness of the refinement rules. We implement IFbCOO in the tool CorC and conduct a feasibility study by successfully implementing case studies.
KW - Correctness-by-construction
KW - Information flow control
KW - Security-by-design
UR - https://www.scopus.com/pages/publications/85140434158
U2 - 10.1007/978-3-031-17108-6_13
DO - 10.1007/978-3-031-17108-6_13
M3 - Conference Paper
AN - SCOPUS:85140434158
SN - 978-3-031-17107-9
T3 - Lecture Notes in Computer Science
SP - 209
EP - 226
BT - Software Engineering and Formal Methods - 20th International Conference, SEFM 2022, Proceedings
A2 - Schlingloff, Bernd-Holger
A2 - Chai, Ming
PB - Springer Science+Business Media B.V.
CY - Cham
T2 - 20th International Conference on Software Engineering and Formal Methods, SEFM 2022
Y2 - 26 September 2022 through 30 September 2022
ER -