TY - GEN
T1 - ProChecker
T2 - 41st IEEE International Conference on Distributed Computing Systems, ICDCS 2021
AU - Karim, Imtiaz
AU - Hussain, Syed Rafiul
AU - Bertino, Elisa
N1 - Publisher Copyright:
© 2021 IEEE.
PY - 2021/7
Y1 - 2021/7
N2 - Cellular protocol implementations must comply with the specifications, and the security and privacy requirements. These implementations, however, often deviate from the security and privacy requirements due to under specifications in cellular standards, inherent protocol complexities, and design flaws inducing logical vulnerabilities. Detecting such logical vulnerabilities in the complex and stateful 4G LTE protocol is challenging due to operational dependencies on internal-states, and intertwined complex protocol interactions among multiple participants. In this paper, we address these challenges and develop ProChecker which- (1) extracts a precise semantic model as a finite-state machine of the implementation by combining dynamic testing with static instrumentation, and (2) verifies the properties against the extracted model by combining a symbolic model checker and a cryptographic protocol verifier. We demonstrate the effectiveness of ProChecker by evaluating it on a closed-source and two of the most popular open-source 4G LTE control-plane protocol implementations with 62 properties. ProChecker unveiled 3 new protocol-specific logical attacks, 6 implementation issues, and detected 14 prior attacks. The impact of the attacks range from denial-of-service, broken integrity, encryption, and replay protection to privacy leakage.
AB - Cellular protocol implementations must comply with the specifications, and the security and privacy requirements. These implementations, however, often deviate from the security and privacy requirements due to under specifications in cellular standards, inherent protocol complexities, and design flaws inducing logical vulnerabilities. Detecting such logical vulnerabilities in the complex and stateful 4G LTE protocol is challenging due to operational dependencies on internal-states, and intertwined complex protocol interactions among multiple participants. In this paper, we address these challenges and develop ProChecker which- (1) extracts a precise semantic model as a finite-state machine of the implementation by combining dynamic testing with static instrumentation, and (2) verifies the properties against the extracted model by combining a symbolic model checker and a cryptographic protocol verifier. We demonstrate the effectiveness of ProChecker by evaluating it on a closed-source and two of the most popular open-source 4G LTE control-plane protocol implementations with 62 properties. ProChecker unveiled 3 new protocol-specific logical attacks, 6 implementation issues, and detected 14 prior attacks. The impact of the attacks range from denial-of-service, broken integrity, encryption, and replay protection to privacy leakage.
UR - http://www.scopus.com/inward/record.url?scp=85117144236&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85117144236&partnerID=8YFLogxK
U2 - 10.1109/ICDCS51616.2021.00079
DO - 10.1109/ICDCS51616.2021.00079
M3 - Conference contribution
AN - SCOPUS:85117144236
T3 - Proceedings - International Conference on Distributed Computing Systems
SP - 773
EP - 785
BT - Proceedings - 2021 IEEE 41st International Conference on Distributed Computing Systems, ICDCS 2021
PB - Institute of Electrical and Electronics Engineers Inc.
Y2 - 7 July 2021 through 10 July 2021
ER -