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/1317 Thanks!
[Music]
please welcome Daniel and Tanya for the
talk about her about high assurance
crypto software
thank you so why is - scripto software
thing why do we worry about the
correctness of software or the quality
of software so just some recent news
results about well doctor getting broken
so badly that the private keys leak
these are just reports from October
November and this one nice deep and it's
a pond saying timing is everything so
these were some timing attacks which
completely broke elliptic curve based
cryptography so badly that the private
keys came out timing attacks are not a
new thing so back in the days when you
log into a server and that is looking at
your password it might be doing a
character by character check so for
instance you is starting by well let's
find out what the first character is so
he's sending AAA well BBB c bc CC now of
course none of them will actually work
that will be very surprising if this was
a right password but you do observe the
time it takes to say this password is
wrong and then you notice that ccc takes
a little bit longer to fail
yay CCC then you're trying CAA CBB and
so on and so on still fails in the old
tape about the same time to fail until
you're getting to see oh oh and then
you're trying again for the third
character and so on and so on and so on
so eventually you get the password and
this was actually a thing that was 1974
the Tenex systems there was an operating
system where you well back in 1974
before most of us were born here you
could log in and it would be just doing
this character by character checking so
timing attacks to break cryptography or
break security have been known for a
long time but of course things are
getting more subtle when you go into
cryptography rather than just character
by character comparisons so for instance
if you're implementing your favorite
crypto system be it if a Hama and find
fields or be at RSA then each time you
have to compute an exponentiation and
then you go back to your cup - 101
lectures and don't compute C times C
times D times
why do you remember that there was a
square and multiply algorithm which
tells you okay you're looking at the
bits of the exponent
so here I'm going for the representation
of D in bits I'm look in the lengths and
bits and then I start by initializing so
he can't run this this just sage code
initializing you're finally gonna be the
message in the RSA and then for each
step you're doing a squaring and if the
bit is said you're doing a
multiplication and this runs from well
the first bit we've dealt with already
so the second highest bid till all the
way to two to the zero which okay in in
sage this is well like in python so this
is the range is not included and then
you output the cipher text at the
plaintext now there are some problems
with this so if you're an attacker and
you know that your user is using this to
compute an RSA decryption then you
observe that this loop length gives us
some information on D namely the length
of D in bits this L was defined as well
how many bits does D have and then some
DS well this D looks rather short this D
is much shorter than n it's much shorter
than Phi of n so this would be an
unusual D and so it would leak that it's
a little bit shorter also here we have a
branch I go if this bit is 1 and not
then well I'll just continue so
depending on the level of fine-grained
access somebody could even see where I'm
going for a multiplication or just
moving on to the next squaring in the
worst case somebody could read out the
pattern of zeros and ones by just
knowing where they enter this branch
here or not now if you're a remote
attacker you only see the overall time
now I have a picture from something
similar it's not an explanation for RSA
it's a little too curved scalar
multiplication this is from a recent
paper from TPM fail and they observe how
long it takes to compute well they cool
in elliptic curves scalar multiplication
so you do double in ed instead of
squared multiplied and you can nicely
see that the bulk of the computation
well
most experienced skaters it takes this
long and if you have some leading zero
bits it's much faster to still somewhat
faster now there is some variability and
it could be faster because UD is very
sparse it could be just one and a whole
bunch of zeros and then another one that
would also be as fast as something which
is a few bits shorter but then more
dense so that you don't know exactly
whether it was short and therefore fast
or whether it was sparse
so few modifications and therefore fast
but if it's a lot faster it's probably
both the top bits are missing and
therefore you don't have modifications
there so if you're very fast you have a
good guess that this thing was actually
short and so there's a strong dependency
on the lengths that is also depends on
the density now typically your
implementation will actually not be
doing it I was surprised that this paper
include the Texians
found an example where you're really
going bit by bit because of most of the
time our time is very precious and so we
want to speed up things so if you're
taking your favorite number like 14 19
also known as 3063 and your writers and
binary and then you want to do your
multiplication while you're scaling on
vacation starting from the top bit all
the way down sooner to the RSA loop but
you want to save on the number of
multiplication slash squarings
then you would be grabbing two bits at
once you pre-compute a few values you
can pre-compute your C C Square and C
cubed and then to compute this
exponentiation you kind of doing two
squares at once so you're doing two of
these positions at once the first one
you can skip because it's both zeros the
next one the one one gives you a cube so
we starting with C cubes which we nice
enough have pre computed now we're
moving on by two bits so instead of
squaring once we scare twice so that's
why the fourth come in here next
position is one next position is two so
we see a multiplication by C
computing the fourth power by C squared
so in everything is like in the previous
loop except for we doing two bits at a
time and so instead of saying oh if the
next bit is said we do a multiplication
we look at the value of the next bit and
then select from C C squared C cubed or
no modification and this definitely
reduces the number of multiplications
this would have normally taken seven
modifications and this way we only take
four it doesn't change the name of
squarings now this will smoothen out the
effects of having a sparse integer
because well as long as there is a
single one in the window we call this
thing window here then it will cause the
multiplication whereas normally would be
one multiplication and no multiplication
here so when you look at the traces from
this then you get much more accentuated
boxes whether something is zero at the
beginning or not because most of the
other steps in particularly for larger
windows this seems to be taking four
bits at once
so for that larger windows most of the
time I mean if you have four bits then
there are 15 cases or a 16 way you have
to do multiplication and only one out of
those 16 we don't need a multiplication
so it accentuates the length issue and
kind of you have no idea whether the
bits were set or not I mean how many
bits were set now how much does these
few bits do of course you don't want to
leak your secret RSA exponent you don't
want to lick your defeat Hellman but
it's it's not too bad there is it's
really you would need a lot of knowledge
you need to have either extremely short
or extremely sparse to actually break
something with us it's kind of worse if
you're having ours
avis Chinese remainder theorem
decryption because then you can do some
combination tricks so there's something
we gave a few years ago how you can
combine information if you know a few
bits of D of D motor opinion of D
modular Q and then you combine this so
then you'll learn more when it really
goes bad is if you're doing signatures
DSA signatures or ECDSA signatures so
these are systems which are extremely
fragile and it's a strange thing that by
just looking at the scale of
modification for a number which you will
use only one single time so your
signature generation starts with you
pick a random number you do an
explanation or scalar multiplication and
then you do something else with this
number these one-time numbers is one
time exponents if they are somewhat
biased for instance if you know that the
top four bits or top eight bits are
always zero you're getting the secret
key so it is very very strange system
that this is possible and this was
exploited in the two papers from which I
showed you the news coverage so there
was a TPM fail this November by Daniel
McGee me back sooner Tomasz isin but
Nadia Henninger who showed that doing
this to typical TPM in the
implementations of TPM cryptography so
you have your TPM in your computer in
charge of doing the signatures say for
VPN connection then they could get the
keys out of the TPM remotely there was
another paper called we know if I take I
haven't seen the paper yet but they have
a very nice informative webpage young
Janka Peters vendor and vladimir said
much were they doing the same for smart
cards which were actually certified so
this is really bad attack and it's
something where all these
implementations both the TPM and the
smart cards for these signatures should
have been tested for this before but
apparently people didn't test or didn't
realize that this small bias has such a
youth effect there are more text so this
is just the basic you see the overall
timing but this only broke lots of
libraries smart cards and TPMS if you're
getting more detailed information if you
are on the same processor like you're
running a hyper threading attack or
cache timing attack then you might even
be able to figure out when you're doing
the lookup for the pre computed values
where this lookup went so you're kind of
booby trapping the the table where
you're going to look up something and
then depending whether the processor
fetchers
entry which is in cash or that entry
which is not in cash you're learning
into something about the exponent and
you can even recover the exponent from
these things now this should be a
constructive talk we said this is like
80% constructive so let's jump in how
would you fix this so one thing is for
all our cooked augmentations we actually
know kind of an upper bound this is not
an arbitrary explanation it's an RSA
decryption we know that our RSA keys
well we know a bound on the end people
pick 2048 or 90 4096 bit keys so we have
a good upper bound on how long this D
will be so why don't we just use that so
we're making this loop length in depend
of what D actually is but just saying
well we take the number of bits and n
rather than D all right so the problem
then is before that we started
initialize all the message with the
ciphertext and then we kept squaring and
multiplying but there's an easy way out
we just initialize at one and well if
you square one
it stays one until well you have reached
the bits that are actually occupied by D
so when we expand our D we padding to
the full length and windus ties into one
so we have a fixed length loop and this
one takes care of not modifying our
values and then we do the normal thing
we square and we conditionally multiply
except for we don't want to have this if
else I mentioned cache timing attacks
and in general well you might be leaking
well you're definitely leaking how many
bits they are and you might be leaking
more depending on how different your
modification looks for the squaring and
so what we typically then do is we give
up on a bit of performance we do a
multiplication for every bit not just if
the bit is 0 and then we conditionally
select which of the two you take the one
which we just computed the age here that
is with multiplication or the one
without multiplication and we don't want
an even else there because an attacker
could
observe the branch could see whether we
going or we not going and so we do this
whole thing by arithmetic well okay
let's briefly run through this if the
bit is zero then half 1 minus 0 times M
some getting M great and then if this
bit is 0 I'm taking 0 times 8 so for the
zero bit I'm computing M which is what I
wanted and now for the one bit I should
be corrupting h and yeah of course if I
have 1 minus 1 this is 0 times M plus 1
times H so this small modification to
the code comes at a bit of a cost so
it's as slow as the worst case both in
the length so a loop has gotten longer
we're doing more modifications more
squarings and we're doing squaring and
modification for each bit which
otherwise would have just been the worst
case now I've been saying elliptic
curves and I've been saying
diffie-hellman R is a so if you're doing
different find fields you can do exactly
the same thing you can initialize that
one and then multiply by your generator
so that's cool
now if you're doing the same thing with
elliptic curves then things get a little
bit more iffy if you were here by now
it's five years ago at 31 sees three
then I would give me talk about elliptic
curves and we've been rounding a little
bit about vilas curves and one of the
things that makes via truss curves NASA
to implement is that you always have to
talk about this extra point so you have
a nice curve and then there's an extra
point called the point at infinity and
this point of infinity messes up most of
our arithmetic so we don't have nice
formulas we just say hey well this is
our Neutral element and so we start at
this and then we keep on doubling this
most of the formulas have this exact
exactly this exact point is an exception
so we can't initialize there there are
ways around it but the default is not as
easy there's some nice occurs we've been
advertising edward's curves and
Montgomery curves so on Edwards curves
the neutral element is nice as was a
starfish shape and you have this point
twelve O'Clock and you can just do it so
for edwards curves everything is nice
and I should also do a shout-out to
Montgomery curves for instance the
famous curve to 5:19
which you might have in your browser or
in a cell phone that is using formulas
due to Peter Montgomery which are very
happy about this data flow and you even
get any discount so in doing basically
one doubling and one addition for each
bit same as the squaring multiplication
just it's called addition here so it's
like okay then would comment that
probably this is just to make sure that
we mathematicians keep lifetime
employment because nobody could possibly
understand it otherwise so it's all the
same
it's called addition doubling sorry for
that not my fault came before me but
you're getting this combo of addition
and the doubling for less than it would
take otherwise so it's not as bad as it
looks like for RSA of it if you Harmon
in fact the reason the two 519 gets used
with these montgomery formulas is that
for that bit size it's the fastest way
you can implement scalar multiplication
so it has a nice feature of being
constant time and it's cheaper if you
need some more motivation for wanting
constant time there is an additional
benefit of constant time named you have
figured out how long something should
take and so certain things should not
happen so if you know that your
arithmetic does finish in time X you
will not enter an infinite loop as the
Microsoft cryptography libeled it's
recently for Windows 10 oops
yeah constructive talk you said so now
we've had bug bug bug and a little bit
of fixing and maybe you believe that
yeah okay these timing attacks are a
problem and sometimes people do believe
like OpenSSL they've got a few
subroutines which are labeled claimed to
be constant time and there's some other
crypto libraries which say we've got
some constant time code it's not
pervasive by any means but some people
say they're trying to do things in
constant time and avoid these attacks
and then well is that true I mean people
make claims about crypto all the time
like rc4 which was used until pretty
recently sorry
that's bad crypto it is bad crypto but
it was introduced with a claim that it's
great crypto rc4 is the crypto you want
to use
and somebody gives you rc4 software well
originally it was proprietary but
eventually it was leaked and then
everybody had rc4 software and this
software yeah it's a strong cipher and
it's constant time and well how do we
check these things well the strength of
the cipher that's outside the scope of
this talk it's not a good site for yeah
don't use rc4 but how about the constant
time property of rc4 or something else
well this example actually uses rc4 this
code is maybe a little bit weird so let
me first look at what this code does and
then say what valgrind is doing with it
this code is sort of the start of code
to encrypt using rc4 and what it does
you see there's some key running around
there's some space allocated for the key
32 bytes maybe you want to use a
different length you can try this for
different lengths so the key but 32 is a
reasonable length of keys and then okay
that key is allocated the program will
abort if the malloc failed and then at
the end it frees up the key properly it
doesn't ever initialize the key so this
is maybe a work in progress program but
okay there's some space for a key and
then it expands the key rc4 there's a
key expansion process into what OpenSSL
calls this rc4 key structure and then oh
there's supposed to be some encryption
after this well that didn't quite happen
yet either but this program is still
something you can compile and the
compiler with normal optimization
options and without linked on
optimization and so on it won't realize
that this program is doing nothing I
mean maybe the rc4 set key is I don't
know crashing your system or producing
some output or something so the compiler
will call malloc and rc4 set key and
then you can try running this program
under valgrind now I'm sure lots of
people here have used valgrind or
address sanitizer for checking for
memory problems
valgrind has the advantage that it works
on binaries and maybe some people were
in room C for the previous talk about
fuzzing and it's really helpful to have
tools that work on binary so you don't
have to worry about getting into the
whole software engineering process
compilation process you just take the
code that you're gonna run like the rc4
set key from open s install you don't
have to recompile or redo anything with
open s
you can just run valgrind on your
compiled code and it will run this
program and allocate space for a key and
then it'll call the rc4 set key and run
through valgrind interprets every
machine instruction and while it's doing
that it keeps track of all right which
memory is actually memory that's you
know you're allowed to talk to you for
instance the malloc is setting aside
this amount of space on the heap and
then well you're not supposed to be
going before or after that and valgrind
is trying to keep track of what your
pointers are pointing to and then when
you read and write data then it's going
to say oh you're not allowed to do that
and one of the things that it checks is
suppose that you have some uninitialized
data and you use that as a pointer or
you use that as a branch condition and
you try to do an if or an X bracket I
where I is not initialized then valgrind
will give you an error and that actually
happens in this code that the malloc
array
well--that's uninitialized and then
valgrind will track all of the
uninitialized data like taint tracking
it'll figure out all the other
computations on uninitialized data
inside rc4 set key and then it will
complain so you get an error message
looks like this usual kind of valgrind
error for the people who've used this
tool and then it'll say there's some use
of uninitialized value which is not just
any use this means that you've been
doing some array access X racket I where
I is uninitialized and that's where
valgrind I mean what would it mean it
makes sense that valgrind would say oh I
don't want to continue past that X
bracket I and and just guess I mean it's
trying to figure out if you're accessing
some wrong spot in memory and if I is
uninitialized but it just says that's an
error you're not supposed to be doing
that and similarly if you do an if based
on if I where I is uninitialized then
valgrind will say no you're not allowed
to do that
and it'll produce well not exactly the
same error but something else another
complaint about a branch based on
uninitialized data and hey that's
exactly what we want to do to check
whether this rc4 set key is constant
time code this is checking is any of the
key information is that being used for a
branch
anything derived from the key is that
being used for a branch or is it being
used for X racket I which could be
getting into one of those cash timing
attacks and so if Algren says there's a
problem then you investigate and you fix
it by throwing away our c4i or whatever
you have to do to fix your software and
if valgrind says there's no problem then
hey cool all done
alright so it is a happy talk after all
so we really have a situation that we
have constant time excellensation of
scalar multiplication we have constant
time rc4 and a few other conditions so
one of the things is that you arithmetic
I mean in the end you have to implement
your computations on the elliptic curve
or you have to implement your arithmetic
modulo RS a modulus and you have to do
this long integer arithmetic in constant
time but you can again check this well
Greenwood every single machine
instruction it's going to follow through
so valgrind
awesome tool well there's another
condition that the processor doesn't
screw you over the processor tells you
well ok I'm gonna do a multiplication
I'm gonna do division I'm gonna do an
addition now if you have something where
the processor is going to say I do this
in once in your clock cycle and that's
probably ok so you check the manual
check the reference code and sorry the
reference manual and you look of how
long it takes for one multiplication for
one addition you look at like when you
have access to it and so on so that's
fine
but how about other processes so I had a
poor student look at the cortex m3 so
that's a low-end ARM processor and we
asked them to do some nice imitation of
elliptic curve cryptography and if
you're having a multiplication which is
taking two 32-bit words and producing a
64-bit output so twice as long as
multiplication should be doing and then
you look at the cycles count then you're
seeing three to seven cycles footnotes
see footnotes see tells you that this
might be aborting earth terminating
early depending on the size of the
source value there's a worst case
latency of one cycle something more and
after 7 cycles so all right so student
was lots of time
it's only 2 times 32 bits inputs right
you can just know you can test all of
them but you can have a student test a
whole bunch and so he came out with this
flow chart so this cortex m3 gives you
values between 3 and 7 cycles it gives
you actually every number between 3 & 7
cycles except for 4 depending on which
of those branches you are taking whether
something is a special operand yes or no
and whether boughs are special and one
is 0 in that situation valgrind won't
help you in that situation it's
basically by different processor yeah
this is what happens when we decide to
do a constructive talk 80% positive this
is gonna be defense yeah and then we
talk about and realize yeah it's all
broken it's kind of sad it's actually
even worse I mean it's not just that the
tools don't do what we want them to do
for checking for things being constant
time but they also don't check that the
code is correct I mean we spent half the
talk now talking about timing attacks
and there's all these vulnerabilities to
timing attacks appearing in the news and
lots more that don't appear in the news
and then suddenly there's more CVS which
are not just timing is going wrong this
is like okay let me explain this first
of all crypto mem comes this is a
function inside open SSL which says it
would be really embarrassing if open SSL
had that one bite at a time password
checking or Authenticator checking
inside the code so crypto mem come has
been there forever and open SSL and that
is doing supposedly constant time
comparison of two byte strings now it's
not that open SSL does everything in
constant time but it does this in
constant time and the pa-risc
implementation because of an
implementation bug the pa-risc crypto
mem comb function only compares the
least significant bit of each byte now
this is from May 2016 somebody thought
that they knew what pa-risc processors
are and it's a good idea for open SSL to
have assembly code for comparison of two
byte arrays on the PA
risk I don't know how many people
actually have ever used a pa-risc
processor can I see okay I see at least
10 hands being raised I'm impressed
this is not the world's most popular
processor i but it exists and you can
write assembly code for it and maybe you
can even find some machines where you
can run this code and actually it's not
crazy that OpenSSL is doing assembly
code for things because compilers screw
things up pretty frequently on the other
hand as this particular implementation
illustrates humans also screw things up
pretty frequently so what does this bug
do what is the impact well let's look at
the advisory it says this allows an
attacker to Forge messages that would be
considered as authenticated in an amount
of tries lower than guaranteed by the
security claims of the scheme okay let's
figure out what this means so you've got
a message and it's got typically a 16
byte 128-bit Authenticator at the end of
the message and then this crypto map
comp is being used to check it
recomputes the Authenticator with
whatever mathematical function and then
checks is the result equal with crypto
mem come too you know what's coming in
from the network and if somebody's
modified the message then hopefully they
can't compute that same 128-bit result
and now we try with this pa-risc crypto
mem comp on European RISC server we try
comparing the Authenticator that's
computed 128 bits to the 128 bit correct
Authenticator and it's only comparing
the bottom bit of each of the 16 bytes
so it compares 16 bits which means that
instead of a 2 to the minus 128 chance
of forgery it's a 2 to the minus 16
chance of forgery so the attacker just
tries 2 to the 16 messages and one of
the forgeries is going to work say what
sorry it's know what it is lower yes 2
to the 16 is a lower security level than
2 to the 128 it's like classic British
understatement of you'll security level
is perhaps not quite what you wanted um
ok pa-risc
let's forget about PA risk just like the
whole computer industry has and focus on
Intel I
No okay I mean pa-risc it was a nice
idea at the time you know son used to
have the SPARC processors now Fujitsu
still makes SPARC processors I don't
think anybody's trying to preserve
pa-risc but people have these ideas of
making new instruction sets and you know
at some point Intel made a new
instruction set and it got really
popular and they kept extending it and
kept selling nice fast processors so
here's using avx2
there's some that's this 256 bit vector
instruction set on current Intel and AMD
processors there's an implementation of
1024 bit modular exponentiation in
OpenSSL and the code from July 2013 was
discovered in 2017 or announced in CG
2017 3738 to have an overflow book now
what's the consequences of this bug let
me guess it's a lower security level
well they say attacks against eh 1024
are considered just feasible now yeah
you shouldn't be using th 1024 in the
first place but if you are then if the
attacks are getting just feasible does
that mean 2 to the 16 computations does
it mean a day on your laptop does it
mean a year on a cluster I want to know
how hard the attack is and well this
isn't really answered and there's more
that's not really answered in the
advisory because they say well you
you're probably not using dh10 24 but
maybe back when this was announced you
were still using RSA 1024 or maybe DSA
1024 and those would also use the same
subroutine and then the Advisory said
that the attacks against RSA 1024 as a
result of this bug would be very
difficult to perform and are not
believed likely now what's happened here
there's the original crypto system and
then there's a bug which basically makes
a new crypto system doing a wrong
computation and I mean this notion of
wrong as well it's a different crypto
system and then is that new crypto
system this slightly different RSA 1024
it shouldn't criticize it it's just you
know differently-abled RSA 1024 and
that's it's you know maybe it's secure
and they say it's going to be fine and
well has anybody really looked at
normally if we have a new crypto system
then we wanted to go through a whole lot
of review because there's lots of things
you can do wrong and it's really
important to get these things right lots
of people were using RSA 1024 you
shouldn't of course you should use
something much bigger or switch over to
elliptic curves but if people were using
RSA 1024 and they had these wrong
computations happening what are the
consequences where's the papers
analyzing this widely deployed crypto
system it's like saying yeah we've
deployed this crypto system and we've
looked at it ourselves and we've decided
attacks aren't likely and just believe
us well people say this sort of if you
can't break is gonna be fine yeah okay
yeah you're right you're right
everything's fine and similarly a few
weeks ago when open SSL put out another
advisory for another bug like this see V
2019 1551 not it's not that we knew this
was coming and we'd figured we would
have a talk about bugs and crypto
software just to make fun of this I mean
this is these things happen so often
there's so many of these bugs and we
don't know what the consequences of all
these bugs are they just keep happening
here's an example of just one piece of
the patch for the 2017 bug yeah the code
before already has correct it oh you're
right the patch adds some lines saying
correct well okay that's clear enough
next slide how about post quantum crypto
you know you got these topped hundreds
of cryptographers around the world
fighting against the threat of quantum
computers and putting together the next
generation of cryptographic software
protected against quantum threats that's
going to be carefully evaluated right
everything's going to be just fine
well no Falcon for example this is one
of the round two signature competitors
in the nist post quantum cryptography
competition well post quantum
cryptography standardisation project and
this one there was an announcement in
September 2019 which said here's quote
from the author of the software saying
well there's some bugs and the
consequences are the signatures leak
information on the private key and they
also make the software sound faster than
correct
where would have been and interestingly
all of the implementations all of the
latest Falcon round 2 implementations
that were released had the same bug they
all had the same test vectors they all
were you could cross-check them and they
were doing the same leaking wrong oops
sorry
different cryptographic computation
which presumably has lower security and
then are we gonna spend a lot of time
figuring out how low the security level
is the author also commented the fact
that these bugs existed shows that the
traditional development methodology
being super careful has failed all right
so what can we take from here so
mathematical complications and
cryptography is thinking of like
elliptic curves what I mentioned if you
have these special points that need
extra treatments you have to watch out
are you even allowed to add those can
you even represent this in your in your
software those do make your software
more complex something that we saw in
the Falcon implementation it was a new
system and it hasn't been started for
long so something which has been started
for a long time like ours ain't easy
Siva still see issues with it things get
worse if you have such long
countermeasures so as one example you
saw how I was trying to avoid the
leaking that whether the bit is 1 or 0
by introducing arithmetic now if you
have to review that code before we just
says if the bit is 1 do this if the bit
is 0 don't do anything versus the code
which has the arithmetic instruction
it's more complicated so siphon
countermeasures also add more complexity
or then was mentioning this comparison
bug in the pa-risc this was also because
people were trying to make the
comparison not leak information through
timing so they made a new mentation and
use new bugs and then of course was post
chromatography we're getting a whole
bunch of systems like Falcon which have
been less studied where we have less
experience and how to implement it
secure we don't even know all the
pitfalls that add to the complexity
where we have to watch out so it is a
problem than to review cryptography
another problem with crypto is that we
have this drive for speed capture runs
volumes of data so we have to be really
careful we have very small code we have
to run many many many times and we will
optimize the hell out of this doing like
one squaring for each step and one
modification which that read is annoying
so we trying to squeeze it here we
squeeze it there so that makes it more
error-prone as well and also you're
getting a huge amplification of
implementations you will have
implementation for your x86 architecture
you can't see some with AV extra
instructions some without a vex 2
instructions well you might go all the
way down to pa-risc special instructions
so ways for each CPU there is dedicated
mutation not just the reference code and
then if you look at for instance cat
track which was the winner of the shell
3 competition so it's a relatively new
hash function which only exists for like
new platforms but still they're having
more than 20 implementations for
different platforms in their library or
Google in order to get speed for hardest
encryption on some lower end smartphone
so if you have a cheap smartphone they
might have just encode X is 7 rather
than the the new architectures which
have a s support and so they were like
ok we're all maybe we should at full
disk encryption but what we have sitting
around is just too slow during AES
without the hardware support would drain
too much battery and so they went even
down the road of taking the cipher
specified by the NSA the spec cipher and
they put it on there because it seemed
to be the only thing that was satisfying
the speed requirements now they did
switch out to some public outcry in
particular Jason Dunn Feld
did a lot of work there to make them
switch to something better and they then
did another implementation so yet
another code base to having Eve recently
designed combination which I call a
tiantan vez X ChaCha
so there is a lot of code to review and
a lot of places to get errors so how do
we deal with this
well maybe if the problem is all these
complicated implementations of all this
complicated math maybe math is the
solution
so here's help sorry that seems to help
yeah yeah more plus one is two
so that's a comment from the bottom here
from this book from 1910 from this
proposition which is proven in very
comprehensible language here it will
follow after we've defined addition that
one plus one equals two and this is on
page 379 of this book called principia
mathematica
principles of mathematics by I don't
know if they do one plus two equals
three that sounds more complicated but
somehow they find it important to prove
something and like in all this
incredible detail some sort of like
machine language for for proofs and then
people complained that their machine
language has bugs and while people have
worked on this over the last more than a
hundred years and they would actually
recommend there's fans of this who say
that yeah you should be going through
this kind of pain you should spend 379
pages proving that your code works so
you should take your software and you
should write down a formal proof in
incredible detail not just to convince
yourself and some friends but you should
convince a computer that's doing
automated checking of your proofs and
that computer program says yes you have
a correct proof that your software is
computing the right thing and what is
the right thing well you have to
carefully define that specify your
language for your software specify what
the input-output relationship is
supposed to be and then prove that you
have that input-output relationship for
that software assuming of course that
you've gotten all that right then your
proof if it's checked then everything
should be fine these tools they they
work but there's something just to give
some context there's something that
mathematicians who do proofs all the
time don't like these tools occasionally
they'll use them but it's really not a
popular set of tools because there's
such a pain to use nevertheless they
have enough fans that some amazing
results have happened so ever crypts
this is something there's like 15
authors on the paper and they have a
crypto library which has implementations
of all the crypto you need as long as
you don't care about any of those NIST
curves or a post quantum crypto or well
here's a list of what they do support it
it's got some public key stuff and some
signatures some symmetric functions
it's got arguably enough to do you know
like HTTP you can do with these
primitives and that's what ever Crypt
supports in the case of a yes you need
your CPU to have AES instructions so
maybe that's not so portable but ok it
does support some other ciphers on any
platforms and you can use this and
there's proofs people have actually done
the ever crypt papers reporting how they
took some standard proof tools and
actually formally went through this
software does exactly the right
calculation which is like okay that
that's some serious guarantee the good
thing about this is that the code really
has the maximum assurance of any code
that we've seen for cryptography that
it's it's really saying yes this code is
computing the right thing have used ever
crypt then it will compute the right
output for every input exactly what is
specified assuming the specifications
correct assuming the processor is
correct assuming the compiler is correct
because a lot of it's written in C you
need your C compiler to be correct but
well okay you can deal with those
problems separately how do you verify
CPUs how do you verify compilers etc and
have people review the cryptographic
specification so it actually it's
feeling like something serious is being
accomplished here the only problem is
that it's such a pain to do for every
implementation you have to do quite a
bit more work and people are getting
lots of practice building better tools
but it's still a ton of work to do these
formally verified pieces of
cryptographic software an example of how
hard it is is just illustrated by that
list of whatever crypt supports they've
got some implementations of these
functions they even have for Intel chips
some fast implementations of some of the
functions but if you want something
that's fast on your smartphone or
SmartWatch where maybe performance is
more of an issue than on your say big
laptop then no ever [ __ ] doesn't give
you fast implementations it does have
something that works but it's going to
be several times slower and nowhere near
what Tonya was mentioning about trying
to squeeze out all the last speed it's
really far behind the state-of-the-art
in speed because it takes a lot of human
time to take a new implementation and
prove something about it so what do you
do when you don't have proofs well of
course you test stuff
now we could spend the whole hour about
like how cool testing is and just I mean
let me actually see a show of hands here
how many people here have ever had this
feeling of oh I I wish I had done some
more tests of this code like that you
know this bug that I had let me see a
show of hands I see pretty much
everybody in the audience raising their
hands okay now how many people have ever
had this feeling of oh I did too many
tests I I see okay maybe and maybe about
20 people out there have this feeling
out of that I don't know a thousand
something applications sorry who's in
both camps people who thought they
tested watch ant little yeah yeah yeah
of course testing is fantastic you
should test everything and if you find
that testing is something hard to do
then it's probably because you screwed
up in your factoring of the software
that you're trying to test you have too
much cohesion you should be modularizing
it more and have a piece that you can
test if you do test-driven development
then you will basically have working
code all the time and that's a really
nice feeling except well there's a
little problem which I'll get to but
something like the crypto mem comp bug
for example in open SSL for pa-risc
where it was only testing like the
bottom bit and seeing what do the bottom
bits match that's something which gives
the wrong results for 1 out of 2 to the
16 inputs just random inputs will will
give the wrong results so if they try to
to the 16 or tried millions billions of
tests doesn't take that long and then
it's gonna catch that or instead of
trying just totally random test the
whole fuzzing philosophy says let's try
to smartly choose what you're gonna test
and you try for instance you try a
string and then try flipping a few bits
here and there doesn't give the right
result of a comparison and that very
quickly finds that the crypto mm come
doesn't work and these are not just
things that you you could think of doing
retroactively Lee this was actually
implemented in the super cop crypto test
framework before the bug was introduced
in open SSL and it's just well though
the crypto code wasn't plugged into that
framework so
well we didn't catch the bug but it's
it's like we almost could have if there
had been a bit better organization of
the testing effort in general if you see
a bug then at least retroactively Lee
you should find yourself thinking all
right how can I make tests that will
catch that bug and usually there's a
pretty easy answer to that and then you
add that to your regression test suite
and make sure it never happens again
and then if these regression test suites
are shared enough then it never happens
to anybody again
and that's really effective except well
the main thing that goes wrong with
testing is that you're not testing all
of the possible inputs and so we've seen
time and time again millions of security
holes which are the attacker is finding
some input which nobody thought of
testing for it wasn't part of your
random testing it wasn't even caught by
fuzzing it's just some obscure kind of
input where the attacker says haha if I
try and input it exactly that length
after setting off the following
condition and then the following weird
thing is going to happen and then I can
take advantage of it like this there's
some input that behaves in the wrong way
which you're never going to find through
testing or even with the most advanced
fuzzing that we have so how do you deal
with this well that's not so easy and
it's something which definitely affects
crypto for instance November 2019 never
one of the standard elliptic curves out
there curve 448 high-security modern
elliptic curve cryptography 519 if you
want something at a higher security
level there's a bug that randomly
happens with probability one and two to
the 64 well that's a lot of tests that's
yeah I'm not gonna do two to the 64 test
me we've done some computations at that
scale that it takes a lot of effort to
set that up and it's not something you
do with lots of different pieces of
software again and again could an
attacker find those inputs while it's
clear in the the paper announcing this
Nath and Sarkar say all right here's
some inputs which make this operation
fail inside like a subroutine doesn't
mean the attacker can find inputs to the
whole crypto operation that make it fail
should there be more analysis of like
how devastating this bug is or should we
just get rid of the bug in the first
place
say alright certain kinds of inputs the
code gives wrong results but it's very
low probability so known answer tests
are not gonna give not going to find
this and so they say you have to prove
correctness and this is the dichotomy
that people often say you have to either
well do some tests that'll find the
common bugs or do proofs that's a lot
more work really painful but that'll
find all of the the books there's
another approach which is symbolic
testing and this is something where I'll
take memory comparison example not for
pa-risc but on the left side here let's
not think about this as testing the code
auditing on the left side here is crypto
mmm come for normal intel chips x86 64
inside open ssl and you can read through
that well maybe you can't because the
font size is too small but you read
through our maybe you're not fluent to
an assembly but you read through and
eventually you say here is the
computation that it's doing for some
particular size of input let's take for
example three byte inputs of course you
have to try every length that you care
about like 16 bytes is very common
so for each length you figure out what
is this code do and for instance for 3
byte inputs it's taking x0 x1 x2
comparing to y0 y1 y2 and then well how
is it doing that comparison in constant
time well it's exclusive oaring x0 and
y0 together exclusive warning x1 and y1
together exclusive wearing x2 and y2
together so now it has three white X ORS
it ORS them together bitwise so that's a
number between 0 and 255 where if the
arrays matched you would get 0 0 0 and
then everything else is going to be 0 if
there's any difference then the X ORS
will be between 1 and 255 and the or the
bitwise or will also be between 1 and
255 and then you convert that to a
64-bit integer prutte 56 extra zeroes on
it and negate that integer shift right
if you think about this for a moment you
see that you always get 1 if there's any
differences in the inputs that's a logic
you can go through as a code reviewer to
say yes this does work correctly you
start from the assembly you figure out
what it means for each size do you care
about that's this graph this computation
graph showing the arithmetic
from these inputs to dag a directed
acyclic graph that shows how the inputs
give you some output through a series of
computations and then while you analyze
this graph and say yes this works
correctly and do it again for each
length all right
there's tools which make this really
really easy to do let me highlight anger
it's not the only tool out there but it
has the big advantage of working on
binaries it starts from valgrind from
lib necks inside valgrind and then
builds a lot of extra cool stuff on top
of that what anger does is that whole
red arrow inside the previous slide it
does that for you automatically it will
take your binary and it will run through
the instructions and tell you all right
here's what that did for your input
arrays x and y and here's how the output
is a graph from those inputs now this
makes your code review easy because you
don't have to think about memory access
pointers you don't have to deal with the
complications of the assembly
instruction set the the output of anger
is a much simpler instruction set
there's no jumps it's just completely
unrolled this dag that you get is output
there is a constraint which is that
anger if it reaches a branch based on
one of the inputs x and y then it's
going to say oh there's there's two
possibilities maybe you take the branch
or maybe you don't and if you do an
array access based on any of those
variable inputs it'll similarly split
that and say well there's all these
possibilities for which array index
you're accessing but hey we were getting
rid of that that was the first part of
the talk is we don't want to be doing
these variable time instructions we're
just gonna have straight line
computations maybe you have some some
loops but it's based on public data not
based on the the secrets that you're
trying to work with so we get rid of
this blow-up in crypto code anyway we
want to do that to protect against
timing attacks and then that means that
anger runs really fast and it gives you
the unrolled code and then it can even
sometimes check the correctness of that
code for you so for instance this crypto
mem comfor 3 byte inputs it will tell
you yes this works now we have only nine
minutes left so maybe I'll just very
very quickly show you what some code
looks
but I'll skip a bunch of details this is
a simple call to crypto mmm come on some
arrays of size and you define n to be 3
or 16 or whichever length you care about
through this again and again and this
takes X and y those arrays compares them
puts the result into Z the compiler
won't get rid of this code with normal
optimizations because who knows what
happens after main maybe the exit is
going to look at the Z value because
it's a global variable and maybe it's
going to do something with it so this
crypto mem come will be called and then
anger well okay there's some setup of
grabbing the binary telling anger that
the memory is all filled with zeros to
begin with you tell anger all right
you're gonna run the code in anger but
instead of having zeros coming in for
the x and y let's replace those spots in
memory with some variables let's say
that the x bracket 0 in memory that's
going to be the X 0 variable where we
don't know what that is it could be
anything 0 through 255 and same for X 1
X 2 and y 0 and so on and then you run
the program and you extract some Z's out
of all the possible universes you get at
the end and for each one that all the
magic is happening in the last lines
here after angers run through the the
code you can just ask it do any of the
following classes of bugs can they
possibly happen and then there's some
automated tools called SMT solvers which
can sometimes answer this question they
might run a very very long time for but
for this example it runs in under a
minute and tells you yes the code always
works all right last slide here what is
missing what are the people who are
trying this approach working on well you
can always do if you have constant time
code you can always do this anger
translation another tool which will do
this for you which I haven't used
personally but Manticore supposedly can
do the same thing from binary xand comes
with a lot of the same kinds of analyses
that I've worked with hangar works just
fine also it has this cool GUI called
anger management so anger yeah it'll
it'll always convert your code into this
deck and then the right the red arrow
there it'll always give you the results
of that and then all of the the
interesting problem at
that point is if the SMT solvers aren't
smart enough to see that the resulting
code works then you have to build some
new tools which we'll look at for
instance you get one dag for your
reference code which you're you've
reviewed and you're sure it works
they have another dag for your
complicated fancy vectorized assembly
implementation and then you want to see
are those doing the same computation and
you have to kind of match up those decks
and people will give these arguments
that yeah this is why this is the same
and the whole game here is to build
tools which are doing this this is maybe
I'll skip the sorting example aside from
giving the URL just an example of doing
this is for sorting code where right now
the fastest Intel chip sorting code for
integer arrays in memory is some new
sorting code which is constant time it's
like three times faster than Intel's
integrated performance primitives
library where they were trying to
optimize sorting and it is verified to
produce the right results with some
tools which look at the DAGs coming out
of anger and say yes that is a correct
sorting program if you're interested in
doing this sort of thing then you should
say all right here's some crypto code
where nobody's claimed that it's
verified which is most crypto code you
can just take random examples and then
say all right let's make a constant time
first if it's not then forget it it's
going to be vulnerable to timing attacks
throw it away but if it is constant time
then use anger and get this dag out of
it and then say well okay why does that
match some other code which is supposed
to be doing the same computation like
assembly versus some reference C code
for example and then figure out how you
can match up those decks and usually a
little bit of Python scripting will do
that matching for you it'll tell you if
there's any problems sometimes you have
to get into the details of how the
crypto computations are done but it's
actually fun that's the great thing
about this approach compared to all the
the proving tools doing symbolic testing
symbolic execution with anger followed
by matching up the DAGs analyzing the
DAGs
it's fun it's actually a fun way to
analyze crypto suffer at this point
we'll be happy to take questions so
thank you for your attention
[Applause]
[Music]
thank you all right we will do a very
high-speed Q&A session so please limit
yourselves to questions not comments
microphone number one place I think if
the very short question is constant I'm
really the only mitigation against
timing attacks well it's a mandatory
thing I mean you can do more you can do
randomization and such things but you
want to have that those don't depend on
the secret dater you're a participant
under two please thanks for the talk
can any approaches from real-time
operating systems can be applied to
cryptography so real time is usually
trying to say you want to make sure the
operation finishes at most this amount
of time but the thing that happens in
fancier timing effects like
hyper-threading attacks is that before
you've even reached near the end of the
computation the attackers already
extracted the secret data and so it's
it's a different game that real-time
operating systems are playing if you
have constant time code that can be
useful in the real time context but it's
a stronger constraint good things all
right back to one please thanks for this
amazing talk I just had a question
regarding ever crypt you said that the
curve to 5519 implementation was slower
than the other stuff that's available
from my knowledge the curve two five
five one night and crew of two five one
nine implementation ever Crypt is
actually one of the fastest ones on
intelligence an arm it's slower on Intel
it sits at the state-of-the-art but on
arm it's a few times slower okay thanks
alright Internet go
the formal verification of ever crypt
also check for the lack of side channel
attacks or address for the functional
correctness it checked for functional
correctness and a lack of timing attacks
it's actually a constructive way of
producing code which is constant time
all right
mic number seven you mentioned you
mentioned compiler bucks how would it be
that in buck and anger covers up a buck
in your code
it's it's possible definitely the whole
situation for testing is say you've got
your original code maybe you made a
mistake there you've got your test
framework maybe you made a mistake there
and you're trying to have these be sort
of independent
tests and then ultimately of course if
everything's proven then yeah you can
imagine proving that anger works
correctly do that once and then it works
for everything but since it includes
some kind of complicated stuff and all
of Python and SMT solvers and so on it's
going to be some time before we're at
that point so yes there's definitely a
possibility of bugs in anger it's
something to worry about as long as
they're kind of independent of the bugs
that you'll make in your crypto code
then you're reducing the risk of errors
all right Mike the signal angel please
is there progress and the formal proof
of true randomness that's enough of an
answer I think Mike number one please
what's the status of doing pairing
friendly over the arithmetic and pairing
friendly curves in constant time so this
is again a little more complicated so if
you just want the scalar multiplication
the TPM fail paper was also attacking
the BN curves so just the same issue
appeared there as well as the
implementation but not constant time
even though the way inside the TPM code
which should have been validated the
pairing on top of it is is looking a
little bit like exponentiation
computation so the same tricks will work
at this moment the best reddit code
apparently was not constant time all
right
microphone number one last question what
about superscalar processors do they
mess up your carefully crafted constant
time algorithms or is that at least from
a certain distance not relevant anymore
they're short the way to think about it
is that you want to have there's like
some isolated data which is holding all
your secrets and then there's never
anything which is copied out of that
sort of safe environment into the
metadata which is controlling timing now
if you have a superscalar processor
you've got multiple instructions
happening in a cycle but as long as the
decision of which instructions are being
executed is not based on the data that
you're working with then you're good and
that's where you have to be sure that
the processor is handling
you know each instruction the time that
it takes is only based on the other
metadata outside the secure environment
okay thank you for this great talk and
please thank our speakers again
[Applause]
[Music]