1
00:00:00,199 --> 00:00:03,280
hello everyone I am Jan from huaj

2
00:00:03,280 --> 00:00:05,440
University of Science and Technology

3
00:00:05,440 --> 00:00:08,599
this is a joint work with professors at

4
00:00:08,599 --> 00:00:10,639
University of Indiana University

5
00:00:10,639 --> 00:00:14,519
Bloomington and nanai

6
00:00:14,519 --> 00:00:17,039
University today with the popularity of

7
00:00:17,039 --> 00:00:19,480
the internet of things there is growing

8
00:00:19,480 --> 00:00:22,199
demand for effectively connecting iot

9
00:00:22,199 --> 00:00:25,119
devices and users lots of messaging

10
00:00:25,119 --> 00:00:28,240
Protocols are proposed to meet this

11
00:00:28,240 --> 00:00:31,080
demand according to top communication

12
00:00:31,080 --> 00:00:34,360
protocols from Eclipse iot developer

13
00:00:34,360 --> 00:00:38,160
survey and the results of four common

14
00:00:38,160 --> 00:00:40,520
used messaging protocols on Google

15
00:00:40,520 --> 00:00:44,559
Trends our research subject mqtt has

16
00:00:44,559 --> 00:00:48,039
become AR's most widely adopted FY in

17
00:00:48,039 --> 00:00:51,320
the wild due to its lightweight and

18
00:00:51,320 --> 00:00:53,879
efficient

19
00:00:54,680 --> 00:00:58,800
features so how mq Works mqt use a

20
00:00:58,800 --> 00:01:01,640
publish subscribe p P to DEC compose the

21
00:01:01,640 --> 00:01:04,640
clients that send a message from clients

22
00:01:04,640 --> 00:01:07,600
that receive message by allowing them to

23
00:01:07,600 --> 00:01:09,759
communicate without having direct

24
00:01:09,759 --> 00:01:13,159
connections or knowledge of each other's

25
00:01:13,159 --> 00:01:15,840
existence the essence of this pattern is

26
00:01:15,840 --> 00:01:19,159
that a middleman world called broker is

27
00:01:19,159 --> 00:01:21,960
responsible for rooting and distributing

28
00:01:21,960 --> 00:01:25,280
all messages publisher send message with

29
00:01:25,280 --> 00:01:29,000
a topic to to broker and subscribers

30
00:01:29,000 --> 00:01:32,640
subscribe to topic from the broker to

31
00:01:32,640 --> 00:01:35,880
receive message of Interest however is

32
00:01:35,880 --> 00:01:38,000
this decoupled method of message

33
00:01:38,000 --> 00:01:40,840
transmission pattern truly secure

34
00:01:40,840 --> 00:01:42,759
especially considering that there are

35
00:01:42,759 --> 00:01:45,920
over 70 open source implementations at

36
00:01:45,920 --> 00:01:49,159
GitHub each with it own heterogenous

37
00:01:49,159 --> 00:01:50,719
mqtt

38
00:01:50,719 --> 00:01:53,280
implementation one of the most popular

39
00:01:53,280 --> 00:01:58,200
broker is mosquito with more than

40
00:01:58,200 --> 00:02:01,039
800,000 deployments according to the

41
00:02:01,039 --> 00:02:04,399
data gathered from Zumi the saber space

42
00:02:04,399 --> 00:02:07,240
search engine however little work has

43
00:02:07,240 --> 00:02:11,000
been done to verify security of mity

44
00:02:11,000 --> 00:02:13,840
implementations especially for delivery

45
00:02:13,840 --> 00:02:14,640
of

46
00:02:14,640 --> 00:02:17,840
messages so as a messaging protocol

47
00:02:17,840 --> 00:02:19,680
there are numerous messaging flows

48
00:02:19,680 --> 00:02:23,239
specified in the mity specification for

49
00:02:23,239 --> 00:02:26,959
example the iot device can initiate a

50
00:02:26,959 --> 00:02:30,720
connection to the mut broker by sending

51
00:02:30,720 --> 00:02:33,760
a connect package with a whe

52
00:02:33,760 --> 00:02:36,599
message as a specification States the

53
00:02:36,599 --> 00:02:38,920
whe message must be published after

54
00:02:38,920 --> 00:02:43,319
network connection is subsequently

55
00:02:43,319 --> 00:02:46,000
closed except for those predefined

56
00:02:46,000 --> 00:02:47,840
messaging flows in the

57
00:02:47,840 --> 00:02:50,319
specification customized messaging flows

58
00:02:50,319 --> 00:02:53,560
are often tailored to specific business

59
00:02:53,560 --> 00:02:57,480
requirements or application scenarios in

60
00:02:57,480 --> 00:03:00,920
implementations for example plus 2

61
00:03:00,920 --> 00:03:03,920
offers the highest level quality of

62
00:03:03,920 --> 00:03:05,200
service in

63
00:03:05,200 --> 00:03:08,319
mqtt ensuring that each message is

64
00:03:08,319 --> 00:03:12,400
delivered exactly once to the receivers

65
00:03:12,400 --> 00:03:15,200
as shown in the figure mosquito stores

66
00:03:15,200 --> 00:03:20,799
unfinished qs2 messages in an infl queue

67
00:03:20,799 --> 00:03:24,120
after the infl que is full the new valid

68
00:03:24,120 --> 00:03:27,799
c 2 messages will be catched in a catch

69
00:03:27,799 --> 00:03:31,040
C thus the m messages in the cat queue

70
00:03:31,040 --> 00:03:33,319
will not be delivered until there is a

71
00:03:33,319 --> 00:03:35,760
vacancy in the infl

72
00:03:35,760 --> 00:03:38,120
queue additionally found that the

73
00:03:38,120 --> 00:03:40,040
implementation of the authorization

74
00:03:40,040 --> 00:03:42,840
mechanism is also diverse even though

75
00:03:42,840 --> 00:03:45,360
most of the Brokers we analyzed

76
00:03:45,360 --> 00:03:47,599
exhibited a relatively consistent

77
00:03:47,599 --> 00:03:50,760
authorization model which can be modeled

78
00:03:50,760 --> 00:03:56,280
as a three tle client topic and right to

79
00:03:56,280 --> 00:03:58,879
indicate that subject client is

80
00:03:58,879 --> 00:04:02,640
authorized to access the object topic

81
00:04:02,640 --> 00:04:06,360
with a access right however due to the

82
00:04:06,360 --> 00:04:08,200
protocol's flexibility in the

83
00:04:08,200 --> 00:04:11,200
authorization mechanism when and how

84
00:04:11,200 --> 00:04:14,480
permission checks are executed is

85
00:04:14,480 --> 00:04:16,680
entirely up to the

86
00:04:16,680 --> 00:04:19,639
developer this could lead to incorrectly

87
00:04:19,639 --> 00:04:22,120
implementing authorization

88
00:04:22,120 --> 00:04:25,639
checks and such customized messaging

89
00:04:25,639 --> 00:04:28,840
flaws and authorization mechanisms in

90
00:04:28,840 --> 00:04:31,800
open source implementations lead to Ming

91
00:04:31,800 --> 00:04:34,080
authorization related logic

92
00:04:34,080 --> 00:04:37,720
flaws however there are no comprehensive

93
00:04:37,720 --> 00:04:40,720
methods to analyze the security of

94
00:04:40,720 --> 00:04:45,160
messaging flaws of Open Source mity

95
00:04:45,160 --> 00:04:48,360
Brokers here is a motivating example

96
00:04:48,360 --> 00:04:51,800
about logic floss in mosquito as sh in

97
00:04:51,800 --> 00:04:54,639
the figure malicious user first

98
00:04:54,639 --> 00:04:59,039
publishes a qos to message to the broker

99
00:04:59,039 --> 00:05:02,199
and kuto chooses to store the message

100
00:05:02,199 --> 00:05:06,160
and await the Publishers publish release

101
00:05:06,160 --> 00:05:10,240
package for delivering the qs2 message

102
00:05:10,240 --> 00:05:11,600
to

103
00:05:11,600 --> 00:05:14,759
subscribers despite despite permission

104
00:05:14,759 --> 00:05:18,160
voke action to marked in red the

105
00:05:18,160 --> 00:05:21,600
malicious user is still be able to send

106
00:05:21,600 --> 00:05:24,520
the instruction like open the door open

107
00:05:24,520 --> 00:05:28,319
the lock to the device through the delay

108
00:05:28,319 --> 00:05:32,120
triggered quest to m in step four this

109
00:05:32,120 --> 00:05:34,479
is because mosquito likes permission

110
00:05:34,479 --> 00:05:37,360
check for the cender of the publish

111
00:05:37,360 --> 00:05:39,840
release

112
00:05:39,840 --> 00:05:43,600
package in our analysis we focus on iot

113
00:05:43,600 --> 00:05:47,120
systems that use mqt Brokers to manage

114
00:05:47,120 --> 00:05:49,280
and immediate communication between

115
00:05:49,280 --> 00:05:53,440
clients including users and iot devices

116
00:05:53,440 --> 00:05:56,680
the administrator can grant other users

117
00:05:56,680 --> 00:05:58,639
accessorise for

118
00:05:58,639 --> 00:06:01,680
devices the malicious user can collect

119
00:06:01,680 --> 00:06:04,720
and adlines network traffic between the

120
00:06:04,720 --> 00:06:08,560
broker and their own clients but cannot

121
00:06:08,560 --> 00:06:11,199
If drop on or interfere with

122
00:06:11,199 --> 00:06:14,520
communication between other users and

123
00:06:14,520 --> 00:06:17,160
broker we consider the situation of

124
00:06:17,160 --> 00:06:19,960
device sharing which has become

125
00:06:19,960 --> 00:06:22,840
pervasive today in places like hotels

126
00:06:22,840 --> 00:06:26,240
Airbnb apartments and other vacation

127
00:06:26,240 --> 00:06:29,880
rental homes in these scenarios us

128
00:06:29,880 --> 00:06:35,599
access R are subject to replication and

129
00:06:36,120 --> 00:06:39,039
exploration next we will detail our

130
00:06:39,039 --> 00:06:43,240
method for analyzing open source andity

131
00:06:43,240 --> 00:06:45,680
implementations specifically we propose

132
00:06:45,680 --> 00:06:48,400
a specification driving and static

133
00:06:48,400 --> 00:06:52,840
analysis based approach to model and

134
00:06:52,840 --> 00:06:55,560
verify messaging Flows In open source

135
00:06:55,560 --> 00:06:57,599
and City broker

136
00:06:57,599 --> 00:07:00,080
implementations in simple terms

137
00:07:00,080 --> 00:07:03,199
we use some mqtt specification to guide

138
00:07:03,199 --> 00:07:07,080
us in ident identifying Key State

139
00:07:07,080 --> 00:07:09,280
transitions in mq

140
00:07:09,280 --> 00:07:12,520
implementations then we created an

141
00:07:12,520 --> 00:07:15,960
abstruct implementation specific model

142
00:07:15,960 --> 00:07:18,759
finally we apply the model checking to

143
00:07:18,759 --> 00:07:22,440
your spin to verify safety properties on

144
00:07:22,440 --> 00:07:23,960
the

145
00:07:23,960 --> 00:07:27,199
model firstly we propose the general

146
00:07:27,199 --> 00:07:30,199
definition of an muted broker model

147
00:07:30,199 --> 00:07:33,400
which we described using a state machine

148
00:07:33,400 --> 00:07:36,720
here V is a finite set of whose value

149
00:07:36,720 --> 00:07:39,759
collectively constitute the states of

150
00:07:39,759 --> 00:07:44,879
theity broker specifically we extracted

151
00:07:44,879 --> 00:07:46,720
this information from the M commity

152
00:07:46,720 --> 00:07:49,400
specification for example this

153
00:07:49,400 --> 00:07:52,520
specification States uh the session set

154
00:07:52,520 --> 00:07:57,280
in the server consists of the client's

155
00:07:57,280 --> 00:08:01,199
subscriptions like this we we have fully

156
00:08:01,199 --> 00:08:04,280
analyzed the entire protocol

157
00:08:04,280 --> 00:08:06,479
specification and constructed the

158
00:08:06,479 --> 00:08:09,039
following table containing All State

159
00:08:09,039 --> 00:08:11,599
variables moreover in the model

160
00:08:11,599 --> 00:08:14,680
definition all is a set of generalized

161
00:08:14,680 --> 00:08:18,280
lowlevel operation on the variables in

162
00:08:18,280 --> 00:08:24,000
the set V and S is the set of States a

163
00:08:24,000 --> 00:08:26,080
is the client

164
00:08:26,080 --> 00:08:30,080
actions uh and data is a transition

165
00:08:30,080 --> 00:08:32,479
function that drives the system

166
00:08:32,479 --> 00:08:36,320
transition from one state to the next

167
00:08:36,320 --> 00:08:40,519
and SP is a secur properties to be

168
00:08:40,519 --> 00:08:43,279
verified next we will deta how to

169
00:08:43,279 --> 00:08:46,600
construct a state transition model from

170
00:08:46,600 --> 00:08:49,440
source code for hm cre broker based on

171
00:08:49,440 --> 00:08:52,880
model definition in the first step we

172
00:08:52,880 --> 00:08:57,200
apply of share static analysis to svf to

173
00:08:57,200 --> 00:09:00,480
help identify kis block blocks in the

174
00:09:00,480 --> 00:09:03,200
code a key basic block is the basic

175
00:09:03,200 --> 00:09:06,680
block in the broker sa G that performs

176
00:09:06,680 --> 00:09:10,480
at least one operation on a state

177
00:09:10,480 --> 00:09:14,720
variable speciically we first ma the

178
00:09:14,720 --> 00:09:16,680
state variables to the corresonding

179
00:09:16,680 --> 00:09:19,720
variables in the source code manually

180
00:09:19,720 --> 00:09:23,959
then we used pointer analysis to locate

181
00:09:23,959 --> 00:09:27,079
all the places where the state variables

182
00:09:27,079 --> 00:09:30,279
are accessed or modified

183
00:09:30,279 --> 00:09:32,760
we recorded this information and marked

184
00:09:32,760 --> 00:09:35,600
the relevant bis blocks as key bis

185
00:09:35,600 --> 00:09:39,519
blocks for example uh the second line of

186
00:09:39,519 --> 00:09:40,760
of the

187
00:09:40,760 --> 00:09:44,519
code is a read operation on on state

188
00:09:44,519 --> 00:09:48,040
variable where message and third line is

189
00:09:48,040 --> 00:09:50,079
a remove

190
00:09:50,079 --> 00:09:53,560
operation the next step is to extract

191
00:09:53,560 --> 00:09:56,240
the execution order of these blocks in

192
00:09:56,240 --> 00:09:58,360
control flow which is also defined as

193
00:09:58,360 --> 00:10:01,279
pass types plus typ is a unique sequence

194
00:10:01,279 --> 00:10:04,600
of key basic blocks and represents the

195
00:10:04,600 --> 00:10:07,760
processing logic semantics of an mq

196
00:10:07,760 --> 00:10:09,120
packet in the

197
00:10:09,120 --> 00:10:10,959
implementation we also request

198
00:10:10,959 --> 00:10:13,200
permission related constraints along P

199
00:10:13,200 --> 00:10:16,680
types finally uh since there are many

200
00:10:16,680 --> 00:10:19,720
mutely exclusive conditions on the P

201
00:10:19,720 --> 00:10:22,720
types we construct it just like the

202
00:10:22,720 --> 00:10:26,079
figure on the right the conditions for

203
00:10:26,079 --> 00:10:29,480
variable a on the pass cannot be set

204
00:10:29,480 --> 00:10:31,480
find

205
00:10:31,480 --> 00:10:33,680
simultaneously so we use a symol

206
00:10:33,680 --> 00:10:38,120
execution to hayar to serve uh past

207
00:10:38,120 --> 00:10:41,720
conditions and exclude forse P types

208
00:10:41,720 --> 00:10:45,160
thus obtaining effective P types here is

209
00:10:45,160 --> 00:10:49,040
a complete workflow of modeling mqt

210
00:10:49,040 --> 00:10:51,720
implementations we converted source code

211
00:10:51,720 --> 00:10:56,120
of implementation into airm IR as input

212
00:10:56,120 --> 00:10:59,720
and use static code analysis to uh

213
00:10:59,720 --> 00:11:03,399
identify keis blocks and extract all

214
00:11:03,399 --> 00:11:05,480
effective pass types from the control

215
00:11:05,480 --> 00:11:08,880
flow graph we completed this process

216
00:11:08,880 --> 00:11:12,200
separately for different mqd actions or

217
00:11:12,200 --> 00:11:16,720
packet like publish And subscribe

218
00:11:16,720 --> 00:11:20,079
consequently we cently get the handle

219
00:11:20,079 --> 00:11:23,639
logic of each mqd action or package in

220
00:11:23,639 --> 00:11:24,839
the

221
00:11:24,839 --> 00:11:27,200
implementation then we translate the P

222
00:11:27,200 --> 00:11:29,639
types into the prula modeling language

223
00:11:29,639 --> 00:11:33,800
for model checking know that each mqt

224
00:11:33,800 --> 00:11:36,519
action has multiple different pass types

225
00:11:36,519 --> 00:11:39,079
and corresponding handling logic

226
00:11:39,079 --> 00:11:40,760
therefore we create a transition

227
00:11:40,760 --> 00:11:42,800
function for each P type which drives

228
00:11:42,800 --> 00:11:45,519
the state transition of the entire model

229
00:11:45,519 --> 00:11:48,959
the model Checker then help us explore

230
00:11:48,959 --> 00:11:52,160
all possible States and checks if this

231
00:11:52,160 --> 00:11:54,720
stat VI as secur properties defined in

232
00:11:54,720 --> 00:11:57,519
the model definition for example a

233
00:11:57,519 --> 00:12:00,480
property can be when when a message is

234
00:12:00,480 --> 00:12:03,720
is accepted and delivered by the broker

235
00:12:03,720 --> 00:12:05,839
the sender of the message should have

236
00:12:05,839 --> 00:12:08,600
the right to send that

237
00:12:08,600 --> 00:12:12,480
message okay

238
00:12:12,480 --> 00:12:15,560
uh let's look at an example that

239
00:12:15,560 --> 00:12:16,800
violates the

240
00:12:16,800 --> 00:12:19,440
property this this is one of

241
00:12:19,440 --> 00:12:21,839
authorization related logical flaws

242
00:12:21,839 --> 00:12:23,839
identified in Flash

243
00:12:23,839 --> 00:12:27,440
mq specifically malicious user as a

244
00:12:27,440 --> 00:12:29,680
hotel or Airbnb C

245
00:12:29,680 --> 00:12:32,600
can take control of any device that does

246
00:12:32,600 --> 00:12:37,360
not belong to him by creating a re real

247
00:12:37,360 --> 00:12:41,000
message with Divine specific topic the

248
00:12:41,000 --> 00:12:43,880
underlying reason is that the broker NE

249
00:12:43,880 --> 00:12:46,440
checks the permission when accepting the

250
00:12:46,440 --> 00:12:49,880
we message nor when deliver

251
00:12:49,880 --> 00:12:53,959
it okay noise findings by applying two2

252
00:12:53,959 --> 00:12:56,600
seven open source implementations we

253
00:12:56,600 --> 00:12:59,959
uncovered seven types of zero day

254
00:12:59,959 --> 00:13:02,399
authorization related to logic

255
00:13:02,399 --> 00:13:06,199
flaws and mqt Brokers of major iot

256
00:13:06,199 --> 00:13:11,240
service providers like AWS IBM are also

257
00:13:11,240 --> 00:13:14,480
susceptible to the flaws we have

258
00:13:14,480 --> 00:13:19,720
identified okay that's all thank you