A model for provably secure software design

Publikationstyp
Conference Paper
Date Issued
2017-05
Sprache
English
Author(s)
Van Den Berghe, Alexander  
Yskout, Koen  
Joosen, Wouter  
Scandariato, Riccardo  
TORE-URI
http://hdl.handle.net/11420/12138
Start Page
3
End Page
9
Article Number
7967986
Citation
5th IEEE/ACM International FME Workshop on Formal Methods in Software Engineering (FormaliSE 2017)
Contribution to Conference
5th IEEE/ACM International FME Workshop on Formal Methods in Software Engineering, FormaliSE 2017  
Publisher DOI
10.1109/FormaliSE.2017.6
Scopus ID
2-s2.0-85027436570
Both academia and industry advocate the security by design principle to stress the importance of dealing with security from the earliest stages in software development. Nevertheless, designers often have to resort to their own knowledge and experience to pro-actively identify and mitigate potential security problems. Moreover, research shows that correctly applying security solutions is a much more significant challenge for designers, rather than finding an adequate solution. Therefore, there is a need for techniques that ensure a correct application of a security design solution. The contribution of this paper is a model in which the security-relevant aspects of a design can be precisely expressed in an integrated manner, enabling thorough reasoning about these aspects. We illustrate this model with a sizeable model of a banking system and show how the precise semantics of this model enables the tool-supported construction of proofs about the correctness of the applied design solutions. Our proposal thus enables designers to obtain stronger guarantees, ensuring the correctness of their solutions. The presented model can serve as the foundation for security by design, in time enabling automated security verification throughout the software development cycle.
Subjects
Security analysis
Security by design
Software design