hello everyone I am Jan from huaj
University of Science and Technology
this is a joint work with professors at
University of Indiana University
Bloomington and nanai
University today with the popularity of
the internet of things there is growing
demand for effectively connecting iot
devices and users lots of messaging
Protocols are proposed to meet this
demand according to top communication
protocols from Eclipse iot developer
survey and the results of four common
used messaging protocols on Google
Trends our research subject mqtt has
become AR's most widely adopted FY in
the wild due to its lightweight and
efficient
features so how mq Works mqt use a
publish subscribe p P to DEC compose the
clients that send a message from clients
that receive message by allowing them to
communicate without having direct
connections or knowledge of each other's
existence the essence of this pattern is
that a middleman world called broker is
responsible for rooting and distributing
all messages publisher send message with
a topic to to broker and subscribers
subscribe to topic from the broker to
receive message of Interest however is
this decoupled method of message
transmission pattern truly secure
especially considering that there are
over 70 open source implementations at
GitHub each with it own heterogenous
mqtt
implementation one of the most popular
broker is mosquito with more than
800,000 deployments according to the
data gathered from Zumi the saber space
search engine however little work has
been done to verify security of mity
implementations especially for delivery
of
messages so as a messaging protocol
there are numerous messaging flows
specified in the mity specification for
example the iot device can initiate a
connection to the mut broker by sending
a connect package with a whe
message as a specification States the
whe message must be published after
network connection is subsequently
closed except for those predefined
messaging flows in the
specification customized messaging flows
are often tailored to specific business
requirements or application scenarios in
implementations for example plus 2
offers the highest level quality of
service in
mqtt ensuring that each message is
delivered exactly once to the receivers
as shown in the figure mosquito stores
unfinished qs2 messages in an infl queue
after the infl que is full the new valid
c 2 messages will be catched in a catch
C thus the m messages in the cat queue
will not be delivered until there is a
vacancy in the infl
queue additionally found that the
implementation of the authorization
mechanism is also diverse even though
most of the Brokers we analyzed
exhibited a relatively consistent
authorization model which can be modeled
as a three tle client topic and right to
indicate that subject client is
authorized to access the object topic
with a access right however due to the
protocol's flexibility in the
authorization mechanism when and how
permission checks are executed is
entirely up to the
developer this could lead to incorrectly
implementing authorization
checks and such customized messaging
flaws and authorization mechanisms in
open source implementations lead to Ming
authorization related logic
flaws however there are no comprehensive
methods to analyze the security of
messaging flaws of Open Source mity
Brokers here is a motivating example
about logic floss in mosquito as sh in
the figure malicious user first
publishes a qos to message to the broker
and kuto chooses to store the message
and await the Publishers publish release
package for delivering the qs2 message
to
subscribers despite despite permission
voke action to marked in red the
malicious user is still be able to send
the instruction like open the door open
the lock to the device through the delay
triggered quest to m in step four this
is because mosquito likes permission
check for the cender of the publish
release
package in our analysis we focus on iot
systems that use mqt Brokers to manage
and immediate communication between
clients including users and iot devices
the administrator can grant other users
accessorise for
devices the malicious user can collect
and adlines network traffic between the
broker and their own clients but cannot
If drop on or interfere with
communication between other users and
broker we consider the situation of
device sharing which has become
pervasive today in places like hotels
Airbnb apartments and other vacation
rental homes in these scenarios us
access R are subject to replication and
exploration next we will detail our
method for analyzing open source andity
implementations specifically we propose
a specification driving and static
analysis based approach to model and
verify messaging Flows In open source
and City broker
implementations in simple terms
we use some mqtt specification to guide
us in ident identifying Key State
transitions in mq
implementations then we created an
abstruct implementation specific model
finally we apply the model checking to
your spin to verify safety properties on
the
model firstly we propose the general
definition of an muted broker model
which we described using a state machine
here V is a finite set of whose value
collectively constitute the states of
theity broker specifically we extracted
this information from the M commity
specification for example this
specification States uh the session set
in the server consists of the client's
subscriptions like this we we have fully
analyzed the entire protocol
specification and constructed the
following table containing All State
variables moreover in the model
definition all is a set of generalized
lowlevel operation on the variables in
the set V and S is the set of States a
is the client
actions uh and data is a transition
function that drives the system
transition from one state to the next
and SP is a secur properties to be
verified next we will deta how to
construct a state transition model from
source code for hm cre broker based on
model definition in the first step we
apply of share static analysis to svf to
help identify kis block blocks in the
code a key basic block is the basic
block in the broker sa G that performs
at least one operation on a state
variable speciically we first ma the
state variables to the corresonding
variables in the source code manually
then we used pointer analysis to locate
all the places where the state variables
are accessed or modified
we recorded this information and marked
the relevant bis blocks as key bis
blocks for example uh the second line of
of the
code is a read operation on on state
variable where message and third line is
a remove
operation the next step is to extract
the execution order of these blocks in
control flow which is also defined as
pass types plus typ is a unique sequence
of key basic blocks and represents the
processing logic semantics of an mq
packet in the
implementation we also request
permission related constraints along P
types finally uh since there are many
mutely exclusive conditions on the P
types we construct it just like the
figure on the right the conditions for
variable a on the pass cannot be set
find
simultaneously so we use a symol
execution to hayar to serve uh past
conditions and exclude forse P types
thus obtaining effective P types here is
a complete workflow of modeling mqt
implementations we converted source code
of implementation into airm IR as input
and use static code analysis to uh
identify keis blocks and extract all
effective pass types from the control
flow graph we completed this process
separately for different mqd actions or
packet like publish And subscribe
consequently we cently get the handle
logic of each mqd action or package in
the
implementation then we translate the P
types into the prula modeling language
for model checking know that each mqt
action has multiple different pass types
and corresponding handling logic
therefore we create a transition
function for each P type which drives
the state transition of the entire model
the model Checker then help us explore
all possible States and checks if this
stat VI as secur properties defined in
the model definition for example a
property can be when when a message is
is accepted and delivered by the broker
the sender of the message should have
the right to send that
message okay
uh let's look at an example that
violates the
property this this is one of
authorization related logical flaws
identified in Flash
mq specifically malicious user as a
hotel or Airbnb C
can take control of any device that does
not belong to him by creating a re real
message with Divine specific topic the
underlying reason is that the broker NE
checks the permission when accepting the
we message nor when deliver
it okay noise findings by applying two2
seven open source implementations we
uncovered seven types of zero day
authorization related to logic
flaws and mqt Brokers of major iot
service providers like AWS IBM are also
susceptible to the flaws we have
identified okay that's all thank you