Automated Security Analysis for Real-World IoT Devices
Abstract
Automatic security protocol analysis is a fruitful research topic that demonstrates the application of formal methods to security analysis. Several endeavors in the last decades successfully verified security properties of large-scale network protocols like TLS, sometimes unveiling unknown vulnerabilities.
In this work, we show how to apply these techniques to the domain of IoT, where security is a critical aspect. While most existing security analyses for IoT tackle individually either protocols, firmware or applications, our goal is to treat IoT systems as a whole. We focus our work on a case study, the Armadillo-IoT G4 device, highlighting the specific challenges we must tackle to analyze the security of a typical IoT device. We propose a model using the Tamarin prover, that allows us to state certain key security properties about the device and to prove them automatically.
Cite
@inproceedings{brun_automated_2023,
address = {New York, NY, USA},
series = {{HASP}'23},
title = {Automated {Security} {Analysis} for {Real}-{World} {IoT} {Devices}},
copyright = {All rights reserved},
isbn = {979-8-4007-1623-2},
url = {https://www.leliobrun.net/publication/hasp23/paper.pdf},
doi = {10.1145/3623652.3623667},
abstract = {Automatic security protocol analysis is a fruitful research topic that demonstrates the application of formal methods to security analysis. Several endeavors in the last decades successfully verified security properties of large-scale network protocols like TLS, sometimes unveiling unknown vulnerabilities.
In this work, we show how to apply these techniques to the domain of IoT, where security is a critical aspect. While most existing security analyses for IoT tackle individually either protocols, firmware or applications, our goal is to treat IoT systems as a whole. We focus our work on a case study, the Armadillo-IoT G4 device, highlighting the specific challenges we must tackle to analyze the security of a typical IoT device. We propose a model using the Tamarin prover, that allows us to state certain key security properties about the device and to prove them automatically.},
language = {en},
booktitle = {Proceedings of the 12th {International} {Workshop} on {Hardware} and {Architectural} {Support} for {Security} and {Privacy}},
publisher = {Association for Computing Machinery},
author = {Brun, Lelio and Hasuo, Ichiro and Ono, Yasushi and Sekiyama, Taro},
month = oct,
year = {2023},
pages = {29--37},
}
