Dear viewer, these subtitles were generated by a machine via the service Trint and therefore are (very) buggy. If you are capable, please help us to create good quality subtitles: https://c3subtitles.de/talk/731 Thanks!
All right, your speakers
are Felix.
He is a student at
the Castro Institute for Technology,
the baseline for a talk, basically
both his bachelor's thesis, which was
actually awarded the.
International Student Award for
Undergraduate Research at the
University of Vienna,
um, we been on stage is
Vladimir Klibanoff, who
supervises teachers and provided
feedback and guidance.
And to help, they also
developed an automated tool
using that framework.
So please welcome them with a
warm round of applause.
Thank you very much.
This work was supported by Karlsruhe
Institute of Technology and also the
German National Research Council.
Under the priority program
are a three research into reliable,
secure software systems.
And sometime ago, we started to ask
ourselves the question, how do we know
that our engines are working properly?
And not soon after we started asking
the question, we actually realized that
the answer is spoiler alert.
We hope they do.
And.
This is an important question.
Does anyone have any idea what this list
represents?
Um, the well, the younger
generation probably does not remember
this event, but the older generation
will know that this is the list of
services that were affected when
Debbie and Miss Page, the open as
parent. And as you can see, this is
almost everything.
So, uh, wonderful example
of a single point of failure here.
And, um.
Well, this was
a really defining moment in
the history of pseudo random
number generation.
This is really great example
of a great story.
We will go a little bit into technical
detail later, but I would encourage
you actually to talk to Google it and
to read the full account of what
happened. This is really thrilling story
of fine Greek tragedy where
technical, human
and organizational factors aligned
to create this perfect storm that
actually caused, um,
well, for two years a back door
in all of these things.
And well, at some point,
it was discovered there was a talk
at the 25th Congress about
that, and then one could ask
ourselves, well, what actually happened
afterward?
So what were the technical measures
taken to prevent reoccurrence of such
incidents in the future?
Well, the
technical consequence of the disaster was
to add these two comments
that you see here.
Um, so what what what happened how
the disaster came to be is that the Deben
maintain due to some
quite reasonable logic, to remove this
particular line in
the code. And essentially, one reinstated
the line and then added the comment to do
not remove this line.
This is a very specific remediation
and this was it.
Um, so
in the end, we will see that one can
actually do better things
to make sure that things are working
correctly, but also that they're good
technical reasons.
High quality assurance is difficult.
But nonetheless, and while we're here
talking about comments, I would
like to show you some more comments
from other implementations
of other hearings just to give you a
feeling of what the state of
implementation is in the wild
and.
These are not some obscure
implementations, these are actually
things that you have on your devices.
This is what we use every day.
And you might be saying, well,
you're not being fair.
You are taking things out of context.
And indeed,
this is in some sense, right.
But I can also tell it's only mildly
unfair and there is not a lot of context
accompanying these things.
And also, they really do transport the
feeling that at least I get when I look
at that code,
for example.
So in one implementation, we read
Hashemites to use the number of binary
taught by computers to use to form a wide
area returning by the next pieds method.
Note that this implementation uses
Moabites and that is defined in the above
specification.
What?
Uh, so
it is it is really difficult to
understand what is going on here.
And to this day I am actually not quite
sure.
I think the author just wanted to say
we define that the Schavan return
to digest of 20 bytes, but
in the end.
The intent of this message
is completely unclear.
And if you more so, here is another
one, put the data into the entropy
at some data from the unknown state
recede, we see
terminology is really difficult
and it is so.
But you have to make
an effort, take
some random data and make more random
looking data from it.
I don't know what it means.
Um.
Yeah, the
only comment at a particular
place in the code.
Yeah, this is this is
the code that has the potential to put
a backdoor into all your applications.
Uh, yeah.
Here is here is another nice
statement.
This is from the end user documentation
of the period. And here one has really
to say, hey, you have end
user documentation.
Great. Really, really fantastic
do this.
But of course, nobody is perfect.
So at a particular function,
it just says be very careful.
Otherwise bad things happen and you have
no idea why
you're supposed to be careful, how you're
supposed to be careful what's going
on.
Um.
To to to make well, to
to make the point a little bit more
precise, so I'm showing this, of
course, to entertain you, but the idea
here is not to blame the developer
and not to say, well, this was a bad
developer.
If it were a better developer, then this
wouldn't be there.
And I will not
make these mistakes, of course.
Now, if you think so, you have it coming.
The point is that there is well,
there is a process and they are actually
natural forces that make
things the way they are today.
And typically things start with some kind
of personal project or
research project, or sometimes it's a
clean room implementation
and well, slowly, Fujiko
down there and then people notice.
And then maybe in the meantime, it ends
up on a bigger project
that is under the auspices of some
respected entity like the Apache
Foundation or Mozilla or something else.
And then in the end of the supply chain,
there is some kind of dealer and inventor
who has a need
for appearing period.
And then they will go and say, oh,
there's this code.
Um, and, uh, it
looks really great. We'll just
incorporate that into our product and we
will not do any further due diligence.
We solve our problem.
Schippert And I think
these guys are actually responsible for
most of the problems that we have.
The vendors who take the open
source code to not put in the effort
and just include it into the product
and ship it up.
So we need to really take care of the
process, which is
putting software on our devices.
I don't really have a better
recommendation here, but let me show
you one more example.
So this is more or less the only comment
attached to critical function of
yet another hearing.
And I can assure you, if you know what's
going on, it makes total sense.
But if you do not know what's going on,
you have no chance to understand it.
Um, so
we need documentation, but we need
actually to write documentation for
people who do not understand what
is going on because otherwise your
documentation is useless.
What we find
works best is if you have something like
a one page design document
where you explain in abstract terms, in
mathematical terms, the design
of your Premji and then you can refine
that into the implementation.
So it's not just sufficient to add some
comments to the functions that you have
in the code.
And but
I should say it is really good that
you have this kind of comment there.
So it's abstracted away from the code.
But you have to phrase it in
a different way. You have to to
target the different audience.
And in this hearing, at least, there
was a link to a scientific paper that
describes kind
of the inspiration for this kind of
schema. And that was
that was that part was really helpful.
Anyway, you hopefully get an
idea that there is a need actually to
to to do something and there is a need to
improve the state of things and there is
a need for quality assurance and
well, what are the options
for quality assurance that we have today?
So here is a top five of things you may
or may not be doing.
And the first one is what one does
with whatever other
software that you have.
You typically have some kind of system
test or maybe even apply
some formal methods to verify that
your software does what you think it
should be doing.
But in this particular case, this
is very difficult almost.
Well, I would say impossible.
We have to say that the specification
of appearing, it's it's a piece
of software that takes a
little piece of random data somewhere
from outside of the system and then
stretches it into a stream of
other data that is indistinguishable
from random to computationally bounded
observer.
So it is actually not a
property of single
output stream.
So you cannot really check
this property by looking at one output
stream that you are having.
You cannot try to test for the particular
stream that actually tells
if this is true or not.
It is a property of all the output
streams that appear and can produce.
So this is really
difficult here.
Um, the thing that one could
be doing is to have.
Unit tests for individual units
that have well-defined functional
behavior, for example,
we know is also from implementations in
the wild, that it is difficult to
implement a circular buffer.
It is indeed surprisingly difficult to
do so correctly.
But of course, no self-respect and C
programing goes and says, I will
implement the data structure and I
will write tests for this data structure
and then I will use this data structure
in my other code.
No, everything is baked into one
monolithic thing because
that's what one doesn't see or because
performance, I don't know.
It doesn't really make
sense. So the recommendation
here is clearly try to make your code
modular, let the compiler take
care of the compiler will in line things.
Don't worry about that.
There will be, if any,
very small performance overhead.
But then you obtain units
with clear functionality and you can test
it and be safe.
And they say don't risk
things then.
Another kind of testing that one sees
from time to time, and also this is
recommended from time to time, is
statistical tests.
There is a whole bunch of them here, a
few examples.
What these do, they look at the
individual output stream
and they try to find bad
smells in the stream.
So if your stream has way more
zeros than once, then this test would
say, oh, this is suspicious,
OK, you can do
that.
But it is not helpful and it is not
helpful for one reason because.
Well, most of the things
we are talking about here are
cryptographically oranges, and that means
on one side that they are intended
to be used for cryptography.
The output is intended to be used for
cryptography.
And on the other side, that they actually
have cryptographic building blocks within
them. And these cryptographic
building blocks have the property that
once you pipe whatever you
have through them, the output
will immediately satisfy
this statistical test.
So your appearance can be as almost
as badly broken as you wish.
It will still pass this test
so it doesn't hurt to do them.
Sometimes regulatory agencies require
them. These are remnants from the days
passed when the pure energy output was
not meant for cryptography, but.
Essentially, this is a waste of your
time, you can skip this step.
On the other hand, what is useful, but
what is also not done enough is
regression testing.
Regression tests are
collections of reference seeds
and reference outputs
and.
By comparing the output of your
implementation with this reference
values, you can at least
be as good or as bad as other
people in particular if you are
implementing.
Uh, this particular appearing standard,
which not many people do, but what some
do you have this reference values
in the standard and so you can be as good
or as bad as the standard and
you can hope that more people have looked
at the standard.
So also, if
you change something, if
you do maintenance and it is
not supposed to change the outcome, then
at least you can be sure that you didn't
change something that you didn't want to.
So do regression tests.
This is really helpful.
Not done enough.
Well, almost.
Almost the only thing that we see
for many, many implementation, this is
really the only thing that
stands between you and the disaster.
This is the manual code review.
So people are just looking at the code
and say, OK, it looks fine
and think about it.
Would you accept such a situation
for any other piece of software?
Doesn't matter. How unimportant
would you feel?
Fine. If I told you this piece of
software was never tested.
We looked at it. We think it's fine.
But we never tested.
We never did any quality assurance,
any technical quality assurance.
Would you accept that situation?
This is what you have at the center of
your security infrastructure.
Um, so.
We do not have bad news, but we also
try to improve things a little bit, and
here we did two things.
First, we looked at many,
many incidents with springs that
occurred previously, and we
identified a particular property that
has been violated in many of these
incidents.
And on top of that, we also
developed a tool, we developed a method,
a particular specialized static analysis
that will find violations of this
property in your implementations,
in real world implementations,
open SSL and the like.
And in this talk, we will try to
explain what the property is, what
the tool does, and what was the result of
applying it actually to implementations.
But first, I need to.
Explain a little bit
how a typical parent works,
and this is a very simplified model
in practice, of course, things
are more complicated, but nonetheless,
in the middle you have,
um, some kind of state sometimes
called entropy pool. But this
is this just the state of entropy is
collected.
And then there is a seating function that
takes this little piece of
random seed that is.
Has its origins somewhere outside of
the system. Typically, you ask the
operating system for it in the operating
system, will also typically derive
it from hardware, from
disk latency, from timing
of your keystrokes, from interrupt timing
and so on.
So then you obtain this
kind of very short about 20 bytes,
typical value of
random speed and you transfer
it into your state and the
rest of operation goes in cycles.
And in every cycle you somehow
perturb this internal state
and then you derive a little chunk of
output from the state
and then the next cycle begins.
So you perturb the state again and derive
the next chunk and so on and so forth.
And then you obtain a stream
in the model.
All of these things that you see here
deterministic.
So all of this
procedure is completely deterministic and
the only source of randomness,
the only source of natural determinism is
actually the choice of the seed.
So we will go ahead and we will
actually treat this
whole cascade as a function
from an MBA seed to and
end with prefix of the output stream
genes for generator.
And you will see the symbol from time to
time during the talk.
This is what we are concerned with.
And
before.
I explained the problem that we actually
solve. I would also like to
make clear that there are a lot of
problems that we do not solve and it is
important to name some of them.
So first problem that we do not take care
of is the choice of the city.
This is a difficult problem, but it
is completely orthogonal to making sure
that this procedure is working correctly.
And there was a talk about
seat selection yesterday.
And, uh, well,
there are also popular mistakes then you
can have in the choice of the seat.
For example, if you ever seat
with something related to time,
you will have a bad time.
Um, yeah,
for reasons first, because the
typically the resolution of the time is
not large enough. So your seat will have
a small range and also because
time is often a
publicly known entity.
So the attacker might actually know.
And now know the seed and then
all the construction collapses, and by
the way, if you are doing this in the
embedded world, then I'm really sorry.
You have very few options to
get good seats.
But again, luckily
not our problem.
Um, the other thing
we are not considering is.
Typically, all of these functions that
you have seen will contain cryptographic
building blocks and here
we assume that these blocks are there.
We can actually check if they're there,
but for the time
being, we'll just assume that they are
there. And also we will assume that
they are really one way, in
particular colloquial sense.
There has been only one incident, the
dual elliptic curve generator.
Also quite thrilling story.
You can you can Google that where it
turned out that these
functions were not one way for everybody,
but they were not one way for
the NSA.
But, uh, yeah,
but that's that's a completely different
thing. And another thing we do to take
care of, uh, is we don't take care
of very powerful attackers.
So here we assume that the attacker knows
the code of appearance, but they do
not know the seed and they do not know
the internal state.
If you have an attacker that knows
some of these things, you're
on your own.
If a three letter agency is standing with
the tempest when in front of your
building, sorry, we cannot help you.
Um, but we cannot
we can help you detect entropy
loss in your implementation and entropy
loss. There are several different ways to
define entropy loss.
So all of the following are equivalent.
For example, if you have
two seeds that produce the same
output stream, this is entropy loss.
So there is a collision and European
energy.
And this is equivalent to the fact that
part of your see, this is where the
collision will be is not used for the
output. It also means that there are
fewer possible outputs than you have
seeds. And here you already get the
intuition why this is bad.
So you are wasting some of the entropy
you have collected in your seed and
probably you are wasting quite a lot of
it.
And then your seed, your output will
be much more predictable than
the seed. And this is bad.
We do not want this mathematically.
It all boils boils down that you have
a problem if the function G is not an
objective, this is
what we will be looking for.
So we have a whole machinery
to check if functions are in
a..
Security, by the way, that's an
interesting observation, is often about
injectivity, it's it's either about
injectivity or not injectivity, but many
things like privacy and integrity and so
on can be defined in these terms
mathematically.
Just quickly, this is just a mathematical
formal definition of
injectivity of the function.
And this is indeed what our tool will be
checking. But now
we'll show you examples of entropy
also that you get a better intuition.
So that's first come back
to what happened in
the division of SSL disaster.
So this is this is the model that
we slightly adopted for the transparency.
We adopted it the way that we have here
in the mixed function edition
to edit the PID.
So the SSL PMG
does not only take the seat as a random
input, but it also takes
the process idea of your process as
random input used in
the mix function to perturb
the state and then derive
output.
So then what happened?
That line was removed and yeah,
the seed was cut off.
Badly, they had the video
here contained in the mixed function, so
the stage, the output of the energy was
still random. Looking out, if you have a
punji and get all this the same key
somewhere, someone would have noticed
that.
But this way it was
not wonky, but thirty
two thousand keys.
So it was not easy to
notice that.
And as you can see, that's that's an easy
instance of entropy.
So you're not using part of the CJA,
you're not using anything of the seed.
And what we can learn from here is you
should separate your energy out, take
the random data at
one place, use it in some
way, but not at random data
at different points in your code,
but also help us later when we talk
about how we verify that
the code works correctly and does not
lose any of your entropy.
Another prominent example is what
happened in the Android pseudo random
number generator, so this
is a large Java Intertrade
that's used in that period.
It's called seed, but the seed is
only here.
Generally, it's the whole internal state
of the P.A.
and the seat should be
written from Java interests
zero to drama and such as for yeah that
would be five Java Indigenous feet.
That's good for
a good number of output streams to not
be able to.
Do attacks, but what accidentally
happened? Yeah, they would want to
try the counter and the padding here
afterwards, but what they
did is they did not update the
pointer, so they wrote the counter and
the padding here overriding more
than half of the seats.
So what was left were two Java integers.
Sixty four. But that's not much
that's more than what was left
with Davian. Yeah, but it's
you see more than the half is gone.
So that's a clear example
that you cannot detect such issues
when looking at the output and looking at
how the PMG works.
And the nadelberg that's the one that
we detected was like Decrypt.
And we'll discuss that in greater
detail later.
So what do we do to analyze,
first of all, the user has to take that
the user of our tool use that wants to
analyze has to take the pinchy and
isolate the currently isolated,
deterministic part, remove other
all other entropy sources
that are not directly the seed
so that the tool can check that the whole
random data from the seed is included in
the output.
Then it has to choose a scope
which we want to analyze.
So we have to define a fixed length
of input and output length that we want
to check injectivity.
So, yeah,
typically we we do that and just
take one cycle.
Then the user needs to
find a way around the crypto functions
because the crypto functions are
essentially hard to be proven
ineffective. That's the whole point
of the crypto functions.
So we need to circumvent
that in a way that our Trouville can
prove around those crypto functions that
the rest of the code does its job
correctly.
And then our tool comes into play,
generates the condition
it generates the condition that we
described earlier and verifies that this
condition is true.
And finally, the weekend
results. Is there a yes
or no?
And I would like to show you that in
short now so.
What's here, that's the that's
part of the open here, and
that's the function that would add random
data to the appearance's internal state.
Now, that's the seed arrow.
Pillow comes the part where where
where something was moved and what
you want to do now is we just want to
introduce a simple problem that I
have here.
The problem kills one bit
in the input, so we will not
use one bit of the input.
And now I will run the analysis.
And the analysis will now translate to
the program of
energy into a logical formula,
a formula describing what the
G actually does.
Then our tool comes into play,
duplicates the formula and specifies the
condition that we will to have two
different inputs and when applying
this function, this will result
in the same output.
And finally, we have here
solver for such a formulas
and the formula that the solve quickly
said, yeah, we have a we have
a solution here.
And the solution is giving those two
inputs.
We receive these same outputs.
So now you have to check
what's wrong.
Oh, oh. Here, here's exactly one
bit wrong.
Why is the Punji not using this bit?
So in the end, you would probably
want to debunk that and hopefully
stumble across the instruction that we
edit here.
And remove that again,
and then you can run the analysis again
and again, the whole program
gets now translated into a logical
formula.
That that takes its time, so that's
a 30 megabyte of logical formula,
then we double that size
because we want to have two invocations
of the program, which have different
inputs resulting in the same outputs.
And finally.
Yeah, the the solar cell
shows, yeah, we have we have no example.
There's no example where this function
loses random data.
So how can we deal
with this cryptographic functions, that's
the part that I skipped and Vladimir will
now take over to
explain to you how we do that.
Um, yeah, so this is the bit that we
have conveniently swept under the rug so
far.
I will show you an example.
So the thing that you see at the top,
this is one invocation
of the shower, one that
is part of the seed.
Um, the function of the openness is
healthier and that takes the
seed somewhere from outside and transfers
it into the internal state.
And what you see here is a concatenation
of one, two, three, four different
things.
And.
I can tell you that on the first
invocation, only the
third parameter here, only the buff,
this is the actually the parameter to the
function will contain entropy
and all the other
parameters have fixed values.
And altogether, this is
sixty eight, I think, bytes
long. And the short on cash
will derive a 20 byte,
uh, digest from that.
And the cryptographers promise
us that, well
if the
input has more than
well at least two to the power of 160
different values, then we will see
at least two to the power of 106, the
different outputs.
This is what we hope for.
But again, as I said, we cannot
really check for injectivity of
this call of this function
because this function has been
specifically designed to
make this very expensive.
So if we could check that, if we
could check the injectivity here, that we
would basically have an attack
on SHABAAN or we could prove
that it's that there is no attack.
So we cannot do that.
We have to simplify the problem
and we simplify it by offloading,
um, the reasoning about
one onto, again, onto somebody
else. So we say the cryptographers
take care of the behavior of
one and we only check the code
that is outside of Chavan
because this is the code that is
nonstandard and this is the code that is
error prone, the SHABAAN
itself. This is a standard primitive,
their standard implementations.
You have standard tests used.
Um, it is difficult to break
that, but it is very easy to break the
code outside of it.
So we will look only at the code
outside and we do this
in the following manner.
So here is a
little visualization of the same
call that is shown on top.
Uh, and.
Now, there are two steps, actually, to
replace this call with something
that is easier to reason about, but at
the same time, that still
gives you useful information about all
the cold outside.
So we want to replace that call
by something in a..
Any particular sense.
And there are two steps to that.
The first step is to identify
the part of the input that will
contain the entropy
and.
You could say, well, but this is
difficult, but in fact, it is not as
difficult as one thinks so
first.
We let the user do this, we could also
automate that, but for the time being, we
didn't bother.
So we let the user do this first with the
contextual clues, with the names
of the variables and so on and so forth.
Then with the information
that we provide
on counterexamples.
And I will talk a little bit
about that later.
And also, you could just try
different things.
So here you have a choice
actually between three different things.
So the fourth is not big enough for
for the 20 byte output.
You can choose between these three
things. You can just brute force it if
you choose wrong that you will get a
false alarm in the end.
So the whole construction will not be
objective and you can fix the
problem and try again.
So.
First, we find.
And input parameter with the length
of 20 by it, because the output is 25.
And then we have to replace that
function by something else.
And here we have two possibilities with
what to replace it.
And the first one is
very simple. We can just replace
this Chavan function by identity.
We can just copy the content
of the seed to the output.
This is very simple and it also
has many advantages because
if you do this, um,
well, with a little bit of luck, actually
a holperin construction will become
an identity function.
So the output that
the parent produces after you do this
replacement will look very much like the
seed, maybe the seed repeated
and you can test for that.
So you can immediately check
that all the other code is
fine.
This construction is not sound because
you have replaced one function with an
unrelated function, but
often or most of the time it will work
and it will work and it will be OK.
So the results will be trustworthy
because you can imagine a
typical parent is actually
agnostic of the concrete data that
you have in your seed.
So it would be it
would be strange if the parent would do
different things, depending on what
exactly
the data is that it is operating on.
So you can actually substitute
this data for something else.
You can substitute the one hash by the
just copy of the seed.
So this is this is very useful.
This is great for debugging.
Uh, you can already test many things for
this replacement, but it is still
unsound.
And what we can do because
we are not just testing things, but we
are applying a formal reasoning
tool, is that we can.
Here, instead of this
identity function, use something else
we can use a mathematical construct, we
can say we replace
at this particular.
Um, this particular function is an
abstraction, we replace it with an
underspecified injector
function, so we do not say what it is,
but it is something that is injected.
And this is an approximation of the
behavior of the hash function here.
And the results that you get will
also transform to the original
code that you have.
So we would typically do the first thing.
And that will help us to find bugs,
um, it will show us collisions, if
the any we can actually look at the
trace, we can we can see how the
speech pattern of the seed propagates
along the implementation.
We can just print
at print statements along the way and
we see where these, um,
how this flow is working.
We will not show that today, but
we do have a nice visualization there.
And then in the end we switch over to the
sound of idealization and then we prove
that the positive result that we get and
then the good result is indeed.
All right.
A few words about the implementation.
So little commercial break here.
We could get
that far because we were standing on the
shoulders of giants and the two giants.
Here is the CBC
Endemol check.
It means it is a static analysis tool
that you can, uh,
feed your implementation in here
in Java and it will
happily take it, even if it's something
complex, like open SSL or Linux kernel
or something.
So this is this is really the advantage
with this tool.
It's a really robust and fantastic tool.
It will explore the behavior of
your program to a particular depth
and it will detect.
Uh, well, certain things that can
detect predefine things like Buffa or
flaws and so on, but it can also check
user specified assertions.
So even if you have
nothing to do with cryptographically
ranges formally recommended to use that
tool to gain to gain
confidence in your implementation.
And on the other hand, we are using
many such Sasolburg,
which is also quite an amazing piece
of technology.
I mean, there are, of course, other
tools. The other verification
tools and other such told us this is just
what we are familiar with and you
know, that satyrs and then complete
problem. But it doesn't really matter for
us in practice. We can feed formulas that
the gigabytes and size to the solver.
And within seconds it will tell us if
this formula says that is viable, if
there is a problem in the appearing or
not, and we use
these tools to combine
these tools with our
own code.
So we use BMC to
generate a description.
Of what the parent does as a formula,
and then we combine this description
into this definition of injectivity that
I have shown you previously, and we feed
the result in two minutes, 10 minutes,
and we'll see if it is possible to find
a violation of injectivity in this
formula.
And if it does, then we show
the resulting traces for
the two seats and the same
output to the user.
And they call procedures you have seen
takes some seconds so you can use
you can use the tool interactively.
What are the results from applying
this?
So that rule was applied on various
pages and first the good parts.
So we check those.
We did not found anything suspicious
there that we could verify
that the punji code around the
cryptographic primitives is objective
and does not loose entropy.
Now, we, as I said
previously, had this known problem,
when we reinstate the problem, we would
have detected that.
And when we removed the problem, we
detect no further problem.
You know, Vanessa's l
that's quite similar.
Yeah, we would have detected if you
remove the code.
We also detected other problems
in code that is
may or may not be used in practice,
and that has
problem managing the circular buffer
with the array going off by one
writing one byte outside the buffer
doing doing strange stuff.
But all that was not very fatal.
Yeah. And then finally, we
found the critical back in
Viji that
we then cost to be fixed.
And I will show you how
that works, how the other back
works, whether that's the problem and how
the bug could be gone undetected
for so long.
So.
So first of all, there was there
was a paper that proposed
how we could operate, apparently, and
first I would like to show you how it was
designed to be implemented.
So we have the Buffa with with
random data here.
And what we're looking at here
is the perturbing function that
mixes the buffer internally
in some strange way using cryptographic
primitives. And what was suggested here
is that we would take
84 bytes of the
of the buffer.
Hash them using hash function and
override the middle
20 bytes that we
have above here and then
this this buffer would go
up there again, you would ask
after hashing, we would move to the next
to the next block and hash
that again moved to the next
block and so on and so on until
the end where there that
happens and wrap around.
And finally, the last block would be
calculated by hashing this
blocks and the block here at front.
Then we would get the last block.
And then finally, this this buffer would
be handed out to the user as this is your
random data.
We had an hash function that was
that that took smaller input sizes, not
eighty four, but sixty four bytes,
and for reasons that are not
that clear, they decided
to just have a 60 bytes
hash function that just left the middle
bit out here.
Yeah, we are overriding that anyway so we
can do that. I don't know really what
was the intention, but what happens
with the dog is we would have them
write that down and so on and
so on and so on
until the end.
Where would take this one,
this one, hash them and write them here.
And this buffer is now should not be
random.
It's that buffer really random.
When we take this block and this
block, they are here
and here again and
hash them we to get this last
block.
The buffer cannot be run.
We can calculate the last 20
bytes when we use these
44 and these 20 bytes,
hashing them would get exactly
this block.
Yeah, so so that's that's
what happened, though, that's
that's a thinking problem.
Yeah, that's not really off by one
implementation problem.
But that's yeah, that's yeah, that's
essentially.
What happened there?
So the.
You know what the consequences are?
Yeah, I'm
on keys, they were hopefully
not that bad, but
yeah, hopefully we spotted that problem,
that problem lay dormant there
for a long period of time,
had several security audits.
Nobody spotted that.
Yeah, we looked at the code.
It said initial import.
So for several
years, years old and or we
can take away from that is that
audits are necessary.
Looking at the code is necessary,
that the code has grown too complex
to to fully understand
it manually.
So we have to take technical assurance
to verify that
the code is correct.
So thank you for your attention
and the.
Thank you.
If you have questions, please line up at
the microphones on stage and it's all
there are four of them,
and if you would like to leave now,
please do that quietly so that other
people can still listen to the Q&A
on the right hand side.
The.
Yes, hello.
Thank you for the presentation.
Very interesting.
Is there some kind of implementation
for mere mortals like us that
can take their
current stack of whatever they have?
For example, generate
a.. 20 RSX,
upload them to you and you tell
us whether those look and
or random enough from each other
and thus my system actually generate
correctly, you know?
Yeah. As we as we try to explain
the problems that we are looking here at
cannot be detected when just
looking at the output of the PMG.
So when you have one output stream of
your fiancÃ©e, that would still
look random. So statistical test
suites, one, detect anything.
So the only thing that you could do is
check for known issues and have
known all all streams that the known
issues produce.
So with the with
the open SSL disaster that we luckily
only only a few
so that you can have all those thirty
thousand keys and check against them.
But just looking at the keys and
not knowing what to look for,
I think that's not possible.
Apparent on the right.
Yeah.
So could your techniques beneficially
be applied to other cryptographic
primitives like block ciphers or the
building blocks that go into block
ciphers?
Um, that's a good question.
So you could I think
you could apply them to particular
auxiliary code
that accompanies the,
um, the primitives.
So the techniques that we've shown you
are purely information theoretical.
So they are not concerned with
cryptography as such,
but also in cryptographic code
you need these things.
So for key expansion, for example,
Qiqi expansion is supposed to have the
same injectivity properties you could you
could apply there.
So there are some applications, but
they are also very clear limitations.
All right, let's it's that question from
the IOC.
No, it's not OK to let that
one in the back.
Hello.
If I understood your definition of
entropy correctly, you mean if you have
two seats that go to the same
output that you would consider a problem?
Um, and you had several
examples with one, I think for myself.
And I think the Linux kind is also using
Shravan. And that would mean, as far
as I understand, that if you have
a hash function with, uh, with a
collision, then this would
generate a situation of entropy loss.
So what that mean that and
we assume that one will have collision
problems within the next couple of years.
So is there any practical problem
if you use a non existent
hash function here?
OK, so this is a little subtle.
Um, there are two answers to this.
So first, um,
well, first, we are
trying actually to look at the code that
is outside of Schavan
because this is where the
mistakes often are.
So we try actually not to say
Siobhan is someone else's problem,
but also to be more exact, the
collisions.
So we are looking at injectivity from a
20 byte input to a 20
byte output.
And of course, if you find a collision
there, then, well, this will
weaken your power and give a little bit.
But, uh, hopefully they are not too many
of these collisions because if there were
too many, they would be easy to find.
But at some point, of course, you also
probably have to upgrade the hash
function and you up your energy.
So
it's very we can discuss that later in
detail.
OK, on the left up front
in the theory of, uh, deterministic
on the notions of forward
and Peckford and enhance
that secrecy, um,
as I understood, your
theory is going forward.
So detecting entropy
loss, would it be possible in
principle to detect,
uh, not fulfillment
of enhanced Peckford
secrecy? So if you know
or so the output
and in the state to go
backward to
guess form outputs?
Um,
that's a good question. I will have to
think about that, OK.
Yeah. I think we
are not looking at, uh, secrecy
in forward secrecy
or backward secrecy.
We are just focusing on two
different seeds derive different outputs
so that that does not have
any implications on whether we
have knowing some random output
means that you can calculate the next
random output or the other way round.
Yeah, but in the sense it's looking at
the injectivity
of two of the three functions and
what we need for backward secrecy
would be the inverse function, not
not only so the inverse function would be
having the output stream and being
able to derive the seed.
But what factor secrecy would mean
is that you would have a part
of the output function that is behind
other states.
So I don't need to
see it. But, uh, in the state.
And that the G function is from the seat
to the outlook.
So, yeah, OK, but
just to clarify, the attack model here is
that the attackers observed the output
and tries to brute force the seed.
This is the attacker model.
If you want more things, you need to the
model.
OK, we do have a question from the
Internet.
Yeah, basically we have two questions.
First of all, Agonistic is asking
our physical implementations of R&D
better or do we need them to test the
same way?
I think we need to test them the same way
and yeah,
because they typically also have some
kind of hardware source of randomness.
And then there is this deterministic
expansion also on top of
that. So you need to check that.
Yeah, the answer is you do and
you can.
Thank you. And second,
the IOC or
some people on the street were not able
to see your explanation of the
new piggyback.
So could you please repeat that
without using the laser pointer?
OK, so the whole
problem finally boils down to that.
If you take blocks that
are not overwritten, so
they are visible in the output stream and
have them together using the hash
function that you hopefully know,
having the code,
then you can derive from that the last
20 bytes.
So.
First 44 and
not the last, but the before last 20
heads together, we'll
give you the last 20 bites.
And that's a problem because that's not
when.
Maybe not the way to formulate this
is when you have this dream and
you are looking at the last chunk in the
stream, then everything
that this chunk depends on
comes earlier in the stream.
And this is the problem.
So when you output the stream to
to the observer, the observer can
observe everything that
is needed to calculate the last chunk
in the stream. So there is no
more data that the observer
doesn't see going into the calculation
of the last chunk.
And yeah, OK, that's
your first microphone on the right.
One comment about hardware
implementations, because
usually you take two and
it's entropy and compress
them first to one.
And that's because
you ask this question or comment
is a problem for the detection
of entropy loss, because you're too sad,
because your heart will have a bias.
And you said, OK,
that is just an offset of
the comparators, something like that.
The bias is OK, you
solve the problem is bias by
compressing two and bit
to one and bits.
And I think you're checkerboard
detect that as entropy loss because
you really take two
end bits, compress it to one
and bits. And so obviously and bits
are lost.
Yeah. We assume that the seed
indeed is uniformly distributed
in um well in whatever
a lengthy test so that there's
a hardware entropy source.
It doesn't have this uniform distribution
and by compressing it with a hash
function, you get a uniform
distribution.
And that's the first step to
send you expand from the uniform,
from the compressed version.
And then so you have to
be careful of them using your check
because the input is
not completely uniformly distributed
mostly, but not perfectly
ancestors', because hardwares,
analog design and you have offsets
and things like that.
The other thing I did of
checking excuse me,
please come to the question is
when you have something like this
is a problem.
I write the first
round of the first 32
bytes into a file and I check
each time I initialize my
fiancee and I check if
that pattern has been set before
and due to the birthday paradoxal,
if I reduce my
initial seed, I
get to the square root.
So then I have this
problem. I would have after,
uh, two hundred fifty
six iterations, I would
have a 50 percent chance to see
that I have a problem.
Yeah, yeah. But we showed, for example,
the harmony problem.
Yeah. And the margins are much bigger.
So they are 70 after
to kick up.
Yeah.
But if every user does this, check
every user a chance to
see it is pretty
good.
OK, the other one on the right please.
I am so at some point you talk
about, uh, checking the, um,
the generation by simplifying
the hash function.
So, for example, you talked about
replacing one with
Mohapi.
So I was wondering, you said
that some implementations,
um, could, um,
outputs, um, like
the C material in the
output when you use Mkapa.
Do you have any examples of that, like in
real punji implementations
of, for example, openness as well?
We'll do that.
OK. And then to make it clear, this is
just for for analysis purposes here, this
is, uh.
Yeah.
Uh, both on the left.
Um, I'm very happy to see more
formal methods, informal verification
popping up and making this useable.
So thank you for that.
And my question is, you said
that you can trace the Entropia, you
can trace the changes in state or
in the production function.
Um, how does this actually work?
Is this a feature of the C proof
stuff you used or did you implement
it? And how can you actually.
Well, go ahead and trace
where my entropy gets lost.
How does this work?
You show the other
the seapower and models
the whole state of your program.
And so every every position
where the the seed is used
are variables in the logic of formula
that C approver outputs.
And that way, uh,
that that tracks the data.
OK, but is this part of the of the
C approver or did you add this
to.
I think this is a slightly different
point. Uh, this is not part
of this approver. This is actually
something that we do
after the supernova analysis
has, uh, terminated
because. Well, what we do get is we get
the model of the formula and we extract
the actual seeds that exhibit the
problem. And then we run
the pairing with these two seeds.
And, uh, we output
the intermediate states.
Just we we write them on the console and
we show you side by side.
And you can so you use the the
the variables that satisfy
your
injectivity. And then by having the
two two sides to break injectivity,
you can trace.
OK, yeah.
All right. Thanks a lot to me in Phenix.
Please give them some applause for this
one.