1
00:00:06,320 --> 00:00:11,499
[Music]

2
00:00:15,440 --> 00:00:20,000
good morning for our next presentation

3
00:00:18,080 --> 00:00:21,199
gernard heiser is going to talk to us

4
00:00:20,000 --> 00:00:23,600
about the

5
00:00:21,199 --> 00:00:26,960
scl4 foundation

6
00:00:23,600 --> 00:00:29,679
gernot is the micro conaldo lude

7
00:00:26,960 --> 00:00:32,239
having for over 25 years led the

8
00:00:29,679 --> 00:00:35,120
development of various l4

9
00:00:32,239 --> 00:00:37,600
microkernels which were develo deployed

10
00:00:35,120 --> 00:00:41,280
by the billions including the secure

11
00:00:37,600 --> 00:00:44,160
enclave of all ios devices

12
00:00:41,280 --> 00:00:47,039
his team has developed the scl4

13
00:00:44,160 --> 00:00:49,680
microkernel the world's first operating

14
00:00:47,039 --> 00:00:52,559
system kernel that is mathematically

15
00:00:49,680 --> 00:00:56,559
proven to be free of implementation bugs

16
00:00:52,559 --> 00:00:59,440
and that was open sourced in july 2014

17
00:00:56,559 --> 00:01:02,000
gernot is planning to have plenty of

18
00:00:59,440 --> 00:01:04,879
time for questions at the end

19
00:01:02,000 --> 00:01:08,640
so please enter any questions in the

20
00:01:04,879 --> 00:01:10,880
chat or the question tab in the chat

21
00:01:08,640 --> 00:01:13,520
over to go not

22
00:01:10,880 --> 00:01:16,479
hello welcome to my talk

23
00:01:13,520 --> 00:01:19,360
i tend to talk about that roughly every

24
00:01:16,479 --> 00:01:22,400
second lca in average last time was two

25
00:01:19,360 --> 00:01:24,560
years ago so it's up um this time again

26
00:01:22,400 --> 00:01:27,280
um typically my talks are pretty

27
00:01:24,560 --> 00:01:30,079
technical this one is different because

28
00:01:27,280 --> 00:01:32,079
i'm looking at the community around seo

29
00:01:30,079 --> 00:01:34,240
four and what happened in the seo four

30
00:01:32,079 --> 00:01:37,119
ecosystem in the past few years

31
00:01:34,240 --> 00:01:39,280
especially the seo four foundation

32
00:01:37,119 --> 00:01:41,680
these two years were really tumultuous

33
00:01:39,280 --> 00:01:43,920
it's not just covad thing worse things

34
00:01:41,680 --> 00:01:46,399
have happened that hit us

35
00:01:43,920 --> 00:01:49,439
but before i go into this

36
00:01:46,399 --> 00:01:50,960
let's have a look first on what is seo

37
00:01:49,439 --> 00:01:52,960
for for those who are not really

38
00:01:50,960 --> 00:01:55,200
familiar with seo for

39
00:01:52,960 --> 00:01:57,360
um so some background

40
00:01:55,200 --> 00:01:59,439
seo four is an open source high

41
00:01:57,360 --> 00:02:01,759
assurance high performance operating

42
00:01:59,439 --> 00:02:04,479
system microkernel and every word in

43
00:02:01,759 --> 00:02:06,799
this tag line is operational

44
00:02:04,479 --> 00:02:09,360
um it's a micro kernel so the kernel is

45
00:02:06,799 --> 00:02:10,479
a piece of software that runs at the

46
00:02:09,360 --> 00:02:12,640
um

47
00:02:10,479 --> 00:02:15,440
in the privileged mode of the hardware a

48
00:02:12,640 --> 00:02:17,920
microkernel is a kernel that's reduced

49
00:02:15,440 --> 00:02:20,319
to its absolute minimum in the case of

50
00:02:17,920 --> 00:02:23,200
seo four that's about ten thousand lines

51
00:02:20,319 --> 00:02:25,840
of code compared to tens of millions of

52
00:02:23,200 --> 00:02:28,400
lines of code in linux

53
00:02:25,840 --> 00:02:30,400
it's high performance i'll get to that

54
00:02:28,400 --> 00:02:32,160
that we claim it's the world's fastest

55
00:02:30,400 --> 00:02:34,000
micro kernel

56
00:02:32,160 --> 00:02:36,160
it's high assurance

57
00:02:34,000 --> 00:02:38,560
in the sense that it has the most

58
00:02:36,160 --> 00:02:40,879
comprehensive mathematical proof story

59
00:02:38,560 --> 00:02:43,120
of any operating system kernel around

60
00:02:40,879 --> 00:02:44,000
and i'll explain that in a little bit

61
00:02:43,120 --> 00:02:47,599
and

62
00:02:44,000 --> 00:02:50,879
it's open source under the gpl v2

63
00:02:47,599 --> 00:02:52,480
license available on github

64
00:02:50,879 --> 00:02:54,800
and this

65
00:02:52,480 --> 00:02:57,920
combination of properties

66
00:02:54,800 --> 00:03:01,120
make it the most trustworthy foundation

67
00:02:57,920 --> 00:03:02,400
for secured safety and security critical

68
00:03:01,120 --> 00:03:05,120
systems

69
00:03:02,400 --> 00:03:06,319
and it is already used in many of those

70
00:03:05,120 --> 00:03:08,800
um

71
00:03:06,319 --> 00:03:10,400
not surprisingly the initial users were

72
00:03:08,800 --> 00:03:12,879
in the defense space where people are

73
00:03:10,400 --> 00:03:17,280
the most paranoid but also

74
00:03:12,879 --> 00:03:19,840
um more interest and more

75
00:03:17,280 --> 00:03:21,120
keen to take risks for trying out new

76
00:03:19,840 --> 00:03:24,159
technology

77
00:03:21,120 --> 00:03:26,159
um but it's also used in automotive in

78
00:03:24,159 --> 00:03:28,640
communications in

79
00:03:26,159 --> 00:03:30,720
aviation space critical infrastructure

80
00:03:28,640 --> 00:03:33,200
protection and all sorts of cyber

81
00:03:30,720 --> 00:03:34,879
physical systems

82
00:03:33,200 --> 00:03:38,080
so what's really

83
00:03:34,879 --> 00:03:39,360
the defining property of seo for its the

84
00:03:38,080 --> 00:03:41,599
court of its

85
00:03:39,360 --> 00:03:42,720
uniqueness is the mathematical proof

86
00:03:41,599 --> 00:03:45,280
story

87
00:03:42,720 --> 00:03:48,400
so what that means is the seo four

88
00:03:45,280 --> 00:03:50,000
kernel is implemented mostly in c

89
00:03:48,400 --> 00:03:52,159
there's just the absolute minimum of

90
00:03:50,000 --> 00:03:54,400
assembler as i said it's about 10 000

91
00:03:52,159 --> 00:03:56,439
lines maybe 15 give and take depending

92
00:03:54,400 --> 00:03:58,879
on the architecture and platform

93
00:03:56,439 --> 00:03:59,840
necessities etc

94
00:03:58,879 --> 00:04:02,879
and

95
00:03:59,840 --> 00:04:05,840
besides the c implementation it has an

96
00:04:02,879 --> 00:04:08,799
abstract model that is written in a

97
00:04:05,840 --> 00:04:10,959
mathematical logic that defines exactly

98
00:04:08,799 --> 00:04:13,360
the operations

99
00:04:10,959 --> 00:04:16,079
how how the kernel operates

100
00:04:13,360 --> 00:04:17,359
in a in a mathematical precise

101
00:04:16,079 --> 00:04:19,759
description

102
00:04:17,359 --> 00:04:21,840
and the core of its mathematical

103
00:04:19,759 --> 00:04:25,280
assurance is this functional correctness

104
00:04:21,840 --> 00:04:27,280
proof which proves that under the

105
00:04:25,280 --> 00:04:29,919
semantics of the c language the

106
00:04:27,280 --> 00:04:31,600
implementation behaves as specified by

107
00:04:29,919 --> 00:04:35,520
this abstract model

108
00:04:31,600 --> 00:04:38,000
so in that very strong sense seo four

109
00:04:35,520 --> 00:04:40,400
its implementation is about free

110
00:04:38,000 --> 00:04:42,880
and it was the world's first operating

111
00:04:40,400 --> 00:04:44,720
system kernel with such a proof there's

112
00:04:42,880 --> 00:04:46,639
now a few more around

113
00:04:44,720 --> 00:04:50,080
all the others i claim are pretty much

114
00:04:46,639 --> 00:04:53,040
academic toys seo four was designed for

115
00:04:50,080 --> 00:04:55,120
real world use from the beginning

116
00:04:53,040 --> 00:04:58,000
that's not the complete story in terms

117
00:04:55,120 --> 00:05:01,039
of the assurance

118
00:04:58,000 --> 00:05:03,840
if that is all we what all we had which

119
00:05:01,039 --> 00:05:06,400
initially is what we had um then we'd be

120
00:05:03,840 --> 00:05:08,000
at the mercy of the sea compiler so to

121
00:05:06,400 --> 00:05:10,720
get rid of that

122
00:05:08,000 --> 00:05:13,520
we also have a proof of translation

123
00:05:10,720 --> 00:05:15,039
correctness meaning that the binary that

124
00:05:13,520 --> 00:05:17,440
actually runs on the hardware that's

125
00:05:15,039 --> 00:05:19,360
produced by the compiler and the linga

126
00:05:17,440 --> 00:05:21,600
are a correct

127
00:05:19,360 --> 00:05:24,080
translation of our c code

128
00:05:21,600 --> 00:05:26,560
that takes the compiler and the linga

129
00:05:24,080 --> 00:05:29,440
out of the trusted computing base

130
00:05:26,560 --> 00:05:31,919
also our assumptions on the c semantics

131
00:05:29,440 --> 00:05:34,320
are no longer security or safety

132
00:05:31,919 --> 00:05:36,639
critical because they fall out in this

133
00:05:34,320 --> 00:05:38,880
combination of proofs

134
00:05:36,639 --> 00:05:42,240
that's all very strong

135
00:05:38,880 --> 00:05:43,680
but it's not sufficient because just

136
00:05:42,240 --> 00:05:45,680
because we have a model that is

137
00:05:43,680 --> 00:05:48,000
correctly implemented doesn't mean the

138
00:05:45,680 --> 00:05:51,199
model is any good so we have a further

139
00:05:48,000 --> 00:05:55,280
set of proofs that show that the kernel

140
00:05:51,199 --> 00:05:56,400
is able to enforce the traditional cia

141
00:05:55,280 --> 00:05:58,880
prop

142
00:05:56,400 --> 00:06:01,840
security properties of confidentiality

143
00:05:58,880 --> 00:06:02,880
integrity and availability

144
00:06:01,840 --> 00:06:05,440
and

145
00:06:02,880 --> 00:06:08,560
that those proofs compose

146
00:06:05,440 --> 00:06:10,800
so we know that the binary that runs on

147
00:06:08,560 --> 00:06:12,319
the hardware actually has these security

148
00:06:10,800 --> 00:06:13,919
properties

149
00:06:12,319 --> 00:06:16,240
all these proofs are machine checked

150
00:06:13,919 --> 00:06:18,160
using interactive theorem privilege

151
00:06:16,240 --> 00:06:20,080
otherwise they would be pretty worthless

152
00:06:18,160 --> 00:06:22,319
because in average we have about 20

153
00:06:20,080 --> 00:06:24,560
lines of proof script per lines of

154
00:06:22,319 --> 00:06:26,400
kernel code if this was all pen and

155
00:06:24,560 --> 00:06:29,120
paper there would be more bugs in the

156
00:06:26,400 --> 00:06:31,360
proofs than in the code um the

157
00:06:29,120 --> 00:06:35,520
interactive theorem proof of prevents us

158
00:06:31,360 --> 00:06:37,360
from doing incorrect proofs

159
00:06:35,520 --> 00:06:39,759
on top of that it's still the world's

160
00:06:37,360 --> 00:06:41,680
only capability based os kernel with

161
00:06:39,759 --> 00:06:43,600
such a correctness proof interestingly

162
00:06:41,680 --> 00:06:45,919
the academic toys don't really worry

163
00:06:43,600 --> 00:06:47,199
about real security challenges

164
00:06:45,919 --> 00:06:49,440
and

165
00:06:47,199 --> 00:06:52,479
use traditional

166
00:06:49,440 --> 00:06:54,720
attack security models

167
00:06:52,479 --> 00:06:57,440
this core functional correctness proof

168
00:06:54,720 --> 00:07:00,240
was originally done on 32-bit arm

169
00:06:57,440 --> 00:07:02,800
it was then later repeated on 64-bit

170
00:07:00,240 --> 00:07:06,160
intel platforms as well as just more

171
00:07:02,800 --> 00:07:09,199
recently the 64-bit risk 5 platform

172
00:07:06,160 --> 00:07:12,400
the translation correctness is also

173
00:07:09,199 --> 00:07:15,199
originally done for arm 32 and is now

174
00:07:12,400 --> 00:07:18,000
done for 64-bit risk 5 and the same

175
00:07:15,199 --> 00:07:19,680
holds true for the security properties

176
00:07:18,000 --> 00:07:22,240
so for arm and

177
00:07:19,680 --> 00:07:24,400
32-bit arm and 64-bit risk five we've

178
00:07:22,240 --> 00:07:26,800
got the full proof sorry

179
00:07:24,400 --> 00:07:28,960
there's some um disclaimers here there's

180
00:07:26,800 --> 00:07:31,120
still some unverified code in particular

181
00:07:28,960 --> 00:07:34,160
the boot code because that's

182
00:07:31,120 --> 00:07:36,000
boring as bad menu

183
00:07:34,160 --> 00:07:37,680
and we're waiting for someone to put

184
00:07:36,000 --> 00:07:39,440
money on the table to actually prove

185
00:07:37,680 --> 00:07:40,800
that because there's nothing interesting

186
00:07:39,440 --> 00:07:42,720
to learn from that

187
00:07:40,800 --> 00:07:45,680
but of course it should be done there's

188
00:07:42,720 --> 00:07:48,720
also some details on how cases behave

189
00:07:45,680 --> 00:07:51,759
and details of the mmu that are

190
00:07:48,720 --> 00:07:54,479
abstracted and not proved to the isa

191
00:07:51,759 --> 00:07:56,720
level and we have a high performance

192
00:07:54,479 --> 00:07:58,879
multi-core implementation but no

193
00:07:56,720 --> 00:08:00,960
verification no proofs about multi-core

194
00:07:58,879 --> 00:08:03,360
these are still outstanding

195
00:08:00,960 --> 00:08:06,560
so this is the the proof story

196
00:08:03,360 --> 00:08:09,360
and the interesting bit about seo for is

197
00:08:06,560 --> 00:08:12,479
that we get this strength of assurance

198
00:08:09,360 --> 00:08:14,319
without compromising performance my

199
00:08:12,479 --> 00:08:16,000
catchphrase is

200
00:08:14,319 --> 00:08:18,080
security is no excuse for bad

201
00:08:16,000 --> 00:08:20,720
performance and you don't have to take

202
00:08:18,080 --> 00:08:24,560
my word for it this is

203
00:08:20,720 --> 00:08:26,879
analysis done by researchers at shanghai

204
00:08:24,560 --> 00:08:29,440
tung university who in two papers

205
00:08:26,879 --> 00:08:33,039
compared three open source microkernels

206
00:08:29,440 --> 00:08:36,000
seo for the fiasco oc microkernel and

207
00:08:33,039 --> 00:08:38,640
google circon the numbers you see here

208
00:08:36,000 --> 00:08:40,880
are latencies of the ipc message passing

209
00:08:38,640 --> 00:08:44,159
operations so small is good

210
00:08:40,880 --> 00:08:46,320
and you see that seo four is about a

211
00:08:44,159 --> 00:08:49,279
factor two three faster than the other

212
00:08:46,320 --> 00:08:50,959
l4 microkernel and a order of magnitude

213
00:08:49,279 --> 00:08:53,200
faster than silcon

214
00:08:50,959 --> 00:08:54,880
and this despite at one stage when they

215
00:08:53,200 --> 00:08:58,240
did the one paper we had a temporary

216
00:08:54,880 --> 00:09:01,440
performance regression um by 50 we still

217
00:08:58,240 --> 00:09:04,160
were twice as fast as the other kernel

218
00:09:01,440 --> 00:09:06,560
and um so i claim he's still the world's

219
00:09:04,160 --> 00:09:09,200
first fastest microkernel obviously

220
00:09:06,560 --> 00:09:11,279
there's no data on propriety kernels

221
00:09:09,200 --> 00:09:14,080
that are widely used in safety critical

222
00:09:11,279 --> 00:09:16,560
systems in particular qnx and green

223
00:09:14,080 --> 00:09:18,240
hills integrity but i know from other

224
00:09:16,560 --> 00:09:21,040
sources that their performance is more

225
00:09:18,240 --> 00:09:23,440
like circon than scl4 so about an order

226
00:09:21,040 --> 00:09:26,480
of magnitude smaller the other sources

227
00:09:23,440 --> 00:09:27,839
you can check them in the slides later

228
00:09:26,480 --> 00:09:30,720
so important to understand is a

229
00:09:27,839 --> 00:09:32,800
microkernel is not an operating system

230
00:09:30,720 --> 00:09:34,880
so in a microkernel based system

231
00:09:32,800 --> 00:09:37,680
anything interesting all the operating

232
00:09:34,880 --> 00:09:40,240
system services you expect to have are

233
00:09:37,680 --> 00:09:42,320
implement as user level applications

234
00:09:40,240 --> 00:09:44,720
user level processes

235
00:09:42,320 --> 00:09:47,040
um so that includes file systems device

236
00:09:44,720 --> 00:09:50,399
drivers network stacks power management

237
00:09:47,040 --> 00:09:52,320
virtual machines all the stuff runs on

238
00:09:50,399 --> 00:09:54,000
in user level side by side with

239
00:09:52,320 --> 00:09:55,839
applications

240
00:09:54,000 --> 00:09:58,880
isolated from each other and

241
00:09:55,839 --> 00:10:00,399
applications by these bulletproof

242
00:09:58,880 --> 00:10:02,480
isolation walls put up by the

243
00:10:00,399 --> 00:10:04,320
microkernel and in operation the

244
00:10:02,480 --> 00:10:05,839
microkernel is basically a fast context

245
00:10:04,320 --> 00:10:08,640
switching machine that

246
00:10:05,839 --> 00:10:11,279
switches between those

247
00:10:08,640 --> 00:10:13,440
sandboxes and provide

248
00:10:11,279 --> 00:10:14,880
delivers function call arguments

249
00:10:13,440 --> 00:10:17,440
basically

250
00:10:14,880 --> 00:10:19,040
what's also not unique about seo for but

251
00:10:17,440 --> 00:10:22,320
the unique about

252
00:10:19,040 --> 00:10:24,399
verified kernels is capability based

253
00:10:22,320 --> 00:10:25,600
access control

254
00:10:24,399 --> 00:10:27,920
these are not

255
00:10:25,600 --> 00:10:29,920
like capabilities in linux they are so

256
00:10:27,920 --> 00:10:31,680
called object capabilities that have

257
00:10:29,920 --> 00:10:34,800
much more

258
00:10:31,680 --> 00:10:36,720
interesting properties

259
00:10:34,800 --> 00:10:38,880
in particular they allow very

260
00:10:36,720 --> 00:10:41,600
fine-grained access

261
00:10:38,880 --> 00:10:43,680
control to objects in

262
00:10:41,600 --> 00:10:45,519
particular that means in a seo

263
00:10:43,680 --> 00:10:47,360
four-based system you can when these

264
00:10:45,519 --> 00:10:50,000
channels exist then

265
00:10:47,360 --> 00:10:51,839
components can communicate where such a

266
00:10:50,000 --> 00:10:53,760
channel has not been explicitly opened

267
00:10:51,839 --> 00:10:55,680
no direct communication is possible so

268
00:10:53,760 --> 00:10:58,399
in this case the untrusted native

269
00:10:55,680 --> 00:11:00,640
component can

270
00:10:58,399 --> 00:11:03,360
communicate with the virtual machine in

271
00:11:00,640 --> 00:11:05,279
the middle only via the trusted native

272
00:11:03,360 --> 00:11:07,839
component that can filter and whatever

273
00:11:05,279 --> 00:11:07,839
protect it

274
00:11:08,399 --> 00:11:11,519
so

275
00:11:09,279 --> 00:11:14,480
this strong property of no communication

276
00:11:11,519 --> 00:11:19,519
on links explicitly authorized as a core

277
00:11:14,480 --> 00:11:23,200
to a security enforcement as in seo4

278
00:11:19,519 --> 00:11:24,399
so what has seo4

279
00:11:23,200 --> 00:11:28,160
completed

280
00:11:24,399 --> 00:11:30,160
seo 4 and its verification in july oh

281
00:11:28,160 --> 00:11:31,839
nine this was in a

282
00:11:30,160 --> 00:11:33,920
government organization called nikta

283
00:11:31,839 --> 00:11:35,920
which has been while being absorbed into

284
00:11:33,920 --> 00:11:39,360
csiro

285
00:11:35,920 --> 00:11:40,720
over the next few years we completed

286
00:11:39,360 --> 00:11:43,040
most of the

287
00:11:40,720 --> 00:11:46,160
other proofs about seo force or binary

288
00:11:43,040 --> 00:11:49,440
correctness security enforcement also

289
00:11:46,160 --> 00:11:51,279
um the world's first

290
00:11:49,440 --> 00:11:53,760
sound and complete

291
00:11:51,279 --> 00:11:53,760
assess

292
00:11:53,920 --> 00:11:57,519
assessment of worst case execution time

293
00:11:56,320 --> 00:11:59,440
latencies

294
00:11:57,519 --> 00:12:02,160
of any protected mode operating system

295
00:11:59,440 --> 00:12:03,680
kernel which is what you need for re for

296
00:12:02,160 --> 00:12:04,800
hard real time

297
00:12:03,680 --> 00:12:07,279
and then

298
00:12:04,800 --> 00:12:09,600
in july we open sourced seo for under

299
00:12:07,279 --> 00:12:11,519
the gpl v2 license took us a while to

300
00:12:09,600 --> 00:12:12,399
get permission to do that

301
00:12:11,519 --> 00:12:15,680
and

302
00:12:12,399 --> 00:12:18,880
a year later we had the first publicly

303
00:12:15,680 --> 00:12:21,519
visible great success when the

304
00:12:18,880 --> 00:12:24,560
a boeing unmanned helicopter flew

305
00:12:21,519 --> 00:12:26,480
autonomously on seo 4 under the darpa

306
00:12:24,560 --> 00:12:28,160
hackins program

307
00:12:26,480 --> 00:12:30,240
and

308
00:12:28,160 --> 00:12:31,440
that was the

309
00:12:30,240 --> 00:12:33,760
mid

310
00:12:31,440 --> 00:12:37,200
program demo if you like and then in

311
00:12:33,760 --> 00:12:39,360
april 17 the final demo showed seo for

312
00:12:37,200 --> 00:12:44,079
stopping the

313
00:12:39,360 --> 00:12:45,760
helicopter from being attacked by cyber

314
00:12:44,079 --> 00:12:48,720
attackers

315
00:12:45,760 --> 00:12:50,800
initially the linux space system it took

316
00:12:48,720 --> 00:12:51,760
the attackers two weeks to completely

317
00:12:50,800 --> 00:12:54,000
own it

318
00:12:51,760 --> 00:12:56,480
once we have had re-architected the

319
00:12:54,000 --> 00:12:58,399
system for seo four the hackers couldn't

320
00:12:56,480 --> 00:13:00,800
do anything even though we gave them

321
00:12:58,399 --> 00:13:03,839
root access to a virtual machine running

322
00:13:00,800 --> 00:13:06,000
linux on top of the seo four platform

323
00:13:03,839 --> 00:13:07,920
and it started shipping and defense

324
00:13:06,000 --> 00:13:10,160
products and then

325
00:13:07,920 --> 00:13:12,000
just under two years ago we created the

326
00:13:10,160 --> 00:13:13,440
seo4 foundation under the linux

327
00:13:12,000 --> 00:13:15,920
foundation

328
00:13:13,440 --> 00:13:18,560
and meanwhile we kept on working with

329
00:13:15,920 --> 00:13:20,079
technical achievements we did the proofs

330
00:13:18,560 --> 00:13:21,200
for risk five versus the functional

331
00:13:20,079 --> 00:13:22,880
correctness

332
00:13:21,200 --> 00:13:24,320
and then the other proofs throughout the

333
00:13:22,880 --> 00:13:25,680
last year

334
00:13:24,320 --> 00:13:28,720
and um

335
00:13:25,680 --> 00:13:31,360
a noteworthy invent was last august when

336
00:13:28,720 --> 00:13:32,639
darpa at defcon had to steal this drone

337
00:13:31,360 --> 00:13:33,360
challenge where

338
00:13:32,639 --> 00:13:36,240
a

339
00:13:33,360 --> 00:13:39,680
quadcopter that was hardened protected

340
00:13:36,240 --> 00:13:42,160
by seo4 was presented to the hackers

341
00:13:39,680 --> 00:13:44,800
with a challenge to compromise it and

342
00:13:42,160 --> 00:13:49,120
again given even root access to a linux

343
00:13:44,800 --> 00:13:50,160
virtual machine they couldn't break out

344
00:13:49,120 --> 00:13:53,199
so

345
00:13:50,160 --> 00:13:55,440
looks like good continuous progress so

346
00:13:53,199 --> 00:13:57,279
what's the issue well

347
00:13:55,440 --> 00:13:59,920
what i want to talk specifically is of

348
00:13:57,279 --> 00:14:01,760
course the seo 4 foundation and what

349
00:13:59,920 --> 00:14:02,800
happened to it in its

350
00:14:01,760 --> 00:14:05,680
first

351
00:14:02,800 --> 00:14:08,800
20 months or so of its lifetime and it

352
00:14:05,680 --> 00:14:09,680
as i said it was tumultuous two years

353
00:14:08,800 --> 00:14:12,320
so

354
00:14:09,680 --> 00:14:14,880
the seo 4 foundation

355
00:14:12,320 --> 00:14:16,880
was created in april 20

356
00:14:14,880 --> 00:14:18,800
and if we look at how the membership

357
00:14:16,880 --> 00:14:19,760
developed we had six members to start

358
00:14:18,800 --> 00:14:22,560
with

359
00:14:19,760 --> 00:14:25,600
and um great hopes of exploding

360
00:14:22,560 --> 00:14:27,680
membership and so we collected members a

361
00:14:25,600 --> 00:14:29,760
few more came on board

362
00:14:27,680 --> 00:14:31,040
but there wasn't anything

363
00:14:29,760 --> 00:14:32,000
radical

364
00:14:31,040 --> 00:14:33,600
and

365
00:14:32,000 --> 00:14:35,839
until then

366
00:14:33,600 --> 00:14:38,800
after may 21

367
00:14:35,839 --> 00:14:41,519
membership started to increase a lot and

368
00:14:38,800 --> 00:14:44,079
there is still more significant number

369
00:14:41,519 --> 00:14:45,040
of more members in the pipeline

370
00:14:44,079 --> 00:14:47,760
and

371
00:14:45,040 --> 00:14:49,519
the just even more impressive if you

372
00:14:47,760 --> 00:14:51,440
look at it in dollar terms the

373
00:14:49,519 --> 00:14:53,040
membership fees

374
00:14:51,440 --> 00:14:54,399
that brought been brought in by those

375
00:14:53,040 --> 00:14:56,800
members

376
00:14:54,399 --> 00:15:00,160
we grew from a budget of about 38 000

377
00:14:56,800 --> 00:15:02,639
u.s and then suddenly from may we jumped

378
00:15:00,160 --> 00:15:05,120
to a just on the half million dollar u.s

379
00:15:02,639 --> 00:15:07,279
budget which is really awesome because i

380
00:15:05,120 --> 00:15:09,199
always said we need about a quarter

381
00:15:07,279 --> 00:15:12,800
million u.s to run the foundation

382
00:15:09,199 --> 00:15:15,279
properly we will well above this now

383
00:15:12,800 --> 00:15:17,600
so the question is what happened in may

384
00:15:15,279 --> 00:15:20,160
21 which triggered all that

385
00:15:17,600 --> 00:15:23,279
and this is really what my talk is about

386
00:15:20,160 --> 00:15:24,480
so what happened in may 21

387
00:15:23,279 --> 00:15:27,680
um

388
00:15:24,480 --> 00:15:29,680
there was a event when data 61 which

389
00:15:27,680 --> 00:15:32,240
housed the trustworthy systems group

390
00:15:29,680 --> 00:15:35,120
which is the developers of seo four

391
00:15:32,240 --> 00:15:38,160
decided to junk the trustworthy systems

392
00:15:35,120 --> 00:15:40,480
group so is the telling article in

393
00:15:38,160 --> 00:15:42,000
innovation us drops world class seo for

394
00:15:40,480 --> 00:15:44,720
security team

395
00:15:42,000 --> 00:15:46,959
and there was a fair amount of un pretty

396
00:15:44,720 --> 00:15:49,040
uncomplimentary press uncomplimentary

397
00:15:46,959 --> 00:15:51,120
about xyron not us

398
00:15:49,040 --> 00:15:55,440
innovation hostile take a world leading

399
00:15:51,120 --> 00:15:57,759
secure kernel and get into the curb

400
00:15:55,440 --> 00:16:00,560
and really this is basically what

401
00:15:57,759 --> 00:16:03,120
happened and we had a real problem

402
00:16:00,560 --> 00:16:05,600
interestingly there was a lot of support

403
00:16:03,120 --> 00:16:08,560
in the community including major

404
00:16:05,600 --> 00:16:10,880
research labs and companies offering to

405
00:16:08,560 --> 00:16:12,720
just take over the whole team

406
00:16:10,880 --> 00:16:15,600
we didn't want to do that because we

407
00:16:12,720 --> 00:16:17,279
didn't want to work for one particular

408
00:16:15,600 --> 00:16:19,519
organization the

409
00:16:17,279 --> 00:16:21,920
sarah experience had told uh taught us

410
00:16:19,519 --> 00:16:24,399
even if we knew it before but the zara

411
00:16:21,920 --> 00:16:27,040
experience made it abundantly clear that

412
00:16:24,399 --> 00:16:28,320
this is a bad idea we wanted to remain

413
00:16:27,040 --> 00:16:30,320
independent

414
00:16:28,320 --> 00:16:32,639
but we had a real problem in that our

415
00:16:30,320 --> 00:16:34,720
funding was basically completely drawn

416
00:16:32,639 --> 00:16:35,759
out under neath us

417
00:16:34,720 --> 00:16:37,839
and

418
00:16:35,759 --> 00:16:40,800
how could we rescue the team

419
00:16:37,839 --> 00:16:42,399
and fortunately unisw

420
00:16:40,800 --> 00:16:45,199
came to the table

421
00:16:42,399 --> 00:16:46,079
my visionary boss the head of school

422
00:16:45,199 --> 00:16:47,920
aaron

423
00:16:46,079 --> 00:16:49,680
quickly

424
00:16:47,920 --> 00:16:51,519
offered to fund the team to the rest of

425
00:16:49,680 --> 00:16:53,600
the year and that was the buffer we

426
00:16:51,519 --> 00:16:55,440
needed i was very confident that we

427
00:16:53,600 --> 00:16:57,759
would get money into the door within

428
00:16:55,440 --> 00:17:00,320
half a year to sustain the group i was

429
00:16:57,759 --> 00:17:02,639
right but we needed to go get over this

430
00:17:00,320 --> 00:17:03,680
gap and this is what unsw allowed us to

431
00:17:02,639 --> 00:17:04,720
do

432
00:17:03,680 --> 00:17:08,559
so

433
00:17:04,720 --> 00:17:09,679
what does life look like after csiro

434
00:17:08,559 --> 00:17:11,439
this is

435
00:17:09,679 --> 00:17:13,439
gives you an idea of the importance of

436
00:17:11,439 --> 00:17:14,959
this unsw funding so

437
00:17:13,439 --> 00:17:17,120
this is the staffing level in the

438
00:17:14,959 --> 00:17:19,919
trustworthy systems teams the developers

439
00:17:17,120 --> 00:17:22,799
and supporters of seo four

440
00:17:19,919 --> 00:17:25,280
blue is unsw academics of basically

441
00:17:22,799 --> 00:17:27,600
people who with permanent or tenure

442
00:17:25,280 --> 00:17:28,720
track positions at unsw who are part of

443
00:17:27,600 --> 00:17:30,720
the team

444
00:17:28,720 --> 00:17:32,880
red is what almost all the complete

445
00:17:30,720 --> 00:17:34,080
balance of the team was which is cyrus

446
00:17:32,880 --> 00:17:36,799
stuff

447
00:17:34,080 --> 00:17:38,720
and i say csiro funded because the money

448
00:17:36,799 --> 00:17:40,320
was under cyber control there was really

449
00:17:38,720 --> 00:17:42,640
money we had brought in we had brought

450
00:17:40,320 --> 00:17:44,400
in millions every year

451
00:17:42,640 --> 00:17:46,559
but as soon as we had a gap in this

452
00:17:44,400 --> 00:17:47,679
funding they cut us loose

453
00:17:46,559 --> 00:17:50,320
so

454
00:17:47,679 --> 00:17:52,240
it we were a total of two dozen staff

455
00:17:50,320 --> 00:17:53,600
roughly at the beginning of

456
00:17:52,240 --> 00:17:54,640
21

457
00:17:53,600 --> 00:17:56,960
and

458
00:17:54,640 --> 00:17:59,280
then in may zaro announced that they

459
00:17:56,960 --> 00:18:01,840
will stop funding us this is after they

460
00:17:59,280 --> 00:18:05,039
withered us down a fair bit already

461
00:18:01,840 --> 00:18:06,720
um i had already to rescue a number of

462
00:18:05,039 --> 00:18:09,200
people put them

463
00:18:06,720 --> 00:18:11,200
on external funds at unisw so this is

464
00:18:09,200 --> 00:18:13,440
the the green

465
00:18:11,200 --> 00:18:15,919
bit that's been growing a bit

466
00:18:13,440 --> 00:18:18,320
and then um the

467
00:18:15,919 --> 00:18:21,520
unis w bridging fund which is the yellow

468
00:18:18,320 --> 00:18:23,679
bit here this yellow lake um is really

469
00:18:21,520 --> 00:18:26,400
what got us over the gap and by the end

470
00:18:23,679 --> 00:18:29,919
of the year we had a few million new

471
00:18:26,400 --> 00:18:31,280
money external funds lined up to

472
00:18:29,919 --> 00:18:32,960
support the team and we are

473
00:18:31,280 --> 00:18:35,679
self-sustaining again

474
00:18:32,960 --> 00:18:36,960
without this unisw money we would be

475
00:18:35,679 --> 00:18:39,440
dead

476
00:18:36,960 --> 00:18:41,600
and um

477
00:18:39,440 --> 00:18:44,240
this is really scary right we were by

478
00:18:41,600 --> 00:18:45,919
any definition a really successful

479
00:18:44,240 --> 00:18:49,039
product with a lot of worldwide

480
00:18:45,919 --> 00:18:52,000
attention and interest a lot of

481
00:18:49,039 --> 00:18:53,679
support from foreign governments

482
00:18:52,000 --> 00:18:54,960
including in particular the us

483
00:18:53,679 --> 00:18:58,720
government

484
00:18:54,960 --> 00:19:01,120
and inside cyril we were inside data61

485
00:18:58,720 --> 00:19:03,360
at least we were with the exception of

486
00:19:01,120 --> 00:19:05,679
the boeing project by far the most

487
00:19:03,360 --> 00:19:08,080
successful group in pulling in money

488
00:19:05,679 --> 00:19:11,360
from outside and particular

489
00:19:08,080 --> 00:19:13,679
non-australian government money

490
00:19:11,360 --> 00:19:16,320
but that didn't stop them from running

491
00:19:13,679 --> 00:19:18,320
down the team not extending contracts

492
00:19:16,320 --> 00:19:20,480
leading to projects being laid or

493
00:19:18,320 --> 00:19:23,919
failing to deliver which of course is a

494
00:19:20,480 --> 00:19:26,480
really reputational damage to us which

495
00:19:23,919 --> 00:19:28,240
of no fault of ours it was basically

496
00:19:26,480 --> 00:19:30,480
penalizing success so i don't really

497
00:19:28,240 --> 00:19:31,520
know what went on in the mind of those

498
00:19:30,480 --> 00:19:34,400
people

499
00:19:31,520 --> 00:19:36,240
um so basically the story is we knew for

500
00:19:34,400 --> 00:19:37,919
a long time we had to get out but the

501
00:19:36,240 --> 00:19:39,360
problem is we didn't know how to do it

502
00:19:37,919 --> 00:19:41,760
because

503
00:19:39,360 --> 00:19:44,880
it takes a while to build up a funding

504
00:19:41,760 --> 00:19:46,400
pipeline and um it's hard to do that in

505
00:19:44,880 --> 00:19:49,200
the background while you're committed to

506
00:19:46,400 --> 00:19:51,840
osiro because they're giving you money

507
00:19:49,200 --> 00:19:53,840
so only once the cut was made we could

508
00:19:51,840 --> 00:19:55,440
really fully focus on getting additional

509
00:19:53,840 --> 00:19:58,320
money into the door and this is where

510
00:19:55,440 --> 00:20:00,799
the unsw bridge funding was a real life

511
00:19:58,320 --> 00:20:00,799
saver

512
00:20:02,000 --> 00:20:04,400
so the

513
00:20:04,720 --> 00:20:10,240
this next slide is sort of um

514
00:20:07,440 --> 00:20:14,080
interesting view on how the staff the

515
00:20:10,240 --> 00:20:16,559
people developed in january 20 we had 38

516
00:20:14,080 --> 00:20:18,320
people four of which whom were at unisw

517
00:20:16,559 --> 00:20:19,600
arrested cyro

518
00:20:18,320 --> 00:20:23,440
um by

519
00:20:19,600 --> 00:20:25,600
a year later this had reduced to 26 um

520
00:20:23,440 --> 00:20:28,240
because cyro stopped

521
00:20:25,600 --> 00:20:30,400
extending contracts etc despite we're

522
00:20:28,240 --> 00:20:31,440
having well-funded projects

523
00:20:30,400 --> 00:20:34,960
and then

524
00:20:31,440 --> 00:20:35,840
they cut us out and a year later january

525
00:20:34,960 --> 00:20:38,720
now

526
00:20:35,840 --> 00:20:40,880
we have about 22 people which is less

527
00:20:38,720 --> 00:20:43,280
than we were a year ago but

528
00:20:40,880 --> 00:20:45,200
about the same size as we were in may

529
00:20:43,280 --> 00:20:48,320
when they announced us the stopping of

530
00:20:45,200 --> 00:20:50,559
funding so the group has recovered um

531
00:20:48,320 --> 00:20:52,159
despite the fact that of course our

532
00:20:50,559 --> 00:20:54,320
people are extremely employable as soon

533
00:20:52,159 --> 00:20:55,840
as the news was out that sarah was

534
00:20:54,320 --> 00:20:57,280
cutting us loose

535
00:20:55,840 --> 00:20:59,200
everyone

536
00:20:57,280 --> 00:21:01,280
the headhunters were after everyone and

537
00:20:59,200 --> 00:21:03,840
most people had java offers literally

538
00:21:01,280 --> 00:21:03,840
within days

539
00:21:04,080 --> 00:21:07,600
so it's really it was really important

540
00:21:05,840 --> 00:21:09,679
that i could tell people look we've got

541
00:21:07,600 --> 00:21:12,400
the money stay with us

542
00:21:09,679 --> 00:21:15,200
we get over this

543
00:21:12,400 --> 00:21:16,960
it's also interesting to see what

544
00:21:15,200 --> 00:21:19,600
happened to the people who have left so

545
00:21:16,960 --> 00:21:21,360
at the moment we have 22 people 30 in

546
00:21:19,600 --> 00:21:23,600
our people we retained from the original

547
00:21:21,360 --> 00:21:26,720
team nine are newcomers

548
00:21:23,600 --> 00:21:28,480
this is the biggest influx of new talent

549
00:21:26,720 --> 00:21:31,440
we've seen in many many years and

550
00:21:28,480 --> 00:21:33,600
they're mostly unswi undergrad students

551
00:21:31,440 --> 00:21:35,760
or fresh graduates and they're awesome

552
00:21:33,600 --> 00:21:37,600
it's it's not only the biggest number of

553
00:21:35,760 --> 00:21:41,760
inflow into the team we had in a long

554
00:21:37,600 --> 00:21:43,440
year time it's also the the best quality

555
00:21:41,760 --> 00:21:45,840
and

556
00:21:43,440 --> 00:21:47,600
then of the people we lost

557
00:21:45,840 --> 00:21:48,720
this is over a period of roughly two

558
00:21:47,600 --> 00:21:49,600
years

559
00:21:48,720 --> 00:21:51,520
10

560
00:21:49,600 --> 00:21:53,120
were lost completely and 10 stayed in

561
00:21:51,520 --> 00:21:54,799
the community so moved into other

562
00:21:53,120 --> 00:21:57,919
companies and this is also a change from

563
00:21:54,799 --> 00:22:00,559
before where people who left the team

564
00:21:57,919 --> 00:22:03,679
typically went into other jobs and were

565
00:22:00,559 --> 00:22:05,600
lost from the seo4 ecosystem now half of

566
00:22:03,679 --> 00:22:08,159
them went into the community and i have

567
00:22:05,600 --> 00:22:10,159
hoped of getting some of the lost ones

568
00:22:08,159 --> 00:22:13,120
back

569
00:22:10,159 --> 00:22:14,559
um so yeah it's an amazing influx of

570
00:22:13,120 --> 00:22:17,760
talent

571
00:22:14,559 --> 00:22:19,360
what's behind that so obviously

572
00:22:17,760 --> 00:22:21,600
the the

573
00:22:19,360 --> 00:22:24,240
cyrus abandoned triggered the spill into

574
00:22:21,600 --> 00:22:27,200
the community and fortunately there was

575
00:22:24,240 --> 00:22:28,559
enough community around now to absorb

576
00:22:27,200 --> 00:22:30,400
many of them

577
00:22:28,559 --> 00:22:33,280
they would have absorbed all of them but

578
00:22:30,400 --> 00:22:35,440
some got attractive offers elsewhere

579
00:22:33,280 --> 00:22:38,720
so the upside of the split is that we

580
00:22:35,440 --> 00:22:39,679
have now less organizational dependency

581
00:22:38,720 --> 00:22:41,760
and

582
00:22:39,679 --> 00:22:43,760
we also have a broad enough meaning of

583
00:22:41,760 --> 00:22:45,840
the developer base with our former

584
00:22:43,760 --> 00:22:48,000
people moving into various companies

585
00:22:45,840 --> 00:22:49,200
training people up there and spreading

586
00:22:48,000 --> 00:22:51,760
the skills

587
00:22:49,200 --> 00:22:54,400
the the biggest downside is that we lost

588
00:22:51,760 --> 00:22:56,159
a lot of experience in the ts team

589
00:22:54,400 --> 00:22:58,240
even though we kept

590
00:22:56,159 --> 00:23:00,320
a lot of the people we lost most of the

591
00:22:58,240 --> 00:23:01,200
really experienced ones and really only

592
00:23:00,320 --> 00:23:02,799
two

593
00:23:01,200 --> 00:23:04,960
experienced people left and all the

594
00:23:02,799 --> 00:23:07,200
others are relatively fresh so while

595
00:23:04,960 --> 00:23:09,280
we're rebuilding the skills base there's

596
00:23:07,200 --> 00:23:11,200
a delay there this will take up

597
00:23:09,280 --> 00:23:13,280
a while to get everyone up to speed even

598
00:23:11,200 --> 00:23:16,080
though the newcomers are really awesome

599
00:23:13,280 --> 00:23:16,880
and very fast learners

600
00:23:16,080 --> 00:23:19,840
then

601
00:23:16,880 --> 00:23:22,400
but it is clear without had unisw not

602
00:23:19,840 --> 00:23:24,640
decided to support us for half a year we

603
00:23:22,400 --> 00:23:28,720
the team would be dead we would not be

604
00:23:24,640 --> 00:23:28,720
able to keep on the people or recover

605
00:23:29,919 --> 00:23:33,280
and

606
00:23:31,760 --> 00:23:35,200
we need to

607
00:23:33,280 --> 00:23:37,280
broaden the developer base which is

608
00:23:35,200 --> 00:23:39,840
happening partially by

609
00:23:37,280 --> 00:23:42,080
ts people moving into the community

610
00:23:39,840 --> 00:23:43,520
as i said in the past they typically

611
00:23:42,080 --> 00:23:45,039
were less

612
00:23:43,520 --> 00:23:46,960
but also

613
00:23:45,039 --> 00:23:49,279
there's a great deal of industrial

614
00:23:46,960 --> 00:23:51,760
adoption which leads up to building the

615
00:23:49,279 --> 00:23:53,919
skills based in industry and part of the

616
00:23:51,760 --> 00:23:56,799
problem here is really we need to be

617
00:23:53,919 --> 00:23:59,120
able to scale the skills development

618
00:23:56,799 --> 00:24:00,960
beyond what we can do at unsw

619
00:23:59,120 --> 00:24:03,120
and so this is part of where the

620
00:24:00,960 --> 00:24:05,360
foundation comes in it has to develop

621
00:24:03,120 --> 00:24:07,120
train the trainer modules to build up

622
00:24:05,360 --> 00:24:09,760
the skill base

623
00:24:07,120 --> 00:24:11,360
um it's interesting that most of the

624
00:24:09,760 --> 00:24:13,520
contributors we see

625
00:24:11,360 --> 00:24:15,120
for seo for open source contributors

626
00:24:13,520 --> 00:24:17,760
seem to be doing that as part of their

627
00:24:15,120 --> 00:24:19,679
job it's hard to say for sure but i i

628
00:24:17,760 --> 00:24:22,159
estimate about three quarters of the

629
00:24:19,679 --> 00:24:24,240
active contributors

630
00:24:22,159 --> 00:24:26,799
this sort of is a

631
00:24:24,240 --> 00:24:29,600
look at community grade growth look

632
00:24:26,799 --> 00:24:32,080
based on number of pool requests

633
00:24:29,600 --> 00:24:34,720
over the past few years and you can see

634
00:24:32,080 --> 00:24:36,640
that over the past year the number of

635
00:24:34,720 --> 00:24:38,320
pool requests really went up a lot this

636
00:24:36,640 --> 00:24:41,840
is a bit misleading

637
00:24:38,320 --> 00:24:43,039
because prior to april last year

638
00:24:41,840 --> 00:24:44,880
the ts

639
00:24:43,039 --> 00:24:46,720
internal development happened on an

640
00:24:44,880 --> 00:24:48,880
internal bug bit bucket and then got

641
00:24:46,720 --> 00:24:49,760
pushed out as a release onto the public

642
00:24:48,880 --> 00:24:52,240
source

643
00:24:49,760 --> 00:24:54,720
we moved to completely open development

644
00:24:52,240 --> 00:24:56,720
model in april 21 just before cyril

645
00:24:54,720 --> 00:24:58,480
abandoned us

646
00:24:56,720 --> 00:25:00,720
the green bits are the

647
00:24:58,480 --> 00:25:02,720
ts contributions they are actually going

648
00:25:00,720 --> 00:25:05,120
down this is because we lost a lot of

649
00:25:02,720 --> 00:25:07,279
the skilled people as you see and so

650
00:25:05,120 --> 00:25:08,960
it's make being made up by the yellow

651
00:25:07,279 --> 00:25:11,200
bits which are our former people

652
00:25:08,960 --> 00:25:13,760
contributing from their industry jobs

653
00:25:11,200 --> 00:25:16,480
but also significant rise in

654
00:25:13,760 --> 00:25:19,919
contributions from outsiders or people

655
00:25:16,480 --> 00:25:22,159
who are not ts or former ts

656
00:25:19,919 --> 00:25:24,799
and you can see that they now really

657
00:25:22,159 --> 00:25:26,400
dominate the poor requests

658
00:25:24,799 --> 00:25:29,120
this is also seen in the number of

659
00:25:26,400 --> 00:25:30,960
people are not quite as extreme

660
00:25:29,120 --> 00:25:33,600
the number of people submitting pull

661
00:25:30,960 --> 00:25:36,320
requests each month you can see the blue

662
00:25:33,600 --> 00:25:39,600
bar which is the externals are now very

663
00:25:36,320 --> 00:25:41,440
visible much more than so in the past

664
00:25:39,600 --> 00:25:43,600
you may wonder why the total number of

665
00:25:41,440 --> 00:25:46,080
pull requests is not that big it's only

666
00:25:43,600 --> 00:25:47,200
about of the order of a dozen or so a

667
00:25:46,080 --> 00:25:48,880
month

668
00:25:47,200 --> 00:25:49,760
this has a lot to do

669
00:25:48,880 --> 00:25:52,400
with

670
00:25:49,760 --> 00:25:54,240
seo for itself and how it works so

671
00:25:52,400 --> 00:25:56,480
remember it's this verified high

672
00:25:54,240 --> 00:25:59,200
performance microcurrent lens about code

673
00:25:56,480 --> 00:26:00,960
size only about 10 to 15 000 lines of

674
00:25:59,200 --> 00:26:03,039
code

675
00:26:00,960 --> 00:26:04,960
in order to keep it that keep it high

676
00:26:03,039 --> 00:26:07,919
performance verifiable it needs to be

677
00:26:04,960 --> 00:26:09,440
built on very strong design principles

678
00:26:07,919 --> 00:26:10,640
which need to be understood by a

679
00:26:09,440 --> 00:26:12,720
contributor

680
00:26:10,640 --> 00:26:14,520
and the contributors also need to

681
00:26:12,720 --> 00:26:16,960
understand the verification

682
00:26:14,520 --> 00:26:19,440
practicabilities not any code that works

683
00:26:16,960 --> 00:26:20,640
is verifiable and you need to know what

684
00:26:19,440 --> 00:26:22,480
code

685
00:26:20,640 --> 00:26:24,400
can be verified and this is really

686
00:26:22,480 --> 00:26:25,520
tricky in terms of scaling up the

687
00:26:24,400 --> 00:26:27,360
community

688
00:26:25,520 --> 00:26:29,600
in the past the strength of the group

689
00:26:27,360 --> 00:26:31,440
was that they developed the systems

690
00:26:29,600 --> 00:26:33,840
developer kernel developers and the

691
00:26:31,440 --> 00:26:36,640
verifiers were sitting close together

692
00:26:33,840 --> 00:26:39,679
and there was lots of information flow

693
00:26:36,640 --> 00:26:42,240
between them now that they are mostly

694
00:26:39,679 --> 00:26:44,320
out in different organizations this is

695
00:26:42,240 --> 00:26:47,200
much harder to maintain

696
00:26:44,320 --> 00:26:48,240
obviously corvette forced us to do this

697
00:26:47,200 --> 00:26:50,400
anyway

698
00:26:48,240 --> 00:26:52,320
but it was very observable that the

699
00:26:50,400 --> 00:26:54,320
speed of development really slowed down

700
00:26:52,320 --> 00:26:56,400
because there wasn't less communication

701
00:26:54,320 --> 00:26:58,400
even before the split

702
00:26:56,400 --> 00:27:00,640
so this is one of the challenges we are

703
00:26:58,400 --> 00:27:02,400
facing is to keep this

704
00:27:00,640 --> 00:27:04,320
because most people have one skill or

705
00:27:02,400 --> 00:27:06,480
the other they are either experienced

706
00:27:04,320 --> 00:27:09,039
kernel developers or the verification

707
00:27:06,480 --> 00:27:11,360
people only very a handful of people

708
00:27:09,039 --> 00:27:14,480
really understands both sides well

709
00:27:11,360 --> 00:27:17,039
and to keep on the development

710
00:27:14,480 --> 00:27:19,600
with the these few people understanding

711
00:27:17,039 --> 00:27:23,039
both sides that scattered around the

712
00:27:19,600 --> 00:27:25,760
world and different companies etc is a

713
00:27:23,039 --> 00:27:27,600
practical challenge fortunately

714
00:27:25,760 --> 00:27:29,919
it's not such a big challenge because

715
00:27:27,600 --> 00:27:32,080
we're not doing that much more work on

716
00:27:29,919 --> 00:27:34,159
the kernel itself and that probably

717
00:27:32,080 --> 00:27:36,720
makes it doable

718
00:27:34,159 --> 00:27:39,039
another interesting stats is to look at

719
00:27:36,720 --> 00:27:41,360
the success rate of these external pull

720
00:27:39,039 --> 00:27:43,279
requests so people pull requests from

721
00:27:41,360 --> 00:27:45,440
people who are neither

722
00:27:43,279 --> 00:27:46,320
current nor former trustworthy systems

723
00:27:45,440 --> 00:27:49,200
people

724
00:27:46,320 --> 00:27:51,360
green are poor requests from those

725
00:27:49,200 --> 00:27:53,200
people that are merged or at least

726
00:27:51,360 --> 00:27:55,760
approved for merger

727
00:27:53,200 --> 00:27:57,919
and the red is the ones that are

728
00:27:55,760 --> 00:27:59,919
basically abandoned closed unmerged and

729
00:27:57,919 --> 00:28:02,480
then there's the open one and you can

730
00:27:59,919 --> 00:28:04,559
see that the success rate of those that

731
00:28:02,480 --> 00:28:07,919
get pushed is actually pretty high

732
00:28:04,559 --> 00:28:10,399
there's a relatively small fraction of

733
00:28:07,919 --> 00:28:12,720
pull requests that get rejected or

734
00:28:10,399 --> 00:28:15,679
overtaken by other developments

735
00:28:12,720 --> 00:28:17,440
so that's that's sort of a good

736
00:28:15,679 --> 00:28:19,600
indication that we can actually make it

737
00:28:17,440 --> 00:28:21,440
happen

738
00:28:19,600 --> 00:28:22,880
right but you need money for doing

739
00:28:21,440 --> 00:28:26,480
anything right so

740
00:28:22,880 --> 00:28:28,720
how are we going with money as i said

741
00:28:26,480 --> 00:28:30,480
my estimate was we need about a quarter

742
00:28:28,720 --> 00:28:33,200
million u.s a year to keep the

743
00:28:30,480 --> 00:28:36,399
foundation running well and we got now

744
00:28:33,200 --> 00:28:39,200
about twice of that in our annual budget

745
00:28:36,399 --> 00:28:40,480
this is what the 22 budget could look

746
00:28:39,200 --> 00:28:42,480
like

747
00:28:40,480 --> 00:28:45,360
it's very indicative because it hasn't

748
00:28:42,480 --> 00:28:47,600
been discussed with the foundation board

749
00:28:45,360 --> 00:28:50,159
it's basically my hunch based on the

750
00:28:47,600 --> 00:28:51,919
discussion we had in september when we

751
00:28:50,159 --> 00:28:53,360
did the last update of the previous

752
00:28:51,919 --> 00:28:56,399
year's budget

753
00:28:53,360 --> 00:28:58,559
and we see that okay there's linux

754
00:28:56,399 --> 00:29:00,559
foundation creams of nine percent

755
00:28:58,559 --> 00:29:02,159
and then we spend more money on linux

756
00:29:00,559 --> 00:29:04,880
foundation services these are mostly

757
00:29:02,159 --> 00:29:07,120
legal services for trademark etc

758
00:29:04,880 --> 00:29:09,760
and then we have administrative stuff so

759
00:29:07,120 --> 00:29:10,480
we hired a part-time ceo who is one of

760
00:29:09,760 --> 00:29:12,399
the

761
00:29:10,480 --> 00:29:15,520
core verifiers

762
00:29:12,399 --> 00:29:17,360
to an andronic and a um

763
00:29:15,520 --> 00:29:18,720
support staff for helping us manage

764
00:29:17,360 --> 00:29:21,600
activities

765
00:29:18,720 --> 00:29:23,360
and so these together make up about 20

766
00:29:21,600 --> 00:29:26,080
of the overall budget

767
00:29:23,360 --> 00:29:29,760
and then there's some sysadmin at

768
00:29:26,080 --> 00:29:32,080
unsw to keep the continuous integration

769
00:29:29,760 --> 00:29:36,559
infrastructure running that's all the

770
00:29:32,080 --> 00:29:38,640
stuff i take to unisw i keep i try very

771
00:29:36,559 --> 00:29:40,720
hard to not take foundation money as

772
00:29:38,640 --> 00:29:43,760
much as possible because i want to keep

773
00:29:40,720 --> 00:29:46,320
stay independent as the chairman

774
00:29:43,760 --> 00:29:49,919
so we we have this setup here and this

775
00:29:46,320 --> 00:29:51,840
is funding a fraction of a sysadmin to

776
00:29:49,919 --> 00:29:54,000
keep everything running and then the

777
00:29:51,840 --> 00:29:56,640
rest is really for benefiting the

778
00:29:54,000 --> 00:29:58,159
technology so the plan is to spend a

779
00:29:56,640 --> 00:30:00,159
fair amount of money in community

780
00:29:58,159 --> 00:30:02,000
support so basically people whose job is

781
00:30:00,159 --> 00:30:04,320
to help other people

782
00:30:02,000 --> 00:30:06,159
contribute to seo for

783
00:30:04,320 --> 00:30:08,240
and

784
00:30:06,159 --> 00:30:10,880
actually development and this is mostly

785
00:30:08,240 --> 00:30:13,200
seed funding so

786
00:30:10,880 --> 00:30:16,399
projects we kick off with foundation

787
00:30:13,200 --> 00:30:18,159
money in the expectation to draw in

788
00:30:16,399 --> 00:30:20,000
industry funds and that seems to be

789
00:30:18,159 --> 00:30:21,600
working

790
00:30:20,000 --> 00:30:25,360
but this is only a small part of the

791
00:30:21,600 --> 00:30:27,919
story so of the old budget i see going

792
00:30:25,360 --> 00:30:31,840
into the seo four ecosystem

793
00:30:27,919 --> 00:30:34,720
um the foundation is about four percent

794
00:30:31,840 --> 00:30:38,080
money i get directly into unis w to

795
00:30:34,720 --> 00:30:40,159
mostly fund research is is way higher

796
00:30:38,080 --> 00:30:42,159
and then the really exciting development

797
00:30:40,159 --> 00:30:43,760
of an emerging industry consortium to

798
00:30:42,159 --> 00:30:47,120
build a secure

799
00:30:43,760 --> 00:30:49,840
seo4 based operating system open source

800
00:30:47,120 --> 00:30:51,840
for the automotive industry is way

801
00:30:49,840 --> 00:30:54,480
bigger we're talking about a digit u.s

802
00:30:51,840 --> 00:30:54,480
dollar budget

803
00:30:54,720 --> 00:30:59,120
and so what about the community well

804
00:30:57,600 --> 00:31:02,080
we certainly learned

805
00:30:59,120 --> 00:31:03,600
something we knew before

806
00:31:02,080 --> 00:31:05,600
so we can't say we learned it the hard

807
00:31:03,600 --> 00:31:07,760
way but we got it reinforced the hard

808
00:31:05,600 --> 00:31:09,600
way that depending on one particular

809
00:31:07,760 --> 00:31:11,360
organization is really dangerous and

810
00:31:09,600 --> 00:31:13,440
that was from the beginning the main

811
00:31:11,360 --> 00:31:14,880
foundation motivation for setting up the

812
00:31:13,440 --> 00:31:16,640
foundation

813
00:31:14,880 --> 00:31:19,279
but it needs to be complemented by

814
00:31:16,640 --> 00:31:20,320
broadening developer based we cannot

815
00:31:19,279 --> 00:31:22,320
keep

816
00:31:20,320 --> 00:31:24,399
supporting this ecosystem with the team

817
00:31:22,320 --> 00:31:26,720
we have at unisw we need to develop the

818
00:31:24,399 --> 00:31:29,039
scale support based

819
00:31:26,720 --> 00:31:31,039
we still have now the depends on unisw

820
00:31:29,039 --> 00:31:33,519
but that's much more benign because

821
00:31:31,039 --> 00:31:36,640
money i bring into unisw i control

822
00:31:33,519 --> 00:31:38,080
there's no management that talks into

823
00:31:36,640 --> 00:31:40,880
tells me what to do

824
00:31:38,080 --> 00:31:43,200
that's very different from csiro

825
00:31:40,880 --> 00:31:45,440
but the really good takeaway was that

826
00:31:43,200 --> 00:31:47,120
seo4 has now become critically important

827
00:31:45,440 --> 00:31:48,799
for many organizations and this is

828
00:31:47,120 --> 00:31:50,159
industry as well as government and they

829
00:31:48,799 --> 00:31:51,279
are putting money on the table to

830
00:31:50,159 --> 00:31:53,120
support it

831
00:31:51,279 --> 00:31:55,200
there's going to be some exciting

832
00:31:53,120 --> 00:31:57,919
announcements coming very soon for very

833
00:31:55,200 --> 00:32:00,880
significant money flowing into the seo

834
00:31:57,919 --> 00:32:02,159
four ecosystem either directly to unisw

835
00:32:00,880 --> 00:32:04,880
or

836
00:32:02,159 --> 00:32:07,039
industry consortia or the the proofcraft

837
00:32:04,880 --> 00:32:09,519
company that's been spun out for during

838
00:32:07,039 --> 00:32:11,039
verification

839
00:32:09,519 --> 00:32:13,039
and

840
00:32:11,039 --> 00:32:14,799
communication as we all know is

841
00:32:13,039 --> 00:32:17,039
important but it's actually tricky so

842
00:32:14,799 --> 00:32:19,600
when the split happened with csiro we

843
00:32:17,039 --> 00:32:21,600
really agonized on how

844
00:32:19,600 --> 00:32:22,399
how do we talk about this

845
00:32:21,600 --> 00:32:24,399
um

846
00:32:22,399 --> 00:32:26,640
it's very easy to create a smell of

847
00:32:24,399 --> 00:32:28,960
death which has people run away

848
00:32:26,640 --> 00:32:31,039
on the other side we needed to be honest

849
00:32:28,960 --> 00:32:32,240
and open about what's happening

850
00:32:31,039 --> 00:32:33,600
and um

851
00:32:32,240 --> 00:32:35,840
we weren't really sure whether the

852
00:32:33,600 --> 00:32:38,320
communication we're putting out of what

853
00:32:35,840 --> 00:32:40,720
you can do to help now was the right one

854
00:32:38,320 --> 00:32:42,559
um it may or may not have been but it

855
00:32:40,720 --> 00:32:43,919
worked we got people

856
00:32:42,559 --> 00:32:46,000
jumping on

857
00:32:43,919 --> 00:32:48,320
immediately within two months we had

858
00:32:46,000 --> 00:32:51,039
this huge increase in membership and the

859
00:32:48,320 --> 00:32:52,799
budget etcetera

860
00:32:51,039 --> 00:32:55,360
and also

861
00:32:52,799 --> 00:32:57,760
unsurprising media presence helps and

862
00:32:55,360 --> 00:32:59,600
this is one of the main factors behind

863
00:32:57,760 --> 00:33:02,640
this strong inflow and really smart

864
00:32:59,600 --> 00:33:04,720
students into the seo 4 team at unisw

865
00:33:02,640 --> 00:33:06,480
seo4 has just been in the media a lot

866
00:33:04,720 --> 00:33:08,480
and students it catches students

867
00:33:06,480 --> 00:33:11,360
attention

868
00:33:08,480 --> 00:33:13,600
so there's definitely now a change of

869
00:33:11,360 --> 00:33:15,440
the approach happening so our old

870
00:33:13,600 --> 00:33:18,640
development model was all around

871
00:33:15,440 --> 00:33:21,200
trustworthy systems we did the research

872
00:33:18,640 --> 00:33:23,919
we then pushed things out into real

873
00:33:21,200 --> 00:33:26,159
world deployment from those deployments

874
00:33:23,919 --> 00:33:28,559
we learned about we gained insights to

875
00:33:26,159 --> 00:33:31,919
drive to further research and this was

876
00:33:28,559 --> 00:33:34,720
mostly funded by public sector funding

877
00:33:31,919 --> 00:33:36,320
and it was a strong focus on the kernel

878
00:33:34,720 --> 00:33:38,559
the new model

879
00:33:36,320 --> 00:33:41,120
still has the same main components but

880
00:33:38,559 --> 00:33:43,519
they work differently so ts research is

881
00:33:41,120 --> 00:33:44,399
still there to drive the state of the

882
00:33:43,519 --> 00:33:47,039
art

883
00:33:44,399 --> 00:33:48,880
development deployment now is basically

884
00:33:47,039 --> 00:33:51,039
industry driven

885
00:33:48,880 --> 00:33:53,600
but we still stay engaged and get the

886
00:33:51,039 --> 00:33:56,960
insights to drive the research

887
00:33:53,600 --> 00:34:00,480
public money still goes in the system

888
00:33:56,960 --> 00:34:01,279
but mostly into the actual research

889
00:34:00,480 --> 00:34:03,679
and

890
00:34:01,279 --> 00:34:05,039
whereas the deployment is really

891
00:34:03,679 --> 00:34:06,720
industry dollars and of course much

892
00:34:05,039 --> 00:34:07,519
bigger dollars

893
00:34:06,720 --> 00:34:10,480
and

894
00:34:07,519 --> 00:34:12,720
the industry deployment is now

895
00:34:10,480 --> 00:34:14,879
focusing on platforms user mode

896
00:34:12,720 --> 00:34:17,679
components tools etc

897
00:34:14,879 --> 00:34:19,520
and the um and the verification of the

898
00:34:17,679 --> 00:34:20,720
remaining kernel bits

899
00:34:19,520 --> 00:34:23,359
whereas

900
00:34:20,720 --> 00:34:27,520
the s t research is also broadening

901
00:34:23,359 --> 00:34:27,520
beyond the kernel into overall systems

902
00:34:28,159 --> 00:34:33,280
so this is where we are now

903
00:34:31,040 --> 00:34:34,960
now what's next

904
00:34:33,280 --> 00:34:37,040
things we have and of course yeah in the

905
00:34:34,960 --> 00:34:38,399
middle sits the foundation to coordinate

906
00:34:37,040 --> 00:34:40,320
everything

907
00:34:38,399 --> 00:34:42,159
so what's coming up

908
00:34:40,320 --> 00:34:44,399
in terms of um

909
00:34:42,159 --> 00:34:47,200
community and deployment

910
00:34:44,399 --> 00:34:49,119
we have the seo 4 foundation that

911
00:34:47,200 --> 00:34:50,480
is responsible for developing the

912
00:34:49,119 --> 00:34:52,480
community

913
00:34:50,480 --> 00:34:54,720
and then as i said we have this industry

914
00:34:52,480 --> 00:34:57,839
consortium working on

915
00:34:54,720 --> 00:34:59,200
building this next generation secure car

916
00:34:57,839 --> 00:35:00,720
os

917
00:34:59,200 --> 00:35:03,680
driven by

918
00:35:00,720 --> 00:35:06,640
electric cars in autonomy and this will

919
00:35:03,680 --> 00:35:09,680
also fund our major outstanding big

920
00:35:06,640 --> 00:35:11,280
ticket verification item 64-bit arm and

921
00:35:09,680 --> 00:35:13,680
multi-core

922
00:35:11,280 --> 00:35:15,599
and the critical bit remains people we

923
00:35:13,680 --> 00:35:17,200
need to scale up the development of the

924
00:35:15,599 --> 00:35:19,520
skills we're doing the best we can at

925
00:35:17,200 --> 00:35:20,400
unsw but that's of course not scaling

926
00:35:19,520 --> 00:35:22,560
enough

927
00:35:20,400 --> 00:35:25,839
working on enticing lost people back but

928
00:35:22,560 --> 00:35:28,000
as i said earlier core is really to

929
00:35:25,839 --> 00:35:30,320
decentralize this

930
00:35:28,000 --> 00:35:32,400
skills development and this is driven by

931
00:35:30,320 --> 00:35:35,440
the foundation with developing training

932
00:35:32,400 --> 00:35:38,800
packages etc

933
00:35:35,440 --> 00:35:41,119
research keeps producing exciting stuff

934
00:35:38,800 --> 00:35:43,200
obviously as always there's a continuum

935
00:35:41,119 --> 00:35:44,800
between applied and really cutting-edge

936
00:35:43,200 --> 00:35:46,880
research

937
00:35:44,800 --> 00:35:48,800
on the more mountain thing we're working

938
00:35:46,880 --> 00:35:51,839
on various performance improvements for

939
00:35:48,800 --> 00:35:53,520
seo for again these are always

940
00:35:51,839 --> 00:35:55,359
tempered by the need to have being able

941
00:35:53,520 --> 00:35:56,720
to verify them

942
00:35:55,359 --> 00:35:59,740
and

943
00:35:56,720 --> 00:36:00,800
then we get into device virtualization

944
00:35:59,740 --> 00:36:02,560
[Music]

945
00:36:00,800 --> 00:36:04,880
verifying mapping from system

946
00:36:02,560 --> 00:36:07,359
specification to the actual code

947
00:36:04,880 --> 00:36:08,560
real-time guarantees verified time

948
00:36:07,359 --> 00:36:11,359
protection i talked about time

949
00:36:08,560 --> 00:36:12,960
protection two years ago the systematic

950
00:36:11,359 --> 00:36:14,880
approach for

951
00:36:12,960 --> 00:36:16,000
preventing microarchitectural timing

952
00:36:14,880 --> 00:36:18,000
channels

953
00:36:16,000 --> 00:36:20,320
provably secure general purpose

954
00:36:18,000 --> 00:36:22,720
operating system

955
00:36:20,320 --> 00:36:24,240
device drivers that are verified

956
00:36:22,720 --> 00:36:26,640
work correctly

957
00:36:24,240 --> 00:36:28,400
and general automation of system

958
00:36:26,640 --> 00:36:30,320
verification

959
00:36:28,400 --> 00:36:31,839
so in summary

960
00:36:30,320 --> 00:36:33,040
we went through this near death

961
00:36:31,839 --> 00:36:35,599
experience

962
00:36:33,040 --> 00:36:38,480
survived thanks to unisw and the general

963
00:36:35,599 --> 00:36:41,119
community support that

964
00:36:38,480 --> 00:36:43,119
saw us through and we're now in a much

965
00:36:41,119 --> 00:36:46,160
stronger position with strong support

966
00:36:43,119 --> 00:36:47,520
both from unisw as well as industry and

967
00:36:46,160 --> 00:36:49,359
governments and you'll see some

968
00:36:47,520 --> 00:36:50,720
announcement about that growing

969
00:36:49,359 --> 00:36:52,400
development base

970
00:36:50,720 --> 00:36:56,000
and strong in

971
00:36:52,400 --> 00:36:58,480
flux of people but we still need to

972
00:36:56,000 --> 00:37:00,160
master the the main challenge of

973
00:36:58,480 --> 00:37:02,800
skill uh

974
00:37:00,160 --> 00:37:04,560
scanning up the skill space so please

975
00:37:02,800 --> 00:37:07,520
join us

976
00:37:04,560 --> 00:37:09,280
and this is a snapshot of the actual seo

977
00:37:07,520 --> 00:37:12,800
4

978
00:37:09,280 --> 00:37:14,560
team as of december

979
00:37:12,800 --> 00:37:17,200
okay thank you gernot

980
00:37:14,560 --> 00:37:19,520
we understand that you don't oh you do

981
00:37:17,200 --> 00:37:20,720
have your camera there now

982
00:37:19,520 --> 00:37:22,880
that's good

983
00:37:20,720 --> 00:37:25,760
so we have a few questions

984
00:37:22,880 --> 00:37:29,320
and we are a little over time so

985
00:37:25,760 --> 00:37:29,320
yeah thanks for watching

986
00:37:30,240 --> 00:37:36,880
first of all have you looked into oxide

987
00:37:32,560 --> 00:37:39,520
computers hubris a rust rtos given its

988
00:37:36,880 --> 00:37:42,320
similar assurance goals how do you feel

989
00:37:39,520 --> 00:37:44,800
about its architecture based on tasks

990
00:37:42,320 --> 00:37:47,200
with a supervisor mode sorry outside the

991
00:37:44,800 --> 00:37:48,160
kernel

992
00:37:47,200 --> 00:37:51,119
yeah

993
00:37:48,160 --> 00:37:53,200
interesting developments um

994
00:37:51,119 --> 00:37:56,079
rust is definitely an interesting space

995
00:37:53,200 --> 00:37:58,560
we looked at it um as well but the main

996
00:37:56,079 --> 00:38:00,960
issue with rust is that hey in a any

997
00:37:58,560 --> 00:38:03,520
rust based os you have a lot of unsafe

998
00:38:00,960 --> 00:38:05,599
code that's outside the rus guarantees

999
00:38:03,520 --> 00:38:07,760
and if you look at it in detail that

1000
00:38:05,599 --> 00:38:09,599
code is not that much smaller than seo

1001
00:38:07,760 --> 00:38:12,400
four so you still have an assurance

1002
00:38:09,599 --> 00:38:13,359
problem and of course on top of that

1003
00:38:12,400 --> 00:38:15,680
rust

1004
00:38:13,359 --> 00:38:18,800
there's been work going on for three or

1005
00:38:15,680 --> 00:38:21,599
five years on just formalizing rust so

1006
00:38:18,800 --> 00:38:25,119
you can actually do verification in rust

1007
00:38:21,599 --> 00:38:27,200
that still hasn't succeeded yet so um i

1008
00:38:25,119 --> 00:38:29,599
i think this will be a while until you

1009
00:38:27,200 --> 00:38:31,599
get a similar assurance level in a rust

1010
00:38:29,599 --> 00:38:33,839
environment i see rust as a really

1011
00:38:31,599 --> 00:38:36,400
useful team for writing

1012
00:38:33,839 --> 00:38:38,320
user level components but again not

1013
00:38:36,400 --> 00:38:40,079
verifiable ones that which is why we're

1014
00:38:38,320 --> 00:38:42,960
looking at other languages which have a

1015
00:38:40,079 --> 00:38:45,520
verification story

1016
00:38:42,960 --> 00:38:48,720
thank you are there any outside code

1017
00:38:45,520 --> 00:38:51,760
contributors to scl4 save from the

1018
00:38:48,720 --> 00:38:53,760
risc-five foundation

1019
00:38:51,760 --> 00:38:55,839
um not from the raise five foundation

1020
00:38:53,760 --> 00:38:58,240
directly but from companies working with

1021
00:38:55,839 --> 00:39:00,400
risk five and so one of the major

1022
00:38:58,240 --> 00:39:02,320
contributors has been hensel cyber who

1023
00:39:00,400 --> 00:39:04,800
are very committed to risk five they

1024
00:39:02,320 --> 00:39:07,040
have their own risk five processor a lot

1025
00:39:04,800 --> 00:39:09,839
of the work happening in the autonomous

1026
00:39:07,040 --> 00:39:11,680
driving space electric car space

1027
00:39:09,839 --> 00:39:14,880
these are companies very strongly

1028
00:39:11,680 --> 00:39:16,640
engaged in risk five so we see as risk

1029
00:39:14,880 --> 00:39:18,720
five being possibly the main

1030
00:39:16,640 --> 00:39:20,480
architecture for seo four in about five

1031
00:39:18,720 --> 00:39:22,960
years time unless i'm get the act

1032
00:39:20,480 --> 00:39:25,200
together and for example funds the

1033
00:39:22,960 --> 00:39:29,040
verification of or contributed to the

1034
00:39:25,200 --> 00:39:31,359
funding of verification of 64-bit uh um

1035
00:39:29,040 --> 00:39:32,800
arm processors oh yeah risk-five there's

1036
00:39:31,359 --> 00:39:34,079
definitely a lot happening there and a

1037
00:39:32,800 --> 00:39:36,240
lot of com

1038
00:39:34,079 --> 00:39:38,560
contributions not coming from risk five

1039
00:39:36,240 --> 00:39:40,720
itself but from people engaged in risk

1040
00:39:38,560 --> 00:39:44,320
five and seo four

1041
00:39:40,720 --> 00:39:47,280
okay uh sel uh four has always seemed

1042
00:39:44,320 --> 00:39:49,440
quite intimidating to me says one user

1043
00:39:47,280 --> 00:39:50,960
uh is there a hello world example i can

1044
00:39:49,440 --> 00:39:53,599
get into

1045
00:39:50,960 --> 00:39:56,160
can i write it on a raspberry pi

1046
00:39:53,599 --> 00:39:58,800
there's actually a tutorial

1047
00:39:56,160 --> 00:40:00,160
so if you go to the risc fi i saw the

1048
00:39:58,800 --> 00:40:02,000
seo four

1049
00:40:00,160 --> 00:40:04,319
dot systems website

1050
00:40:02,000 --> 00:40:06,720
there's tutorials around there that lead

1051
00:40:04,319 --> 00:40:10,240
you through building simple systems

1052
00:40:06,720 --> 00:40:12,400
on seo four

1053
00:40:10,240 --> 00:40:14,560
raspberry pi is a bit tricky because

1054
00:40:12,400 --> 00:40:16,560
it's very poorly documented and it's

1055
00:40:14,560 --> 00:40:18,560
difficult to write drivers and reliable

1056
00:40:16,560 --> 00:40:20,079
platform support etc unfortunately

1057
00:40:18,560 --> 00:40:22,720
because it would be otherwise an

1058
00:40:20,079 --> 00:40:24,640
extremely good platform this is a one

1059
00:40:22,720 --> 00:40:26,240
struggle to have a really a cheap very

1060
00:40:24,640 --> 00:40:29,599
accessible platform that is well

1061
00:40:26,240 --> 00:40:31,760
supported by seo4 i don't um

1062
00:40:29,599 --> 00:40:35,040
at the moment i guess the disablers were

1063
00:40:31,760 --> 00:40:37,920
the last one we had quite support for

1064
00:40:35,040 --> 00:40:40,160
um things are changing and people are

1065
00:40:37,920 --> 00:40:43,760
contributing platform support court and

1066
00:40:40,160 --> 00:40:43,760
obviously we welcome that

1067
00:40:44,000 --> 00:40:49,359
okay are there abstract models for user

1068
00:40:46,560 --> 00:40:50,560
space components

1069
00:40:49,359 --> 00:40:53,280
yes

1070
00:40:50,560 --> 00:40:55,440
there is um i alluded to that very

1071
00:40:53,280 --> 00:40:58,000
briefly so there's this camcas framework

1072
00:40:55,440 --> 00:41:00,560
which allows you which has a formal

1073
00:40:58,000 --> 00:41:03,359
specification language for a system

1074
00:41:00,560 --> 00:41:04,960
composed of components and connections

1075
00:41:03,359 --> 00:41:07,760
and we are

1076
00:41:04,960 --> 00:41:10,240
doing something similar for the the new

1077
00:41:07,760 --> 00:41:13,359
environment called the core platform um

1078
00:41:10,240 --> 00:41:16,240
and they have a mapping from this

1079
00:41:13,359 --> 00:41:18,160
system spec down to seo four that

1080
00:41:16,240 --> 00:41:21,200
mapping is partially verified not

1081
00:41:18,160 --> 00:41:21,480
completely but this is ongoing work and

1082
00:41:21,200 --> 00:41:23,040
um

1083
00:41:21,480 --> 00:41:25,839
[Music]

1084
00:41:23,040 --> 00:41:28,319
within a few weeks you'll see a release

1085
00:41:25,839 --> 00:41:29,839
of a verified system initializer which

1086
00:41:28,319 --> 00:41:31,040
is part of this

1087
00:41:29,839 --> 00:41:33,839
very

1088
00:41:31,040 --> 00:41:36,480
verification chain from the system spec

1089
00:41:33,839 --> 00:41:39,280
to the actual seo four based system so

1090
00:41:36,480 --> 00:41:42,960
that the code that boots up the user

1091
00:41:39,280 --> 00:41:45,920
land into what's represented by the the

1092
00:41:42,960 --> 00:41:47,599
high levels architecture spec

1093
00:41:45,920 --> 00:41:50,319
okay

1094
00:41:47,599 --> 00:41:52,960
sel4 has proven its worth and its

1095
00:41:50,319 --> 00:41:55,680
success what does this say about

1096
00:41:52,960 --> 00:41:59,040
australia's innovation ecosystem that's

1097
00:41:55,680 --> 00:41:59,040
cyro carved off

1098
00:42:00,319 --> 00:42:03,920
i can't think of any polite way of

1099
00:42:02,720 --> 00:42:06,319
putting that

1100
00:42:03,920 --> 00:42:08,720
okay good so next question

1101
00:42:06,319 --> 00:42:10,800
uh to what extent can verification aid

1102
00:42:08,720 --> 00:42:13,440
in the present day in the presence of a

1103
00:42:10,800 --> 00:42:14,319
router in hardware

1104
00:42:13,440 --> 00:42:16,720
yeah

1105
00:42:14,319 --> 00:42:18,160
hardware bugs are the thing that keeps

1106
00:42:16,720 --> 00:42:20,400
me

1107
00:42:18,160 --> 00:42:21,839
awake at night not only hardware bugs

1108
00:42:20,400 --> 00:42:24,400
but actually

1109
00:42:21,839 --> 00:42:27,040
hardware trojans that are maliciously

1110
00:42:24,400 --> 00:42:29,280
grounded there

1111
00:42:27,040 --> 00:42:31,359
disclosure i'm the chief scientist

1112
00:42:29,280 --> 00:42:35,200
software for henshaw cyborg but they

1113
00:42:31,359 --> 00:42:37,440
built a risk 5 chip with a

1114
00:42:35,200 --> 00:42:40,640
supply chain

1115
00:42:37,440 --> 00:42:42,800
security story using logic encryption

1116
00:42:40,640 --> 00:42:44,800
where they basically

1117
00:42:42,800 --> 00:42:46,560
in a cryptographically secure way

1118
00:42:44,800 --> 00:42:48,880
obfuscate the circuit so you can't

1119
00:42:46,560 --> 00:42:51,520
easily reverse engineer it and slip the

1120
00:42:48,880 --> 00:42:53,359
trojan in in production

1121
00:42:51,520 --> 00:42:56,000
that's part of the story there's still

1122
00:42:53,359 --> 00:42:57,839
the bug story in the end

1123
00:42:56,000 --> 00:42:59,200
verification needs to be pushed down

1124
00:42:57,839 --> 00:43:01,520
into the hardware designs and there's

1125
00:42:59,200 --> 00:43:03,760
people working on that and

1126
00:43:01,520 --> 00:43:06,079
given that now risk five and arm both

1127
00:43:03,760 --> 00:43:08,000
have a formal spec of the isa which is

1128
00:43:06,079 --> 00:43:10,319
the master spec

1129
00:43:08,000 --> 00:43:12,400
this is the interface the formalized

1130
00:43:10,319 --> 00:43:15,040
interface between the the kernel and the

1131
00:43:12,400 --> 00:43:17,440
hardware and we can work towards that

1132
00:43:15,040 --> 00:43:19,280
from both sides and then we know that if

1133
00:43:17,440 --> 00:43:20,880
the kernel is verified against that spec

1134
00:43:19,280 --> 00:43:24,000
the hardware is then we have a

1135
00:43:20,880 --> 00:43:26,480
consistent story that goes through

1136
00:43:24,000 --> 00:43:28,319
okay thank you gernot for uh those

1137
00:43:26,480 --> 00:43:30,960
responses and for a wonderful

1138
00:43:28,319 --> 00:43:32,720
presentation apologies to all for

1139
00:43:30,960 --> 00:43:35,520
running over time

1140
00:43:32,720 --> 00:43:38,560
uh yeah apologies for this network

1141
00:43:35,520 --> 00:43:40,960
i'm not sure what happened there

1142
00:43:38,560 --> 00:43:42,880
thank you all right

1143
00:43:40,960 --> 00:43:46,520
thanks for your interest how many people

1144
00:43:42,880 --> 00:43:46,520
were here by the way