scale.bythebay.io: Colt Frederickson, Fixing the rusty core of the internet with functional prog.
you so today I'm going to talk about well kind of this I'm gonna talk about encryption and why some things we believe about our Krypton aren't necessarily true so I'm Colt I'm live up in Bozeman Montana and do remote skala full time that's just to give hope to people who can't necessarily move to the bay and want to do I don't do awesome things so I've come to like FP and and found that that's like a great way to reason about programs total functions like help me eliminate all these weird edge cases and so recently I joined a start-up iron core labs and we're doing some really cool stuff with some of what I'm going to show you today but I started reasoning about it using functional programming which is not something encryption people normally do usually it's all about fiddling bits and getting the most speed but not about safety necessarily which is it's kind of one of the problems so so open SSL open SSL like everybody probably knows HTTPS everything is over SSL nowadays and it powers most of the internet like and this doesn't include like IMAP and other things that actually use SSL or things that use SSL on the command line like for us to say H or whatever so everybody uses it and ever it's probably older than some people in this room so it must be good like everybody's using it must be good it's old oh no no additional run run so like but but like what kind of metric am I using to say it's not good well the test coverage out after 18 years or 20 years is under 50% like none of us would go to production would suffer now I think we wrote in the last six weeks with with unit test coverage silo so it must be rock-solid right like clearly it's not tested but but it probably works nope so like over the last they I mean this is the last basically ten years ID excluding this year like these are the the number of high low and moderate vole Nura buildings that have been found in open SSL and it turns out openness to sell the more people poke at it it turns out the more bugs are finding and well that's strange because like you think that they would be like focusing on code coverage now right because people are poking holes and there's no but there's not that concerned about it they try to test it and they test it some but it's it's hard to test because this mutable ball of mud and it's really really hard to figure out what's going on so it must be because it's hard like it has to be hard otherwise somebody else would have solved this problem no no no no it's not it's not really really hard it's just subtle and and the distinction there is is actually like one that I'm gonna try to show you today but it's it's important all right so we're gonna cover like elliptic curves and talk about that and I'll try not to like get too many eyes glaze over when we talk about elliptic curves it's not scary it's just some algebra and we'll talk about the laws and stuff and then we'll actually look at implementation so elliptic curves this is an elliptic curve it's basically just a curve that is symmetric around the x-axis and there are points like you could solve this equation for any given X or Y value and like that would give you those two those a single point and anytime you draw a line between two points you end up at it exactly one other point okay and that's only not true for values that I've inverted x and y or in the inverted Y and for that point we call that the point at infinity and that's treated as like basically our zero case especially if we're like talking about mods so point addition is just find that intersection point and flip it over there x-axis and this is the entire construction of of elliptic curves now I wish I would have put it on one slide so I could have been like ruin our and been like this slide is all you need to know about category theory but like I'm not quite that cool apparently so it's it's that's alright so there's certain laws that hold for this so the point that goes through P and Q is the same as the point that goes through Q and P that's pretty obvious the point that goes through negative Q and Q always ends up at at infinity like a dozen ever ends to intersect the curve again there's an associative law which is like a little more involved to show but it does hold them the identity is like if you had that the point the pointed infinity to a to a particular point we just assume that comes back to the same point it gives us the identity so let's just look at something we want to do an elliptic curve cryptography is at a point to itself a lot it's called point multiplication and so when we do when we add a point to itself obviously there's only one point so drawing a line through one point well what do you do there so we use the line tangent to the curve at that point so that means the line tangent to y equals zero goes off to infinity but everywhere else it's defined okay so that P intersects over there when you when you add it to itself and just like addition you flip it over the x-axis and that's adding P twice so 2p what if you wanted to add it again well you just draw the line again through a to P and P and just keep doing this keep doing it over and over and you do it hundreds of billions of times or more okay so like what are we seeing here like you showed me some curves you showed me some numbers and there's a PE like oh well so the in this example 3 is our private key just by the way would be a terrible private key don't maybe don't choose one that's like you know at the bottom of the scale P is the public generator point so that's like when you when you talk people talk about a Bitcoin or whatever there's a public point that everybody agrees upon that is like where everybody starts so three is the private key and P is the public generator point and so three P is our public key so that's like the number that I send out to the world and say hey this is me that's what we do for GPG or you know any of those any of those things you like send out that information to it to public place but like all right I still haven't told you anything yes yes yes three three P is three times P so P plus P plus P yep okay so let's let's just take a quick example so if n is Bob's private key and M is Alice's private key would gather we gotta have Bob and Alice in any crypto presentation then NP and MP are the two public keys so what this is really used for though is is elliptic curve diffie-hellman which is really just a fancy way to say if you have a somebody else's public key you can use your private key to come up with a shared secret so and then you can use AES or salsa 20 or you can use any symmetric encryption you want at that point but you got to come up with a shared secret so like why does that work maybe like well it seems like dark magic well we talked about community and associativity and whether or not you can add points over and over again well n p and x m is the same as moving the moving the ends and M's doesn't matter okay so this is just math like we've talked about some math and these are well known algorithms like there's their equations and everything is good well I kind of lied so what we saw when we saw that pretty curve is when we evaluate this thing over the real numbers well real numbers go on for well forever so like we don't want to represent those as bits because how would you represent something that was a thousand bits long like well you want it you want to constrain it down to a certain size so the first thing you should think of is well what if we just modded all these numbers by P like we just invent some crime and we mod everything by that prime well if you evaluate a curve mod a prime this is what it looks like it's not a curve visually anymore but it still is a curve and holds all the laws that we just talked about and because of that you can basically take and add any two points on this scatter plot together and you will get another point on the scatter plot and where that point is cannot be determined except for by doing the work there's there's no way to like reverse engineer it and that's really important because if you could reverse engineer it and figure out then you you wouldn't have to really solve much of a problem would you like you just reverse it and everything would be really really bad on the internet so this is called a point multiplication and this is the algorithm this to do it like to do it over and over and over again this algorithm is not really that important other than its Haskell and I just wanted to put it on the slide but really the math is like looks almost identical to the Haskell and I thought this conveyed it slightly better so it's just doubling the point and then dividing the N by 2 each time so what do we say when we mean large like I keep talking about these numbers and we to use 3 in our example which is bad so this is the number of atoms in the universe ish and this is a prime that is chosen for like I think this one is specifically like the Bitcoin prime but anyways like this is it's two orders of magnitude off but this number is very very big and these are 256 bit Prime's now we're getting into more like 512-bit primes so like numbers twice as big as the number of atoms in the universe so we're talking really really big numbers so it turns out when you have these huge numbers and you have a curve that is not pathologically like circular or some dumb then curve that this problem right here on the slide is hard very very hard like thousands of computer years hard and so that's what the entire security of the internet is relying on because open SSL under the hood just does this elliptic curve diffie-hellman and if you have that shared secret everything is compromised so this is this basic math that we've just talked about is the entire basis for the way the security works inside of open SSL now I'm gonna show code and it would be like irresponsible of me to be like this thing is so easy you should just go and start using this code in production you know that kind of stuff crypto is very subtle there side channel attacks there's constant space and constant time algorithms there's different point representations to avoid like doing inversions like there's all kinds of very subtle things but that doesn't mean that the underlying core stuff that we're going to see here today is wrong it's just I'm not gonna bet my career on so well I said finite field where I said we're gonna operate with that scatter plot well all that really means in skull code is this like don't let somebody create this F P type with the with an I that's arbitrary first modded by some prime you might be wondering why I don't use mod here instead of writing my own mod well it turns out mod in Java are on the JVM gives you the remainder not the actual mod and like that's a whole deal too but just don't just don't put a percent in there it's not gonna work um so I wrote this field if anybody's work to aspire before this is just a field implementation using the spire type class and so this is just showing like that full implementation and it's very trivial I mean we're just negating values and modding him by primes and multiplying them and adding I'm like it's not hard it's just math okay so what about points I said they had an X and a Y and we had to solve that equation well I guess if we're gonna be good functional programmers right we're gonna use some parameter like we're prioritizing on type a until we absolutely can't so let's make a parametric and like see what happens so it turns out that there's other representations of points there's XY and Z so you can carry along this remainder and like there's stuff that's really clever math tricks that allow you to do cool stuff which I only mentioned so that if you look the stuff afterwards and you're like this this paper doesn't talk about like a fine points it talks about homogeneous points or Jacobian points or something else like there are weird tricks that people use to get better performance in certain situations but they all they are all isomorphic to each other so they can go back and forth very easily so let's just look at a fine points so this is the implementation for adding to a fine points so note here that the a fine points over some arbitrary type a and I enforced that they that that a has a field implementation well we just showed field for F P there are field implementations for many things including complex numbers and other really crazy things but this implementation is completely abstract away from that implement from the underlying field definition so now we know this should work for any field like that's what we're that's or asserting at least I haven't shown any proof of that so I won't go through this code extensively so well-known algorithm for finding the slope of the line in yadda yadda yadda so I used doubling points in that point multiplication that's also really easy you find the line tangent to the curve at that point again just a math problem not hard so that's that's actually pretty easy to also continue to note like we're talking about some parameter type a on the a fine point so this is that nice Haskell definition turned into some some Scala that has a tail rec and I want tail calls so bad so yeah this is that same thing but I I implemented in Scala just to show like it could be done so it turns out that if you have all of those things I just showed that points themselves form a group an additive group so all we need is the ability to add a point over and over and over again to do a lip takur for cryptography and so if all we have if all we need to do is add things over all we need is an additive group as we need to add and we need to negate that's all we need so this is the definition for that and if you run this through scholar check for thousands upon thousands of times with different field definitions you will always get the right answer like it will tell you that it's lawful every time okay so I may be thinking thank you so what well what I just showed was like this point implementation and all of the code that I showed today doesn't rely on the underlying like bit patterns it doesn't rely on anything to do with that all it's doing is like it's just doing very general math and we know by the laws of pyramid to see that like nothing is fiddly is going on here so we if we find a bug in our system we don't need to like oh did we screw up point multiplication no we we know for a fact we didn't screw up point multiplication because we've proved it with the laws right so we're we're in the place where we can we can know things about the way the points work without thinking about the way that the numbers work without thinking about the way the complex expressions work that we're using for these X's and Y's we can prove things about each individual piece which is what we want to do is functional programmers like I want to prove this this thing this piece works and move on now yeah if you're if you've done a crypto before you know the reason that people fiddle all the bits it's because it's slow if you don't fit all all the bits and it is like there's there's no doubt like this isn't like this isn't a panacea where I've invented this cool thing that's like faster than open SSL and everybody's happy like this is slow this is it especially this code that I show is very slow like it's using big int it's not using proper new types so it's like boxing sometimes it's like it's terrible so you can you can solve those problems irrespective of this particular solution though because you can get a different numeric type underneath this and as long as that numeric type works you're still good and you can test that independently so I I just don't understand why people people are so scared of crypto and like any anybody I talked to at this conference leading up to this they were like well crypto scary and I'm like yeah yeah I like it's not great in terms of like I mean it's very subtle like side-channel attacks are super scary like what if I use different amount of voltage on the CPU during this time like that stuff is scary but like people just believe in the crypto is good because it's old it's not it's not right and we need to like individually test small pieces and move on so I I'm I'm building stuff on top of constructions similar to this using pairing based cryptography and some other stuff that's not in most crypto libraries and when we get done with it like I'm gonna have to send it off to a bunch of people to like try to get it reviewed and and get researchers to look at it and like there's gonna be a bunch of work but as a community as especially as a folks your programming community like we should be getting behind things that are testable and things that are good and things that we can reason about instead of just being like oh that's old so it must be good so like I thought by the time we got to 2017 like we'd have like flying cars and hoverboards and maybe like crypto that was tested but like since we didn't get those things like I guess I'll just have to settle for us moving in the right direction for crypto so thanks [Applause]