Bridging the Gap: Automated Analysis of Sancus
arxiv(2024)
摘要
Techniques for verifying or invalidating the security of computer systems
have come a long way in recent years. Extremely sophisticated tools are
available to specify and formally verify the behavior of a system and, at the
same time, attack techniques have evolved to the point of questioning the
possibility of obtaining adequate levels of security, especially in critical
applications. In a recent paper, Bognar et al. have clearly highlighted this
inconsistency between the two worlds: on one side, formal verification allows
writing irrefutable proofs of the security of a system, on the other side
concrete attacks make these proofs waver, exhibiting a gap between models and
implementations which is very complex to bridge. In this paper, we propose a
new method to reduce this gap in the Sancus embedded security architecture, by
exploiting some peculiarities of both approaches. Our technique first extracts
a behavioral model by directly interacting with the real Sancus system and then
analyzes it to identify attacks and anomalies. Given a threat model, our method
either finds attacks in the given threat model or gives probabilistic
guarantees on the security of the system. We implement our method and use it to
systematically rediscover known attacks and uncover new ones.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要