ProChecker: An Automated Security and Privacy Analysis Framework for 4G LTE Protocol Implementations
ProChecker: An Automated Security and Privacy Analysis Framework for 4G LTE Protocol Implementations
复制标题
ProChecker：用于 4G LTE 协议实施的自动安全和隐私分析框架
DOI：
10.1109/icdcs51616.2021.00079
复制
发表时间：
2021
期刊：
影响因子：
--
通讯作者：
E. Bertino
中科院分区：
文献类型：
--
作者：
Imtiaz Karim;Syed Rafiul Hussain;E. Bertino
蜂窝协议实现必须符合规范以及安全和隐私要求。然而，由于蜂窝标准中的规范、固有的协议复杂性以及引起逻辑漏洞的设计缺陷，这些实现经常偏离安全和隐私要求。由于对内部状态的操作依赖性以及多个参与者之间交织的复杂协议交互，检测复杂且有状态的4G LTE协议中的此类逻辑漏洞具有挑战性。在本文中，我们解决了这些挑战，并开发Proximity-（1）提取一个精确的语义模型作为有限状态机的实现相结合的动态测试与静态仪器，和（2）验证属性对提取的模型相结合的符号模型检查器和加密协议验证。我们证明了Proximity的有效性，通过评估它的封闭源代码和两个最流行的开源4G LTE控制平面协议实现62属性。Prologan公布了3个新的协议特定的逻辑攻击，6个实现问题，并检测到14个先前的攻击。攻击的影响范围从拒绝服务、破坏完整性、加密和重放保护到隐私泄露。
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.