TY - GEN
T1 - Security-aware modeling and analysis for HW/SW partitioning
AU - Li, Letitia W.
AU - Lugou, Florian
AU - Apvrille, Ludovic
N1 - Publisher Copyright:
© 2017 by SCITEPRESS - Science and Technology Publications, Lda.
PY - 2017/1/1
Y1 - 2017/1/1
N2 - The rising wave of attacks on communicating embedded systems has exposed their users to risks of information theft, monetary damage, and personal injury. Through improved modeling and analysis of security, we propose that these flaws could be mitigated. Since HW/SW partitioning, one of the first phases, impacts future integration of security into the system, this phase would benefit from supporting modeling security abstractions and security properties, providing designers with useful partitioning feedback obtained from a security formal analyzer. In this paper, we present how our toolkit supports security modeling, automated security integration, and formal analysis during the HW/SW partitioning phase for secure communications in embedded systems. We introduce "Cryptographic Configurations", an abstract representation of security that allows us to verify security formally. Our toolkit further assists designers by automatically adding these security representations based on a mapping and security requirements.
AB - The rising wave of attacks on communicating embedded systems has exposed their users to risks of information theft, monetary damage, and personal injury. Through improved modeling and analysis of security, we propose that these flaws could be mitigated. Since HW/SW partitioning, one of the first phases, impacts future integration of security into the system, this phase would benefit from supporting modeling security abstractions and security properties, providing designers with useful partitioning feedback obtained from a security formal analyzer. In this paper, we present how our toolkit supports security modeling, automated security integration, and formal analysis during the HW/SW partitioning phase for secure communications in embedded systems. We introduce "Cryptographic Configurations", an abstract representation of security that allows us to verify security formally. Our toolkit further assists designers by automatically adding these security representations based on a mapping and security requirements.
KW - Embedded systems
KW - Formal verification
KW - Partitioning
KW - ProVerif
UR - https://www.scopus.com/pages/publications/85043324734
U2 - 10.5220/0006119603020311
DO - 10.5220/0006119603020311
M3 - Conference contribution
AN - SCOPUS:85043324734
T3 - MODELSWARD 2017 - Proceedings of the 5th International Conference on Model-Driven Engineering and Software Development
SP - 302
EP - 311
BT - MODELSWARD 2017 - Proceedings of the 5th International Conference on Model-Driven Engineering and Software Development
A2 - Pires, Luis Ferreira
A2 - Hammoudi, Slimane
A2 - Selic, Bran
PB - SciTePress
T2 - 5th International Conference on Model-Driven Engineering and Software Development, MODELSWARD 2017
Y2 - 19 February 2017 through 21 February 2017
ER -