1
00:00:00,270 --> 00:00:03,120
- Um coming up next,
we've got a talk on Ada.

2
00:00:03,120 --> 00:00:05,790
It's Exploitation in the
Era of format Verification:

3
00:00:05,790 --> 00:00:08,250
A Peek at a New Frontier
with AdaCore Spark.

4
00:00:08,250 --> 00:00:11,509
So please help me welcome
to the stage Alex and Adam.

5
00:00:11,509 --> 00:00:14,676
(audience applauding)

6
00:00:19,928 --> 00:00:21,090
- Hello, everyone,

7
00:00:21,090 --> 00:00:22,828
and welcome to the presentation,

8
00:00:22,828 --> 00:00:25,637
Exploitation in the Era
of format Verification:

9
00:00:25,637 --> 00:00:28,320
A Peek at a New Frontier
with AdaCore Spark.

10
00:00:28,320 --> 00:00:30,637
Some folks already approach us and ask,

11
00:00:30,637 --> 00:00:32,670
"What is this picture here?"

12
00:00:32,670 --> 00:00:35,190
What you can see, the
answer is pretty dumb

13
00:00:35,190 --> 00:00:36,930
because there is no logic behind that.

14
00:00:36,930 --> 00:00:38,850
You just kind of visualization that,

15
00:00:38,850 --> 00:00:42,240
in any kind of the software,
you might have a wrong path,

16
00:00:42,240 --> 00:00:43,728
correct path, failed path.

17
00:00:43,728 --> 00:00:45,660
And some of the path are just correctly,

18
00:00:45,660 --> 00:00:46,800
could be correctly verified.

19
00:00:46,800 --> 00:00:49,890
Some of the path is just
wrong or undefined behavior.

20
00:00:49,890 --> 00:00:50,850
This picture looks cool.

21
00:00:50,850 --> 00:00:52,140
That's why we decided to use it,

22
00:00:52,140 --> 00:00:54,660
but don't find any meanings
here because there is not.

23
00:00:54,660 --> 00:00:57,160
If you find, let me know,
I'll be happy to listen.

24
00:00:58,260 --> 00:01:01,440
So I don't wanna spend too
much time on this slide.

25
00:01:01,440 --> 00:01:05,190
My name is Adam Zabrocki,
and together with Alex,

26
00:01:05,190 --> 00:01:07,860
we have been doing some
security research for some time

27
00:01:07,860 --> 00:01:10,380
already for a few decades, to be honest.

28
00:01:10,380 --> 00:01:13,590
And yeah, there is some
private contact to us,

29
00:01:13,590 --> 00:01:15,150
some short bio to us.

30
00:01:15,150 --> 00:01:18,390
And this research has been
done during our work at Nvidia.

31
00:01:18,390 --> 00:01:20,910
Both of us works at Nvidia currently.

32
00:01:20,910 --> 00:01:24,600
So yes, apparently this research
which are going to present,

33
00:01:24,600 --> 00:01:27,990
it's not only the results
of both of our work,

34
00:01:27,990 --> 00:01:29,940
but entire offensive
security research team,

35
00:01:29,940 --> 00:01:31,500
which I'm currently leading.

36
00:01:31,500 --> 00:01:34,890
And big kudos also to
Jared, Max, and Nikola,

37
00:01:34,890 --> 00:01:37,563
which also are involved in this research.

38
00:01:38,610 --> 00:01:41,880
And before we also move to the
format verification problem,

39
00:01:41,880 --> 00:01:42,930
especially in the software,

40
00:01:42,930 --> 00:01:45,690
we need to speak a bit more
about software vulnerabilities,

41
00:01:45,690 --> 00:01:47,850
because this is what the
format verified methods

42
00:01:47,850 --> 00:01:48,930
supposed to address.

43
00:01:48,930 --> 00:01:51,279
And you cannot speak about the format

44
00:01:51,279 --> 00:01:52,560
software vulnerabilities

45
00:01:52,560 --> 00:01:55,080
without touching the
problem of memory safety.

46
00:01:55,080 --> 00:01:57,240
So just quick intro about memory safety,

47
00:01:57,240 --> 00:01:58,350
what is memory safety?

48
00:01:58,350 --> 00:02:00,960
It's apparently a term
used by security engineers

49
00:02:00,960 --> 00:02:02,730
to describe a state of being protected

50
00:02:02,730 --> 00:02:06,188
from various bugs
related to memory access.

51
00:02:06,188 --> 00:02:08,400
And of course there's a bunch of bugs

52
00:02:08,400 --> 00:02:09,750
who falls into this category,

53
00:02:09,750 --> 00:02:11,730
including every type of overflow,

54
00:02:11,730 --> 00:02:14,280
some memory like on the stack,
on the heap, on the global,

55
00:02:14,280 --> 00:02:16,230
every piece of the memory,
which can be overflowed,

56
00:02:16,230 --> 00:02:18,420
any kind of out-of-bound read and write,

57
00:02:18,420 --> 00:02:20,757
an invalid page, including
null pointer de-reference,

58
00:02:20,757 --> 00:02:23,160
any kind of use after
free, use after return,

59
00:02:23,160 --> 00:02:24,810
use after scope, et cetera.

60
00:02:24,810 --> 00:02:27,000
There is many types of use after bugs.

61
00:02:27,000 --> 00:02:30,570
Also, any time of unused
memory, including wild pointers,

62
00:02:30,570 --> 00:02:33,090
or memory leaks, invalid
free, all of that,

63
00:02:33,090 --> 00:02:34,470
it's a memory safety issue.

64
00:02:34,470 --> 00:02:36,270
But not all of the
security vulnerabilities

65
00:02:36,270 --> 00:02:37,920
are memory safety issues.

66
00:02:37,920 --> 00:02:40,200
So some of them like any
type of the overflows,

67
00:02:40,200 --> 00:02:42,480
integer overflows, automatic overflows,

68
00:02:42,480 --> 00:02:44,359
are not memory safety issues.

69
00:02:44,359 --> 00:02:47,880
Logical issues is also
not memory safety issue,

70
00:02:47,880 --> 00:02:48,713
error handling, race conditions.

71
00:02:48,713 --> 00:02:52,140
There is a star because race
condition and data access

72
00:02:52,140 --> 00:02:53,820
is type of the memory safety issue,

73
00:02:53,820 --> 00:02:55,560
but in general, it's not.

74
00:02:55,560 --> 00:02:57,900
And there's a few more, but
what is worth to mention that

75
00:02:57,900 --> 00:03:00,210
even this is not a memory safety issues,

76
00:03:00,210 --> 00:03:02,850
they often result in a
memory safety issues.

77
00:03:02,850 --> 00:03:06,420
So if you have any kind of
integer overflow on the size

78
00:03:06,420 --> 00:03:07,770
of how much data you wanna copy,

79
00:03:07,770 --> 00:03:08,603
it's not memory safety issues,

80
00:03:08,603 --> 00:03:10,563
but when it starts to copy the data,

81
00:03:12,000 --> 00:03:14,073
then you will have a memory safety issue.

82
00:03:15,000 --> 00:03:16,980
So, why even speak about memory safety?

83
00:03:16,980 --> 00:03:19,800
Because apparently memory
safety errors are today

84
00:03:19,800 --> 00:03:21,150
the biggest attack surface.

85
00:03:21,150 --> 00:03:21,990
And I really mean it,

86
00:03:21,990 --> 00:03:24,750
it's the biggest software
type of the bugs.

87
00:03:24,750 --> 00:03:26,400
And there's a few reasons behind that.

88
00:03:26,400 --> 00:03:29,160
Some of them are easy
to spot like this one,

89
00:03:29,160 --> 00:03:31,331
memory-and safe language
has been chosen to use,

90
00:03:31,331 --> 00:03:33,720
to develop a core of the
execution environment,

91
00:03:33,720 --> 00:03:36,360
so every type of the operating system like

92
00:03:36,360 --> 00:03:37,710
Windows, Linux, Macintosh,

93
00:03:37,710 --> 00:03:40,830
are within in memory-and
safe languages like C/C++.

94
00:03:40,830 --> 00:03:42,360
And the question is, why?

95
00:03:42,360 --> 00:03:43,230
Because at that time,

96
00:03:43,230 --> 00:03:45,330
when this ecosystem has been developed,

97
00:03:45,330 --> 00:03:46,920
we already have memory-safe language,

98
00:03:46,920 --> 00:03:49,830
which could give us opportunity
to not have these bugs

99
00:03:49,830 --> 00:03:52,620
but we still developed them
in the memory-safe language.

100
00:03:52,620 --> 00:03:54,090
There's a few reasons behind that.

101
00:03:54,090 --> 00:03:56,070
Some of them is because at that time

102
00:03:56,070 --> 00:03:58,560
the hardware was not
performed as well as today.

103
00:03:58,560 --> 00:03:59,700
That was much slower,

104
00:03:59,700 --> 00:04:02,490
and the code in the memory-and
safe language was faster.

105
00:04:02,490 --> 00:04:04,680
And also it gives
developers for fine-grained

106
00:04:04,680 --> 00:04:06,080
control over the memory address

107
00:04:06,080 --> 00:04:08,550
where the code can be
executed with the attributes.

108
00:04:08,550 --> 00:04:11,670
And this is one of the reasons
why memory safe was chosen

109
00:04:11,670 --> 00:04:13,200
to develop these ecosystems.

110
00:04:13,200 --> 00:04:15,150
Also memory safety bugs
are very well researched,

111
00:04:15,150 --> 00:04:16,289
as everybody knows.

112
00:04:16,289 --> 00:04:18,960
Some professional exploiters even develop

113
00:04:18,960 --> 00:04:20,610
the exploitation framework

114
00:04:20,610 --> 00:04:22,410
to targeting specific software stack.

115
00:04:22,410 --> 00:04:24,990
I seen by myself, reverse
engineers, one of the framework

116
00:04:24,990 --> 00:04:27,780
developed to exploit to
Windows kernel vulnerabilities.

117
00:04:27,780 --> 00:04:28,890
You have a full framework.

118
00:04:28,890 --> 00:04:32,121
You just find the bug and
expose primitive like with right

119
00:04:32,121 --> 00:04:34,170
and include into the framework

120
00:04:34,170 --> 00:04:36,480
and entire exploitation
process magically runs.

121
00:04:36,480 --> 00:04:39,540
It bypass ASLR, it bypass
any modern mitigation.

122
00:04:39,540 --> 00:04:41,250
So just find the bug,
plug in the framework,

123
00:04:41,250 --> 00:04:42,750
run and it's done.

124
00:04:42,750 --> 00:04:44,310
So it's a very well researched area.

125
00:04:44,310 --> 00:04:47,220
And additionally, memory
researchers do automation

126
00:04:47,220 --> 00:04:49,710
on focusing for memory
safety bug detection.

127
00:04:49,710 --> 00:04:52,590
They don't even need to
understand what the software does.

128
00:04:52,590 --> 00:04:54,690
You just take an open source project.

129
00:04:54,690 --> 00:04:55,918
You- eh.

130
00:04:55,918 --> 00:04:59,340
compile this with the various
code coverage instrumentation.

131
00:04:59,340 --> 00:05:01,257
Then you spin up cost
coverage even faster,

132
00:05:01,257 --> 00:05:03,930
and you just run it and you have bugs.

133
00:05:03,930 --> 00:05:08,790
And apparently it's kind of
not rare that some researchers,

134
00:05:08,790 --> 00:05:11,040
they just pick up most popular libraries

135
00:05:11,040 --> 00:05:12,780
without going to into details to analyze

136
00:05:12,780 --> 00:05:14,340
what the architecture it is.

137
00:05:14,340 --> 00:05:16,018
We like just find it,
so let's find the bug

138
00:05:16,018 --> 00:05:18,303
and we have benefits, yes?

139
00:05:19,140 --> 00:05:22,009
So it's not also a theory
because a big corporation

140
00:05:22,009 --> 00:05:24,870
starting to struggle with
this problem more and more,

141
00:05:24,870 --> 00:05:26,040
and they can't ignore it anymore.

142
00:05:26,040 --> 00:05:28,740
And they want to study a few cases.

143
00:05:28,740 --> 00:05:31,100
And the biggest corporation
who produce software

144
00:05:31,100 --> 00:05:32,760
is apparently Microsoft.

145
00:05:32,760 --> 00:05:36,240
And they also face this problem for ages

146
00:05:36,240 --> 00:05:38,460
and they make a few
presentation about that,

147
00:05:38,460 --> 00:05:39,360
which I'm gonna recap here.

148
00:05:39,360 --> 00:05:43,346
So in 2002, Microsoft
created something called

149
00:05:43,346 --> 00:05:45,930
"Trustworthy Computing," TWC,

150
00:05:45,930 --> 00:05:49,080
where they wanted to-
they cannot ignore anymore

151
00:05:49,080 --> 00:05:50,670
the security issues in their ecosystem

152
00:05:50,670 --> 00:05:53,520
because larger customers
where government agencies,

153
00:05:53,520 --> 00:05:55,740
financial companies,
starting to be impacted

154
00:05:55,740 --> 00:05:58,080
by the security problems on the Windows,

155
00:05:58,080 --> 00:06:00,510
and this is Microsoft products,
so they cannot ignore it

156
00:06:00,510 --> 00:06:02,850
and they needed to do something on that.

157
00:06:02,850 --> 00:06:03,808
So they created TWC.

158
00:06:03,808 --> 00:06:07,020
They focus on a few areas
and one of them was security,

159
00:06:07,020 --> 00:06:09,870
and as the pillars of this initiative.

160
00:06:09,870 --> 00:06:13,530
And they developed as a
direct implication of that,

161
00:06:13,530 --> 00:06:16,043
a few interesting things
like TWC developed

162
00:06:16,043 --> 00:06:18,083
SDLC, Security Development Lifecycle,

163
00:06:18,083 --> 00:06:21,769
process to be able to make
the quality of the code higher

164
00:06:21,769 --> 00:06:23,130
from the beginning.

165
00:06:23,130 --> 00:06:24,420
They also created MSRC,

166
00:06:24,420 --> 00:06:26,370
which is Microsoft
Security Response Center,

167
00:06:26,370 --> 00:06:29,790
which treated security bugs
differently than another bugs.

168
00:06:29,790 --> 00:06:32,490
So they also know that this
is something which can impact

169
00:06:32,490 --> 00:06:34,020
the security of the ecosystem.

170
00:06:34,020 --> 00:06:35,970
So they also starting
to fast by themselves,

171
00:06:35,970 --> 00:06:38,220
some of the software, they also
starting to do bug hunting.

172
00:06:38,220 --> 00:06:40,140
They also starting to do exploit research.

173
00:06:40,140 --> 00:06:42,643
So they did a lot of interesting stuff.

174
00:06:42,643 --> 00:06:45,600
And traditionally in
2019, they said, "okay,

175
00:06:45,600 --> 00:06:47,160
we spend so much engineered effort.

176
00:06:47,160 --> 00:06:50,220
We spend so much money on
that. Do we see improvements?

177
00:06:50,220 --> 00:06:53,637
Do we see any benefits of
all of that?" And in 2019,

178
00:06:53,637 --> 00:06:58,230
they analyzed last 12 years
of all of the security cases

179
00:06:58,230 --> 00:07:01,200
reported to them. And this what they saw.

180
00:07:01,200 --> 00:07:04,050
So this is slide from Microsoft
itself, as you can see,

181
00:07:04,050 --> 00:07:05,710
and the type of the bugs security bugs,

182
00:07:05,710 --> 00:07:08,550
which are reported to them
are more or less the same over

183
00:07:08,550 --> 00:07:10,380
the time in the 2006,

184
00:07:10,380 --> 00:07:13,230
around 70% of all of the
security issues was memory safety

185
00:07:13,230 --> 00:07:14,063
issues.

186
00:07:14,063 --> 00:07:17,250
In 2018, we still see 70%
of memory safety issues.

187
00:07:17,250 --> 00:07:19,770
So doesn't mean nothing
changes over the time, even,

188
00:07:19,770 --> 00:07:22,140
or even of the CS of investment.

189
00:07:22,140 --> 00:07:25,290
It's not obviously, because
this lights show what changes.

190
00:07:25,290 --> 00:07:27,990
So we see that the type of
the memory safety issues,

191
00:07:27,990 --> 00:07:29,490
which are reported are differently.

192
00:07:29,490 --> 00:07:31,590
So in the beginning 2006,

193
00:07:31,590 --> 00:07:33,960
we see the quarter of the
bugs are stack overflow

194
00:07:33,960 --> 00:07:36,420
vulnerabilities. While in the 2004- 14,

195
00:07:36,420 --> 00:07:38,010
there is almost 0 of them.

196
00:07:38,010 --> 00:07:40,200
And the reason is not
because this bug disappear,

197
00:07:40,200 --> 00:07:42,900
it just doesn't give benefits
for the hacker because the

198
00:07:42,900 --> 00:07:45,300
modern mitigation makes
the exploitation this bug

199
00:07:45,300 --> 00:07:47,550
sometimes impossible or very hard.

200
00:07:47,550 --> 00:07:50,040
But in the same time they
saw the rise of other type of

201
00:07:50,040 --> 00:07:53,730
issues like receptor free.
This is this gray bugs here.

202
00:07:53,730 --> 00:07:56,160
You can see the huge rise of
them because there's no any

203
00:07:56,160 --> 00:07:57,150
mitigation on that.

204
00:07:57,150 --> 00:08:00,030
So it's must to exploit and
then they introduce mitigation

205
00:08:00,030 --> 00:08:02,880
and you can see that the amount
of the bug are shrinking.

206
00:08:02,880 --> 00:08:03,713
And now we can see,

207
00:08:03,713 --> 00:08:05,697
there is a rise on the edge of this area.

208
00:08:05,697 --> 00:08:07,170
You can see the rise of yellow,

209
00:08:07,170 --> 00:08:08,880
which is type of the
confusion because there is no

210
00:08:08,880 --> 00:08:11,130
mitigation. So people move
to that type of the attack.

211
00:08:11,130 --> 00:08:12,060
So something changes,

212
00:08:12,060 --> 00:08:15,750
but overall 70% of the
bug are memory issues.

213
00:08:15,750 --> 00:08:17,400
And Google case,

214
00:08:17,400 --> 00:08:19,800
let's speak about that because
it's slightly different.

215
00:08:19,800 --> 00:08:22,680
They wanted to avoid the problem
which Microsoft had instead

216
00:08:22,680 --> 00:08:26,400
of patching bad software with
adding new security layers,

217
00:08:26,400 --> 00:08:28,230
they wanted to make something differently.

218
00:08:28,230 --> 00:08:31,740
So they designed Google Chrome
in the security in mind,

219
00:08:31,740 --> 00:08:33,570
they have a high code quality.

220
00:08:33,570 --> 00:08:35,760
They constantly fast that since 2015,

221
00:08:35,760 --> 00:08:37,230
because they knew the bugs will be there.

222
00:08:37,230 --> 00:08:39,960
They wanted to catch them in
house as soon as possible.

223
00:08:39,960 --> 00:08:41,790
And you know, Google has power.

224
00:08:41,790 --> 00:08:43,890
So they facet in the various platform.

225
00:08:43,890 --> 00:08:47,310
They use OSS fast platform.
They use Google Cloud platform,

226
00:08:47,310 --> 00:08:49,950
which essentially means they
have essentially unlimited

227
00:08:49,950 --> 00:08:51,150
computer power.

228
00:08:51,150 --> 00:08:53,345
They also have dedicated
team to improve various

229
00:08:53,345 --> 00:08:57,330
mitigation. And in 2020, they
did exactly the same job.

230
00:08:57,330 --> 00:09:00,570
They analyzed all of the
security issues since 2015,

231
00:09:00,570 --> 00:09:01,890
when they starting too fast,

232
00:09:01,890 --> 00:09:05,000
what were reported to them
with the high and critical

233
00:09:05,000 --> 00:09:06,813
severity. And guess what happened?

234
00:09:08,190 --> 00:09:10,050
They end up in exactly the same place.

235
00:09:10,050 --> 00:09:11,910
Even they took different approach.

236
00:09:11,910 --> 00:09:15,330
Roughly 70% of the bugs
are memory safety issues.

237
00:09:15,330 --> 00:09:18,450
And half of these bugs
are used after feedbacks.

238
00:09:18,450 --> 00:09:20,640
And even more, they knew
that this bugs will be there.

239
00:09:20,640 --> 00:09:23,250
So they designed the Google
Chrome in such a case that this

240
00:09:23,250 --> 00:09:24,083
bugs will be there.

241
00:09:24,083 --> 00:09:26,400
They knew this there's
heavy sent bugs then,

242
00:09:26,400 --> 00:09:29,550
and they make a warranty that
one of the bugs is not enough

243
00:09:29,550 --> 00:09:31,290
to take over of the host machine.

244
00:09:31,290 --> 00:09:33,367
Although this is a quote from the blog,

245
00:09:33,367 --> 00:09:35,970
"but we are reaching the
limits of sandboxing and site

246
00:09:35,970 --> 00:09:36,803
isolation."

247
00:09:36,803 --> 00:09:39,480
And yeah, that's pretty concerning.

248
00:09:39,480 --> 00:09:41,460
And what about open source world?

249
00:09:41,460 --> 00:09:42,600
Is open source world is

250
00:09:42,600 --> 00:09:44,400
different than corporation world?

251
00:09:44,400 --> 00:09:47,100
And there is not many
research in this area.

252
00:09:47,100 --> 00:09:50,730
Although we found one
interesting research done by

253
00:09:50,730 --> 00:09:53,610
Universi-, Technical
University in Germany,

254
00:09:53,610 --> 00:09:55,230
Continental AG and Intel Labs,

255
00:09:55,230 --> 00:09:56,277
which summarize it as

256
00:09:56,277 --> 00:09:58,230
"we find no clear evidence that the

257
00:09:58,230 --> 00:10:00,240
vulnerability rate of
widely used software,

258
00:10:00,240 --> 00:10:02,108
decreases over time:
Even in the popular and

259
00:10:02,108 --> 00:10:04,089
'stable' releases, the fixing of the bug

260
00:10:04,089 --> 00:10:05,948
does not seems to reduce the rate of

261
00:10:05,948 --> 00:10:08,520
newly identified vulnerabilities."

262
00:10:08,520 --> 00:10:11,400
So it's not much better, I guess.

263
00:10:11,400 --> 00:10:13,463
So are we doomed?

264
00:10:13,463 --> 00:10:14,880
Is memory safety something

265
00:10:14,880 --> 00:10:17,250
who will be for- with us forever that we

266
00:10:17,250 --> 00:10:18,630
cannot fix anything.

267
00:10:18,630 --> 00:10:20,574
So apparently no,

268
00:10:20,574 --> 00:10:22,470
people trying to approach this problem

269
00:10:22,470 --> 00:10:23,910
because we understand it much more.

270
00:10:23,910 --> 00:10:27,180
And we have a various ways
how to try to address that.

271
00:10:27,180 --> 00:10:29,220
We have a new mitigation
push to the hardware,

272
00:10:29,220 --> 00:10:30,330
like memory tagging,

273
00:10:30,330 --> 00:10:31,530
who are physically in the hardware

274
00:10:31,530 --> 00:10:34,410
trying to stop the memory safety
issues from being exploited

275
00:10:34,410 --> 00:10:35,673
or even happens before it happens

276
00:10:35,673 --> 00:10:38,730
that first time, that's
the memory tagging idea.

277
00:10:38,730 --> 00:10:42,345
We also have ideas of creating
a new architecture of the

278
00:10:42,345 --> 00:10:44,820
memory like cherry architecture,

279
00:10:44,820 --> 00:10:47,160
cherry architecture
treats differently memory.

280
00:10:47,160 --> 00:10:49,590
So it also will be
redesigned the hardware.

281
00:10:49,590 --> 00:10:51,810
And there is a different
approach, different path,

282
00:10:51,810 --> 00:10:54,960
lesser write all of our software
in the formatly verified

283
00:10:54,960 --> 00:10:58,260
languages or use the language
which has static matter of

284
00:10:58,260 --> 00:11:00,690
proving that the memory
safety doesn't exist.

285
00:11:00,690 --> 00:11:04,020
So we have rust and people
starting to write the program in

286
00:11:04,020 --> 00:11:06,270
the rust, but we have
also the format methods,

287
00:11:06,270 --> 00:11:07,830
which is even stronger.

288
00:11:07,830 --> 00:11:11,280
Which can formatly prove that
there's absence of memory

289
00:11:11,280 --> 00:11:14,310
safety issues. And there is
absence of undefined behavior.

290
00:11:14,310 --> 00:11:17,280
So past format verification,
you must to be safe.

291
00:11:17,280 --> 00:11:19,740
And one of the language, which gives the,

292
00:11:19,740 --> 00:11:21,540
which is the most advanced

293
00:11:21,540 --> 00:11:23,070
of giving the attributes of the format

294
00:11:23,070 --> 00:11:25,890
verified software is apparently
at the core Spark where Alex

295
00:11:25,890 --> 00:11:27,213
will speak more about now.

296
00:11:28,380 --> 00:11:29,730
- Yeah, let's read just a few key points

297
00:11:29,730 --> 00:11:31,330
from our presentation last year.

298
00:11:34,770 --> 00:11:37,285
Spark is a subset of other core language.

299
00:11:37,285 --> 00:11:40,620
It's basically a programming
language, formatly defined,

300
00:11:40,620 --> 00:11:42,750
including a set of analysis tools.

301
00:11:42,750 --> 00:11:44,865
And this- the real strength of this

302
00:11:44,865 --> 00:11:47,460
comes from this analysis tools.

303
00:11:47,460 --> 00:11:50,010
There is a not proven
that stack a few more.

304
00:11:50,010 --> 00:11:54,300
So one of the key features is
that is statically provable,

305
00:11:54,300 --> 00:11:58,800
and the proof is produced
by this grant proof tool.

306
00:11:58,800 --> 00:12:01,530
So you have to run it after
you compile, build your code.

307
00:12:01,530 --> 00:12:02,363
So-

308
00:12:03,720 --> 00:12:06,990
what can you achieve with
this then format proof?

309
00:12:06,990 --> 00:12:10,025
So this tool can prove.

310
00:12:10,025 --> 00:12:13,692
(microphone sound goes out)

311
00:12:42,210 --> 00:12:43,980
- Using this form of verify,

312
00:12:43,980 --> 00:12:46,350
you can prove that certain
dynamic checks cannot fail.

313
00:12:46,350 --> 00:12:48,510
So you can just emit them.

314
00:12:48,510 --> 00:12:51,660
The compiler may emit them
and do not build that may

315
00:12:51,660 --> 00:12:53,730
give you some performance benefits.

316
00:12:53,730 --> 00:12:56,250
Also, it can prove that there
may not be runtime error.

317
00:12:56,250 --> 00:12:58,800
So everything runs in
a well defined state.

318
00:12:58,800 --> 00:13:02,640
You will not have any errors
that raise in run time

319
00:13:02,640 --> 00:13:05,253
and you will have hard
proofs like format verify.

320
00:13:06,660 --> 00:13:11,100
So also AdaCore Spark is memory
safe, language like Rust,

321
00:13:11,100 --> 00:13:14,640
but it also has very strong typing system,

322
00:13:14,640 --> 00:13:16,860
uh- which is much stronger than Rust.

323
00:13:16,860 --> 00:13:19,500
Uh- so for example, you do
not have mathematic overflows,

324
00:13:19,500 --> 00:13:22,470
integer overflow or stuff like that.

325
00:13:22,470 --> 00:13:23,784
And because of this,

326
00:13:23,784 --> 00:13:28,784
it traditionally is used in
industry such as automotive IOT

327
00:13:28,813 --> 00:13:31,143
Spark is safety, safety certified.

328
00:13:32,130 --> 00:13:34,590
So Nvidia constantly used that for build

329
00:13:34,590 --> 00:13:36,556
safety certified code.

330
00:13:36,556 --> 00:13:40,620
So they key points is that
you can build buggy code,

331
00:13:40,620 --> 00:13:42,630
but the problems are
detected by the tools.

332
00:13:42,630 --> 00:13:45,395
You really have to run them to see,

333
00:13:45,395 --> 00:13:49,230
to actually verify that your
code doesn't have any problems

334
00:13:49,230 --> 00:13:50,760
and tools have to go onto each other.

335
00:13:50,760 --> 00:13:53,010
You have to run all these
tools because they detect

336
00:13:53,010 --> 00:13:54,570
different kinds of problems.

337
00:13:54,570 --> 00:13:56,880
So when we first approached
the project Written and Spark,

338
00:13:56,880 --> 00:14:01,380
we thought about this attack
surface that we can use.

339
00:14:01,380 --> 00:14:03,930
So obviously,

340
00:14:03,930 --> 00:14:06,090
no memory corruption
bugs are there anymore

341
00:14:06,090 --> 00:14:08,070
because it is memory safety language.

342
00:14:08,070 --> 00:14:12,120
So also there are no pointers.

343
00:14:12,120 --> 00:14:15,240
And so problems with pointers
do not apply to Spark,

344
00:14:15,240 --> 00:14:18,240
but since 2019 Spark-

345
00:14:18,240 --> 00:14:19,501
has a feature.

346
00:14:19,501 --> 00:14:23,134
So it's introduced the concept
of pointers pretty much like

347
00:14:23,134 --> 00:14:25,230
Rust's borrow checking.

348
00:14:25,230 --> 00:14:26,520
Um

349
00:14:26,520 --> 00:14:27,453
So uh,

350
00:14:29,190 --> 00:14:30,960
what about automatic security?

351
00:14:30,960 --> 00:14:32,910
So we have very strong typing systems.

352
00:14:32,910 --> 00:14:36,120
So that's why automatic
issues also don't apply.

353
00:14:36,120 --> 00:14:37,470
Uh we uh-

354
00:14:37,470 --> 00:14:38,940
Our project was single threaded.

355
00:14:38,940 --> 00:14:40,890
So we didn't care about
parallel execution,

356
00:14:40,890 --> 00:14:42,480
but if you do care about it,

357
00:14:42,480 --> 00:14:45,000
there is extension to
Spark called Raven square.

358
00:14:45,000 --> 00:14:47,400
We- which we can use.

359
00:14:47,400 --> 00:14:51,315
Um- So what is left at a is a tax surface.

360
00:14:51,315 --> 00:14:53,340
These are logic bugs and bad design.

361
00:14:53,340 --> 00:14:55,890
Obviously, if you prove wrong things,

362
00:14:55,890 --> 00:14:59,148
you can have correct proofs
about wrong assumptions and you

363
00:14:59,148 --> 00:15:01,173
will have bugs in this case.

364
00:15:05,550 --> 00:15:06,383
- Um yes.

365
00:15:06,383 --> 00:15:10,410
So everything, what Alex
said, it's compelling,

366
00:15:10,410 --> 00:15:13,740
sounds compelling, apparently (indistinct)

367
00:15:13,740 --> 00:15:16,500
You can have a buggy
code. You just might run,

368
00:15:16,500 --> 00:15:17,580
must run all the tools.

369
00:15:17,580 --> 00:15:18,413
If you don't run them,

370
00:15:18,413 --> 00:15:22,170
you still have the bugs and the
tools are orthogonal itself.

371
00:15:22,170 --> 00:15:25,020
So you must run all of them.
If you just pick some of them,

372
00:15:25,020 --> 00:15:26,460
you'll not have all of these benefits.

373
00:15:26,460 --> 00:15:28,890
And most of the potential
security issues must be in the

374
00:15:28,890 --> 00:15:32,760
design issues or in the logical errors.

375
00:15:32,760 --> 00:15:36,141
And bugs also can be introduced
by the compiler itself,

376
00:15:36,141 --> 00:15:38,970
which we can see later on the slides.

377
00:15:38,970 --> 00:15:42,390
So everything sounds very
compelling and pretty interesting,

378
00:15:42,390 --> 00:15:43,920
but benefits,

379
00:15:43,920 --> 00:15:47,100
do we really see benefits in
the software written in Spark

380
00:15:47,100 --> 00:15:48,540
or any form of verified language

381
00:15:48,540 --> 00:15:52,290
compared to non-Spark code
in memory safe language?

382
00:15:52,290 --> 00:15:54,870
And apparently before we do go there,

383
00:15:54,870 --> 00:15:58,050
I just wanna quickly said that
what our team does because we

384
00:15:58,050 --> 00:16:00,360
did this evaluation. So
just to give you overview,

385
00:16:00,360 --> 00:16:03,600
why we think we are the good
guys to do this corporation.

386
00:16:03,600 --> 00:16:06,090
We essentially work as a third
party company inside of the

387
00:16:06,090 --> 00:16:06,923
company.

388
00:16:06,923 --> 00:16:09,030
We just take a product after
the pass of the check bugs.

389
00:16:09,030 --> 00:16:10,800
And they said, okay, ship it it's secure.

390
00:16:10,800 --> 00:16:12,450
Then we said, no, don't ship it.

391
00:16:12,450 --> 00:16:13,380
Let's review something,

392
00:16:13,380 --> 00:16:15,270
which is the most critical
and can impact component.

393
00:16:15,270 --> 00:16:16,410
So that's what we do.

394
00:16:16,410 --> 00:16:19,020
And so we, since 2020,

395
00:16:19,020 --> 00:16:23,520
we analyzed 17 very high
product impact product.

396
00:16:23,520 --> 00:16:26,220
So which it's not a small
venture, it's a huge product.

397
00:16:26,220 --> 00:16:29,036
And 10 of them used a software written

398
00:16:29,036 --> 00:16:30,540
in memory and safe language.

399
00:16:30,540 --> 00:16:33,090
And four of them had a
software written in Spark.

400
00:16:33,090 --> 00:16:37,140
And what is important that
four of this project was fully

401
00:16:37,140 --> 00:16:37,973
written in Spark.

402
00:16:37,973 --> 00:16:40,407
There was not even single line
of code written in the non

403
00:16:40,407 --> 00:16:42,660
formatly verified language.

404
00:16:42,660 --> 00:16:46,440
And two of them was written
in Spark and the Spark was the

405
00:16:46,440 --> 00:16:51,440
like imposer and enforcer of
the security warranties of the

406
00:16:51,900 --> 00:16:55,410
software while inside they
could be still software written

407
00:16:55,410 --> 00:16:56,700
in the memory and safe language,

408
00:16:56,700 --> 00:17:00,930
but they didn't change the
security of the entire ecosystem.

409
00:17:00,930 --> 00:17:02,580
So it's fine to have it there.

410
00:17:02,580 --> 00:17:05,850
So we get a closer look on
them and we wanted to compare,

411
00:17:05,850 --> 00:17:07,920
do we really see the benefits?

412
00:17:07,920 --> 00:17:09,840
And so first question,
how do we compare them?

413
00:17:09,840 --> 00:17:12,180
How do you compare them as some
apple, to apple, not apple,

414
00:17:12,180 --> 00:17:15,540
to anything else and have some
kind of bad impression about

415
00:17:15,540 --> 00:17:17,790
the quality of that. So it's difficult.

416
00:17:17,790 --> 00:17:18,623
So what we did,

417
00:17:18,623 --> 00:17:20,160
we just-

418
00:17:20,160 --> 00:17:22,320
we just put the raw data
of all of the project,

419
00:17:22,320 --> 00:17:23,790
which we reviewed.

420
00:17:23,790 --> 00:17:26,160
We choose the one which could be compared.

421
00:17:26,160 --> 00:17:28,470
We start them out by the
timeframe of the review,

422
00:17:28,470 --> 00:17:31,050
which we spent analyzing the software.

423
00:17:31,050 --> 00:17:34,890
We also put, what is
the total backgrounds?

424
00:17:34,890 --> 00:17:36,810
What is the percentage of
the memory safety issue

425
00:17:36,810 --> 00:17:39,300
and what is the type of the
software which we review?

426
00:17:39,300 --> 00:17:40,530
And by sorting by the type,

427
00:17:40,530 --> 00:17:43,410
we could be able somehow to
compare because if the type of

428
00:17:43,410 --> 00:17:46,200
the software is the same,
we can more or less compare,

429
00:17:46,200 --> 00:17:48,690
how do they behave with the
format verified language?

430
00:17:48,690 --> 00:17:52,526
So first project in Spark
could be also not could do,

431
00:17:52,526 --> 00:17:56,400
does not apply to this corporation
because it's focused on

432
00:17:56,400 --> 00:17:59,070
the harder modeling and we have
nothing in the memory, safe,

433
00:17:59,070 --> 00:18:00,480
and safe language to compare with it.

434
00:18:00,480 --> 00:18:01,890
So it was out of scope.

435
00:18:01,890 --> 00:18:04,260
So we left with the free project in Spark,

436
00:18:04,260 --> 00:18:06,840
which we can compare. So
let's look at the first one.

437
00:18:06,840 --> 00:18:08,880
This is operating system-like software,

438
00:18:08,880 --> 00:18:11,700
which we fully develop in
Spark in the format proof,

439
00:18:11,700 --> 00:18:13,440
this operating system-like software.

440
00:18:13,440 --> 00:18:15,990
And also we had the
memory and safe language,

441
00:18:15,990 --> 00:18:18,240
another type of the software,
our internal develop,

442
00:18:18,240 --> 00:18:21,033
which was developing C and
C++, and as you can see,

443
00:18:21,033 --> 00:18:24,090
we spent three weeks in the
memory and safe language for the

444
00:18:24,090 --> 00:18:27,510
reviewing and six weeks, which
was twice as long on Spark,

445
00:18:27,510 --> 00:18:30,390
but we found only five, ten bugs in Spark.

446
00:18:30,390 --> 00:18:31,410
While the,

447
00:18:31,410 --> 00:18:34,710
while we spent twice as longer
serving the memory and safe

448
00:18:34,710 --> 00:18:36,600
language. And in the memory safe language,

449
00:18:36,600 --> 00:18:40,260
we found 45 total back counts.
It's a huge difference.

450
00:18:40,260 --> 00:18:41,490
Additionally, as you can see,

451
00:18:41,490 --> 00:18:43,590
there is almost 52% of the bugs.

452
00:18:43,590 --> 00:18:46,590
53% of the bugs are memory safety issues

453
00:18:46,590 --> 00:18:48,900
in the memory and safe
language while in Spark

454
00:18:48,900 --> 00:18:50,430
it's zero.

455
00:18:50,430 --> 00:18:51,330
Another software,

456
00:18:51,330 --> 00:18:55,080
which is also good to compare
is the project for the last

457
00:18:55,080 --> 00:18:57,690
project in the Spark,
which is a boot software,

458
00:18:57,690 --> 00:18:58,860
also written in Spark.

459
00:18:58,860 --> 00:19:01,380
And we spent almost the same
amount of the time of reviewing

460
00:19:01,380 --> 00:19:04,800
as booting software in the
memory and safe language,

461
00:19:04,800 --> 00:19:06,270
and apparently memory safe language,

462
00:19:06,270 --> 00:19:09,120
boot software was not written
by us, not written by Nvidia.

463
00:19:09,120 --> 00:19:10,860
It was written by external company,

464
00:19:10,860 --> 00:19:13,290
although it was using in Nvidia products.

465
00:19:13,290 --> 00:19:14,490
So that's why we review it.

466
00:19:14,490 --> 00:19:15,450
And as you can see,

467
00:19:15,450 --> 00:19:19,470
we found around five bugs in the Spark

468
00:19:19,470 --> 00:19:22,410
and 17 bugs in the
memory and safe language.

469
00:19:22,410 --> 00:19:23,490
Again, huge difference.

470
00:19:23,490 --> 00:19:25,740
If you look at the percentage
of the memory safety,

471
00:19:25,740 --> 00:19:29,460
it matches the industry
standard 65% are memory safety

472
00:19:29,460 --> 00:19:32,850
issue in memory safe
language and 0% in Spark.

473
00:19:32,850 --> 00:19:36,690
The last project is a pretty
difficult let's say because

474
00:19:36,690 --> 00:19:39,480
it's kind of hybrid project
combining two different other

475
00:19:39,480 --> 00:19:40,313
software.

476
00:19:40,313 --> 00:19:42,670
It's a boot- it's a
root of trust software.

477
00:19:42,670 --> 00:19:44,130
And additionally,

478
00:19:44,130 --> 00:19:46,530
there is a functionality of
being resource management

479
00:19:46,530 --> 00:19:48,810
software and apparently in
the memory and safe language,

480
00:19:48,810 --> 00:19:51,030
we had two separate project
doing exactly the same

481
00:19:51,030 --> 00:19:52,020
functionality.

482
00:19:52,020 --> 00:19:54,480
So two of this project in the memory safe,

483
00:19:54,480 --> 00:19:56,880
combined together gives more
or less the same functionality

484
00:19:56,880 --> 00:19:59,700
and the same code size of
the software return in Spark.

485
00:19:59,700 --> 00:20:02,250
So we spent more or less the
same amount of the timeframe,

486
00:20:02,250 --> 00:20:03,360
four weeks plus,

487
00:20:03,360 --> 00:20:05,520
less than two weeks,
and five weeks in Spark.

488
00:20:05,520 --> 00:20:07,200
So more or less the same timeframe.

489
00:20:07,200 --> 00:20:09,530
We found around 40 bugs in the memory

490
00:20:09,530 --> 00:20:12,720
and safe language and 28 bugs in Spark.

491
00:20:12,720 --> 00:20:14,643
Again, big benefits.

492
00:20:15,570 --> 00:20:17,130
And so in the recap,

493
00:20:17,130 --> 00:20:19,230
it's a conclusion based on
this average data formula

494
00:20:19,230 --> 00:20:21,600
verified software can be free
from the memory safety problem

495
00:20:21,600 --> 00:20:23,670
that's a start, as you can see later,

496
00:20:23,670 --> 00:20:27,240
there is still some room for
abuse, but in general, yes,

497
00:20:27,240 --> 00:20:28,560
it can be memory safe.

498
00:20:28,560 --> 00:20:30,810
Formula verified software has
much higher quality because

499
00:20:30,810 --> 00:20:33,510
Spark apparently enforces
a lot of attributes

500
00:20:33,510 --> 00:20:35,460
like secure and strict coding practice,

501
00:20:35,460 --> 00:20:36,897
strong typing system.

502
00:20:36,897 --> 00:20:40,290
You need to correctly analyze
any data otherwise before you

503
00:20:40,290 --> 00:20:42,450
use it, you will be like
killed by the compiler.

504
00:20:42,450 --> 00:20:43,500
You cannot use it.

505
00:20:43,500 --> 00:20:46,440
And also what is worth to
mention Spark is not a silver

506
00:20:46,440 --> 00:20:47,273
bullet.

507
00:20:47,273 --> 00:20:48,990
You just sit that you can
apply and all of your problem

508
00:20:48,990 --> 00:20:49,823
disappear.

509
00:20:49,823 --> 00:20:52,200
It's a pretty heavy software
programming language.

510
00:20:52,200 --> 00:20:54,600
So you cannot just sit down
and write a code like in the C

511
00:20:54,600 --> 00:20:56,970
you write a function, you
write another function, no.

512
00:20:56,970 --> 00:20:59,850
You must be really sit down,
think about the software,

513
00:20:59,850 --> 00:21:02,970
design it properly, map any object.

514
00:21:02,970 --> 00:21:05,310
And then when you have that,
then you can start, write,

515
00:21:05,310 --> 00:21:07,860
starting to compile them
together and write a software.

516
00:21:07,860 --> 00:21:09,440
So you need to keep this in mind.

517
00:21:09,440 --> 00:21:10,500
Additionally,

518
00:21:10,500 --> 00:21:13,650
Spark can prove that there is
no dynamic checks cannot fail.

519
00:21:13,650 --> 00:21:16,800
There is something called
absent of front and errors,

520
00:21:16,800 --> 00:21:18,510
and depends on your level of assurance.

521
00:21:18,510 --> 00:21:20,670
You might have warranty,
they will never appear.

522
00:21:20,670 --> 00:21:23,156
So these checks might not be
in the binary because you don't

523
00:21:23,156 --> 00:21:24,630
need them anymore.

524
00:21:24,630 --> 00:21:27,330
Also it's enables much more
efficient security efforts

525
00:21:27,330 --> 00:21:30,210
because at first you will
not see dummy bugs there.

526
00:21:30,210 --> 00:21:31,740
Like we sometimes seen in the the

527
00:21:31,740 --> 00:21:33,750
member safe software and something which

528
00:21:33,750 --> 00:21:36,810
is not verified or unprovable
is very clearly marked with

529
00:21:36,810 --> 00:21:37,643
the attributes.

530
00:21:37,643 --> 00:21:38,670
So we just focus on this function,

531
00:21:38,670 --> 00:21:42,570
what is improved and what is
unverified and focus there.

532
00:21:42,570 --> 00:21:44,280
And there is also something
called peak condition,

533
00:21:44,280 --> 00:21:45,200
post condition, ghost code,

534
00:21:45,200 --> 00:21:47,670
and not go want to go
into the trace on that,

535
00:21:47,670 --> 00:21:50,550
but essentially you can
clearly define the state of the

536
00:21:50,550 --> 00:21:52,290
software in that specific waste of time.

537
00:21:52,290 --> 00:21:54,341
So you know what to expect
from the software and how to

538
00:21:54,341 --> 00:21:56,880
behave. You just read that stuff.

539
00:21:56,880 --> 00:21:59,220
And you know what the purpose of

540
00:21:59,220 --> 00:22:01,260
the specific software state machine

541
00:22:01,260 --> 00:22:04,560
and um what also is uh

542
00:22:04,560 --> 00:22:05,880
the work to went from is that

543
00:22:05,880 --> 00:22:06,713
most of the bugs,

544
00:22:06,713 --> 00:22:08,760
which we found in Spark
requires apparently very deep

545
00:22:08,760 --> 00:22:10,560
knowledge and understanding
of the software.

546
00:22:10,560 --> 00:22:12,281
So in the end of the day, the bugs,

547
00:22:12,281 --> 00:22:13,730
which we found are very
deep type of the bugs.

548
00:22:13,730 --> 00:22:15,422
We have architecture
issues, design issues.

549
00:22:15,422 --> 00:22:18,930
And if you look from the
statistical perspective,

550
00:22:18,930 --> 00:22:20,880
when we do review the project

551
00:22:20,880 --> 00:22:21,960
in the memory safe language,

552
00:22:21,960 --> 00:22:25,470
on average, on, in four weeks,
we found around 40, 50 bugs.

553
00:22:25,470 --> 00:22:27,240
While in Spark, we spent six weeks,

554
00:22:27,240 --> 00:22:30,150
which is longer on average.
We found around five, 10 bugs,

555
00:22:30,150 --> 00:22:32,190
which you can see there is a benefits,

556
00:22:32,190 --> 00:22:34,705
which you can see
internally in our company.

557
00:22:34,705 --> 00:22:36,870
So what is the real bugs?

558
00:22:36,870 --> 00:22:37,870
What are the example of the bugs,

559
00:22:37,870 --> 00:22:39,810
which are speaking about here?

560
00:22:39,810 --> 00:22:40,643
So yeah,

561
00:22:40,643 --> 00:22:42,540
formula verified software
can produce you the software,

562
00:22:42,540 --> 00:22:45,120
which is very strong,
but there is always bot.

563
00:22:45,120 --> 00:22:48,183
So let's look at this bot in the Spark.

564
00:22:49,230 --> 00:22:51,362
So first problem is the
problem with the signature

565
00:22:51,362 --> 00:22:54,120
verification, which we
found in one of the project.

566
00:22:54,120 --> 00:22:57,450
So there was a function
who called, let's say,

567
00:22:57,450 --> 00:22:59,520
verified public key and is verified.

568
00:22:59,520 --> 00:23:01,830
Public key has a specific checks.

569
00:23:01,830 --> 00:23:04,681
If the software is configured
to verify the signature,

570
00:23:04,681 --> 00:23:06,810
then it verifies the signature.

571
00:23:06,810 --> 00:23:09,990
So what is this route of trust
for this functional verify

572
00:23:09,990 --> 00:23:11,880
signature let's take closer look.

573
00:23:11,880 --> 00:23:15,420
And we can see that this
function get authentication has

574
00:23:15,420 --> 00:23:17,130
apparently three states,

575
00:23:17,130 --> 00:23:20,970
which a state authentication
known authentication RSI,

576
00:23:20,970 --> 00:23:23,610
but there is also state
authentication, unknown,

577
00:23:23,610 --> 00:23:26,550
but the function verified
public key never takes into

578
00:23:26,550 --> 00:23:28,620
account this first state.

579
00:23:28,620 --> 00:23:31,260
So is the state even possible
to appear because if you have

580
00:23:31,260 --> 00:23:33,360
authentication RSI, everything is fine,

581
00:23:33,360 --> 00:23:36,210
every authentication known,
we don't need to verify.

582
00:23:36,210 --> 00:23:38,640
So it's okay. What about
authentication unknown?

583
00:23:38,640 --> 00:23:39,780
And apparently the root of trust,

584
00:23:39,780 --> 00:23:42,390
of authentication unknown is
coming from the register on the

585
00:23:42,390 --> 00:23:45,180
hardware and register occupied free bits.

586
00:23:45,180 --> 00:23:48,150
But three bits gives you
eight states, not two states.

587
00:23:48,150 --> 00:23:50,940
So eight states apparently means
that authentication unknown

588
00:23:50,940 --> 00:23:54,870
will be assigned to six
states of this hardware.

589
00:23:54,870 --> 00:23:56,694
Not- so- and these states,

590
00:23:56,694 --> 00:23:59,203
these six states are never
taken into account in the

591
00:23:59,203 --> 00:24:01,800
verified public key because
we only taking into account

592
00:24:01,800 --> 00:24:03,600
verified known, and verified RSI.

593
00:24:03,600 --> 00:24:06,060
So what happens if we
have authentication known?

594
00:24:06,060 --> 00:24:09,330
Apparently the software we
treat is in the same ways as our

595
00:24:09,330 --> 00:24:10,620
authentication known.

596
00:24:10,620 --> 00:24:12,570
So in the out of eight states,

597
00:24:12,570 --> 00:24:15,327
only one state enforces
signature verification and seven

598
00:24:15,327 --> 00:24:18,480
states are handled as there
is no verification at all.

599
00:24:18,480 --> 00:24:19,313
And again,

600
00:24:19,313 --> 00:24:20,940
prover will not be able to catch that

601
00:24:20,940 --> 00:24:22,620
because it's a logical error.

602
00:24:22,620 --> 00:24:25,890
It's a logical error, how
it's defined by the developer.

603
00:24:25,890 --> 00:24:28,203
So this type of bugs
you can still have here.

604
00:24:29,468 --> 00:24:31,290
And this is the problem with compiler,

605
00:24:31,290 --> 00:24:32,850
which Alex speak more about.

606
00:24:32,850 --> 00:24:35,520
- Yeah, one of the projects we
reviewed had fault injection

607
00:24:35,520 --> 00:24:36,693
protection in scope.

608
00:24:37,908 --> 00:24:40,860
So the code must incorporate
some kind of mitigation against

609
00:24:40,860 --> 00:24:44,640
fault protection, is true to
enable this fault mitigation.

610
00:24:44,640 --> 00:24:48,300
So here you see a
disassembly of the binary

611
00:24:48,300 --> 00:24:49,542
that we analyzed.

612
00:24:49,542 --> 00:24:53,910
We see some memory
compare function are uh-

613
00:24:53,910 --> 00:24:57,240
um implemented in a constant way

614
00:24:57,240 --> 00:25:00,810
so that we, this is protected um

615
00:25:00,810 --> 00:25:03,120
constant time execution.

616
00:25:03,120 --> 00:25:04,140
But at the same time,

617
00:25:04,140 --> 00:25:05,670
we see a single point of weakness,

618
00:25:05,670 --> 00:25:07,140
which is definitely a bad thing.

619
00:25:07,140 --> 00:25:10,080
If you care about fault injections. Um.

620
00:25:10,080 --> 00:25:11,010
So what happened here,

621
00:25:11,010 --> 00:25:13,050
we analyzed the source code
and saw that developers

622
00:25:13,050 --> 00:25:15,360
implemented everything correctly.

623
00:25:15,360 --> 00:25:17,010
But for some reason,

624
00:25:17,010 --> 00:25:19,650
compiler optimized out certain functions,

625
00:25:19,650 --> 00:25:21,270
which weakened the protection.

626
00:25:21,270 --> 00:25:25,080
So this was essentially
a compiler problem there,

627
00:25:25,080 --> 00:25:27,150
and you only can see that in the binary.

628
00:25:27,150 --> 00:25:29,610
So that's why you not only have
to analyze your source code,

629
00:25:29,610 --> 00:25:30,573
but the binaries.

630
00:25:33,360 --> 00:25:36,780
- Yes. And that's another
interesting example of the issue.

631
00:25:36,780 --> 00:25:37,980
It's not the one issue.

632
00:25:37,980 --> 00:25:40,260
We found a very small
issues here and there,

633
00:25:40,260 --> 00:25:42,360
but then we realize when
we combine them together,

634
00:25:42,360 --> 00:25:44,970
we have a pretty serious security issues.

635
00:25:44,970 --> 00:25:47,130
It's a problem with the out
neutralization problem with the

636
00:25:47,130 --> 00:25:50,490
absent front mirror problem,
with the design performance.

637
00:25:50,490 --> 00:25:52,110
And then in the end, when
we mix them together,

638
00:25:52,110 --> 00:25:53,760
we found something interesting.

639
00:25:53,760 --> 00:25:54,810
So first thing first,

640
00:25:54,810 --> 00:25:57,480
Spark of course cannot
prove the correctness of

641
00:25:57,480 --> 00:26:00,060
some metadata coming
from untrusted sources,

642
00:26:00,060 --> 00:26:02,040
like from the external
media, from the wrong,

643
00:26:02,040 --> 00:26:05,010
because how it can, you
don't know what's there,

644
00:26:05,010 --> 00:26:06,900
but although if you wanna
prove such kind of software,

645
00:26:06,900 --> 00:26:08,910
you can provide this
knowledge to the provers.

646
00:26:08,910 --> 00:26:09,870
So the prove know,

647
00:26:09,870 --> 00:26:13,230
was that the limits or what are
the bounce track of specific

648
00:26:13,230 --> 00:26:14,310
untrusted data?

649
00:26:14,310 --> 00:26:15,990
And this is what the developer did here.

650
00:26:15,990 --> 00:26:19,980
They essentially provide
some manual verification of,

651
00:26:19,980 --> 00:26:23,370
specific eh- for specific
contracts to help prove

652
00:26:23,370 --> 00:26:26,400
or proof what they wanted
to be proved essentially.

653
00:26:26,400 --> 00:26:27,960
So what was verified there?

654
00:26:27,960 --> 00:26:29,130
Essentially, they verified

655
00:26:29,130 --> 00:26:31,440
the maximum size of external media to not

656
00:26:31,440 --> 00:26:34,470
cross through the out
of band of the memory.

657
00:26:34,470 --> 00:26:36,630
They also verified what the local buffers,

658
00:26:36,630 --> 00:26:38,070
what the minimal size is.

659
00:26:38,070 --> 00:26:40,020
And also there is some other
checks which are boring.

660
00:26:40,020 --> 00:26:41,790
So I didn't include
there, but there is also,

661
00:26:41,790 --> 00:26:44,400
you cannot start reading from
the beginning of the media,

662
00:26:44,400 --> 00:26:45,720
but from the offset of the media.

663
00:26:45,720 --> 00:26:49,080
So you also don't wanna
go out of the media size.

664
00:26:49,080 --> 00:26:52,200
So all of that is there. And in short,

665
00:26:52,200 --> 00:26:54,983
all of this sanitization for the prover

666
00:26:54,983 --> 00:26:58,485
allows you to read the
data between X and Y.

667
00:26:58,485 --> 00:27:00,450
Then they will pass the check

668
00:27:00,450 --> 00:27:01,950
and the prover will be happy then.

669
00:27:01,950 --> 00:27:05,070
And X apparently was some
kind of small number,

670
00:27:05,070 --> 00:27:06,330
let's say eight bytes.

671
00:27:06,330 --> 00:27:08,850
And Y always warranty is that

672
00:27:08,850 --> 00:27:11,100
you never go outside of the media size.

673
00:27:11,100 --> 00:27:12,930
So everything is fine.

674
00:27:12,930 --> 00:27:13,763
It's okay.

675
00:27:13,763 --> 00:27:16,080
So far we just have some
bounce track and the prover can

676
00:27:16,080 --> 00:27:17,190
prove it's okay.

677
00:27:17,190 --> 00:27:20,040
And then what we saw that when

678
00:27:20,040 --> 00:27:22,500
we starting to execute
further dysfunction,

679
00:27:22,500 --> 00:27:24,577
the starting to read from
external media, some image,

680
00:27:24,577 --> 00:27:28,020
and this image had another header inside,

681
00:27:28,020 --> 00:27:30,207
which had different size that
the minimum size verified by

682
00:27:30,207 --> 00:27:31,260
the prover,

683
00:27:31,260 --> 00:27:34,500
because the minimum size of
this header was five- 12 bytes,

684
00:27:34,500 --> 00:27:35,730
not eight bytes.

685
00:27:35,730 --> 00:27:37,920
Which essentially means that
some portion of the data,

686
00:27:37,920 --> 00:27:39,660
if you read will be not really,

687
00:27:39,660 --> 00:27:42,240
internalizing the internal
representation of the buffer and

688
00:27:42,240 --> 00:27:44,610
internal states of the
buffer based on this header,

689
00:27:44,610 --> 00:27:45,690
also, won't be internalized

690
00:27:45,690 --> 00:27:46,860
because you just didn't treat them.

691
00:27:46,860 --> 00:27:49,110
So you cannot parse them,
et cetera, et cetera.

692
00:27:49,110 --> 00:27:50,760
But because before you wanted to

693
00:27:50,760 --> 00:27:52,530
reference any memory in Spark,

694
00:27:52,530 --> 00:27:54,900
or you want use any type
system in the Spark,

695
00:27:54,900 --> 00:27:56,010
you must internalize them

696
00:27:56,010 --> 00:27:58,170
because otherwise you're not
even compile the software.

697
00:27:58,170 --> 00:27:59,160
So what happens, I mean,

698
00:27:59,160 --> 00:28:01,170
prover will be not unhappy if you do that.

699
00:28:01,170 --> 00:28:04,920
And what happens then the
developers force internalization.

700
00:28:04,920 --> 00:28:06,240
So they zero this memory. Yes.

701
00:28:06,240 --> 00:28:07,350
So it's fine. Yes.

702
00:28:07,350 --> 00:28:09,270
We zero. The memory which you don't use.

703
00:28:09,270 --> 00:28:10,650
So it's fine. Yes.

704
00:28:10,650 --> 00:28:11,820
So let's go forward.

705
00:28:11,820 --> 00:28:14,040
What we see that somewhere in the middle,

706
00:28:14,040 --> 00:28:15,480
later on the stage execution,

707
00:28:15,480 --> 00:28:17,438
we see the function who
also tried to revise

708
00:28:17,438 --> 00:28:20,400
some pieces of the memory
from this second image,

709
00:28:20,400 --> 00:28:21,360
which we read.

710
00:28:21,360 --> 00:28:23,640
And this is pretty
interesting function because

711
00:28:23,640 --> 00:28:24,630
first thing first,

712
00:28:24,630 --> 00:28:27,720
they internalize the entry
points to be always success

713
00:28:27,720 --> 00:28:29,700
should be failed, but
they make it success.

714
00:28:29,700 --> 00:28:31,380
So, okay that's a first red flag.

715
00:28:31,380 --> 00:28:33,090
Second red flag they said, "okay,

716
00:28:33,090 --> 00:28:35,130
if you already verified
some portal of the image,

717
00:28:35,130 --> 00:28:36,840
why you wanna verify it again?

718
00:28:36,840 --> 00:28:37,920
So if it's already verified,

719
00:28:37,920 --> 00:28:40,770
we have some local cache don't
verify anymore performance

720
00:28:40,770 --> 00:28:44,160
improvements and just go to
exit and return success."

721
00:28:44,160 --> 00:28:47,430
But there is also, as you
can see, there is ID zero.

722
00:28:47,430 --> 00:28:49,903
This ID zero is internal
representation of the state based

723
00:28:49,903 --> 00:28:52,320
on the header, which you
read in the second image.

724
00:28:52,320 --> 00:28:54,630
And because you never
fully read this image,

725
00:28:54,630 --> 00:28:56,100
this ID was centralized by zero

726
00:28:56,100 --> 00:28:57,510
as an alt internalization.

727
00:28:57,510 --> 00:29:00,090
But apparently this software
probably written by different

728
00:29:00,090 --> 00:29:02,820
team assumes that this
ID in the internal memory

729
00:29:02,820 --> 00:29:04,020
representation is zero.

730
00:29:04,020 --> 00:29:06,180
You means there is some
performance improvements,

731
00:29:06,180 --> 00:29:09,420
internal states, so go out
and never verify anything.

732
00:29:09,420 --> 00:29:11,640
So in the end, because of
this alt internalization,

733
00:29:11,640 --> 00:29:15,570
this zero was there and you
will never verify the image.

734
00:29:15,570 --> 00:29:17,070
And that say verification never happened.

735
00:29:17,070 --> 00:29:17,903
It skipped.

736
00:29:21,335 --> 00:29:23,190
- Let's see another example of the bug.

737
00:29:23,190 --> 00:29:26,790
So this one is a memory
visualization code,

738
00:29:26,790 --> 00:29:29,910
and you see that a
developer for some reason,

739
00:29:29,910 --> 00:29:32,610
decided to make a certain piece
of memory readable for both

740
00:29:32,610 --> 00:29:35,490
super super user mode and user mode.

741
00:29:35,490 --> 00:29:37,860
So basically there is a lack
of memory isolation between

742
00:29:37,860 --> 00:29:38,996
these two modes,

743
00:29:38,996 --> 00:29:42,810
but problem was that Spark
didn't know the context of this

744
00:29:42,810 --> 00:29:43,643
code.

745
00:29:43,643 --> 00:29:44,647
So uh-

746
00:29:44,647 --> 00:29:46,068
it was a fine code,

747
00:29:46,068 --> 00:29:47,218
compiled correctly,

748
00:29:47,218 --> 00:29:49,620
but since there was no context,

749
00:29:49,620 --> 00:29:52,110
prover didn't catch any
kind of issue with that.

750
00:29:52,110 --> 00:29:53,130
So it's a logical error.

751
00:29:53,130 --> 00:29:56,370
We didn't want this memory to
be readable by both user and

752
00:29:56,370 --> 00:29:57,570
supervisor mode,

753
00:29:57,570 --> 00:30:00,030
um but uh- since

754
00:30:00,030 --> 00:30:02,340
there was no good model of the hardware,

755
00:30:02,340 --> 00:30:05,880
the uh- prover could
not find this problem,

756
00:30:05,880 --> 00:30:08,990
but it's possible to build such
knowledge via a ghost code,

757
00:30:08,990 --> 00:30:10,653
but it's very difficult to do.

758
00:30:12,240 --> 00:30:16,080
Another example of the
issue is in this code

759
00:30:16,080 --> 00:30:17,910
that performs um

760
00:30:17,910 --> 00:30:21,300
installation of the
tasks during task switch.

761
00:30:21,300 --> 00:30:22,980
And you see that

762
00:30:22,980 --> 00:30:24,210
um-

763
00:30:24,210 --> 00:30:28,440
certain um - certain features
of the cache management

764
00:30:28,440 --> 00:30:31,920
have been enabled to be accessible
from the less privileged

765
00:30:31,920 --> 00:30:32,753
mode.

766
00:30:32,753 --> 00:30:36,000
And also the cash is not
invalidated on task switch.

767
00:30:36,000 --> 00:30:39,510
Eh, so it gives a less privileged mode

768
00:30:39,510 --> 00:30:42,450
an ability to perform
side channel attacks.

769
00:30:42,450 --> 00:30:44,849
Again, without a good hardware model,

770
00:30:44,849 --> 00:30:46,533
the prover could not catch that.

771
00:30:49,410 --> 00:30:52,350
- Yeah, so essentially, if you
write the software in Spark,

772
00:30:52,350 --> 00:30:55,170
you also should care about
the hardware model, everything

773
00:30:55,170 --> 00:30:56,820
otherwise the prover might be blind.

774
00:30:56,820 --> 00:30:58,107
So this knowledge is possible to be done,

775
00:30:58,107 --> 00:30:59,910
but it's difficult.

776
00:30:59,910 --> 00:31:03,270
So that's another problem which we found.

777
00:31:03,270 --> 00:31:05,160
It's pretty interesting.
So, as I mentioned,

778
00:31:05,160 --> 00:31:08,700
we developed some specific
operating system in Spark and

779
00:31:08,700 --> 00:31:12,060
this works on the top
of the custom Risk Five

780
00:31:12,060 --> 00:31:15,209
micro possessor, we see also
develop develop in Nvidea,

781
00:31:15,209 --> 00:31:17,400
and this is a problem which
we found during the short

782
00:31:17,400 --> 00:31:18,233
memory.

783
00:31:18,233 --> 00:31:20,460
I don't wanna go to the details
how this entire operating

784
00:31:20,460 --> 00:31:23,490
system works, because you can
have another talk about that.

785
00:31:23,490 --> 00:31:24,690
Although it's already public,

786
00:31:24,690 --> 00:31:26,760
it's nothing new that we discuss here.

787
00:31:26,760 --> 00:31:29,220
And there is a talk made
by the Demarco (indistinct)

788
00:31:29,220 --> 00:31:31,650
who fully goes over all of the details,

789
00:31:31,650 --> 00:31:34,710
how this operating system
software works written in Spark.

790
00:31:34,710 --> 00:31:37,320
In short, just to recap,
this is architecture.

791
00:31:37,320 --> 00:31:38,340
You have a hardware,

792
00:31:38,340 --> 00:31:43,340
hardware is sliced by specific
sub portion of the hardware.

793
00:31:43,350 --> 00:31:46,080
And this sub portion of the
hardware is being seen as

794
00:31:46,080 --> 00:31:48,690
exclusive independent hardware
for each of the software

795
00:31:48,690 --> 00:31:49,560
partition.

796
00:31:49,560 --> 00:31:51,480
And the- and the Spark code,

797
00:31:51,480 --> 00:31:54,270
which here in as a part of
the separation kernel and this

798
00:31:54,270 --> 00:31:58,380
separation kernel essentially
enforce the limits

799
00:31:58,380 --> 00:32:00,570
of what the partition can
have access to or not.

800
00:32:00,570 --> 00:32:02,970
And because it's formatly
proved and formatly verified,

801
00:32:02,970 --> 00:32:05,910
we have warranties that
we didn't miss anything

802
00:32:05,910 --> 00:32:08,310
that what we divided and slice

803
00:32:08,310 --> 00:32:10,980
it's exclusively only accessible for that

804
00:32:10,980 --> 00:32:12,360
specific software partition.

805
00:32:12,360 --> 00:32:15,000
So we can have multiple
partitions that each of them have

806
00:32:15,000 --> 00:32:17,490
exclusive view of some specific
portion of the hardware.

807
00:32:17,490 --> 00:32:21,030
And we prove there is no way
other way around than that.

808
00:32:21,030 --> 00:32:24,090
So essentially everything when
we verified looks fine and

809
00:32:24,090 --> 00:32:24,923
looks okay,

810
00:32:24,923 --> 00:32:27,060
but then we realize that
from the performance reasons,

811
00:32:27,060 --> 00:32:30,000
which of course makes sense if
you have the shared libraries

812
00:32:30,000 --> 00:32:31,650
used by two separate partition,

813
00:32:31,650 --> 00:32:33,735
we do not want to lose the memory

814
00:32:33,735 --> 00:32:36,660
and map the same shared library twice

815
00:32:36,660 --> 00:32:38,130
in the different physical page. Yes?

816
00:32:38,130 --> 00:32:39,810
So you just shared the same page.

817
00:32:39,810 --> 00:32:42,090
So you have a shared page
between the various partition,

818
00:32:42,090 --> 00:32:44,400
if they use exactly the
same shared libraries.

819
00:32:44,400 --> 00:32:48,180
And that's interesting because
shared partition not only

820
00:32:48,180 --> 00:32:49,380
include the text section,

821
00:32:49,380 --> 00:32:51,570
but they also can include the data section

822
00:32:51,570 --> 00:32:53,850
and the data section
could be written right.

823
00:32:53,850 --> 00:32:54,683
Yes?

824
00:32:54,683 --> 00:32:55,710
So if it's written right,

825
00:32:55,710 --> 00:32:57,210
and depends on the shared library,

826
00:32:57,210 --> 00:32:59,070
we might have interesting
information there.

827
00:32:59,070 --> 00:33:01,890
This interesting information
might include the global state

828
00:33:01,890 --> 00:33:03,780
of specific shared library,

829
00:33:03,780 --> 00:33:06,540
which could be taken in
the account in the logic of

830
00:33:06,540 --> 00:33:09,060
execution of the specific
software in the partition.

831
00:33:09,060 --> 00:33:11,340
They also might have internalization data.

832
00:33:11,340 --> 00:33:13,380
They also might have
some control flow data.

833
00:33:13,380 --> 00:33:16,290
They also might have if it's
written in the memory and safe

834
00:33:16,290 --> 00:33:17,700
language pointers,

835
00:33:17,700 --> 00:33:20,430
and this is pretty getting
pretty interesting. Yes?

836
00:33:20,430 --> 00:33:23,940
So apparently Spark and the
prover cannot know what you

837
00:33:23,940 --> 00:33:27,420
physically do with the content
of the shared library inside

838
00:33:27,420 --> 00:33:29,460
of the partition, because how?

839
00:33:29,460 --> 00:33:31,980
So essentially this opens
the room for abuse and

840
00:33:31,980 --> 00:33:34,290
depends of course, what
is in the shared memory

841
00:33:34,290 --> 00:33:35,970
and what is in the shared library

842
00:33:35,970 --> 00:33:38,520
and also what is in
the shared global data.

843
00:33:38,520 --> 00:33:41,760
So we found a few interesting
bugs in our use cases,

844
00:33:41,760 --> 00:33:45,660
and we decided to develop a
proof of concept exploit against

845
00:33:45,660 --> 00:33:49,050
some of these shared libraries
in this operating system

846
00:33:49,050 --> 00:33:50,100
written in Spark.

847
00:33:50,100 --> 00:33:52,710
And we wanted to show you how it works.

848
00:33:52,710 --> 00:33:55,980
I'm not sure what will be the
quality of the image here,

849
00:33:55,980 --> 00:33:56,973
but let's try.

850
00:33:57,990 --> 00:34:00,093
So this is apparently-

851
00:34:01,650 --> 00:34:02,911
Oh.

852
00:34:02,911 --> 00:34:06,769
- Mhm.

853
00:34:06,769 --> 00:34:08,186
- Can we somehow?

854
00:34:10,710 --> 00:34:12,720
- Can I ask for a help some of the goons,

855
00:34:12,720 --> 00:34:13,800
because when I switch,

856
00:34:13,800 --> 00:34:16,203
that doesn't switch to
the video mode somehow.

857
00:34:29,310 --> 00:34:30,153
Now we have.

858
00:34:32,610 --> 00:34:33,443
Okay.

859
00:34:33,443 --> 00:34:35,190
Apparently it worked.

860
00:34:35,190 --> 00:34:38,490
So what we see here, I'm not
sure how much you can see here,

861
00:34:38,490 --> 00:34:42,150
but this is software like a partition one.

862
00:34:42,150 --> 00:34:44,200
What I was explaining before this is uh

863
00:34:45,120 --> 00:34:48,000
in the C-written partition
one, it's not very complicated.

864
00:34:48,000 --> 00:34:50,730
As you can see here, this
is one partition main,

865
00:34:50,730 --> 00:34:52,230
and there is also trap handle because

866
00:34:52,230 --> 00:34:53,190
if something screwed up,

867
00:34:53,190 --> 00:34:57,000
we wanna handle the exceptions
and what you can see in this

868
00:34:57,000 --> 00:34:58,140
partition one.

869
00:34:58,140 --> 00:34:59,340
We just-

870
00:34:59,340 --> 00:35:01,650
first, we trying to define the pointer,

871
00:35:01,650 --> 00:35:02,533
specific others of the memory.

872
00:35:02,533 --> 00:35:03,690
As you can see,

873
00:35:03,690 --> 00:35:06,060
the others of the memory
is a shared buffer.

874
00:35:06,060 --> 00:35:07,380
This is a shared buffer,

875
00:35:07,380 --> 00:35:11,070
which is visible in the
partition one and partition two.

876
00:35:11,070 --> 00:35:13,230
And this is the address
of the shared buffer,

877
00:35:13,230 --> 00:35:15,990
a vehicle address of course, 18 and 1000.

878
00:35:15,990 --> 00:35:19,650
So we define the pointer here
exactly to point somewhere in

879
00:35:19,650 --> 00:35:21,660
the middle of the shared library,

880
00:35:21,660 --> 00:35:24,720
which is exactly in the page
where the shared library is

881
00:35:24,720 --> 00:35:25,578
it's 18

882
00:35:25,578 --> 00:35:26,730
eh 4

883
00:35:26,730 --> 00:35:27,960
- 10, essentially.

884
00:35:27,960 --> 00:35:29,910
So it's inside of this point.

885
00:35:29,910 --> 00:35:31,860
We point somewhere inside
of the shared buffer,

886
00:35:31,860 --> 00:35:33,354
which is visible in the both partition.

887
00:35:33,354 --> 00:35:35,850
And then inside of the shared buffer,

888
00:35:35,850 --> 00:35:38,520
we will write some value
and we write this value

889
00:35:38,520 --> 00:35:39,780
in the partition two,

890
00:35:39,780 --> 00:35:42,310
there is definition
where the stack page is

891
00:35:43,290 --> 00:35:45,210
and the stack page is mapped

892
00:35:45,210 --> 00:35:47,850
and the virtual address, 18, 5,000.

893
00:35:47,850 --> 00:35:51,000
So we write to the short
buffer address of the stack.

894
00:35:51,000 --> 00:35:52,830
That's all what we do in partition one.

895
00:35:52,830 --> 00:35:55,590
And then we switch the
partition to partition two.

896
00:35:55,590 --> 00:35:57,990
So that's what the entire software does.

897
00:35:57,990 --> 00:36:00,750
This is the magic tool
which we use internally

898
00:36:00,750 --> 00:36:04,691
in the Nvidia to be able to um

899
00:36:04,691 --> 00:36:07,740
deba- debunk or verify specific hardware,

900
00:36:07,740 --> 00:36:09,210
specific software.

901
00:36:09,210 --> 00:36:11,160
So we run this magic software,

902
00:36:11,160 --> 00:36:15,330
let's say to be able to connect
to the Risk Five engine,

903
00:36:15,330 --> 00:36:17,790
we see we expect this
five engine to be clear,

904
00:36:17,790 --> 00:36:19,200
we checking the de-mask clock.

905
00:36:19,200 --> 00:36:20,033
You see, there is nothing there.

906
00:36:20,033 --> 00:36:21,330
There is no messages.

907
00:36:21,330 --> 00:36:23,880
It's just clear state of Risk Five.

908
00:36:23,880 --> 00:36:26,400
And you can see it's clear
state, but it's still running.

909
00:36:26,400 --> 00:36:28,080
It's here. You see, it's not halted.

910
00:36:28,080 --> 00:36:29,640
Well still Risk Five is running

911
00:36:29,640 --> 00:36:30,870
so what we do now,

912
00:36:30,870 --> 00:36:32,640
we trying to refresh the feed

913
00:36:32,640 --> 00:36:34,740
where of entire Risk
Five engine in the GPU

914
00:36:34,740 --> 00:36:36,930
to exactly have this two
partition running together

915
00:36:36,930 --> 00:36:39,360
under separation kernel software,

916
00:36:39,360 --> 00:36:40,193
which is formatly verified.

917
00:36:40,193 --> 00:36:42,647
And you can see after the flashing,

918
00:36:42,647 --> 00:36:45,510
eh there is some censorship
which you needed to put,

919
00:36:45,510 --> 00:36:47,580
but logic, I guess it's visible.

920
00:36:47,580 --> 00:36:48,450
You can see that it's,

921
00:36:48,450 --> 00:36:50,880
it's something happened and
you see the core is started.

922
00:36:50,880 --> 00:36:52,140
Everything is fine.

923
00:36:52,140 --> 00:36:53,460
And you can see the Risk Five startup

924
00:36:53,460 --> 00:36:55,830
is not halted after the
flashing of this new film

925
00:36:55,830 --> 00:36:56,790
where it's running.

926
00:36:56,790 --> 00:36:58,080
But when you see the de-mask,

927
00:36:58,080 --> 00:37:00,240
you see the partition two crashed,

928
00:37:00,240 --> 00:37:01,860
and we have stack overflow,

929
00:37:01,860 --> 00:37:03,237
and it's formatly verified software,

930
00:37:03,237 --> 00:37:05,850
and formatly verified language.

931
00:37:05,850 --> 00:37:08,340
I can see, be able to do stack overflow.

932
00:37:08,340 --> 00:37:09,173
That's interesting.

933
00:37:09,173 --> 00:37:12,480
So let's check the uh specific page

934
00:37:12,480 --> 00:37:13,860
where we uh write.

935
00:37:13,860 --> 00:37:15,480
So you can see when we done the software,

936
00:37:15,480 --> 00:37:18,107
the page of the stack
page, it's a physical page,

937
00:37:18,107 --> 00:37:20,430
which is only visible
in the partition two.

938
00:37:20,430 --> 00:37:23,010
It's not visible parti-
in the partition one,

939
00:37:23,010 --> 00:37:24,839
we were managed from the partition one,

940
00:37:24,839 --> 00:37:27,789
just put the pointer to the
stack and overflow the stack of

941
00:37:27,789 --> 00:37:30,330
the memory, which you don't
even see after the partitions,

942
00:37:30,330 --> 00:37:33,060
which happens. So you can
see it's exactly the address,

943
00:37:33,060 --> 00:37:34,710
what we overflow.

944
00:37:34,710 --> 00:37:38,580
So let's check again. This is
the address of physical page.

945
00:37:38,580 --> 00:37:42,420
And if you reset the
engine and we check again,

946
00:37:42,420 --> 00:37:44,010
the de-mask, we see it's nothing there.

947
00:37:44,010 --> 00:37:45,180
So we are not faking,

948
00:37:45,180 --> 00:37:48,420
it's really running the firmware,
which we designed to run.

949
00:37:48,420 --> 00:37:50,126
And yes. And then again,

950
00:37:50,126 --> 00:37:53,640
verify the address to be
sure this is what we did.

951
00:37:53,640 --> 00:37:55,380
So you see in the partition one,

952
00:37:55,380 --> 00:37:57,810
we only write the address
of the physical page,

953
00:37:57,810 --> 00:37:59,640
where the stack will be
mapped in the partition tool,

954
00:37:59,640 --> 00:38:02,280
which we don't see in the
partition one and the address of

955
00:38:02,280 --> 00:38:04,980
the page physically matches.

956
00:38:04,980 --> 00:38:06,870
So that's all what we did here.

957
00:38:06,870 --> 00:38:09,870
And this exact page is mapped as a stack.

958
00:38:09,870 --> 00:38:12,150
So that's the proof that
this is a stack page.

959
00:38:12,150 --> 00:38:13,383
So yeah, we are here.

960
00:38:25,230 --> 00:38:26,063
Fast forward.

961
00:38:29,952 --> 00:38:30,785
Mhm.

962
00:38:32,997 --> 00:38:36,840
Eh, so just to summarize
everything at first,

963
00:38:36,840 --> 00:38:41,460
we would like to thank Nvidia
for developing such an amazing

964
00:38:41,460 --> 00:38:43,740
uh, execution environment
that we can analyze.

965
00:38:43,740 --> 00:38:46,230
We want to thanks St. Francis
Security Research Team.

966
00:38:46,230 --> 00:38:48,450
We want to thank the GPU
Software Security Team.

967
00:38:48,450 --> 00:38:50,940
We want to thanks the product
security team and other core

968
00:38:50,940 --> 00:38:53,250
for creating such a brilliant language.

969
00:38:53,250 --> 00:38:57,300
And so everyone who was
involved in this research and to

970
00:38:57,300 --> 00:39:00,870
summarize what we did the use
of the type safety language,

971
00:39:00,870 --> 00:39:04,440
like format verification can
minimize the attack surface,

972
00:39:04,440 --> 00:39:06,240
not only for the memory safety issues,

973
00:39:06,240 --> 00:39:09,390
but for other issues as well,
but it's not a silver bullet.

974
00:39:09,390 --> 00:39:12,090
As you can see here, there
is also other issues,

975
00:39:12,090 --> 00:39:13,890
and we need to keep this in mind.

976
00:39:13,890 --> 00:39:15,390
And also formatly verified software

977
00:39:15,390 --> 00:39:17,970
has a much higher quality
effects to enforcement.

978
00:39:17,970 --> 00:39:20,613
And also can prove that
dynamic checks cannot fail.

979
00:39:22,068 --> 00:39:23,940
If you have assurance of silver
plus it also enables much

980
00:39:23,940 --> 00:39:25,650
more efficient security efforts.

981
00:39:25,650 --> 00:39:27,600
And in short, most of the bugs,

982
00:39:27,600 --> 00:39:30,660
which we saw requires like
a deep knowledge and deep

983
00:39:30,660 --> 00:39:33,330
understanding of the
software and also hardware,

984
00:39:33,330 --> 00:39:34,230
not only software,

985
00:39:34,230 --> 00:39:36,630
you need to analyze entire
execution environment in the

986
00:39:36,630 --> 00:39:37,590
details.

987
00:39:37,590 --> 00:39:40,530
And in as a result, the
bugs, which we found,

988
00:39:40,530 --> 00:39:43,470
it's a more architectural
bugs, more design issues,

989
00:39:43,470 --> 00:39:46,140
more deeper problems, essentially.

990
00:39:46,140 --> 00:39:49,170
And again, in short, just to repeat again,

991
00:39:49,170 --> 00:39:51,120
the summary of the reviews,

992
00:39:51,120 --> 00:39:52,680
if you lose memory safe language,

993
00:39:52,680 --> 00:39:55,830
we internally found around 40 50 bugs.

994
00:39:55,830 --> 00:39:56,820
In average,

995
00:39:56,820 --> 00:39:59,483
during the review in the
timeframe of four weeks in the

996
00:39:59,483 --> 00:40:02,250
memory, safe language,
we found only five 10,

997
00:40:02,250 --> 00:40:04,370
even if you spent 50% more

998
00:40:04,370 --> 00:40:06,090
of the time on them on average,

999
00:40:06,090 --> 00:40:08,580
but the bugs which we found
is better quite of the bugs.

1000
00:40:08,580 --> 00:40:09,993
So that's all thanks.

1001
00:40:10,954 --> 00:40:13,954
(audience applause)

1002
00:40:18,720 --> 00:40:20,760
And we could take some question.

1003
00:40:20,760 --> 00:40:22,510
I think we still have four minutes.

1004
00:40:31,650 --> 00:40:32,483
Come on.

1005
00:40:53,370 --> 00:40:54,203
So the

1006
00:40:58,890 --> 00:40:59,723
So the question is

1007
00:40:59,723 --> 00:41:02,580
how many bugs in Spark
we found in Nvidea when

1008
00:41:02,580 --> 00:41:05,490
we analyze the software written in Spark?

1009
00:41:05,490 --> 00:41:06,323
So in general,

1010
00:41:06,323 --> 00:41:09,840
we haven't seen any software
where we did not find the bugs.

1011
00:41:09,840 --> 00:41:11,430
That's what we can say. So essentially,

1012
00:41:11,430 --> 00:41:14,310
every software which is
written have some bugs,

1013
00:41:14,310 --> 00:41:17,070
eh- we haven't seen
anyone without the bugs.

1014
00:41:17,070 --> 00:41:20,760
Although also it's worth to
mention that the software which

1015
00:41:20,760 --> 00:41:23,280
we write, usually it's a huge
in scale, it's complicated.

1016
00:41:23,280 --> 00:41:25,080
And we also have a custom hardware.

1017
00:41:25,080 --> 00:41:26,730
So this is very difficult to model.

1018
00:41:26,730 --> 00:41:31,410
So most of the bugs we found
in this area, how many of them,

1019
00:41:31,410 --> 00:41:32,550
we cannot say the numbers,

1020
00:41:32,550 --> 00:41:35,340
but certainly it's significantly lower

1021
00:41:35,340 --> 00:41:36,990
than in the memory safe language.

1022
00:41:37,860 --> 00:41:39,260
Memory safe, sorry (laughs).

1023
00:41:44,970 --> 00:41:46,387
- Thanks.

1024
00:41:46,387 --> 00:41:47,708
(audience applause)