1
00:00:00,000 --> 00:00:08,469
foreign

2
00:00:00,500 --> 00:00:08,469
[Music]

3
00:00:12,620 --> 00:00:17,279
core platform security and performance

4
00:00:15,420 --> 00:00:21,060
without the complexity

5
00:00:17,279 --> 00:00:23,100
with Yvonne velichkovic and Lucy Parker

6
00:00:21,060 --> 00:00:25,199
both our speakers are engineers at the

7
00:00:23,100 --> 00:00:27,359
trustworthy systems research group at

8
00:00:25,199 --> 00:00:29,820
unsw Sydney

9
00:00:27,359 --> 00:00:31,679
today they'll speak about the sel4 core

10
00:00:29,820 --> 00:00:34,500
platform which builds upon the secure

11
00:00:31,679 --> 00:00:36,680
sel4 micro kernel please welcome our

12
00:00:34,500 --> 00:00:36,680
speakers

13
00:00:38,110 --> 00:00:42,540
[Applause]

14
00:00:40,200 --> 00:00:43,379
hello thank you for having me

15
00:00:42,540 --> 00:00:45,300
um

16
00:00:43,379 --> 00:00:48,300
so like David said I'm from the

17
00:00:45,300 --> 00:00:50,879
trustworthy systems group we're based in

18
00:00:48,300 --> 00:00:53,640
unsw at Sydney and we're really trying

19
00:00:50,879 --> 00:00:55,219
to basically make Reliable Software so

20
00:00:53,640 --> 00:00:58,680
the group does this

21
00:00:55,219 --> 00:01:01,980
mainly focusing on operating systems and

22
00:00:58,680 --> 00:01:05,460
combining that with formal methods to

23
00:01:01,980 --> 00:01:07,320
um basically use mathematics to actually

24
00:01:05,460 --> 00:01:09,900
give software a high level of assurance

25
00:01:07,320 --> 00:01:12,479
than anything else can

26
00:01:09,900 --> 00:01:14,159
so before I talk about the SEO 4 core

27
00:01:12,479 --> 00:01:16,320
platform specifically I'm going to give

28
00:01:14,159 --> 00:01:19,200
a brief overview of what seo4 actually

29
00:01:16,320 --> 00:01:23,400
is for those that don't know

30
00:01:19,200 --> 00:01:25,619
so uh it's a micro kernel which is quite

31
00:01:23,400 --> 00:01:27,240
a radically different uh philosophy

32
00:01:25,619 --> 00:01:29,340
compared to what you might be used to

33
00:01:27,240 --> 00:01:30,720
with something like Linux or FreeBSD or

34
00:01:29,340 --> 00:01:31,320
Darwin

35
00:01:30,720 --> 00:01:34,979
um

36
00:01:31,320 --> 00:01:37,380
a micro kernel aims for minimality so

37
00:01:34,979 --> 00:01:39,119
what we're trying to do is push anything

38
00:01:37,380 --> 00:01:41,460
that doesn't actually need to be in

39
00:01:39,119 --> 00:01:43,799
kernel space out into user space

40
00:01:41,460 --> 00:01:46,380
and so this has some benefits such as

41
00:01:43,799 --> 00:01:49,159
isolation for example um which I'll

42
00:01:46,380 --> 00:01:49,159
touch on in a bit

43
00:01:49,200 --> 00:01:52,740
um so some examples of this are things

44
00:01:50,880 --> 00:01:54,960
like device drivers Process Management

45
00:01:52,740 --> 00:01:57,420
and even memory management to an extent

46
00:01:54,960 --> 00:01:58,740
are all done in user space and not in

47
00:01:57,420 --> 00:01:59,640
the kernel

48
00:01:58,740 --> 00:02:03,000
um

49
00:01:59,640 --> 00:02:06,600
so to illustrate this here's a diagram

50
00:02:03,000 --> 00:02:09,720
of Linux where inside the kernel in this

51
00:02:06,600 --> 00:02:13,500
blue box we have an IP stack a bunch of

52
00:02:09,720 --> 00:02:17,099
drivers various file systems and say one

53
00:02:13,500 --> 00:02:21,120
user program that wants to use these

54
00:02:17,099 --> 00:02:23,520
whereas on seo4 or you know micro kernel

55
00:02:21,120 --> 00:02:25,980
by seo4 in particular all of these

56
00:02:23,520 --> 00:02:28,220
basically components would be separate

57
00:02:25,980 --> 00:02:31,739
processes so if any one of these fails

58
00:02:28,220 --> 00:02:34,560
the whole system doesn't go down

59
00:02:31,739 --> 00:02:36,780
and then so in order for each of these

60
00:02:34,560 --> 00:02:38,400
uh basically components to communicate

61
00:02:36,780 --> 00:02:40,700
to each other they do that through the

62
00:02:38,400 --> 00:02:40,700
kernel

63
00:02:42,540 --> 00:02:47,459
it is also a verified micro kernel so

64
00:02:45,360 --> 00:02:49,739
what that means is that the

65
00:02:47,459 --> 00:02:53,099
implementation of the kernel is formally

66
00:02:49,739 --> 00:02:55,140
proven to match a specification of Its

67
00:02:53,099 --> 00:02:57,900
Behavior so this is done by having some

68
00:02:55,140 --> 00:03:00,239
abstract specification that then proves

69
00:02:57,900 --> 00:03:02,040
that the implementation in C actually

70
00:03:00,239 --> 00:03:03,319
matches that and then the binary

71
00:03:02,040 --> 00:03:07,019
actually

72
00:03:03,319 --> 00:03:08,400
is correct as well so you can don't

73
00:03:07,019 --> 00:03:12,739
necessarily have to actually trust your

74
00:03:08,400 --> 00:03:12,739
C compiler to emit the right by code

75
00:03:12,780 --> 00:03:16,860
so the code is all open source that's

76
00:03:15,060 --> 00:03:20,159
the kernel and then the proofs are also

77
00:03:16,860 --> 00:03:22,680
available and in terms of organizing the

78
00:03:20,159 --> 00:03:24,300
whole ecosystem that's done by the seo4

79
00:03:22,680 --> 00:03:26,540
foundation which you can find out more

80
00:03:24,300 --> 00:03:26,540
there

81
00:03:26,940 --> 00:03:32,060
so what does seo4 give us

82
00:03:29,940 --> 00:03:32,060
um

83
00:03:32,519 --> 00:03:38,400
seo4 attempts to give a high degree of

84
00:03:36,060 --> 00:03:42,900
freedom of policy so by policy I mean

85
00:03:38,400 --> 00:03:44,700
for example Linux will try to maybe load

86
00:03:42,900 --> 00:03:47,280
balance all the processes that are

87
00:03:44,700 --> 00:03:49,620
running say maybe move a process to

88
00:03:47,280 --> 00:03:51,840
another core or something like that seo4

89
00:03:49,620 --> 00:03:54,900
by Design will not do anything like that

90
00:03:51,840 --> 00:03:57,540
unless it's explicitly told to so you

91
00:03:54,900 --> 00:03:59,580
can attempt to make your ideal policy at

92
00:03:57,540 --> 00:04:02,540
user space rather than the kernel making

93
00:03:59,580 --> 00:04:04,200
these kinds of decisions for you

94
00:04:02,540 --> 00:04:06,299
it's

95
00:04:04,200 --> 00:04:07,739
quite high performance relative to other

96
00:04:06,299 --> 00:04:11,220
micro kernels I don't think there's

97
00:04:07,739 --> 00:04:14,099
anything that matches it so for example

98
00:04:11,220 --> 00:04:17,940
if you heard of fuchsia or the Zircon

99
00:04:14,099 --> 00:04:20,180
micro kernel or Mark or

100
00:04:17,940 --> 00:04:22,560
it's also High Assurance because of the

101
00:04:20,180 --> 00:04:24,120
formal verification aspect of it that I

102
00:04:22,560 --> 00:04:26,100
mentioned before

103
00:04:24,120 --> 00:04:28,380
um

104
00:04:26,100 --> 00:04:31,199
and lastly it has a capability based

105
00:04:28,380 --> 00:04:32,639
system so all of you will probably be

106
00:04:31,199 --> 00:04:35,460
familiar with something called file

107
00:04:32,639 --> 00:04:37,740
descriptors when you try to open a file

108
00:04:35,460 --> 00:04:40,800
on Linux with the open system call

109
00:04:37,740 --> 00:04:42,840
you'll get back a unique identifier that

110
00:04:40,800 --> 00:04:44,759
then you then pass to Linux whenever you

111
00:04:42,840 --> 00:04:45,800
want to actually do an operation on a

112
00:04:44,759 --> 00:04:49,680
file

113
00:04:45,800 --> 00:04:51,780
this same kind of concept in seo4 or a

114
00:04:49,680 --> 00:04:53,400
capability-based system applies to every

115
00:04:51,780 --> 00:04:55,800
resource

116
00:04:53,400 --> 00:04:57,840
so this allows fine-grained access

117
00:04:55,800 --> 00:04:59,520
control basically because if you want to

118
00:04:57,840 --> 00:05:01,800
be able to do any operations on a

119
00:04:59,520 --> 00:05:04,800
specific specific resource you have to

120
00:05:01,800 --> 00:05:07,979
have the capability to it

121
00:05:04,800 --> 00:05:10,460
so for example threads even the

122
00:05:07,979 --> 00:05:13,139
communication between threads memory

123
00:05:10,460 --> 00:05:15,240
interrupts and even to an extent how

124
00:05:13,139 --> 00:05:16,639
much CPU time a certain thread might

125
00:05:15,240 --> 00:05:19,860
spend

126
00:05:16,639 --> 00:05:22,580
executing is also modeled by the

127
00:05:19,860 --> 00:05:22,580
capability system

128
00:05:24,360 --> 00:05:29,880
so what I've said largely sounds like

129
00:05:27,600 --> 00:05:32,520
good things so why do we need the SEO 4

130
00:05:29,880 --> 00:05:36,240
core platform

131
00:05:32,520 --> 00:05:38,759
well building directly on seo4 has some

132
00:05:36,240 --> 00:05:41,340
trade-offs

133
00:05:38,759 --> 00:05:43,320
the apis are quite low level and general

134
00:05:41,340 --> 00:05:45,740
so this for example there's a bunch of

135
00:05:43,320 --> 00:05:48,620
you know architecture specific

136
00:05:45,740 --> 00:05:53,100
invocations or apis that you'll have to

137
00:05:48,620 --> 00:05:55,020
make even for basic systems and so this

138
00:05:53,100 --> 00:05:57,300
adds complexity when you want to

139
00:05:55,020 --> 00:06:00,000
actually use seo4 but the benefit of

140
00:05:57,300 --> 00:06:01,440
this is that you can depending on the

141
00:06:00,000 --> 00:06:05,220
application you're making you can really

142
00:06:01,440 --> 00:06:06,180
design your abstractions to be optimal

143
00:06:05,220 --> 00:06:09,240
for whatever you're trying to building

144
00:06:06,180 --> 00:06:11,280
whatever you're trying to build

145
00:06:09,240 --> 00:06:12,780
so the benefit is that you can build

146
00:06:11,280 --> 00:06:14,160
abstractions yourself because of these

147
00:06:12,780 --> 00:06:15,960
low-level apis

148
00:06:14,160 --> 00:06:17,400
but the cost is obviously that you have

149
00:06:15,960 --> 00:06:20,039
to build the abstractions yourself

150
00:06:17,400 --> 00:06:23,460
there's nothing in seo4 that's just like

151
00:06:20,039 --> 00:06:25,740
give me a bunch of memory for a process

152
00:06:23,460 --> 00:06:28,199
or something like that that involves

153
00:06:25,740 --> 00:06:30,720
several steps

154
00:06:28,199 --> 00:06:33,180
and this ultimately leads to a high

155
00:06:30,720 --> 00:06:36,259
barrier to entry in order to actually

156
00:06:33,180 --> 00:06:39,060
use seo4 correctly or in the first place

157
00:06:36,259 --> 00:06:43,139
there's quite a lot of operating system

158
00:06:39,060 --> 00:06:45,479
specific knowledge just to get started

159
00:06:43,139 --> 00:06:48,060
and so to visualize this

160
00:06:45,479 --> 00:06:50,100
I've got a diagram here or or an image

161
00:06:48,060 --> 00:06:52,259
of all the kernel objects and affiliate

162
00:06:50,100 --> 00:06:53,940
non-trivial system and you can see

163
00:06:52,259 --> 00:06:55,580
there's quite a lot involved to just

164
00:06:53,940 --> 00:06:58,979
getting a system up and running

165
00:06:55,580 --> 00:07:00,660
obviously you can automate this

166
00:06:58,979 --> 00:07:02,819
um but still there's there's a lot going

167
00:07:00,660 --> 00:07:04,139
on

168
00:07:02,819 --> 00:07:06,240
so

169
00:07:04,139 --> 00:07:08,100
to the aims of the core platform well

170
00:07:06,240 --> 00:07:10,139
it's a minimal operating system

171
00:07:08,100 --> 00:07:11,840
framework on top of seo4 so it's

172
00:07:10,139 --> 00:07:15,479
supposed to

173
00:07:11,840 --> 00:07:17,039
first retain seo4's security and

174
00:07:15,479 --> 00:07:20,400
performance so if we're going to

175
00:07:17,039 --> 00:07:23,580
abstract over the kernel we don't want

176
00:07:20,400 --> 00:07:26,699
to inherit or inherently limit anyone

177
00:07:23,580 --> 00:07:28,800
using the core platform itself

178
00:07:26,699 --> 00:07:30,979
so we want to retain seo4 security and

179
00:07:28,800 --> 00:07:33,960
performance that it gives us

180
00:07:30,979 --> 00:07:36,599
and we want to lower seo4's barrier to

181
00:07:33,960 --> 00:07:39,060
entry so we want to abstract over things

182
00:07:36,599 --> 00:07:41,639
like architecture specific details and

183
00:07:39,060 --> 00:07:42,960
make it easy to start processes or get

184
00:07:41,639 --> 00:07:45,419
memory and that kind of thing which I'll

185
00:07:42,960 --> 00:07:47,520
talk about later and you know

186
00:07:45,419 --> 00:07:49,319
practically this is done by providing an

187
00:07:47,520 --> 00:07:50,699
SDK with everything that you need and

188
00:07:49,319 --> 00:07:52,020
then you use whatever build system you

189
00:07:50,699 --> 00:07:55,139
want with your application code and

190
00:07:52,020 --> 00:07:57,240
ultimately you get a bootable image that

191
00:07:55,139 --> 00:07:59,400
you then put on whatever board you're

192
00:07:57,240 --> 00:08:00,419
using and then you can load it up and

193
00:07:59,400 --> 00:08:03,900
run it

194
00:08:00,419 --> 00:08:07,259
and so an example of this was the latte

195
00:08:03,900 --> 00:08:09,319
project done by a guy called Phil maker

196
00:08:07,259 --> 00:08:11,900
I believe and

197
00:08:09,319 --> 00:08:15,300
this was a

198
00:08:11,900 --> 00:08:19,379
experienced system developer programmer

199
00:08:15,300 --> 00:08:21,960
who was not experienced with seo4 at all

200
00:08:19,379 --> 00:08:24,060
and he was given the core platform to

201
00:08:21,960 --> 00:08:27,180
try to make a system used in power

202
00:08:24,060 --> 00:08:29,160
stations that does some kind of men in

203
00:08:27,180 --> 00:08:31,319
the middle defense of a logging control

204
00:08:29,160 --> 00:08:32,279
variables and that kind of thing

205
00:08:31,319 --> 00:08:34,200
um

206
00:08:32,279 --> 00:08:35,880
and it was relatively successful so he

207
00:08:34,200 --> 00:08:36,839
was actually able to

208
00:08:35,880 --> 00:08:40,260
um you know obviously with some

209
00:08:36,839 --> 00:08:42,360
assistance uh make a system on top of

210
00:08:40,260 --> 00:08:44,399
seo4 and leveraging its benefits while

211
00:08:42,360 --> 00:08:47,839
not having super detailed knowledge of

212
00:08:44,399 --> 00:08:47,839
the micro kernel itself

213
00:08:48,660 --> 00:08:52,380
um but one thing I want to stress is

214
00:08:50,279 --> 00:08:54,240
that the core platform is not supposed

215
00:08:52,380 --> 00:08:55,620
to be a general purpose OS it has no

216
00:08:54,240 --> 00:08:56,880
intention of replacing something like

217
00:08:55,620 --> 00:08:59,820
Linux

218
00:08:56,880 --> 00:09:01,800
um one of the main limitations of it by

219
00:08:59,820 --> 00:09:03,120
Design again is that it has a static

220
00:09:01,800 --> 00:09:06,120
architecture

221
00:09:03,120 --> 00:09:09,720
so this means that before you run uh

222
00:09:06,120 --> 00:09:13,019
your you know system you have to lay out

223
00:09:09,720 --> 00:09:15,060
basically everything that you that

224
00:09:13,019 --> 00:09:17,220
everything that's going to exist so that

225
00:09:15,060 --> 00:09:19,320
that'll be clearer later there is some

226
00:09:17,220 --> 00:09:21,420
limited dynamicism also to touch on that

227
00:09:19,320 --> 00:09:23,940
in the next slide

228
00:09:21,420 --> 00:09:25,980
um but yeah so this is targeted at

229
00:09:23,940 --> 00:09:28,080
embedded cyber physical devices like

230
00:09:25,980 --> 00:09:29,940
with the latte project

231
00:09:28,080 --> 00:09:31,320
um that's because it's targeted at these

232
00:09:29,940 --> 00:09:32,519
that's how we can get away with these

233
00:09:31,320 --> 00:09:33,779
kind of you know fairly restrictive

234
00:09:32,519 --> 00:09:35,040
limitations

235
00:09:33,779 --> 00:09:37,560
um because for these small embedded

236
00:09:35,040 --> 00:09:39,839
devices having a static architecture is

237
00:09:37,560 --> 00:09:41,580
um usually okay

238
00:09:39,839 --> 00:09:43,380
so now I'm going to talk about what

239
00:09:41,580 --> 00:09:45,240
actually what abstractions does the

240
00:09:43,380 --> 00:09:47,040
framework provide us in order to build

241
00:09:45,240 --> 00:09:50,660
systems on top of it

242
00:09:47,040 --> 00:09:54,360
so the closest thing that I guess I can

243
00:09:50,660 --> 00:09:56,580
show that's to a protection domain is a

244
00:09:54,360 --> 00:09:58,620
Unix process so it's basically just an

245
00:09:56,580 --> 00:10:00,600
environment a way of executing some code

246
00:09:58,620 --> 00:10:03,120
right if you have some program and you

247
00:10:00,600 --> 00:10:05,640
just want it to run you would use a

248
00:10:03,120 --> 00:10:08,760
prediction domain

249
00:10:05,640 --> 00:10:10,980
um so here uh

250
00:10:08,760 --> 00:10:13,019
we have some Library code that you

251
00:10:10,980 --> 00:10:15,779
basically call into then that that makes

252
00:10:13,019 --> 00:10:17,160
a system call to seo4 and basically is a

253
00:10:15,779 --> 00:10:19,440
minimal abstraction of actually talking

254
00:10:17,160 --> 00:10:21,720
to seo4

255
00:10:19,440 --> 00:10:23,279
and then so all your user code is in the

256
00:10:21,720 --> 00:10:24,660
protection domain that just calls into

257
00:10:23,279 --> 00:10:27,600
the library

258
00:10:24,660 --> 00:10:29,459
this is much more lightweight than a

259
00:10:27,600 --> 00:10:31,320
Unix process so because of the

260
00:10:29,459 --> 00:10:33,660
capability system if we just had a

261
00:10:31,320 --> 00:10:35,580
protection domain by itself by default

262
00:10:33,660 --> 00:10:38,519
it doesn't have access to anything else

263
00:10:35,580 --> 00:10:40,080
we have to explicitly give access to

264
00:10:38,519 --> 00:10:42,680
let's say some memory or any other

265
00:10:40,080 --> 00:10:42,680
resources

266
00:10:43,080 --> 00:10:48,240
so this has three entry points you'd

267
00:10:45,420 --> 00:10:50,899
expect like a main uh entry point with a

268
00:10:48,240 --> 00:10:54,060
typical C program but

269
00:10:50,899 --> 00:10:56,339
on the core platform each protection

270
00:10:54,060 --> 00:10:57,660
domain has initialization procedure so

271
00:10:56,339 --> 00:11:00,000
this gets called when the system boots

272
00:10:57,660 --> 00:11:02,540
up to do any editing a notified

273
00:11:00,000 --> 00:11:05,399
procedure and a protected procedure

274
00:11:02,540 --> 00:11:06,959
these won't be clear until later but

275
00:11:05,399 --> 00:11:08,339
these are basically to allow for

276
00:11:06,959 --> 00:11:10,880
communicating with other protection

277
00:11:08,339 --> 00:11:10,880
domains

278
00:11:10,980 --> 00:11:16,200
and so for the limited dynamicism right

279
00:11:14,100 --> 00:11:18,540
now we have uh just stopping and

280
00:11:16,200 --> 00:11:20,640
starting of these PDS at runtime as well

281
00:11:18,540 --> 00:11:22,200
as loading them at runtime but because

282
00:11:20,640 --> 00:11:25,920
it's a static architecture obviously

283
00:11:22,200 --> 00:11:27,660
you'll have to still specify what um

284
00:11:25,920 --> 00:11:28,560
protection domains will exist in the

285
00:11:27,660 --> 00:11:29,160
system

286
00:11:28,560 --> 00:11:31,800
um

287
00:11:29,160 --> 00:11:33,720
at build time

288
00:11:31,800 --> 00:11:34,980
so the next abstraction is memory

289
00:11:33,720 --> 00:11:36,180
regions

290
00:11:34,980 --> 00:11:38,579
so obviously there's not going to be any

291
00:11:36,180 --> 00:11:40,860
M map in seo4 we need a way of

292
00:11:38,579 --> 00:11:43,200
allocating memory still

293
00:11:40,860 --> 00:11:45,360
memory regions are just a contiguous

294
00:11:43,200 --> 00:11:46,860
block of physical memory so this could

295
00:11:45,360 --> 00:11:48,300
be used for something like regular

296
00:11:46,860 --> 00:11:50,700
memory if you wanted to have a shared

297
00:11:48,300 --> 00:11:52,860
buffer between some protection domains

298
00:11:50,700 --> 00:11:55,019
or device memories like I mentioned

299
00:11:52,860 --> 00:11:56,579
before on seo4 all of your device

300
00:11:55,019 --> 00:11:58,980
drivers are going to be at user level

301
00:11:56,579 --> 00:12:00,660
which means that you need a way of

302
00:11:58,980 --> 00:12:03,620
actually accessing the device registers

303
00:12:00,660 --> 00:12:03,620
and so on to implement

304
00:12:04,440 --> 00:12:08,760
and so these may be mapped into one or

305
00:12:06,660 --> 00:12:11,100
more PDS so like I said before with a

306
00:12:08,760 --> 00:12:12,720
shared buffer and that enables xero copy

307
00:12:11,100 --> 00:12:14,279
communication because both protection

308
00:12:12,720 --> 00:12:16,880
domains will have access to the same

309
00:12:14,279 --> 00:12:16,880
memory

310
00:12:18,060 --> 00:12:24,240
the next is communication channels so if

311
00:12:21,240 --> 00:12:27,240
we have multiple PDS by default they

312
00:12:24,240 --> 00:12:29,640
can't actually talk to each other anyway

313
00:12:27,240 --> 00:12:32,040
because this is part of the isolation

314
00:12:29,640 --> 00:12:34,140
guarantees of seo4 unless we explicitly

315
00:12:32,040 --> 00:12:37,260
say so

316
00:12:34,140 --> 00:12:39,660
so a communication Channel or CC allows

317
00:12:37,260 --> 00:12:41,519
bi-directional communication between a

318
00:12:39,660 --> 00:12:43,920
pair of PDs

319
00:12:41,519 --> 00:12:45,959
so this is for both synchronous and

320
00:12:43,920 --> 00:12:48,779
asynchronous communication

321
00:12:45,959 --> 00:12:51,000
and a communication alone doesn't

322
00:12:48,779 --> 00:12:53,180
necessarily mean that the PDS trust each

323
00:12:51,000 --> 00:12:53,180
other

324
00:12:53,600 --> 00:13:00,839
so now there's two ways of communicating

325
00:12:57,079 --> 00:13:04,139
the first way is via notifications

326
00:13:00,839 --> 00:13:06,839
so say I have two protection domains

327
00:13:04,139 --> 00:13:09,720
here and they have a shared buffer and

328
00:13:06,839 --> 00:13:13,200
let's say the green protection domain is

329
00:13:09,720 --> 00:13:15,540
a consumer of that buffer and the orange

330
00:13:13,200 --> 00:13:17,339
protection domain is a producer and so

331
00:13:15,540 --> 00:13:18,660
it puts them into the buffer and then

332
00:13:17,339 --> 00:13:20,459
the green protection domain will then

333
00:13:18,660 --> 00:13:23,220
consume and process it

334
00:13:20,459 --> 00:13:25,019
and so the orange prediction domain

335
00:13:23,220 --> 00:13:28,440
basically would put something in and

336
00:13:25,019 --> 00:13:29,940
then notify the other protection domain

337
00:13:28,440 --> 00:13:31,620
that something has happened it's

338
00:13:29,940 --> 00:13:34,680
basically to indicate that some event

339
00:13:31,620 --> 00:13:36,480
has happened and we want to wake up the

340
00:13:34,680 --> 00:13:39,060
other protection and wake up it's it's

341
00:13:36,480 --> 00:13:41,459
thread and let it execute and so this is

342
00:13:39,060 --> 00:13:44,820
what this will do is invoke the notified

343
00:13:41,459 --> 00:13:46,260
procedure that I mentioned earlier

344
00:13:44,820 --> 00:13:48,420
and then obviously there's an identifier

345
00:13:46,260 --> 00:13:51,600
given just so you can say so you can

346
00:13:48,420 --> 00:13:55,260
know which protection has invoked you or

347
00:13:51,600 --> 00:13:56,940
has notified you and you can handle that

348
00:13:55,260 --> 00:13:59,279
and so this is asynchronous so the

349
00:13:56,940 --> 00:14:02,220
orange PD once it notifies the green PD

350
00:13:59,279 --> 00:14:05,660
will continue executing and doing um

351
00:14:02,220 --> 00:14:05,660
do whatever else it needs to do

352
00:14:05,940 --> 00:14:09,600
and so interrupts are also delivered as

353
00:14:08,100 --> 00:14:12,000
notifications for implementing device

354
00:14:09,600 --> 00:14:13,680
drivers

355
00:14:12,000 --> 00:14:15,959
the next way

356
00:14:13,680 --> 00:14:18,480
um of communicating is via something

357
00:14:15,959 --> 00:14:23,220
called protection procedure calls so

358
00:14:18,480 --> 00:14:26,459
ppcs are basically a way of executing

359
00:14:23,220 --> 00:14:29,880
some other code in a different PD

360
00:14:26,459 --> 00:14:31,440
so let's say I have this gray PD and

361
00:14:29,880 --> 00:14:33,660
there's some kind of function that I

362
00:14:31,440 --> 00:14:36,000
want let's say the gray PD is a client

363
00:14:33,660 --> 00:14:37,139
and is calling into some server that it

364
00:14:36,000 --> 00:14:39,779
wants and it wants it to do some

365
00:14:37,139 --> 00:14:42,360
operation and so this is a synchronous

366
00:14:39,779 --> 00:14:44,639
form of communication the gray PD would

367
00:14:42,360 --> 00:14:45,839
call into the server wait for the server

368
00:14:44,639 --> 00:14:48,800
to do its processing and then return

369
00:14:45,839 --> 00:14:48,800
back with some result

370
00:14:49,560 --> 00:14:53,220
and so in this case the caller must

371
00:14:51,240 --> 00:14:55,500
trust the call D

372
00:14:53,220 --> 00:14:58,500
um because you're basically

373
00:14:55,500 --> 00:14:58,500
uh

374
00:14:58,820 --> 00:15:04,860
executing the the the quality is

375
00:15:02,779 --> 00:15:06,779
executing basically on the caller's

376
00:15:04,860 --> 00:15:10,279
behalf you're trusting it to do the

377
00:15:06,779 --> 00:15:10,279
right operation when you call into it

378
00:15:10,320 --> 00:15:14,639
and lastly we have virtual machines so

379
00:15:13,019 --> 00:15:17,220
if I wanted to run something like Linux

380
00:15:14,639 --> 00:15:19,320
on top of seo4 I could use a virtual

381
00:15:17,220 --> 00:15:21,180
machine so these are particularly useful

382
00:15:19,320 --> 00:15:25,139
for running software that you don't want

383
00:15:21,180 --> 00:15:28,440
to port to seo4 which might be uh

384
00:15:25,139 --> 00:15:30,240
might be expensive in terms of time

385
00:15:28,440 --> 00:15:32,100
or it's just some Legacy software that

386
00:15:30,240 --> 00:15:34,260
you don't want to touch you could run it

387
00:15:32,100 --> 00:15:36,480
still on top of seo4 but just in a VM

388
00:15:34,260 --> 00:15:39,540
and these are essentially a PD just but

389
00:15:36,480 --> 00:15:42,120
with the ability to uh

390
00:15:39,540 --> 00:15:43,740
run a guest OS and some other properties

391
00:15:42,120 --> 00:15:44,899
it has the same properties as a PD

392
00:15:43,740 --> 00:15:47,279
basically

393
00:15:44,899 --> 00:15:49,620
these are still experimental so they're

394
00:15:47,279 --> 00:15:52,199
not in the mainline source code but

395
00:15:49,620 --> 00:15:53,880
details will be finalized soon

396
00:15:52,199 --> 00:15:56,180
and so I thought I'd illustrate all of

397
00:15:53,880 --> 00:16:01,100
this with just some example system

398
00:15:56,180 --> 00:16:04,079
so say I have seo4 and some

399
00:16:01,100 --> 00:16:06,120
Hardware device and I don't want to

400
00:16:04,079 --> 00:16:07,800
write a driver on seo4 I'd rather just

401
00:16:06,120 --> 00:16:11,519
use a driver that already exists in

402
00:16:07,800 --> 00:16:13,260
Linux so I could have a VM that then has

403
00:16:11,519 --> 00:16:15,540
access to that Hardware device I've told

404
00:16:13,260 --> 00:16:18,540
it it has access to that memory

405
00:16:15,540 --> 00:16:20,699
and the virtual driver uh

406
00:16:18,540 --> 00:16:23,160
can access that Hardware device and then

407
00:16:20,699 --> 00:16:25,560
if any client wants to send stuff to

408
00:16:23,160 --> 00:16:28,139
that driver it can do so and that client

409
00:16:25,560 --> 00:16:29,940
could be either a native seo4 that one

410
00:16:28,139 --> 00:16:33,060
sorry a protection domain which is a

411
00:16:29,940 --> 00:16:36,240
native seo4 thread or it could be

412
00:16:33,060 --> 00:16:37,860
another client in some other VM right

413
00:16:36,240 --> 00:16:41,100
and so in this case we have a transport

414
00:16:37,860 --> 00:16:42,720
layer that allows communication between

415
00:16:41,100 --> 00:16:44,519
all of those or facilitates

416
00:16:42,720 --> 00:16:47,720
communication between all of those

417
00:16:44,519 --> 00:16:47,720
various entities

418
00:16:48,839 --> 00:16:52,740
so

419
00:16:50,040 --> 00:16:54,600
I'd also like to touch on the

420
00:16:52,740 --> 00:16:57,420
verification story of the core platform

421
00:16:54,600 --> 00:16:58,860
so we have a verified micro kernel this

422
00:16:57,420 --> 00:17:01,880
was done using something called

423
00:16:58,860 --> 00:17:05,040
interactive theorem proving

424
00:17:01,880 --> 00:17:07,199
but obviously we want to be able to

425
00:17:05,040 --> 00:17:09,540
trust not just the kernel but anything

426
00:17:07,199 --> 00:17:12,299
we use on top of the kernel as well

427
00:17:09,540 --> 00:17:14,819
and so this includes any code that the

428
00:17:12,299 --> 00:17:15,540
framework runs

429
00:17:14,819 --> 00:17:17,939
um

430
00:17:15,540 --> 00:17:20,100
and so this is an ongoing research

431
00:17:17,939 --> 00:17:21,839
effort by some colleagues at trustworthy

432
00:17:20,100 --> 00:17:25,439
systems but this is using different

433
00:17:21,839 --> 00:17:28,260
techniques to what the main seo4 proofs

434
00:17:25,439 --> 00:17:29,820
were which is using smt solvers

435
00:17:28,260 --> 00:17:31,440
basically to try to automate that

436
00:17:29,820 --> 00:17:35,419
they're improving rather than doing it

437
00:17:31,440 --> 00:17:35,419
in a more kind of manual interactive way

438
00:17:36,600 --> 00:17:42,120
and so one of the main goals is to

439
00:17:39,539 --> 00:17:43,679
verify the core platform runtime code so

440
00:17:42,120 --> 00:17:46,799
the library that I mentioned before has

441
00:17:43,679 --> 00:17:47,820
about 200 lines of C code and there's

442
00:17:46,799 --> 00:17:50,940
also something called a system

443
00:17:47,820 --> 00:17:54,539
initializer so if I show you the basic

444
00:17:50,940 --> 00:17:56,299
boot process of an seo4 system so we

445
00:17:54,539 --> 00:17:59,039
have the kernel that we can trust

446
00:17:56,299 --> 00:18:02,220
because since it's verified but we have

447
00:17:59,039 --> 00:18:03,840
the system initializer and the core

448
00:18:02,220 --> 00:18:05,760
platform library that we can't trust

449
00:18:03,840 --> 00:18:07,260
it's running you know code that we think

450
00:18:05,760 --> 00:18:09,900
is right but we have no way of knowing

451
00:18:07,260 --> 00:18:12,360
that and this is particularly important

452
00:18:09,900 --> 00:18:14,340
because the system initializer is what

453
00:18:12,360 --> 00:18:16,919
sets up all of those capabilities that I

454
00:18:14,340 --> 00:18:20,160
was talking about before right so if I

455
00:18:16,919 --> 00:18:22,799
know that some PD doesn't have access to

456
00:18:20,160 --> 00:18:24,720
this like a certain part of memory I

457
00:18:22,799 --> 00:18:26,220
only know that because I trust that the

458
00:18:24,720 --> 00:18:28,260
initializer has set up the capabilities

459
00:18:26,220 --> 00:18:29,820
correctly if it hasn't done that then I

460
00:18:28,260 --> 00:18:31,200
could easily some prediction domain

461
00:18:29,820 --> 00:18:34,340
could easily access the memory that it

462
00:18:31,200 --> 00:18:34,340
shouldn't be right

463
00:18:35,760 --> 00:18:40,559
um and so

464
00:18:37,320 --> 00:18:42,900
verifying this initializer is uh

465
00:18:40,559 --> 00:18:45,419
basically just leveraging and existing

466
00:18:42,900 --> 00:18:48,679
and already verified initializer and

467
00:18:45,419 --> 00:18:51,720
that's currently in progress as well

468
00:18:48,679 --> 00:18:53,880
and then we have uh for the system

469
00:18:51,720 --> 00:18:56,160
initializers we have a

470
00:18:53,880 --> 00:18:58,200
capability distribution language that

471
00:18:56,160 --> 00:19:01,440
basically needs to be that the system

472
00:18:58,200 --> 00:19:04,080
initializer consumes and we need to make

473
00:19:01,440 --> 00:19:06,120
sure that the mapping from how we

474
00:19:04,080 --> 00:19:09,419
describe our core platform system to

475
00:19:06,120 --> 00:19:11,580
this more machine readable capability

476
00:19:09,419 --> 00:19:13,919
distribution language is correct

477
00:19:11,580 --> 00:19:16,380
otherwise then you know I might describe

478
00:19:13,919 --> 00:19:18,419
some core platform system that then once

479
00:19:16,380 --> 00:19:21,440
it gets to the system initializer the

480
00:19:18,419 --> 00:19:21,440
capabilities all wrong

481
00:19:22,140 --> 00:19:25,440
so to summarize everything I've been

482
00:19:24,419 --> 00:19:30,080
talking about

483
00:19:25,440 --> 00:19:33,840
we can create systems using uh a few

484
00:19:30,080 --> 00:19:36,000
fairly simple abstractions so PDS for

485
00:19:33,840 --> 00:19:38,220
executing use level programs memory

486
00:19:36,000 --> 00:19:40,980
regions for accessing device memory or

487
00:19:38,220 --> 00:19:42,900
shared buffers and so on and channels

488
00:19:40,980 --> 00:19:46,080
for communication between protection

489
00:19:42,900 --> 00:19:47,760
domains and we all we specify all of

490
00:19:46,080 --> 00:19:49,320
these system resources all the

491
00:19:47,760 --> 00:19:51,120
protection domains or the memory regions

492
00:19:49,320 --> 00:19:52,919
that exist or the channels that exist at

493
00:19:51,120 --> 00:19:54,600
build time

494
00:19:52,919 --> 00:19:57,620
and so

495
00:19:54,600 --> 00:20:00,480
by making these abstractions

496
00:19:57,620 --> 00:20:02,520
in the framework we can increase the

497
00:20:00,480 --> 00:20:04,260
usability of seo4 since everyone won't

498
00:20:02,520 --> 00:20:07,140
have to do this process for themselves

499
00:20:04,260 --> 00:20:08,940
when they want to build a system

500
00:20:07,140 --> 00:20:11,880
and so we also have a verification story

501
00:20:08,940 --> 00:20:13,320
in process and you can all the code is

502
00:20:11,880 --> 00:20:14,760
open source so you can have a look at it

503
00:20:13,320 --> 00:20:17,520
if you want

504
00:20:14,760 --> 00:20:18,720
and so lastly what's what's next

505
00:20:17,520 --> 00:20:20,640
well

506
00:20:18,720 --> 00:20:22,440
like I mentioned we have the appropriate

507
00:20:20,640 --> 00:20:25,200
abstractions to build systems on top of

508
00:20:22,440 --> 00:20:27,179
seo4 but there aren't any OS services

509
00:20:25,200 --> 00:20:30,059
like you would expect

510
00:20:27,179 --> 00:20:31,860
and something like Linux so a major part

511
00:20:30,059 --> 00:20:34,500
of an OS that needs to be secure and

512
00:20:31,860 --> 00:20:36,960
reliable is device drivers as you know

513
00:20:34,500 --> 00:20:39,299
they're very fragile and having them in

514
00:20:36,960 --> 00:20:41,340
the kernel can be disastrous and so we

515
00:20:39,299 --> 00:20:43,140
want to make sure that any of this

516
00:20:41,340 --> 00:20:45,840
particular service that an OS would

517
00:20:43,140 --> 00:20:47,880
provide is correct and can be trusted

518
00:20:45,840 --> 00:20:50,039
and so for this I'm going to hand over

519
00:20:47,880 --> 00:20:52,440
to Lucy who's an undergraduate student

520
00:20:50,039 --> 00:20:55,520
at TS and she'll be talking about the

521
00:20:52,440 --> 00:20:55,520
device driver framework

522
00:21:00,660 --> 00:21:06,600
okay so what is the seo4 device driver

523
00:21:03,900 --> 00:21:08,940
framework well as Avon already mentioned

524
00:21:06,600 --> 00:21:11,940
seo4 as a micro kernel prescribes device

525
00:21:08,940 --> 00:21:14,280
drivers to run as user level programs

526
00:21:11,940 --> 00:21:16,140
this has the advantage of reducing a

527
00:21:14,280 --> 00:21:18,179
driver's special privileges to just the

528
00:21:16,140 --> 00:21:20,940
ability to access the control registers

529
00:21:18,179 --> 00:21:23,880
of the device that it's actually driving

530
00:21:20,940 --> 00:21:26,100
this not only significantly reduces The

531
00:21:23,880 --> 00:21:27,660
Trusted Computing base in the system but

532
00:21:26,100 --> 00:21:29,640
it also provides strong fault

533
00:21:27,660 --> 00:21:32,580
containment to what's historically been

534
00:21:29,640 --> 00:21:34,740
very bug prone code earlier research

535
00:21:32,580 --> 00:21:36,659
found that drivers on Linux have seven

536
00:21:34,740 --> 00:21:38,340
times the bug density when compared to

537
00:21:36,659 --> 00:21:40,980
the rest of the OS

538
00:21:38,340 --> 00:21:43,620
and I know a significant the leading

539
00:21:40,980 --> 00:21:46,500
cause actually of Linux cves are because

540
00:21:43,620 --> 00:21:49,500
of buggy device drivers

541
00:21:46,500 --> 00:21:50,880
however the micro kernel design has the

542
00:21:49,500 --> 00:21:53,280
potential to of course lead to

543
00:21:50,880 --> 00:21:54,600
Performance degradation due to the

544
00:21:53,280 --> 00:21:57,120
inherent number of extra context

545
00:21:54,600 --> 00:21:59,340
switches required in such a design so

546
00:21:57,120 --> 00:22:01,679
the device driver framework aims to

547
00:21:59,340 --> 00:22:03,539
rectify this by providing interfaces and

548
00:22:01,679 --> 00:22:08,059
protocols for writing performant yet

549
00:22:03,539 --> 00:22:08,059
secure device drivers on seo4

550
00:22:08,880 --> 00:22:13,679
so the sddf is based on radical

551
00:22:11,520 --> 00:22:16,080
Simplicity where we prioritize a strong

552
00:22:13,679 --> 00:22:18,000
separation of concerns with multiple

553
00:22:16,080 --> 00:22:19,559
components each running with a single

554
00:22:18,000 --> 00:22:22,980
job to do

555
00:22:19,559 --> 00:22:25,860
so with that a driver itself is purely

556
00:22:22,980 --> 00:22:27,900
responsible for Hardware abstraction

557
00:22:25,860 --> 00:22:30,600
for this we assume a general device

558
00:22:27,900 --> 00:22:32,280
model that should enable formal

559
00:22:30,600 --> 00:22:34,740
reasoning with a simple implementation

560
00:22:32,280 --> 00:22:37,140
and this is all based on top of an

561
00:22:34,740 --> 00:22:38,940
asynchronous zero copy transport layer

562
00:22:37,140 --> 00:22:41,039
that provides a means of communication

563
00:22:38,940 --> 00:22:43,880
to other components wishing to utilize

564
00:22:41,039 --> 00:22:43,880
The Driver's Services

565
00:22:44,159 --> 00:22:48,360
it is still a work in progress but

566
00:22:46,380 --> 00:22:50,760
currently supports a networking focused

567
00:22:48,360 --> 00:22:53,760
system which is arguably the most

568
00:22:50,760 --> 00:22:55,380
performant critical system in the OS and

569
00:22:53,760 --> 00:22:57,600
so tackling this is really the first

570
00:22:55,380 --> 00:23:00,539
step to developing high performance iot

571
00:22:57,600 --> 00:23:03,179
cyber physical systems

572
00:23:00,539 --> 00:23:05,780
and it is all implemented on top of the

573
00:23:03,179 --> 00:23:05,780
core platform

574
00:23:06,480 --> 00:23:12,600
so the driver model utilizes three

575
00:23:09,059 --> 00:23:15,419
distinct memory regions or mice

576
00:23:12,600 --> 00:23:18,000
the driver will issue commands to the

577
00:23:15,419 --> 00:23:19,980
devices control registers here labeled

578
00:23:18,000 --> 00:23:22,200
their metadata region and the device

579
00:23:19,980 --> 00:23:23,640
will read and write data to a specified

580
00:23:22,200 --> 00:23:26,460
location

581
00:23:23,640 --> 00:23:27,960
for dma now this data region can also be

582
00:23:26,460 --> 00:23:31,200
mapped into the server's address space

583
00:23:27,960 --> 00:23:33,360
which enables a zero copy interface

584
00:23:31,200 --> 00:23:35,400
the control region provides a means of

585
00:23:33,360 --> 00:23:37,740
communicating between a server utilizing

586
00:23:35,400 --> 00:23:39,659
the drivers and the driver itself so the

587
00:23:37,740 --> 00:23:41,220
server can issue transmit requests and

588
00:23:39,659 --> 00:23:43,320
receive information on newly received

589
00:23:41,220 --> 00:23:44,880
data and then likewise in Reverse for

590
00:23:43,320 --> 00:23:47,460
the driver

591
00:23:44,880 --> 00:23:49,740
now in a networking Focus system the

592
00:23:47,460 --> 00:23:52,260
driver doesn't actually need access to

593
00:23:49,740 --> 00:23:54,720
the data itself so we can further reduce

594
00:23:52,260 --> 00:23:56,640
the trust we place in a device driver by

595
00:23:54,720 --> 00:23:59,720
avoiding mapping this data region into

596
00:23:56,640 --> 00:23:59,720
the driver's address space

597
00:24:01,080 --> 00:24:06,179
so like I said earlier the driver is

598
00:24:04,799 --> 00:24:08,760
purely responsible for Hardware

599
00:24:06,179 --> 00:24:10,200
abstraction so it's translating a

600
00:24:08,760 --> 00:24:12,900
hardware defined specific device

601
00:24:10,200 --> 00:24:16,140
protocol into a hardware independent or

602
00:24:12,900 --> 00:24:18,600
Os specific device class protocol

603
00:24:16,140 --> 00:24:20,940
so with this we model it as single

604
00:24:18,600 --> 00:24:23,039
threaded and it simply just reacts to

605
00:24:20,940 --> 00:24:25,260
updates in either the control region or

606
00:24:23,039 --> 00:24:27,380
the metadata region and these updates

607
00:24:25,260 --> 00:24:29,940
come in the form of seo4 notifications

608
00:24:27,380 --> 00:24:32,880
and of course an interrupt which is

609
00:24:29,940 --> 00:24:34,919
mapped onto an seo4 notification

610
00:24:32,880 --> 00:24:38,700
and we say that it's active in that it

611
00:24:34,919 --> 00:24:39,720
has the ability to execute so it has the

612
00:24:38,700 --> 00:24:43,320
capability

613
00:24:39,720 --> 00:24:46,260
to access CPU time

614
00:24:43,320 --> 00:24:48,960
so the transport layer or control region

615
00:24:46,260 --> 00:24:50,940
is comprised of Lock Free bounded ring

616
00:24:48,960 --> 00:24:53,220
buffer cues and these cues themselves

617
00:24:50,940 --> 00:24:54,659
are single producer single consumer

618
00:24:53,220 --> 00:24:57,480
which is a very intentional

619
00:24:54,659 --> 00:24:59,220
simplification and we utilize two cues

620
00:24:57,480 --> 00:25:01,500
per Direction these cues simply keep

621
00:24:59,220 --> 00:25:02,820
track of addresses in that shared data

622
00:25:01,500 --> 00:25:05,220
region

623
00:25:02,820 --> 00:25:07,140
so for example on the transmit path we

624
00:25:05,220 --> 00:25:09,360
have the transmit used queue which keeps

625
00:25:07,140 --> 00:25:11,760
track of buffers with data that's ready

626
00:25:09,360 --> 00:25:13,679
to be transmitted and then the transmit

627
00:25:11,760 --> 00:25:17,600
free queue which keeps track of buffers

628
00:25:13,679 --> 00:25:17,600
that are free and ready to be reused

629
00:25:17,640 --> 00:25:21,240
and the cues themselves are very simple

630
00:25:19,500 --> 00:25:23,280
like I said we keep track of an address

631
00:25:21,240 --> 00:25:25,200
in the data region as well as the length

632
00:25:23,280 --> 00:25:27,179
of data that's there or potentially the

633
00:25:25,200 --> 00:25:29,220
capacity of the buffer

634
00:25:27,179 --> 00:25:33,059
and then we use head and tail pointers

635
00:25:29,220 --> 00:25:35,039
to enqueue from ndq to

636
00:25:33,059 --> 00:25:37,980
and then we get these really simple NQ

637
00:25:35,039 --> 00:25:40,140
and DQ functions where we can maintain

638
00:25:37,980 --> 00:25:42,900
memory safety without the need for locks

639
00:25:40,140 --> 00:25:44,340
by utilizing a right memory barrier to

640
00:25:42,900 --> 00:25:46,080
ensure that no reads or rights are

641
00:25:44,340 --> 00:25:48,059
reordered by either the compiler or the

642
00:25:46,080 --> 00:25:50,659
processor before we update this head or

643
00:25:48,059 --> 00:25:50,659
tail pointer

644
00:25:51,659 --> 00:25:56,159
so the buffers are continually

645
00:25:53,400 --> 00:25:58,140
continuously reused for example on

646
00:25:56,159 --> 00:25:59,940
transmit the server would grab the next

647
00:25:58,140 --> 00:26:02,279
available free buffer from the transmit

648
00:25:59,940 --> 00:26:03,720
free ring and then write data to the

649
00:26:02,279 --> 00:26:05,580
address specified

650
00:26:03,720 --> 00:26:08,159
and then it would put that address into

651
00:26:05,580 --> 00:26:10,799
the transmit used queue we would then

652
00:26:08,159 --> 00:26:13,320
notify the driver that we have data

653
00:26:10,799 --> 00:26:15,840
ready to be transmitted the driver would

654
00:26:13,320 --> 00:26:18,240
wake up DQ from the transmit used queue

655
00:26:15,840 --> 00:26:21,240
and then write that address to the

656
00:26:18,240 --> 00:26:22,919
device registers to initiate transmit on

657
00:26:21,240 --> 00:26:25,140
the device

658
00:26:22,919 --> 00:26:27,059
sometime later the device would then

659
00:26:25,140 --> 00:26:28,679
interrupt the driver notifying that

660
00:26:27,059 --> 00:26:30,720
either the transmit was complete or

661
00:26:28,679 --> 00:26:32,400
potentially an error had happened and

662
00:26:30,720 --> 00:26:34,620
the driver can get that address and put

663
00:26:32,400 --> 00:26:37,520
it back in the transmit free queue ready

664
00:26:34,620 --> 00:26:37,520
to be reused again

665
00:26:37,980 --> 00:26:43,799
so with all of this here is some pseudo

666
00:26:40,799 --> 00:26:45,860
code for a very simple Network driver so

667
00:26:43,799 --> 00:26:48,720
like I said it simply waits for an event

668
00:26:45,860 --> 00:26:50,880
and then dqs and nq's pointers as

669
00:26:48,720 --> 00:26:52,320
required and this event could be a

670
00:26:50,880 --> 00:26:54,600
hardware event

671
00:26:52,320 --> 00:26:56,760
um in the form of an interrupt

672
00:26:54,600 --> 00:26:59,480
or it could be a request to transmit

673
00:26:56,760 --> 00:26:59,480
from the server

674
00:26:59,700 --> 00:27:04,020
so what's important here is that we loop

675
00:27:02,159 --> 00:27:05,760
around dqing and enqueuing so that we

676
00:27:04,020 --> 00:27:07,860
can potentially process multiple packets

677
00:27:05,760 --> 00:27:10,500
in a single invocation

678
00:27:07,860 --> 00:27:12,960
and we also loop around reading and

679
00:27:10,500 --> 00:27:14,580
clearing the hardware event register so

680
00:27:12,960 --> 00:27:16,740
this means that we can potentially

681
00:27:14,580 --> 00:27:18,840
process multiple Hardware events in a

682
00:27:16,740 --> 00:27:20,400
single invocation of course at low

683
00:27:18,840 --> 00:27:22,080
throughput this is unlikely to be the

684
00:27:20,400 --> 00:27:24,900
case but at high throughput with all

685
00:27:22,080 --> 00:27:26,700
this looping there's High chance that

686
00:27:24,900 --> 00:27:28,500
another Hardware event has occurred and

687
00:27:26,700 --> 00:27:32,840
we can preempt any kind of Kernel

688
00:27:28,500 --> 00:27:32,840
interrupt by reacting to it here early

689
00:27:33,179 --> 00:27:37,940
we also combine the system calls on seo4

690
00:27:36,659 --> 00:27:40,919
whenever we can

691
00:27:37,940 --> 00:27:44,580
so this could be that we're signaling an

692
00:27:40,919 --> 00:27:46,679
update to the server's control region

693
00:27:44,580 --> 00:27:49,380
combine that with the next wait for

694
00:27:46,679 --> 00:27:50,760
event system call or it could also be

695
00:27:49,380 --> 00:27:53,340
that we're acknowledging and

696
00:27:50,760 --> 00:27:55,380
acknowledging and interrupt so on seo4

697
00:27:53,340 --> 00:27:57,900
the kind of actually masks the hardware

698
00:27:55,380 --> 00:27:59,340
events until it has received a

699
00:27:57,900 --> 00:28:01,559
notification from the user level

700
00:27:59,340 --> 00:28:03,659
interrupt Handler that that interrupt

701
00:28:01,559 --> 00:28:05,159
has been dealt with and this

702
00:28:03,659 --> 00:28:07,559
acknowledgment is just a signal to the

703
00:28:05,159 --> 00:28:09,539
kernel so we can combine this signal

704
00:28:07,559 --> 00:28:11,580
with the next wait for event system call

705
00:28:09,539 --> 00:28:15,000
and thus further reduce the number of

706
00:28:11,580 --> 00:28:17,159
system calls required in such a system

707
00:28:15,000 --> 00:28:19,440
so this is all great for a single server

708
00:28:17,159 --> 00:28:21,720
application but what about if we wanted

709
00:28:19,440 --> 00:28:24,620
to have multiple clients

710
00:28:21,720 --> 00:28:28,080
so for that we have a simple multiplexer

711
00:28:24,620 --> 00:28:30,779
whose sole concern is to share the Nick

712
00:28:28,080 --> 00:28:33,240
or share the hardware

713
00:28:30,779 --> 00:28:35,580
we implemented the multiplexer at layer

714
00:28:33,240 --> 00:28:38,760
one so the multiplexer simply has a

715
00:28:35,580 --> 00:28:42,000
mapping of a virtual Mac address to a

716
00:28:38,760 --> 00:28:43,919
client ID this could have been done of

717
00:28:42,000 --> 00:28:47,520
course at layer 2 or layer 3 but then

718
00:28:43,919 --> 00:28:50,279
you'd be confining clients to either a

719
00:28:47,520 --> 00:28:52,320
specific IP address or potentially a set

720
00:28:50,279 --> 00:28:54,120
of ports and then you'd be confining

721
00:28:52,320 --> 00:28:56,940
them to a particular protocol

722
00:28:54,120 --> 00:29:00,120
but this wouldn't be a difficult change

723
00:28:56,940 --> 00:29:02,400
we also separated out the receive and

724
00:29:00,120 --> 00:29:04,380
transmit paths as there's no need for

725
00:29:02,400 --> 00:29:05,760
these to interact

726
00:29:04,380 --> 00:29:08,760
and this means of course we can have

727
00:29:05,760 --> 00:29:10,080
separate policies on each path so the

728
00:29:08,760 --> 00:29:12,600
only thing that really makes sense on

729
00:29:10,080 --> 00:29:15,179
the receipt path is a fifo first in

730
00:29:12,600 --> 00:29:17,279
first out policy but on transmit there's

731
00:29:15,179 --> 00:29:19,559
a few different options

732
00:29:17,279 --> 00:29:21,419
so one of these would be round robin so

733
00:29:19,559 --> 00:29:24,120
taking turns to process each client's

734
00:29:21,419 --> 00:29:27,000
request but it could also be priority

735
00:29:24,120 --> 00:29:28,320
based with one client who takes priority

736
00:29:27,000 --> 00:29:31,080
over another

737
00:29:28,320 --> 00:29:33,299
and we could also limit clients

738
00:29:31,080 --> 00:29:36,480
throughput as well

739
00:29:33,299 --> 00:29:41,039
and rather than coming up with a generic

740
00:29:36,480 --> 00:29:42,899
policy that caters to all of these we

741
00:29:41,039 --> 00:29:43,620
propose instead

742
00:29:42,899 --> 00:29:46,020
um

743
00:29:43,620 --> 00:29:49,220
choosing a simple and specific policy

744
00:29:46,020 --> 00:29:49,220
for your use case

745
00:29:49,679 --> 00:29:53,700
and these policies can also be swapped

746
00:29:51,899 --> 00:29:56,100
out at runtime of course should the need

747
00:29:53,700 --> 00:29:58,320
arise

748
00:29:56,100 --> 00:30:00,659
so how does such a system look

749
00:29:58,320 --> 00:30:03,480
well we have the driver with the shed

750
00:30:00,659 --> 00:30:06,539
ring buffers on either side so one to

751
00:30:03,480 --> 00:30:09,659
the actual hardware and then the other

752
00:30:06,539 --> 00:30:12,360
set would be connected to the transmit

753
00:30:09,659 --> 00:30:14,700
multiplexer and the receive multiplexer

754
00:30:12,360 --> 00:30:16,860
and underneath this is the shared data

755
00:30:14,700 --> 00:30:19,080
region

756
00:30:16,860 --> 00:30:22,020
these would then be connected straight

757
00:30:19,080 --> 00:30:24,600
to the clients or potentially with a

758
00:30:22,020 --> 00:30:26,039
copy component in between so this small

759
00:30:24,600 --> 00:30:29,820
copy component

760
00:30:26,039 --> 00:30:32,340
um that sole job is to copy the data

761
00:30:29,820 --> 00:30:34,260
from the shared data region into the

762
00:30:32,340 --> 00:30:35,760
client's own address space so this

763
00:30:34,260 --> 00:30:39,179
ensures that clients don't have the

764
00:30:35,760 --> 00:30:40,919
ability to access each other's data

765
00:30:39,179 --> 00:30:44,120
this isn't necessary on the transmit

766
00:30:40,919 --> 00:30:46,799
path as we can just map the transmit

767
00:30:44,120 --> 00:30:49,020
data for each client into the transmit

768
00:30:46,799 --> 00:30:51,860
multiplexer and then the hardware can

769
00:30:49,020 --> 00:30:51,860
deal with that directly

770
00:30:51,899 --> 00:30:57,600
so in if we were to expand out the

771
00:30:56,340 --> 00:30:59,640
Simplicity of the system means it's

772
00:30:57,600 --> 00:31:01,679
scalable and we can have each of these

773
00:30:59,640 --> 00:31:03,720
components running on separate cores in

774
00:31:01,679 --> 00:31:07,399
a multi-core system and exploit full

775
00:31:03,720 --> 00:31:07,399
parallelism of such a design

776
00:31:07,500 --> 00:31:13,080
it might also look like we've added an

777
00:31:09,720 --> 00:31:15,059
extra copy to the design but if you

778
00:31:13,080 --> 00:31:17,640
compare it to posix system which copies

779
00:31:15,059 --> 00:31:19,860
on copies into user space and then back

780
00:31:17,640 --> 00:31:22,279
out again we've actually reduced a copy

781
00:31:19,860 --> 00:31:22,279
operation

782
00:31:23,340 --> 00:31:27,539
so in order to minimize round trip times

783
00:31:25,919 --> 00:31:30,240
we run the driver followed by the

784
00:31:27,539 --> 00:31:32,520
transmit multiplexer at highest priority

785
00:31:30,240 --> 00:31:34,140
so this ensures that as soon as packets

786
00:31:32,520 --> 00:31:36,539
are ready to be transmitted the

787
00:31:34,140 --> 00:31:39,480
appropriate components will be invoked

788
00:31:36,539 --> 00:31:42,179
to transmit them so although we're using

789
00:31:39,480 --> 00:31:44,460
asynchronous notifications to Signal

790
00:31:42,179 --> 00:31:46,860
these updates the protocols are

791
00:31:44,460 --> 00:31:50,039
essentially synchronous

792
00:31:46,860 --> 00:31:52,799
this is great except the driver is

793
00:31:50,039 --> 00:31:55,620
reacting to receive events as well and

794
00:31:52,799 --> 00:31:58,500
it then has the potential to monopolize

795
00:31:55,620 --> 00:31:59,940
the CPU if the receive path has high

796
00:31:58,500 --> 00:32:03,960
throughput

797
00:31:59,940 --> 00:32:06,360
so we can either limit the CPU time the

798
00:32:03,960 --> 00:32:08,460
access that the driver has to the CPU or

799
00:32:06,360 --> 00:32:11,580
we can also limit the queue size so this

800
00:32:08,460 --> 00:32:12,899
ensures that the queues will fill up in

801
00:32:11,580 --> 00:32:14,940
the on the driver and then the driver

802
00:32:12,899 --> 00:32:16,559
will no longer have any work to do and

803
00:32:14,940 --> 00:32:18,240
this will ensure that components further

804
00:32:16,559 --> 00:32:20,220
down the line will have opportunity to

805
00:32:18,240 --> 00:32:23,220
run

806
00:32:20,220 --> 00:32:26,039
so how does it all perform

807
00:32:23,220 --> 00:32:28,080
what we first initially evaluated a

808
00:32:26,039 --> 00:32:30,720
simple two component setup so with a

809
00:32:28,080 --> 00:32:33,779
server that is comprised of a simple IP

810
00:32:30,720 --> 00:32:35,700
stack and an echo client

811
00:32:33,779 --> 00:32:37,679
um and as well as a driver running as a

812
00:32:35,700 --> 00:32:40,740
separate protection domain

813
00:32:37,679 --> 00:32:44,220
and then we used a IP bench program

814
00:32:40,740 --> 00:32:46,559
which runs on separate machines to send

815
00:32:44,220 --> 00:32:49,020
UDP packets over specified bite size to

816
00:32:46,559 --> 00:32:50,820
our Target seo4 machine which Echoes

817
00:32:49,020 --> 00:32:52,500
them back and then ipbench counts the

818
00:32:50,820 --> 00:32:54,360
number of successful replies to

819
00:32:52,500 --> 00:32:55,860
determine the throughput as well as the

820
00:32:54,360 --> 00:32:57,840
latency

821
00:32:55,860 --> 00:32:59,940
and this load can be split across four

822
00:32:57,840 --> 00:33:03,120
separate machines so that we can achieve

823
00:32:59,940 --> 00:33:04,500
the desired load we also ran an idle

824
00:33:03,120 --> 00:33:06,779
thread in the background to count the

825
00:33:04,500 --> 00:33:09,059
number of idle Cycles so we could

826
00:33:06,779 --> 00:33:10,919
determine the CPU utilization of the

827
00:33:09,059 --> 00:33:12,840
system

828
00:33:10,919 --> 00:33:15,179
and then we compared this to a typical

829
00:33:12,840 --> 00:33:19,019
Linux setup with an internal IP stack

830
00:33:15,179 --> 00:33:20,940
and driver and a user space Echo client

831
00:33:19,019 --> 00:33:22,559
both of these were running on single

832
00:33:20,940 --> 00:33:24,899
core

833
00:33:22,559 --> 00:33:27,120
we I also have some performance figures

834
00:33:24,899 --> 00:33:29,159
for the larger scale system where we

835
00:33:27,120 --> 00:33:31,740
have a transmit multiplexer oversee

836
00:33:29,159 --> 00:33:36,440
multiplexer this simple copy component

837
00:33:31,740 --> 00:33:36,440
and again the combined IP stack client

838
00:33:36,840 --> 00:33:43,200
so here is the throughput mapped against

839
00:33:40,140 --> 00:33:46,320
the CPU utilization for both Linux and

840
00:33:43,200 --> 00:33:48,120
the two component seo4 in green

841
00:33:46,320 --> 00:33:50,519
so what you want to see is like a nice

842
00:33:48,120 --> 00:33:53,760
straight diagonal line the dotted line

843
00:33:50,519 --> 00:33:56,519
is the CPU utilization so as you can see

844
00:33:53,760 --> 00:33:59,220
seo4 does achieve significantly more

845
00:33:56,519 --> 00:34:01,380
throughput we actually get wire speed it

846
00:33:59,220 --> 00:34:04,380
doesn't quite look like it because we're

847
00:34:01,380 --> 00:34:06,899
accounting for ethernet headers here

848
00:34:04,380 --> 00:34:08,580
but Linux drops out at around 680

849
00:34:06,899 --> 00:34:11,700
megabits per second

850
00:34:08,580 --> 00:34:14,780
we do have higher CPU utilization but I

851
00:34:11,700 --> 00:34:14,780
believe we can get this down

852
00:34:14,879 --> 00:34:21,599
here is a comparison of the median round

853
00:34:18,480 --> 00:34:22,619
trip time from a sample size of 200 000

854
00:34:21,599 --> 00:34:26,599
packets

855
00:34:22,619 --> 00:34:29,520
so seo4 starts nice and low around 100

856
00:34:26,599 --> 00:34:31,320
milliseconds per packet but this does

857
00:34:29,520 --> 00:34:33,780
increase as the system becomes

858
00:34:31,320 --> 00:34:35,700
increasingly overloaded however this is

859
00:34:33,780 --> 00:34:37,980
not to the same extent as Linux as you

860
00:34:35,700 --> 00:34:40,940
can see it's significantly more by about

861
00:34:37,980 --> 00:34:40,940
a factor of 10.

862
00:34:41,339 --> 00:34:46,500
and here is the performance comparison

863
00:34:43,679 --> 00:34:48,000
of the five component set up so this is

864
00:34:46,500 --> 00:34:49,679
the receive multiplexer transmit

865
00:34:48,000 --> 00:34:51,899
multiplexer as well as the copy

866
00:34:49,679 --> 00:34:54,839
component against the two component

867
00:34:51,899 --> 00:34:56,700
which is now in yellow so we achieve

868
00:34:54,839 --> 00:34:58,099
almost the same throughput and there's

869
00:34:56,700 --> 00:35:00,900
only about a 10

870
00:34:58,099 --> 00:35:03,000
utilization increase

871
00:35:00,900 --> 00:35:04,260
um which is fairly insignificant when

872
00:35:03,000 --> 00:35:06,599
you think about how many extra system

873
00:35:04,260 --> 00:35:08,960
calls that are required in a larger

874
00:35:06,599 --> 00:35:08,960
setup

875
00:35:09,240 --> 00:35:12,839
so overall there's some significant

876
00:35:11,280 --> 00:35:15,359
takeaways we can get from this project

877
00:35:12,839 --> 00:35:17,220
we achieve smaller latencies and higher

878
00:35:15,359 --> 00:35:19,680
throughput over Linux and this

879
00:35:17,220 --> 00:35:21,480
ultimately shows that simple works and

880
00:35:19,680 --> 00:35:23,280
you don't necessarily need to pay for it

881
00:35:21,480 --> 00:35:25,859
with performance

882
00:35:23,280 --> 00:35:28,079
the single threaded single producer

883
00:35:25,859 --> 00:35:31,140
single consumer cues also eliminate a

884
00:35:28,079 --> 00:35:34,859
lot of concurrency bugs and will Aid any

885
00:35:31,140 --> 00:35:36,780
future verification effort of the system

886
00:35:34,859 --> 00:35:38,640
our previous research categorized driver

887
00:35:36,780 --> 00:35:40,560
bugs into four separate categories we

888
00:35:38,640 --> 00:35:42,720
had device protocol violations OS

889
00:35:40,560 --> 00:35:45,119
protocol violations concurrency errors

890
00:35:42,720 --> 00:35:47,520
and then generic and the Simplicity of

891
00:35:45,119 --> 00:35:50,900
the system eliminates almost 40 percent

892
00:35:47,520 --> 00:35:50,900
of such bugs

893
00:35:51,240 --> 00:35:56,460
there's still a lot of work to do

894
00:35:53,000 --> 00:35:57,780
including further analysis to improve

895
00:35:56,460 --> 00:35:59,280
performance

896
00:35:57,780 --> 00:36:01,859
and we'd like to get that CPU

897
00:35:59,280 --> 00:36:04,380
utilization underneath Linux ideally

898
00:36:01,859 --> 00:36:07,020
and this would involve benchmarking a

899
00:36:04,380 --> 00:36:09,480
more complicated client something that's

900
00:36:07,020 --> 00:36:11,940
more evocative of an actual use case as

901
00:36:09,480 --> 00:36:14,220
opposed to Echo so something like a web

902
00:36:11,940 --> 00:36:16,619
server or a web client where the traffic

903
00:36:14,220 --> 00:36:19,320
is not necessarily symmetrical on each

904
00:36:16,619 --> 00:36:21,660
side as well

905
00:36:19,320 --> 00:36:23,760
we want to look further into the IP

906
00:36:21,660 --> 00:36:25,940
stack we're using we used lwip

907
00:36:23,760 --> 00:36:28,800
lightweight IP stack just out of the box

908
00:36:25,940 --> 00:36:33,180
but I know Linux Network stack is highly

909
00:36:28,800 --> 00:36:35,040
optimized and I believe with our own

910
00:36:33,180 --> 00:36:37,500
multiplexes we can reduce a lot of the

911
00:36:35,040 --> 00:36:40,920
complexity in a network stack as well

912
00:36:37,500 --> 00:36:43,800
so there's space for optimization there

913
00:36:40,920 --> 00:36:45,119
we also want to extend the device driver

914
00:36:43,800 --> 00:36:46,800
framework to support other device

915
00:36:45,119 --> 00:36:50,579
classes so we're currently looking into

916
00:36:46,800 --> 00:36:52,680
supporting storage devices or block

917
00:36:50,579 --> 00:36:55,380
and then of course we want to evaluate a

918
00:36:52,680 --> 00:36:57,900
proper multi-course setup

919
00:36:55,380 --> 00:37:00,780
where I believe beating Linux throughput

920
00:36:57,900 --> 00:37:02,940
may be more of a challenge

921
00:37:00,780 --> 00:37:04,980
so all the source code is open source

922
00:37:02,940 --> 00:37:06,780
and here are the links again as well as

923
00:37:04,980 --> 00:37:09,240
the links for the device forever

924
00:37:06,780 --> 00:37:10,859
framework and the IP bench program we

925
00:37:09,240 --> 00:37:13,140
use to measure the

926
00:37:10,859 --> 00:37:16,079
system

927
00:37:13,140 --> 00:37:17,470
I'm now ready to um for questions thank

928
00:37:16,079 --> 00:37:21,620
you

929
00:37:17,470 --> 00:37:21,620
[Applause]

930
00:37:25,260 --> 00:37:29,339
uh yeah we've got about four minutes

931
00:37:27,240 --> 00:37:31,579
four or five minutes for questions any

932
00:37:29,339 --> 00:37:31,579
questions

933
00:37:34,140 --> 00:37:36,320
foreign

934
00:37:39,540 --> 00:37:44,280
how does it handle user space drivers

935
00:37:42,180 --> 00:37:47,400
crashing

936
00:37:44,280 --> 00:37:50,099
in the mic up thanks

937
00:37:47,400 --> 00:37:52,260
in the garage

938
00:37:50,099 --> 00:37:54,660
uh how does what handle like you mean

939
00:37:52,260 --> 00:37:57,960
the kernel or the the whole system or

940
00:37:54,660 --> 00:38:00,660
well I mean if if the kernel just won't

941
00:37:57,960 --> 00:38:02,579
uh execute it anymore if it crashes um

942
00:38:00,660 --> 00:38:04,980
so that component's just not executing

943
00:38:02,579 --> 00:38:06,359
anymore everything else is fine um if

944
00:38:04,980 --> 00:38:08,220
something depends on it then obviously

945
00:38:06,359 --> 00:38:11,040
you gotta that component has to handle

946
00:38:08,220 --> 00:38:15,540
that there is obviously also the ability

947
00:38:11,040 --> 00:38:17,220
to restart uh components so let's say if

948
00:38:15,540 --> 00:38:19,500
you have some server that sees a driver

949
00:38:17,220 --> 00:38:21,540
has crashed then you can it could

950
00:38:19,500 --> 00:38:23,700
restart it for example and try to get it

951
00:38:21,540 --> 00:38:25,560
into a working State again

952
00:38:23,700 --> 00:38:28,260
um but yeah the the thing to stress is

953
00:38:25,560 --> 00:38:31,160
that the driver crashing does not take

954
00:38:28,260 --> 00:38:31,160
down the rest of the system

955
00:38:33,540 --> 00:38:36,500
any more questions

956
00:38:42,740 --> 00:38:48,060
what's your development workflow like

957
00:38:45,300 --> 00:38:52,400
for developing device drivers are using

958
00:38:48,060 --> 00:38:52,400
specific Hardware or software

959
00:38:58,200 --> 00:39:04,099
it's largely down to availability

960
00:39:00,800 --> 00:39:06,599
particularly of the

961
00:39:04,099 --> 00:39:09,060
reference manual because not all

962
00:39:06,599 --> 00:39:10,760
Hardware is as well documented as other

963
00:39:09,060 --> 00:39:14,640
bits of hardware

964
00:39:10,760 --> 00:39:16,859
we are limited to a set a small set of

965
00:39:14,640 --> 00:39:21,260
boards at the moment but we hope to make

966
00:39:16,859 --> 00:39:21,260
ports over the next a little bit

967
00:39:25,859 --> 00:39:28,700
any other questions

968
00:39:30,599 --> 00:39:35,520
I was wondering I you guys talked a

969
00:39:33,240 --> 00:39:37,740
little bit about one use case which was

970
00:39:35,520 --> 00:39:38,640
the man in the middle defense I think it

971
00:39:37,740 --> 00:39:42,240
was called

972
00:39:38,640 --> 00:39:44,400
what are yeah what are the other uh

973
00:39:42,240 --> 00:39:47,000
places that you see this being used now

974
00:39:44,400 --> 00:39:47,000
or in the future

975
00:39:48,420 --> 00:39:51,540
uh yeah so the core platform is pretty

976
00:39:50,460 --> 00:39:55,619
new

977
00:39:51,540 --> 00:39:59,160
um it got released into the open uh

978
00:39:55,619 --> 00:40:03,240
about a year ago and so we're working

979
00:39:59,160 --> 00:40:07,320
with a couple of organizations the VMS

980
00:40:03,240 --> 00:40:09,320
that I was referencing earlier uh we've

981
00:40:07,320 --> 00:40:12,119
got a lot of work going on right there

982
00:40:09,320 --> 00:40:13,619
there to basically have secure and

983
00:40:12,119 --> 00:40:15,960
performance

984
00:40:13,619 --> 00:40:18,480
uh VMS and device drivers all

985
00:40:15,960 --> 00:40:21,720
interacting with each other uh so I

986
00:40:18,480 --> 00:40:24,660
guess the use cases for that are

987
00:40:21,720 --> 00:40:27,380
um I don't know maybe drones or iot

988
00:40:24,660 --> 00:40:27,380
devices yeah

989
00:40:28,020 --> 00:40:30,540
yeah

990
00:40:29,280 --> 00:40:32,400
um I think there's also a space company

991
00:40:30,540 --> 00:40:33,960
that uses seo4

992
00:40:32,400 --> 00:40:35,880
um I don't think they'll be using as

993
00:40:33,960 --> 00:40:38,000
your focal platform at least for now but

994
00:40:35,880 --> 00:40:38,000
yeah

995
00:40:40,380 --> 00:40:46,020
that's great any more questions or we

996
00:40:42,780 --> 00:40:47,940
will wrap up uh thank you Lucy thank you

997
00:40:46,020 --> 00:40:50,060
Yvonne it's a great work thanks very

998
00:40:47,940 --> 00:40:50,060
much

999
00:40:50,080 --> 00:40:53,989
[Applause]