MPInspector：一种系统化自动评估IoT消息协议安全性的方法
MPInspector: A Systematic and Automatic Approach for Evaluating the Security of IoT Messaging Protocols
摘要：
通过消息传递协议（MP）的促进，许多家庭设备连接到互联网，为客户带来便利和可访问性。然而，物联网平台上部署的大多数MP都是分散的，并且没有仔细实施以支持安全通信。据我们所知，目前还没有系统的解决方案来对MP实现执行自动安全检查。为了弥补这一差距，我们提出了MPInspector，这是第一个用于审查MP实现安全性的自动和系统解决方案。MPInspector将模型学习与形式化分析相结合，分为三个阶段：（a）使用参数语义提取和交互逻辑提取来自动推断MP实现的状态机，（b）基于Meta属性和状态机生成安全属性，以及（c）应用基于属性的自动形式化验证来识别属性违规。我们在三个流行的MP上评估了MPInspector，包括MQTT，CoAP和AMQP，这些MP在九个领先的物联网平台上实现。它确定了252个财产违规行为，利用这些违规行为，我们进一步确定了两种现实攻击场景下的11种攻击类型。此外，我们还证明了MPInspector是轻量级的（端到端分析的平均开销约为4.5小时），并且在识别属性违规方面具有100%的精度。
英文摘要：
Facilitated by messaging protocols (MP), many home devices are connected to the Internet, bringing convenience and accessibility to customers. However, most deployed MPs on IoT platforms are fragmented and are not implemented carefully to support secure communication. To the best of our knowledge, there is no systematic solution to perform automatic security checks on MP implementations yet. To bridge the gap, we present MPInspector, the first automatic and systematic solution for vetting the security of MP implementations. MPInspector combines model learning with formal analysis and operates in three stages: (a) using parameter semantics extraction and interaction logic extraction to automatically infer the state machine of an MP implementation, (b) generating security properties based on meta properties and the state machine, and (c) applying automatic property based formal verification to identify property violations. We evaluate MPInspector on three popular MPs, including MQTT, CoAP and AMQP, implemented on nine leading IoT platforms. It identifies 252 property violations, leveraging which we further identify eleven types of attacks under two realistic attack scenarios. In addition, we demonstrate that MPInspector is lightweight (the average overhead of end-to-end analysis is ~4.5 hours) and effective with a precision of 100% in identifying property violations.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
