MQTTactic: Security Analysis and Verification for Logic Flaws in MQTT Implementations

MQTTactic: Security Analysis and Verification for Logic Flaws in MQTT Implementations

Speakers: Bin Yuan, Zhanxiang Song, Yan Jia, Zhenyu Lu, Deqing Zou, Hai Jin

Conference: IEEE S&P

YouTube: https://www.youtube.com/watch?v=cpDtMQyry5o

Overview

The Internet of Things (IoT) relies heavily on efficient and lightweight communication protocols, with MQTT (Message Queuing Telemetry Transport) emerging as the most widely adopted standard in the wild. Its publish-subscribe architecture allows for decoupled communication between devices and users, mediated by a central broker. However, the rapid proliferation of IoT and the sheer number of diverse open-source MQTT implementations—over 70 on GitHub, with popular brokers like Mosquitto boasting over 800,000 deployments—introduce significant security challenges. This talk, "MQTTactic," presented by Yan Jia from Huazhong University of Science and Technology, alongside collaborators from Indiana University Bloomington and Nanjing University, delves into these critical security gaps.

The core problem addressed by MQTTactic is the prevalence of logic flaws, particularly those related to authorization mechanisms, within these heterogeneous MQTT broker implementations. While the MQTT specification defines messaging flows, developers often introduce customized logic and authorization checks that can be incorrectly implemented, leading to exploitable vulnerabilities. The research highlights a critical oversight: despite MQTT's pervasive use, little work has focused on formally verifying the security of its implementations, especially concerning message delivery guarantees and authorization. MQTTactic proposes a novel, specification-driven, and static analysis-based approach to model and formally verify these complex messaging flows, revealing a significant number of zero-day vulnerabilities in the process.

The implications of these findings are substantial, affecting not only individual open-source projects but also major IoT service providers such as AWS and IBM, whose MQTT-based offerings are susceptible to the identified flaws. The presentation details a robust methodology involving state machine modeling, static code analysis, and model checking to systematically uncover these subtle yet critical authorization bypasses and logic errors. This work provides a much-needed framework for enhancing the security posture of MQTT ecosystems, offering actionable insights for both developers and defenders in the IoT space.

Background

▶ Watch: Introduction to MQTT and its widespread adoption (0:00)

MQTT has solidified its position as the leading messaging protocol for IoT, a status underscored by its prominence in Eclipse IoT developer surveys and Google Trends data. Its publish-subscribe paradigm elegantly decouples message senders (publishers) from receivers (subscribers), allowing them to communicate without direct connections or explicit knowledge of each other. The broker acts as an intermediary, responsible for routing messages based on topics. This lightweight and efficient design makes MQTT ideal for resource-constrained IoT devices and unreliable network conditions.

However, the very flexibility and popularity that drive MQTT's adoption also introduce significant security complexities. The specification outlines numerous messaging flows, such as a device initiating a connection with a will message that must be published after an unexpected network closure. Beyond these standard flows, implementations frequently tailor custom messaging logic to meet specific business or application requirements. For instance, Quality of Service (QoS) level 2, which guarantees "exactly once" message delivery, often involves intricate internal queuing mechanisms. Mosquitto, a widely deployed broker, illustrates this with its inflight queue and catch queue for managing unfinished QoS2 messages, where new messages are held until space becomes available in the inflight queue. These custom implementations, while necessary for functionality, can introduce subtle logic errors.

A similar challenge arises with authorization mechanisms. While most brokers adopt a consistent authorization model (e.g., a three-tuple of client, topic, and access right), the protocol's flexibility leaves the "when" and "how" of permission checks entirely to the developer. This autonomy frequently results in inconsistent or incorrect authorization checks, creating bypass vulnerabilities. The research emphasizes that a comprehensive methodology for analyzing the security of these customized messaging flows and authorization mechanisms in open-source MQTT brokers has been conspicuously absent. The threat model considered by the researchers focuses on scenarios like device sharing, prevalent in hotels or short-term rentals, where user access rights are dynamic and subject to revocation or expiration. In such environments, a malicious user may collect their own network traffic but cannot eavesdrop on or interfere with other users' communications, aiming to exploit broker logic to gain unauthorized control over devices.

Key Findings

▶ Watch: Demonstrating a logic flaw in Mosquitto with an example (4:10)

The MQTTactic research uncovered a critical landscape of vulnerabilities, identifying seven types of zero-day authorization-related logic flaws across a range of open-source MQTT implementations. These findings are not confined to obscure projects; the researchers explicitly state that MQTT brokers provided by major IoT service providers like AWS and IBM are also susceptible to the identified flaw types, highlighting a systemic issue within the broader MQTT ecosystem.

One compelling motivating example detailed in the talk involves the popular Mosquitto broker and its handling of QoS2 messages. In this scenario, a malicious user initiates a QoS2 message publication. The broker, adhering to the "exactly once" delivery guarantee, stores the message and awaits a subsequent PUBLISH_RELEASE packet from the publisher before delivering it to subscribers. The critical flaw emerges when an administrator revokes the malicious user's permissions in the interim. Despite this revocation, the malicious user can still send the PUBLISH_RELEASE packet. Crucially, Mosquitto's implementation lacks a permission check for the sender of the PUBLISH_RELEASE packet. This oversight allows the previously published, now unauthorized, QoS2 message to be delivered, effectively enabling the malicious user to send instructions like "open the door" or "open the lock" to a device, bypassing the intended security controls. This demonstrates a classic time-of-check to time-of-use (TOCTOU) vulnerability in the authorization flow.

Another significant finding, identified specifically in Flash MQ, concerns the "will message" functionality. The "will message" is designed to be published by the broker when a client disconnects unexpectedly. The vulnerability allows a malicious user, such as a guest in a hotel or Airbnb scenario, to take control of any device that does not belong to them. This is achieved by creating a "will message" with a topic specifically associated with a target device. The underlying reason for this flaw is that the Flash MQ broker neither checks the permission when accepting the "will message" nor when it subsequently delivers it upon the client's disconnection. This complete absence of authorization checks at crucial stages of the "will message" lifecycle grants an attacker arbitrary control over devices by simply crafting a malicious "will message" and then disconnecting.

These examples vividly illustrate the fundamental problem: the protocol's flexibility combined with diverse, often custom, implementation details leads to authorization logic being omitted or incorrectly placed. The 7 types of flaws encompass various scenarios where permissions are either not checked, checked at the wrong time, or can be bypassed due to an incomplete understanding of the protocol's state transitions and message delivery guarantees.

Technical Deep Dive

▶ Watch: Overview of their specification-driven static analysis approach (6:20)

The core of the MQTTactic research lies in its novel methodology for uncovering logic flaws in MQTT broker implementations. The approach is specification-driven and static analysis-based, designed to model and formally verify the intricate messaging flows within these systems. The overall workflow consists of three main phases: defining a general broker model, constructing a state transition model from source code, and applying model checking.

Phase 1: General MQTT Broker Model Definition

The researchers first propose a formal definition of an MQTT broker using a state machine model, represented by the tuple (V, O, S, A, Delta, SP).

• V (Finite Set of State Variables): This represents the collective state of the MQTT broker. The researchers meticulously analyzed the entire MQTT protocol specification to identify and extract these critical variables. Examples include the server's session state, client subscriptions, and the "will message" associated with a client. A comprehensive table of all state variables was constructed from the specification.
• O (Set of Generalized Low-Level Operations): These are fundamental operations performed on the variables in V. This abstraction allows for modeling how the broker manipulates its internal state.
• S (Set of States): The set of all possible configurations the broker can be in, determined by the values of the variables in V.
• A (Set of Client Actions): These are the actions clients can perform, such as CONNECT, PUBLISH, SUBSCRIBE, PUBREC, PUBREL, etc.
• Delta (Transition Function): This function dictates how the system transitions from one state to the next based on client actions and internal operations.
• SP (Security Properties): These are the formal security invariants that the model must satisfy. A crucial example property stated is: "When a message is accepted and delivered by the broker, the sender of the message should have the right to send that message." This property directly targets authorization bypasses.

Phase 2: State Transition Model Construction from Source Code

This phase bridges the gap between the abstract model and concrete broker implementations. The process begins by converting the source code of the MQTT implementation into LLVM Intermediate Representation (IR), which serves as the input for static analysis.

1. Identifying Key Basic Blocks:

• The first step involves applying static analysis to identify key basic blocks within the broker's Control Flow Graph (CFG). A key basic block is defined as a basic block that performs at least one operation (read or modification) on a state variable from the set V.
• To achieve this, the researchers manually map the abstract state variables (V) to their corresponding variables in the source code.
• They then leverage pointer analysis (specifically using the SVF framework) to precisely locate all instances where these state variables are accessed or modified within the code. This information is recorded, and the relevant basic blocks are marked as "key." For example, a line of code reading a "will message" variable or removing an entry from a subscription list would correspond to a key basic block.

1. Extracting Pass Types:

• Once key basic blocks are identified, the next step is to extract the execution order of these blocks within the control flow. This ordered sequence is defined as a pass type.
• A pass type represents the unique processing logic and semantics an MQTT packet undergoes within the implementation.
• Crucially, along with the sequence of key basic blocks, any permission-related constraints encountered along the path are also recorded. This includes conditional checks (if statements) that determine whether an action is authorized.

1. Filtering Effective Pass Types:

• Implementations often contain many mutually exclusive conditions, leading to numerous potential pass types. Many of these, however, might be infeasible or unreachable due to contradictory conditions.
• To obtain only the effective pass types, the researchers employ symbolic execution (using a K-search algorithm). Symbolic execution explores different execution paths by assigning symbolic values to inputs and tracking path conditions. By solving these path conditions, it can identify and exclude "false" or infeasible pass types, ensuring that only realistic execution paths are considered for verification.

Phase 3: Model Checking

The final phase translates the extracted information into a format suitable for formal verification.

• The effective pass types, along with their corresponding handling logic for each MQTT action (e.g., PUBLISH, SUBSCRIBE), are translated into the Promela Modeling Language. Promela is the specification language for the Spin model checker.
• Since each MQTT action can have multiple different pass types and associated logic, a unique transition function is created for each pass type. These transition functions collectively drive the state transitions of the entire model.
• Finally, the Spin model checker is employed. Spin systematically explores all possible states and transitions within the Promela model. During this exploration, it continuously checks if the defined security properties (SP) are violated. If a violation is found, Spin generates a counterexample trace, which is a sequence of events leading to the insecure state, providing crucial debugging information for developers. The property "when a message is accepted and delivered by the broker, the sender of the message should have the right to send that message" is a prime example of what Spin would verify.

This comprehensive, multi-stage methodology allows MQTTactic to systematically analyze complex, real-world MQTT broker codebases, moving beyond simple vulnerability scanning to uncover deep-seated logic flaws that arise from the interplay of protocol specification, custom implementation, and authorization semantics.

Demo / Proof of Concept

▶ Watch: Extracting 'pass types' from source code control flow (9:30)

While the talk did not feature a live, interactive demonstration of the MQTTactic tool in action, the speakers presented concrete proof-of-concept scenarios derived from their analysis. These examples served to illustrate the practical impact and exploitability of the logic flaws discovered by their methodology.

The primary proof-of-concept scenarios discussed were the Mosquitto QoS2 authorization bypass and the Flash MQ "will message" vulnerability. In the Mosquitto case, the speakers walked through the sequence of events: a malicious user publishes a QoS2 message, permissions are revoked, but the broker's lack of a permission check on the subsequent PUBLISH_RELEASE packet allows the message to be delivered anyway. This detailed narrative, accompanied by a diagram, clearly demonstrated how an attacker could leverage this flaw to send unauthorized commands.

Similarly, the Flash MQ "will message" vulnerability was presented as a scenario where a malicious client could craft a "will message" targeting a specific device topic, and due to the broker's failure to perform authorization checks at both message acceptance and delivery, could gain unauthorized control upon disconnection. These examples, though presented as conceptual demonstrations rather than live code execution, effectively showcased the types of critical vulnerabilities MQTTactic is designed to uncover and the potential for real-world impact in IoT environments, particularly in multi-user settings like smart homes or rental properties.

Defensive Implications

▶ Watch: Complete workflow for modeling MQTT implementations (MQTTactic) (10:30)

The findings from MQTTactic offer crucial insights for both MQTT broker developers and IoT system administrators, emphasizing the need for a paradigm shift in how security is approached in MQTT ecosystems.

For MQTT Broker Developers:

• Rigorous Security Verification: The primary takeaway is the absolute necessity for rigorous security verification of all custom logic and authorization mechanisms. Relying solely on the MQTT specification is insufficient; the implementation details are where logic flaws reside. Developers should consider adopting formal methods like model checking, as demonstrated by MQTTactic, into their development lifecycle.
• Comprehensive Authorization Checks: Authorization checks must be consistently applied at all relevant stages of message processing, not just at the initial connection or publication. This includes ensuring checks are performed for subsequent packets in multi-stage flows (e.g., PUBREC, PUBREL, PUBLISH_RELEASE for QoS2), during will message handling (both acceptance and delivery), and any other custom messaging logic.
• "Deny by Default" Principle: Implement a "deny by default" approach for all access control decisions. Explicitly grant permissions rather than assuming they are absent.
• State Machine Thinking: Developers should think in terms of state machines, meticulously defining and verifying state transitions and how permissions evolve across these transitions, particularly when permissions are revoked or modified dynamically.
• Continuous Fuzzing and Static Analysis: Integrate advanced static analysis tools, pointer analysis, and fuzzing techniques into the CI/CD pipeline to proactively identify potential areas where state variables are mishandled or authorization logic is incomplete.

For IoT System Administrators and Users:

• Broker Updates: Keep MQTT brokers updated to the latest versions. The identified zero-day flaws underscore the constant need for patching and vigilance against newly discovered vulnerabilities.
• Least Privilege: Implement the principle of least privilege for all MQTT clients and users. Grant only the minimum necessary permissions to perform their functions and revoke them promptly when no longer needed.
• Network Segmentation: Isolate critical IoT devices and their respective MQTT topics/brokers onto separate network segments with stricter access controls. This can limit the blast radius if an authorization bypass occurs.
• Authorization Proxies/Gateways: Consider deploying an authorization proxy or API gateway in front of the MQTT broker. This proxy can enforce a consistent and centralized authorization policy, acting as a redundant layer of defense that can catch authorization errors missed by the broker's internal logic.
• Monitoring and Alerting: Implement robust logging and monitoring for MQTT broker activity, especially for failed authorization attempts, unusual message patterns, or unexpected device control commands. Set up alerts for suspicious activity.
• Vendor Due Diligence: When choosing commercial IoT platforms or MQTT brokers, inquire about their security verification processes, especially concerning custom logic and authorization. The fact that major providers were susceptible highlights that even well-resourced organizations can have these blind spots.

Ultimately, the MQTTactic research serves as a stark reminder that the security of complex, distributed systems like IoT hinges not just on cryptography or network security, but critically on the correctness and robustness of application-level logic and authorization mechanisms.

Key Takeaways

• Pervasive Logic Flaws: MQTT's popularity and diverse implementations have led to widespread authorization-related logic flaws in open-source brokers.
• Critical Impact: Seven types of zero-day vulnerabilities were uncovered, affecting widely deployed brokers and those from major IoT service providers like AWS and IBM.
• Mosquitto QoS2 Bypass: A key example demonstrated how Mosquitto's lack of permission checks for PUBLISH_RELEASE packets allows unauthorized QoS2 message delivery despite prior permission revocation.
• Flash MQ "Will Message" Vulnerability: Another significant flaw showed how Flash MQ's omission of authorization checks for "will messages" enables unauthorized device control.
• MQTTactic Methodology: The research introduces a novel, specification-driven, static analysis, and model checking framework (using SVF, symbolic execution, and Spin) to systematically identify these complex flaws.
• Developer Responsibility: Developers must prioritize rigorous security verification, particularly for custom logic and authorization mechanisms, by adopting formal methods and comprehensive authorization checks across all message lifecycle stages.

About the Speaker(s)

The talk "MQTTactic: Security Analysis and Verification for Logic Flaws in MQTT Implementations" was presented by Yan Jia from Huazhong University of Science and Technology. The research is a collaborative effort, with co-authors including Bin Yuan, Zhanxiang Song, Zhenyu Lu, Deqing Zou, and Hai Jin, affiliated with institutions such as Huazhong University of Science and Technology, Indiana University Bloomington, and Nanjing University. The team's expertise spans network security, IoT protocols, and formal verification methods, contributing to their in-depth analysis of MQTT broker implementations.