咨询与建议

看过本文的还看了

相关文献

该作者的其他文献

文献详情 >Automatic generation of securi... 收藏
Cyber Security and Applications

Automatic generation of security protocols attacks specifications and implementations

作     者:Garcia, Rémi Modesti, Paolo 

作者机构:Teesside University Middlesbrough United Kingdom 

出 版 物:《Cyber Security and Applications》 (Cyber. Secur. Appl.)

年 卷 期:2024年第2卷

基  金:Teesside University 

主  题:Attack analysis Automatic verification Code generation Formal methods for security Model-driven development 

摘      要:Confidence in a communication protocol s security is a key requirement for its deployment and long-term maintenance. Checking if a vulnerability exists and is exploitable requires extensive expertise. The research community has advocated for a systematic approach with formal methods to model and automatically test a protocol against a set of desired security properties. As verification tools reach conclusions, the applicability of their results still requires expert scrutiny. We propose a code generation approach to automatically build both an abstract specification and a concrete implementation of a Dolev-Yao intruder from an abstract attack trace, bridging the gap between theoretical attacks discovered by formal means and practical ones. Through our case studies, we focus on attack traces from the OFMC model checker, Alice&Bob specifications and Java implementations. We introduce a proof-of-concept workflow for concrete attack validation that allows to conveniently integrate, in a user-friendly way, formal methods results into a Model-Driven Development process and at the same time automatically generate a program that allows to demonstrate the attack in practice. In fact, in this contribution, we produce high-level and concrete attack narrations that are both human and machine readable. © 2024

读者评论 与其他读者分享你的观点

用户名:未登录
我的评分