I am Adam Fultzer. I work at Galois in Portland, Oregon. We're kind of renowned as a place that has been using Haskell in industry for a really long time, like all the way back to 1999. And what we're going to be talking about today is Cryptol, which was born very shortly after the company itself. So this project has been around for a while. It's, for most of its life, been a closed source, but sort of freely available, like we would send it to academics and whatnot. But it turns out security researchers don't like using closed source tools to do their research. So about a year and a half ago, we did like a ground up rewrite, a much simpler, cleaner implementation, and released it as open source. So that is what I am excited to share with you today. It's our domain specific language for specifying cryptographic algorithms as an executable specification so that you can actually run it and see how it works, which can be done with LaTeX, but I wouldn't recommend it. But LaTeX is the typical format for cryptographic specifications. So Cryptol lets you be precise about what you mean when defining an algorithm, but then actually go do stuff with it. So run it, build a formal model of it, prove it equivalent to some other thing, prove correctness properties about your algorithm. And so these are a few of the things that I want to talk about. We probably won't be able to do justice to everything in the amount of time that we have, but I'm hoping to get through as much as possible. And yes, so, you know, plans encountering reality and all. This is like what I have in mind for what we can cover in this time, but of course let's be flexible and if folks have more questions, I'm not going to stop answering them just because I want to adhere to a schedule. So like the idea of formal methods is motivated in large part by wanting to make software that is correct. And there are many different definitions of what correct is. For the purposes of Cryptol, correct is a sort of functional notion that if I have this specification that is supposed to take this value and give you back this other value that is related to that somehow, that it is going to do that every time and there's not like some secret value that you can pass to it that suddenly gives some bogus value and is a backdoor flaw in your security. We also want to apply formal methods to help improve performance of things. So, you know, a lot of people think about formal methods, they think like Coq or Agda and languages that aren't exactly renowned for their runtime performance, but you can use formal techniques to say, have your nice easy to verify specification over here and move it down to a highly performing one and then prove that those two are equivalent. And so you're using formal methods, but you're not sort of bound by the shackles of having to use a research tool in your production code. Like you can prove equivalence with C that's been optimized to Helen back. And so, you know, the standard questions about software correctness are if you hand me an implementation of an algorithm, how do I know that that's actually an implementation of that algorithm? So, again, this is that type of like equivalence checking between implementations that we want to answer. Formal methods are not a replacement for testing, particularly given the scope limiting that I did a moment ago where I said that we're concerned with functional correctness. If you're implementing crypto, you have all sorts of other things to worry about like power and timing that don't necessarily show up in the semantics of programming language like cryptol. You could imagine a programming language that does have those semantics integrated with it, but cryptol is not that language, at least not yet. So, you want to use testing to verify these other properties and also verify or validate rather any sort of integration and glue code that might not be amenable to the formal techniques. Like you write a C module and you prove it equivalent, but then the wrapper function around the call from your website to that C function to run the crypto might have something wrong in it. So, at Galois, sort of generally speaking, we want the software to be trustworthy primarily from correctness or by construction so that you get that correctness property because the software was built in such a way that it has no other choice essentially but to be correct. And depending on what language you use, you can get stronger and stronger notions of what correct means just by the construction. With cryptol, it's sort of a balance between the standard benefits that you get from a typed garbage collected programming language where you're not going to try casting an int to a float. You're good Lord, dereferencing a pointer as an integer or something like that. And you're going to have memory safety, so there's no array out of bounds that can lead you into trouble without raising an exception. And we use this technique of building mathematical models from things in many more domains except cryptography. And we try and be as open as we can, but cryptol one was a hairy mess of a code base and honestly the reason it wasn't open source sooner is because if you have 13 years of development then you've got to go through and make sure that all that stuff is ready to go out and we're only about 40 engineers so cryptol two was born and it is much nicer and more maintainable. So this is kind of what I was talking about. You've got your LaTeX specification of some algorithm and then cryptographers know just enough C preprocessor to write reference implementations that look like this and so you'll get a paper where this code will be in the appendix and so you can compile it and run it and it's like okay it agrees with the tests that they wrote down in the paper but I have no idea if this is actually a reasonable implementation. So I'm going to break with my schedule already and show you an implementation of a cryptographic algorithm. So this is the Zuck cipher. It's one of the stream ciphers used in 3G which I think extends to LTE as well, phone communication and so you have diagrams like this you have lots and lots of subscripts and superscripts and confusion about whether they're zero based or one based and what all of these things mean so this is definitely much better than a lot of crypto specifications but it's not really something that is trivial to sit down and type into C and like okay I'm going to squish the 15 high bits with the 14 low bits of this word and call that x0 that's something that's kind of easy to screw up and so this is the cryptol specification and I'm not going to go into detail because I haven't properly introduced the language yet but I just want to give you a feel for it looks a lot like Haskell it has one colon instead of two for the type signatures as the Lord intended but otherwise things look kind of familiar and sorry about the syntax highlighting it thinks it's Python so when it sees the concatenation operator it's like oh I found a comment but you have your enumerations you have lots and lots of list comprehensions and one little detail here is that you have parallel list comprehensions by default that's like a syntax extension in Haskell but we'll get to more of that stuff later here is this function that I just showed you over here so bit reorganization is sticking these things together in this particular way and so we are just sticking them together in that particular way and then defining what does it mean to be the low bits of a word in this situation so it gives you an idea of how the law tech doesn't have to change too much to become cryptol and so we have S boxes and these are you see them in all kinds of stream ciphers because you don't want your cipher to be linear and so they cook up these magic numbers that accomplish that for you I took a crypto class once and I understood it at the time that's about all I can say for it thank you Everiste Galois for inventing all of these things for us and so let's see here's a quick example of as you're going through one of these specifications it'll occasionally have examples and so here is 12345678 as an example input to this function and wow is the answer oh yeah thank you and so we can basically just copy and paste this into the executable cryptol code and make sure that this evaluates to true and so I guess I could actually go ahead with this it skipped me way ahead and oh boy this is running slowly got QED down there there we go alright so we can just evaluate example 8 because that's like a Boolean so you can like write little things like this to check your work along the way this cipher is notable because in version 1.4 it had a bug and that bug significantly compromised the secrecy that the cipher provided basically as it's sort of expanding the key out into a sequence that it can use to XOR with all of your message and therefore provide you with secrecy it would sometimes take the same keys to the same key sequence so effectively each of those pairs of keys is just one key and the fewer keys you have available in your crypto system the less secure it is that output is not supposed to happen let's restart and so we can express the collision as a property in crypto and say that when you initialize Zuck the first, this is going to keep scrolling on me the first key that you get out in this key stream is not equal to the first key that you get out from the key stream when you use a different initialization vector so as long as for each key I get a unique thing that comes after that then we're fine and of course there we go and so Z3 can tell us that we are safe but we can also set version 1.5 to false and so this not only tells us that we are vulnerable it finds the initialization vectors that expose this flaw or at least a couple examples of them we can ask it for more if we want to that's probably not easy to do in the notebook but basically we like historically crypto was supported by the Trusted Systems Research Group at NSA and when they saw this example their socks flew off like the idea that you can use formal methods tools to actually test cryptographic properties of an algorithm and not only test them but get out useful example data that you can use to then go in and fix the algorithm so that is the kind of power that these approaches deliver on this domain so I'm going to try not to keep talking too much longer I've already gone over a lot of this stuff it's a statically typed language and the weirdest thing about its type system is that everything or sequences are polymorphic in their size so at first glance this looks a whole lot like dependent types because people who give dependent types intros I'm sorry Brian use vectors with a length I know I saw your strange loop talk and you very wisely demurred from that but that's like the canonical hello world I'm dependent types is a vector with a length field and so people see cryptol and see lengths and sequences and think dependent types it's actually not it's more like if you're living on the bleeding edge of GHC the type level NATs that are there where your type system has two kinds one is the kind that we are used to dealing with like functions and values and the other kind is natural numbers and the type checker can reason about inequalities and equalities with natural numbers to make sure that everything has the right length and this is important because when you're dealing with crypto you're dealing with a sequence of 32 bits you're not dealing with like just a generic bit vector that could have any length so that is the weirdest thing about it and it's probably the thing that you will stub your toe on the most once like this in tax feels familiar is that many programs that are easy to write in other languages are very difficult to write in crypto but cryptographic programs are pretty easy to write in crypto so that's sort of your classic domain specific language trade off is that you can write merge sort but God help you instead you're able to reason about these bit vectors on a level of precision that you can't get without having a heavier duty type system like this so the question is how related are the crypto type system and liquid Haskell and refinement types they are definitely like cousins so we call out to SMT solvers under the hood in order to resolve the constraints that come up when we type check a crypto program but the cool part about liquid Haskell is that you can write these more complicated predicates in your refinement types to talk about different kinds of constraints other than just natural number inequalities so we use just enough of that power to get what we need but we don't try and make a more expressive language there right and there like I would say that it's more about having the ability to take the typical case for cryptography and make that the case in your syntax where I don't have to specify that I'm talking about natural numbers I'm just writing a number and it's using that theory and you know there's none of the overhead that would be required if it was more general purpose alright so some more things just about crypto specs functions are pure there's no IO so you can't unfortunately call out directly to crypto and have it back your web server or something please just don't do that our approach here and what we intend for crypto is that the interpreter is all about the reference specification that happens to be executable and can be transformed into these other forms that you might be able to actually then run in a real system like you might generate C code but you're not going to be running that directly in the crypto interpreter let's see so if you're using the crypto repel so just the command line redeval print loop you get these nice few commands I type set them in markdown because they don't work in the notebook and now that I am sharing my VPS with all of you fine people I am happy that you can't load all my files but it would be nice to support that safely in the future you can browse kind of like in Haskell the pretty printer doesn't like this width but this is basically showing the prelude functions that are in scope like the Haskell repel you can ask for the type of something and this is how we write a for all in crypto so these braces mean that for all A as long as A is finite and A is greater than or equal to 2 then this is somebody's editing my notebook I'm going to overwrite them sorry if you go back to this screen and duplicate the original notebook then you can have a copy to work on and we have sort of this built-in ARIF type class to limit the types in the language that arithmetic makes sense for so you can set your base so suddenly I'm printing everything out in octal you can turn ASCII on which all that does is just interpret bytes as ASCII for strings this help output is going to be a lot more comprehensive at the repel because you will have, oh I guess it, that's a bug it shouldn't have all these things and you can look at the available user settings some of those I've already shown you is like setting the base to something else and setting ASCII on so the basic type that makes up pretty much everything in crypto is a bit and it's either true or false not terribly interesting what gets interesting is when you start combining those things together so this is a sequence of length 7 and it contains bits and you can index into the front of it you can index off the end of it because both of those often are how people describe their algorithms we have enumerations and concatenation shifts and rotates among others you can nest sequences so basically each sequence is parameterized by the thing on its right so this is a sequence of length 2 that contains sequences of length 4 that contain 4 bit words essentially and you can index into that and there's also this, it's like a projection where you can pass it some indices and get that set of indices out of a sequence and you can ask the width of a sequence is its length but when you're dealing with cryptographers they like talking about widths you have sequence comprehensions should be familiar to Haskell or Python programmers and words are kind of treated specially so I'm down here dropping the conceit of putting bit there if you just have the sequence notation with nothing else to the right of it it assumes that it's a bit just because it's so common and you can enter your literals in various bases the classic hella world of cryptol is actually 1 plus 1 what do you suppose it equals? 0, I heard it so arithmetic is modular in the length of the words that you're doing the arithmetic over and so if we give one a type signature and say that it is a 2-bit word then we get 2 because there's actually enough room to not wrap around we've got tuples and they are 0 based because we had to please Python programmers it was a great debate in the office and those can be heterogeneous as opposed to the sequences which must all contain one type we have records which are basically tuples with labels and we can also define type aliases so you can use type for other things than records and then use the dot syntax to project out from the records you've got Boolean operators which work in exactly the way you would expect on bits but they are also defined on other types so you can do bitwise operations on words and if you want to you can sort of point wise do bitwise operations across larger structures so I'll type in these definitions and you can see what comes out so we've got or and xor and tilde is the complement we have if then else but you almost never want to use it and if you want to know why try writing a recursive function like factorial in the way you would expect to write it it gets difficult well maybe factorial is not the best example but like a recursive function over a sequence like write the function that adds one to each element of a sequence and you'll see why if then else is a problem we have ware clauses for local bindings so this just is like in Haskell and what not functions can take multiple values separated by arrows and if you want to return multiple values you can tuple them up and we have anonymous functions with lambda and that's kind of the basics so I wanted to stop here and kind of give you all an opportunity to play around with the interpreter if you've downloaded the PDF of the book which is at the top there's a link at the top of this notebook chapter two has a sort of a tutorial walkthrough of these features and some exercises scattered throughout so let's see how we're doing against so let's see it looks like I'm behind schedule so maybe we will maybe we can just like go through if then else is as a quick exercise together so let's add a new cell and let's write a function add ones that if we give it this sequence we'll give us back this sequence sorry see style comments for legacy reasons okay so what is the type or let's try writing it without the type signature first I'm sorry right so we have A is finite and we're taking a sequence of A's and actually let's make sure that it can't be a sequence of anything it has to be a sequence of finite width words thanks okay so the first thing that you'll run into is that you can pattern match on sequences but it doesn't work in the way that you would expect where you could have like one line giving the base case and then another line giving the recursive case and so right well so I'm not sure what direction you're going in with that but yeah so in like a language like Haskell or something you might write something like this if you were doing the explicit recursion and this is totally Haskell syntax so don't actually try and type this in to Cryptol you might write something like this but the way that you want to go about attacking a problem like this in Cryptol is to think instead of pattern matching how can I write a sequence comprehension that will accomplish this and the sequence comprehension winds up looking like a fold very often so instead of this it really thinks it's Python so we are going to say it is x plus one where x is coming from x's uh oh alright so there we go so I had to put this constraint on the width of b so that we aren't trying to add zero bit words together okay so let's go over this again so what we have here is well we can like actually use this as an example so what we have here is a sequence with five elements in it and each element let's say is a four bit word so the thing that comes first is sort of like the outermost level of the sequence like how many things are in that outermost level and then what comes next are the contents of that sequence which happens to be another sequence that contains four bits and so I'm abusing the implicit word syntax there so we have a sequence with five things containing sequences with four things that contain bits and so if we want we can add ones of the empty sequence and it's fine with that but we can also add ones with our example oops I haven't re-evaluated that and get out the result that we want oops did I just kill my audio? okay so it's not actually talking about this A it's talking about a different A that is the contents of this sequence yes and so on our issue tracker is to make these type variable names more informative and less likely to clash with definitions that might be in scope yes it's just like coming up with a name for this unification variable and it's picking A and yeah I think so so the defaulting is a little tricky because there are obviously many choices that you could make for B there but it uses heuristics in various cases to try and come up with something that seems sensible and that's particularly tricky if you are using decimal literals so if I just evaluate five here it's going to assume that A equals three and alright so let's for some reason the short form of the commands doesn't work in the notebook so the literal five has this polymorphic type where the width has to be greater than or equal to three because we need at least three bits to represent that this is as opposed to hex literals that are just basically four bits for each digit so each nibble so any more questions before we go on? hopefully this is mostly familiar stuff so far we try not to get too different from the expectations of people who are familiar with other programming languages but by necessity some things are a bit strange like the fact that these two are the most used control structures in Kryptol and the first one where you just have a single bar here is sort of the list comprehension that you've probably encountered the most where it's basically the Cartesian product like I'm going to combine everything from this list with everything from this list and so the size of the thing that I produce is going to be that length times this length whereas a parallel comprehension this is really like zip or zip width where you're going to pair wise march up a sequence and use some combining function at each point and as soon as one sequence runs out of elements then you're done so even though this Y is coming from all of these we're only going to get three in the output yeah no there are no monads there's no IO so it's just expressions yeah yeah so you can put any expression here for the generators as long as it evaluates to a sequence and so you can nest Cartesian inside a parallel vice versa to your heart's content alright so a bit more about the types we have both monomorphic and polymorphic types so the curly braces are a giveaway that you're dealing with a polymorphic type and then you saw in the add ones example that you can also put constraints on the polymorphic variables so here we're saying that A and B both have to be finite and B has to be greater than or equal to two and then you have your fat arrow to then end your context like in Haskell finite means not infinite so you can't infinite sequence you can but that definition would not be able to operate on it so the semantics of the interpreter are lazy so you can write something like this and of course never use decimal literals really? that's right that was a recent change I'm still not entirely clear on it but you can use the dots for the infinite like it's from enum to inf in the AST so you can build an infinite sequence like this and it's going to wrap around because you're still dealing with elements of a finite bit width but you can keep things going forever and so if you're defining a cipher or a hash function that can operate on things of any length the type signature is that it takes an infinite number of 256 bit blocks so inf is kind of like this special element of the NAT kind so it's not just the naturals it's the NATs plus I'm sorry pragmatism no it's just I really need to fix that bug so let's just say that we have why is that polymorphic that's probably also a bug anyway so all that's happening is that instead of having a finite natural number here you just have this inf that's the extra natural number in a way yes yep so there is a rudimentary module system I cringe to actually call them modules with John in the audience but they kind of work like the Haskell module so it's more of a namespacing thing than an abstraction thing and you've got syntax for qualified names to talk about things in other modules they don't work right now in the notebook because we don't trust the interpreter to go off chasing after other file paths when running in a web browser at the moment and so recurrences are a really common pattern that come up in crypto algorithms and so you can start to think about the combination of these sequences and laziness as a way to describe circuits and so here we have a circuit that has you can think about it as a bit of state that starts at zero and every time through this loop it adds one and we do that by putting the initial state here and then appending to it a sequence comprehension that recursively references our NATs so this is very much like the Fibonacci stunt that people will pull with Haskell and so you are able to get just enough information from the beginning of this sequence in order to have that recursive reference actually give you a value back and so this if we evaluate it and see what it is it's of course assuming that all we need is a one bit word in there and so it's just going back and forth between one and zero that's not very good natural numbers but the compiler would not warn you, you would diverge though or really? that's surprising maybe it's like asking hey what's the length of NATs it's saying zero and it's saying zero, okay that's kind of a surprise to me but Yavor has been working very diligently on the constraint solver and type checker in the past few months so it does not surprise me that I am surprised I guess that's about a solution yeah now if we then gave this thing a type signature though and we said that NATs is an infinite stream of 32 bit words for example now we go off the rails and I have to kill that so the comment was about being able to check productivity of the recurrences and that is something that we are looking at as part of a larger scheme to sort of come up with an easily compilable subset of crypto so if I leave this type signature out the question was NATs is assuming let's actually fix this first NATs is assuming that A equals one and the question is is there a way to tell it to do something different well we can just give it an explicit type signature here when we evaluate it I wonder if I could give it a finite length something like that oh this is, sorry yeah you have to put parens around it just so that the notebook doesn't get confused and think that I am trying to do a standalone type declaration so if you give expressions explicit type signatures you can force the polymorphic variables to be particular types and another way of doing that we'll see another way of doing that later I'll be sure to point it out alright so this is not a very useful circuit here but you very often see patterns like this like if you've ever seen a linear feedback shift register it's like a building block of a lot of hardware and crypto algorithms and in math usually expressed as like this polynomial but you can think about it in circuit form as well as like another one of these infinite streams but where you're sort of tapping back in like a handful of steps potentially so you're not just limited to looking at the last thing that came out of the sequence you can actually go further back and we're actually already here at the point where here is another way to instantiate type variables so this back tick lets you back tick curly brace lets you give explicit arguments to the types of things and to make that more clear let's look at the type of drop so drop has three type variables how long is the front like how many things do I want to drop off how long is the back and what are the types of the elements and in this case all we really care about specifying is well I want to drop one thing off of this so it's either positional or you can like give the explicit names like front equals one, back equals whatever and so on and so in this one we are still doing this recursive sequence but we have to start off with enough initial values that when we drop three elements from it there's actually still something there for us to include in the recurrence but that's all we need like as long as we have enough base cases now we can essentially build this circuit like XORing these things together as it produces values so questions about this cause this is probably about as subtle as it gets for this talk alright cool oh yeah so speaking of take and drop they work kind of how you expect but the weird thing is that your number argument is actually a type variable rather than being some value that you can compute in Haskell and pass to the function and get that many elements so that is coming from the fact that I am using decimal literals here and so as we saw before if you put in a decimal literal it doesn't know exactly how wide to make that word so it just makes it polymorphic and so if I instead said this is a two that is a 32 bit oh yeah that's right I don't think I should try to explain that right now let's see this is like 10 32 bit words the short form of that error that yeah thank you the short version of that error that just happened is that when you're building these enumerations these things are actually NATs in the type system because the length of an enumeration depends on what values you're enumerating between and since we need to know the length of the sequence then they have to be types it's another thing that you'll tend to stub your tail on when you're learning how to use crypto but here since we gave them an explicit width then we don't get any assuming well that the definition that you entered is polymorphic but I'm going to choose a monomorphic type for you and that might not always give you what you want or what you expect and so that's why this warning is on by default is to let you know hey there is something here and that it's this but you might want to go back in and double check it and then the yeah that's just like this is the only variable that I have left unresolved yeah so group by is an interesting one it sort of generalizes like split and join and so if we take the sequence from 1 to 100 and group by 2's then we get all of these two element sequences inside that larger sequence and likewise we can split which sort of does it on the other axis we wind up with a two element sequence each with like 50 elements in it so you can put underscores in types and it will fill in the blank if it can so here it's like alright well maybe I don't want to think very hard about this enumeration and know that there are 100 things here and then have to divide 100 by 2 to like put the correct type here oh look I messed it up didn't I had to provide the the type of the contents so rather than having to like compute this you can just say alright put whatever there the question is can you put a hole in the middle yeah that doesn't parse so I think it's it's only okay so yeah you can you can put it where you would expect a type to be but the underscore itself doesn't have rules in the parser like the brackets do so it doesn't know to expect another type after it that would be kind of interesting though there is zero as you might expect but zero is is polymorphic oh I haven't evaluated it by a point 3D you know what let's just run everything so zero of type sequence of two containing sequence of two point three D's gives you back that structure with everything set to zero so even on larger complicated types it basically goes out to the leaves and makes all the bits false and if you negate zero that is a convenient way to get something with everything set to one because the Boolean operators work on the larger structures in the same way zero does alright so let's get to some real cryptography so rot13 is the hello world of crypto it's a very straightforward cipher and it's a specific instance of a substitution cipher where every character in the ciphertext is replaced by some character from the plaintext according to some dictionary it has the property that rot13 of rot13 of some message equals that original message because there are 26 letters in our dictionary and so you wind up wrapping around and so here is the cryptol definition of this most famous crypto algorithm and just to walk you through this a little bit what we're doing is kind of the same pattern that we had with the add ones example that we did earlier where we're going through the message and running this shift function on each character that we're getting out of the message the shift of a character is and if you forgot this is the sequence indexing operator it is looking into this map at position character minus capital A so if you think about well let's turn ASCII off and just evaluate the character A so A in ASCII is 65 and so if we take any character say C and subtract 65 from it that gives us an index that then we can plug into this map and so if we say map at C minus A with the appropriate parans then we get 80 and if we set ASCII back on so that that turns into a character then it turns out that C maps to P in ROT13 and so all we're doing is converting into an index that we're then looking up in this sequence that we have pre-computed by enumerating all of the capital letters and then rotating them over 13 places so literally ROT13 so any questions about this definition your first cipher you can encode all sorts of messages with it very securely I'm sorry can you repeat the question right so the question is why does this compile because the map is only 26 characters long and C minus A could be greater than 26 so let's try little C which is 99 and so little C minus capital A is 34 and if we index into map at 34 then we get this invalid sequence index so crypto is not a total language it does not check that for every input to a function you are going to necessarily get an answer things could diverge they could throw an exception like this which is different from the concept of memory safety so crypto is memory safe but all that means is that you can't take some invalid index like this and then have shenanigans happen where you're then using that invalid index and the program isn't crashing it's actually letting you mess with memory that you're not supposed to touch so there are exceptions and there are user errors so no so is the question like does crypto check whether a particular value is in the range of a function I mean like when you say map at it knows that maps seek the length of the map no so basically as long as that index is of the right type it's fine there is a mode in the formal methods back end that can be used to check the safety of functions and we're working on getting that hooked up again that was a feature that we had in crypto one where you could type colon safe of a function and it would tell you whether or not that function was safe and that's what it puts it's something that we would like to get back but it's a pretty different technique involved with that versus a totality checker that you might come across in a language like address good question so the fact that the list is indexed is it only for adding different lists together when does the compiler use the notion that there's 26 elements in them so arithmetic because you're sorry the question was when do you actually make use of the information that your sequences are of a particular length and the answer is that since we're doing arithmetic on unsigned integers essentially we need to know when to wrap around like we need to have some semantics of what plus means and so if we didn't have the length associated there it would sort of be you know up to the implementation to just decide that well in this case let's use big nums and then it only overflows if you run out of memory on your computer or let's use machine words and then it wraps around it 32 or 64 bits so when you're writing crypto algorithms you need to be like very precise about overflow behavior and what are the exact semantics of your arithmetic operators so it comes into play there it also let's see it also comes into play when you're using the formal methods tools because those tools need to also be precise so when we run symbolic simulation on the crypto program it's producing essentially SMT live output which is very specific that all bit vectors have to have a length so it's necessary in order to take advantage of the tools in the way that we need to but it's also it also is very much a domain specific thing to more accurately reflect how crypto specifications are written because they're always written with explicit lengths yep that's a good question so this question was what happens when you try and verify the property that ROT13 of ROT13 of x equals x well let's just add to our definition here and say that property ROT13 that's involutivity right bring our x into scope let's get a new cell here so first of all what is the type of ROT13 in vol so it's polymorphic so the first thing that we need to do is actually try this out at a monomorphic type because if we try and do colon proof of ROT13 in vol then it complains that it's not a monomorphic type so what we can do instead is say alright let's check the involutivity at a particular length of message because our ROT13 is polymorphic in the length of the message that we're processing and so let's say that we'll do a message of 32 bits or 32 letters rather and it's false and this goes back to the question over here which is what happens when you have an index that's out of range and so in order to actually state this theorem more precisely we need to do some checking on the message coming in to make sure that it's actually all uppercase letters and being the prepared person that I am let's just copy this whole thing I'll leave that one up as a cautionary tail get another cell here and again let's do it on our 32 letter size this is a lot slower on the VPS okay can we interrupt this yep it died let's just re-run these cells make sure our prover is Z3 because I had you install CVC4 for this because that's the theorem prover that the type system in the currently released version depends on but Z3 is a lot better for most things and so you can also download Z3 have it alongside CVC4 and use it as your prover for theorems the type checker will still use CVC4 because we've written stuff directly binding to that I wonder if that was just yeah so Z3 run off the rails Z3 comes back immediately Z3 is also now liberally licensed so you can just get that and use it for whatever you want whereas before we did CVC4 because Microsoft had like a weird proprietary but academic license on Z3 and so it wasn't really compatible so what we've written down here is a statement of the theorem that essentially for all X if not all is upper X so this is gonna like traverse the entire message and make sure that all of the letters are upper case then about 13 of X is that original message and so what's happening here behind the scenes is a process called symbolic simulation where rather than evaluating a function for a concrete output value like true or false because this thing returns a bit it's generating essentially a circuit representation of the function that would compute a bit of the signals and once it has generated that circuit representation it can pass it off to formal methods tools like Z3 that specialize in taking what is essentially an NP complete problem of checking all the possible inputs to this function and they use incredibly clever heuristics and techniques to make that go much faster in the usual case and therefore provide a proof that this theorem always evaluates to true well it's saying for any possible inputs is it going to evaluate to true it's asking that question later on we'll talk about satisfiability which is maybe more of what you just mentioned where I sort of know the answer that I want to get give me the input that will get me there I think we were trying to prove that but now we're proving the inverse I'm sorry that's just the name so the property here so it is its own inverse is the property but you didn't write that code that was that was code that I wrote before and used it in because I was anticipating this question so that's not going to work because it's possible that some of these inputs here are not going to be uppercase letters and so quite rightly the prover says hey for this input your theorem doesn't hold so if we go back here and do this other one let's set this back to base 10 so it's got a bunch of C's in it for some reason Z3 chose C's and then it has 128 which I don't think is probably a printable character but I don't know what it is and so that's outside of the map and so that would result in an error and so right so so in the formal model yeah it's encoded in such a way that the solver is going to give back unsat essentially or sat actually for the way we encode these it's going to give it back in such a way that indicates that it doesn't hold like this formula just does not hold for this particular input value it doesn't necessarily explain exactly what happened but it's going to find some inconsistency in the formula that it sends off to the prover so let's see we're skipping ahead but this seems like a perfectly good direction to go in instead of prove you can put check here and really like quick check the interpreter is going to come up with a bunch of random values to throw at it and it found an error for this input sequence and since it is actually running the Cryptol concrete interpreter for this now we see that it's invalid sequence index and what would you call that yeah so this is an exception that just happened just as if we were to take this theorem call ROT13 involve of this sequence of course so I want to call the theorem I guess I could just call ROT13 directly okay there are new lines in there there we go so if you call oh dear if you call the function directly with these counter examples essentially you can do the same thing for the counter examples that come out of the prover and so if you're like alright the theorem is false so why then you can take this counter example and run it in the concrete interpreter and then the concrete interpreter will say oh yeah there's no exception here this sequence is out of range yeah right if you choose so the question is this theorem right here instantiated at this particular type is making a much weaker claim than this theorem which is saying for any size x and for all x of any size this property holds right now the automated tools don't support reasoning about polymorphic theorems like that that's where you start to get into very often needing interactive techniques like you would have in Idris or Coq but we're not set on having it be that way forever so it's not like illegal to send something polymorphic to the proof command it's just that right now it doesn't happen to work because we're translating eventually to the bit vector theory in the SMT solver and that theory can't reason about bit vectors of symbolic lengths so due to the needs of the underlying solver we have to be monomorphic about it and a way to sort of mitigate that depending on what you're specifically trying to prove is to basically like take the same definition and like say we have this property that plus with zero on the left is the identity function that's monomorphic but we can run it at all these different sizes and it's like okay well I maybe trust it more now I don't trust it completely but this is sort of going down the path of providing more evidence and another nice thing is that the drum I've been beating about crypto specs always being very explicit about what lengths everything is and all this stuff is that properties that you want to prove while developing a crypto algorithm are monomorphic and if they're not monomorphic it's just because you have something like a hash function where you can run it for an infinite number of blocks and so doing the proof that one block hashes correctly is a monomorphic thing but you have to make a larger argument that the hash function works as expected over arbitrary size blocks so the question is you can quick check or you can prove and why would you want to do one or the other symbolic simulation does not work for all programs that you can express in crypto so if you have essentially a loop that is not statically bound you don't know how many times you are going to loop through this recurrence relation then you can't symbolically simulate it because it just will keep finding more branches to go off of as it's doing the simulation and it's like well it could go in this direction so I do need to come up with more term here and it will just never stop but even with things that do symbolically simulate not all of them work that great with SMT solvers and so it might take a really long time to prove something but you might just want to like have colon check run every time you load your file and so you don't want that to happen every time and so you just want something that's a bit faster and then maybe you run the proof overnight that's usually for things like checking properties about an entire like actual crypto algorithm that's not ROT13 that can take a while or doing equivalence checking between non-trivial functions it doesn't have too many smarts right now I think it tries to do a little bit of that but mostly it's just random that's definitely something that would be nice to have but prove is really the bread and butter any other questions about that stuff yeah so we're actually well caught up in terms of time so let's just take a let's say 20 minute break and or exercise we've already covered a whole lot of this thanks to the excellent questions so far so property driven development is sort of the methodology that you wind up wanting to use once you have tools like call and check and call and prove by your side basically instead of writing your program once and then trying to prove that it is correct after the fact when you're writing crypto algorithms you're very often writing properties along with the algorithm sort of like like it's very common in a spec for to say okay here is function f and here is function g and g is f's inverse and so you can encode that g is f's inverse and prove that as you go to make sure that what you're implementing is correct in small pieces and then either have the proof for the correctness of the larger thing or maybe it's too large for the SMT solvers to tackle directly so you use the small pieces to compositionally build up the assurance that the entire thing that you've built is correct this can also be used once you have a completed specification to evolve that specification into something that is maybe more useful for your target environment and so we have this picture here where you start off with a reference spec and you refine it and optimize it and then finally compile it to your particular target and each step along the way you are building a formal model and making sure that all the way across what you're building is equivalent even though the specific algorithms or techniques that you're using might be slightly different along the way like a classic example of this is the AES cipher sort of the straightforward definition has algebraic expressions that define how to do I believe it's the mix round step of the cipher and for certain implementations they basically will just pre-compute all possible inputs or all possible outputs for that function and put it in a big table it's like a 32k table or something like that and then just look up in that table whenever they need to do that step and it's not necessarily obvious that an implementation that uses that is equivalent to an implementation that looks a lot more like the spec so then you prove that those two are equivalent and then you wind up with a more optimized version of your algorithm that you still have all the same assurance from the original specification that it's correct so already talked a lot about properties in crypto basically the fine print on it is that anything that is either of type bit or a function that eventually returns type bit is a perfectly good property so you can have a property that is just a bit that is sort of like test vectors essentially you're saying well just check that 2 plus 2 is 4 so you can do proof by evaluation and be done with it or you can have these functions or properties that are more polymorphic have more possible input values and then you wind up having to decide whether you want to do colon check for the quick version colon prove for an expensive version how much do you need to monomorphize it to get the assurance that you want yeah so we've already seen all this stuff if you want to just play around with the REPL you can like build lambdas I mean any value that returns a bit is fair game as a property so Brian earlier asked when you would want to use check and when you would want to use prove and I gave an answer that was mostly when do you want to use check well when you want to use prove is when the size of your input is so vastly huge that it would be intractable to prove it by positively checking all the possible inputs so here is a haystack function and haystack just checks x to make sure that x is not dead beef and so this is a this is a function from 32-bit words to bits and so there's 4 billion of these and we're checking 100 and our coverage like is a rounding error for this function but that was fast so these SMT solvers are really really good at taking this kind of problem that you know the worst case is I have to check them all and coming back with an answer much much quicker and the common case when you're dealing with cryptographic algorithms is that you're dealing with functions that are too big to exhaustively check so that's why prove is so important check is like a nice design aid when prove is a little bit too heavy to be running all the time we already went over these yeah so if you do call and prove without any arguments it'll just automatically try to prove every property in your file and likewise with call and check it's just like alright I want all my properties to pass this is like if you were putting up a continuous integration you would just load the file do call and check call and prove and there are your test cases so satisfiability is sort of the I don't want to say dual in a room with category theorists in it but in many ways it's like a mirror image of prove and in fact we implement prove by turning it into a satisfiability problem so prove asks is this property going to return true for all possible inputs and sat asks what input do I have to pass to this function in order to get true out the other side so it might not be a property that is true for all inputs but there might be one in there and so we would like to find out what that is so just to throw in a quick example here we can do sat of haystack and it finds that right away whereas like when we were trying to prove haystack you know it says oh well this thing is false and so here you can kind of see how these are mirror images of each other it's like prove is giving me something that is not dead beef and sat if I set base 16 what? oh sorry right so let's sat lambda x x equals dead beef there you go so here is a stupid crypto trick you can define matrix multiplication forwardly using sequence comprehensions and such I'm not going to go through the details of the definition but it's doing exactly what you would expect like taking the dot products of their rows and columns huh? yes and so here is a 3 by 3 identity matrix so one's on the diagonal and we can use sat to invert the matrix by taking an example matrix here and saying alright find an x such that m mult of this matrix and x is the identity function which is like the definition of great timing and there's the inverted matrix poorly formatted so tada there are a few more exercises that you might want to check out offline that are sort of like good introductions to how these sorts of properties are written and how to check them but I just wanted to close by pointing you toward like the various open source resources wow did I really write homepage why did it not show the link that's annoying alright so iPython's notebook is broken in the way that it renders this markdown so we have cryptall.net which has got links to the book and to the downloads and the mailing list and everything all the development is on github and all of our releases are there it's up on hackage as of a couple months ago and I managed to get it into homebrew and some kind soul has put it into nix packages as well and has been submitting bug reports to me because nix packages breaks so that's awesome it helps us fix things that we didn't know were broken the mailing list is pretty low traffic it's mostly me announcing new cryptall releases but people will also chime in and ask for help getting something to type check which is almost always the problem when writing cryptall and then if you come up with a neat algorithm or a cryptall implementation of your favorite bit manipulating algorithm we are very likely to want to put it in our contrib directory a bunch of great crypto implementations from members of the community definitely check it out we really really love seeing people using cryptall and getting value from it and we aren't getting any money from that we just like it so please don't hesitate to email me email the mailing list just get in touch we'd love to support you as you try messing around with this stuff yeah so that's the cryptall workshop thanks


And I was like, you know, I could have thought like I thought that the kid was literally having like some was like There's a bug or something. Yeah, there was something very dangerous happening to him and And it was not Beating up his minecraft house his minecraft place.  You got to put like a door and a roof on So the bad proof Right That's a life lesson. It was it was and he for like about maybe an hour or so afterwards he was like Kind of shaking a little bit nervous.  And then the harsh reality of Nighttime in Minecraft world Bats come around. Yeah, the the wolves will eat you And it's past the vortex when the bats At night the ice weasels come I Love bats. That's are so cute Sheamus caught a bat in the harbor freight. There was a we stopped by the way to pick up some dollies and harbour freight On the way we need more volume out of you, Patrick You know what I don't know if you change something reboot the whole system. Hold on. No, I Hate bats. There's no way. Did you change something? I didn't touch anything Just talk louder. I think it'd be fine. Yeah But I don't want to talk like this. Yeah, that's great. Yes That's good. Yeah, I know but I'm literally I'm in command voice. This is how I could talk to people when I want them to Delta 49er that is an abort Delta 49er abort abort. It's great. It sounds great No, see that's the television rule Roger if it feels uncomfortable uncomfortable it looks great on television It wasn't supposed to be if you feel in pain. It makes good radio. That was never the rule This is you can't change this rule.  You wake up at six. You've gotten away with something. It's great you you You don't have children and at this particular moment. I'm very jealous in the context of this sleep conversation I understand no I was also a terrible My hours of sleep are broken into four and two hours with an interruption in the middle every year Yeah, you've got it. You've that's it's newborn life I gotta bring her in a bed with me so she stops crying. No, no, no way. No way Put her on the cold Headphones that's how you gotta do that's the only way they'll learn Now that we've solved all of Roger's parenting issues break for some tech news. Oh, oh my goodness. It is time, isn't it? It sure is. Is everyone feel comfortable and ready? Yes Small child is okay. Hey, Trissy. All right, buddy. Okay. Good. You heard a yes All right, here we go three two Lorenzo floris has supported independent tech news directly for five years. Why not be like they're Lorenzo I'm gonna do that again. So I don't screw up his name. All right. Here we go Lorenzo floris has supported independent tech news directly for five years Why not be like Lorenzo become a dts member at patreon.com slash d t n s do it now This is the daily tech news for friday february 15th 2019 in los angeles. I'm tom merit and from studio feline I'm sarah lane from the mid february blues. I'm lenn peralta and from dark gray skies I'm roger jane the shows producer joining us today We're very happy to have the host of tech thing and avi excel patrick norton back on the show How's it going patrick? It just hailed here in beautiful alameda, california Wow Hail hail Yep patrick's here We're expecting a plague of wokus next Patrick's actually here to talk about the plague of invidia graphics cards that's plaguing invidia because they've got an excessive inventory And whether or not that means it's a good time for you to pick up a graphics card We'll talk about that in a little bit. Let's start with a few tech things you should know samsung announced plans to open its first retail locations in the us february 20th in los angeles new york and houston Selling phones tablets wearables tv's and smart home devices The stores will also offer customer support including walk-in repairs for smartphones Sources tell the south china morning post that ea is in talks with tensent to bring apex legends to china Tencent already distributes fortnight and player unknown battlegrounds at china So it would be the trifecta for them the country just ended a nine-month freeze on improving new game licenses Tencent is still waiting on approval for in-game purchases to be sold in fortnight and pubg executives from hsbc Told reuters that it has reduced the cost of settling foreign exchange trades Thanks to its fx everywhere blockchain the system handles between 3500 and 5000 trades per day processing 250 billion dollars in trades since february of 2018 fx everywhere coordinates payments across hsbc's america's europe and asia pacific trading hubs And the company hopes to offer the service to corporate customers with complex cross border trades Yeah, uh more blockchain being used to to make international payments Easier for banks anyway. All right. Let's talk a little more about the ftc and facebook sources tell the wash and post that facebook and the ftc are In negotiations over a multi-billion dollar fine to settle an investigation into the company's privacy practices This has to do mostly with cambridge analytica, but not entirely There's also a few of the other breaches and etc that are part of this investigation The ftc has been investigating whether because of these things facebook violated its 2011 agreement In which facebook agreed to notify users clearly before sharing personal data with third parties And was barred from deceiving users about its privacy practices facebook could do a few things They could agree to a fine and a change of practices The ftc could implement tougher checkups to ensure compliance or facebook could tell the ftc to go shove it and see him in court Patrick i heard you chuckle in i It's facebook, you know They're gonna dance. They're gonna shine. They're gonna say what they need to say And then in two years, they're going to do something. It makes this look kind of reasonable and thoughtful It's just how I feel about facebook. I feel like the upshot of this story is the ft looks like the ftc will find that facebook violated the agreement in some part Uh and slap them on the hand for it. Yeah, I I don't see facebook taking this to court any longer than they have to Yeah, let's see. I mean what how what was their profit this year? Lots Yeah, a lot a lot of things a lot of dollars Uh, why don't we talk about some samsung news samsung announced the galaxy tab S5e at 10.5 inch ammo led android tablet that is 5.5 millimeters thick So nice and thin and weighs in at 400 grams and an 81.8 percent screen to body ratio The tab s5e ships with android pi and bixby 2.0 Although it does lack s pen support so that'll make a few people kind of bummed It'll be available in q2 2019 for $399 In a perhaps less intentional type of product announcement an update to samsung's galaxy wearable app leaked several upcoming products Of them the front page of the app listed a 40 millimeter galaxy watch active smartwatch The galaxy fit and galaxy fit e fitness trackers and the wireless earbuds creatively named the galaxy buds Presumably these will all be announced at samsung's galaxy s10 event on february 20th I'm more excited about the leak stuff Uh than i am about the tablet although i know i know intellectually that tablet is is is the best android tablet We've seen in a long time Yeah, I mean for 400 bucks as well. We were talking before the show of like What's that sweet spot of a price point that you know if something might lack as pen support Okay, well that would be a deal breaker for certain folks Scott johnson might say yeah, I wouldn't want that then right, but you know It wouldn't be a deal breaker for me and $400 is is is is pretty sweet for for for something that has a lot of other features Yeah, uh, I know for a fact that some samsung fans are very excited about the galaxy buds There's a little air pod jealousy But not enough to make them want to break over the the barrier to another brand So, uh, if they if they look good and they end up working well I think samsung will do well with us. We can live with it Yes, maybe we can uh, if you don't know what sarah's talking about, uh, sarah will be living with the jabra Earbuds for three months and reporting back on how well they work. So earbuds all the rage The u.s. Copyright office declined to register alfonso reberos carlton dance alfonso rebero played carlton on fresh prince of bellara Weakening mr. Reberos case against nba 2k's similar in-game character celebration In a letter the copyright office's sascha florence a supervisory registration specialist in the office's performing arts division wrote The combination of these three dance steps is a simple routine that is not Registrable as a choreographic work Of course, we all know that there's been some celebrities trying to sue fortnight or get fortnight to license Dance moves nba 2k also Under this as well. So take two which make nba 2k filed for dismissal of reberos suit Based on that letter saying The letter argues that bank that dance is too basic to be protected by copyright, which only covers more complex choreography and we've talked previously on the show that you can copyright A choreography of dance moves, but you can't copyright a dance move and what it seems like sascha florence is saying here is Three steps, you know three three things is not a choreography. That's not enough And and I would tend to agree Two mili is another example of the mili dance. Um, which is you know, something something that has Been in question whether or not it was ripped off from from something that a person can own It's kind of funny that we're having a discussion about what how many steps is in a actual choreographic dance I would agree that the carlton dance was just sort of a funny Like I it would it would be hard for me to side with him saying. Yeah. Yeah, they they really ripped you off Especially since I don't know that shows been off there for quite some time But what what what is a copyrightable dance? You know what what is a series of moves with one's body That um, that is not okay to end up in a video game later A full dance, uh, you know, I know i'm just envisioning like the difference between And We can't hear what you're doing, but yeah No, I that's the thing on the one end You can't copyright moves or else walking down the streets becomes a copyright violation, right? Sure Thank you with dance moves We're we're not at the extent of of music and written works with dance moves because uh, the bar seems to be farther away I would argue that the carlton dance is fairly recognizable and when you see it you're like Oh, he's doing the carlton dance that seems to be a kind of test You could weigh to say if it's identifiable Then maybe it is Copyrightable, but like you said sarah at a certain point I don't think you should be able to continue to copyright it but that's not the copyright laws We have we have 90 years plus the life of the author. So if the carlton move is copyrightable It's copyrightable for 90 years plus the life of alfonso ribera So that that that's also informing this like, you know what? maybe we should have this line be where you're taking elements of movement and Making them into something distinctive and and that's what florence is saying is you know what even if it's recognizable It's still just an element. It's a it's a few letters in a vocabulary It's not an entire sentence Well, and you you bring up a good point like oh, yeah people know the carlton dance Well, they know the carlton dance because it was on television that it was a you know It was it was a very popular sitcom that a lot of people watched did that happen before? Well, I don't know I would argue that it's less about whether there's general awareness But once you know it can you see it elsewhere? Can you can you pick it out that that's what makes it recognizable? And if it was part of a television show then it would be part of the intellectual property of the television show Well, yeah, that's a that's a separate aspect of this right is whether robaro even owns it or not Or whether the people had a corpus. Yeah, and and that is part of this case This was in this case as well But that didn't pertain specifically to whether the move itself was copyrightable. It's just about whether he had the standing to bring the case At a goldman sacks event this week twitter CEO jack dorsi said that instead of building an edit tweet function Which many people have called for for years the company could possibly let users Clarify tweets in the future instead Dorsi used the example of somebody having tweeted something in the past that maybe they'd like to revisit Maybe they regret and give context as a reason for the tool to exist So users would then only be able to retweet this clarification But not edit the original tweet in question So in In in the sense of keeping us all honest. I see where they're going with this In in in the many cases of me tweeting something I think is really clever and funny But there's a spelling error or something that I just kind of like I got a slightly wrong I still want an edit tweet function But I understand that the company is like hey, we don't want people to rewrite history There there are a lot of tweets that end up being problematic And then there's like a huge threat about it and how can we make it so that The original poster as it were can at least weigh in and be like hey, man. Here's what I meant to say I get that but it's kind of two different elite history But it's funny, right because you can delete tweets, but you can't edit tweets Now, you know, I I feel compelled to make a blockchain joke now There should be blockchain so you could watch the transition of a tweet But it's also, I mean, you know James Gunn like, you know I I crafted these extraordinary movies, but because I was a you know, delete expletive And possibly tweeting drunken thoughtlessly, you know, I mean it's it's it's I get okay, but but So on facebook, you know, if I see somebody has posted something and there's a little edit thing next to it I go again They probably had to go in and you know make a little bit of adjustment. That doesn't really bother me You kind of know that there was there there were a couple revisions being being being made or at least one But I don't understand why twitter is so adverse to this Because twitter has the most bizarre random collection of of Their morality like ebbs and tides and shows up and disappears and for some reason you're like We're gonna make sure there's a standardized record because you know for a while This was ending up in the library of congress and it's like yeah, so people can Tweet incredibly nasty things and either delete their account or delete the tweet But they want to make sure you don't modify the tweet and I get because again it right There's nothing worse than your option if you misspells to be like delete expletive Delete the tweet then type out the correct tweet and repost and then deal with the flood of like dude You just posted that like but yeah, you know, I I had an a instead of a u and I found it, you know incredibly You know it just it bugged me. So I changed it But it's it's funny because you know like if you do a change if you edit an entry in patreon One of the things it does like let your you let your users know this changed right and the idea that How permanent things are or not permanent or if you have a record of the changes Like on one hand if you smell something and you fix it Generally speaking nobody cares except for you maybe me and your english teacher from eighth grade right She spelled it correctly. She used that apostrophe, right? I'm so proud If somebody at the national level or international level in politics or just you know, somebody famous tweets out something You know obnoxious or racist or difficult and then it's like oh, no, no, no This is what I really meant and they retype it or they modified or they've completely flip it I can see where they they wouldn't want to change that but it's weird I mean it's dorsy This is not somebody I look to to have a coherent policy or plan at any time at this point Um, all right We we got to get to this next story because I'm too excited to talk about it software developer philip wang has used an Open source implementation of a gan a generative adversarial network to create a website called this person does not exist dot com The gan runs on nvidia software and creates a human face every two seconds creates doesn't assemble Doesn't mimic it creates a face from scratch every two seconds and as you refresh the website You'll get the latest creation It's important to note that gans don't assemble new faces from real faces But they learn how to create an image from scratch. They don't know it's a face You just train it with a bunch of faces and say come up with stuff that that fits the profile here And the way generative adversarial networks work is you have two networks one that creates the faces Another that's good at recognizing whether something's a face or not telling it That's a face. No, that's not a face until it gets really good And this is really good to the point that it will be hard for you to believe that these are not just actual clip art stock photography in most cases Well, I know we we all spent some time this morning refreshing the page of this person does not exist dot com and I was like They all look perfectly real and at one point roger was like, man There was a hairline that didn't you know didn't fool me but for the most part it is It's the best Fake people I've ever seen. I mean it's it's perfect and sometimes they're vaguely familiar But not familiar enough to be like, oh, yeah I see you took tiger woods picture and you know changed it and you know made it into something else It's not just morphed at morphed real people like no no it's machine learning is getting very good at this Climbing up the other side of the end can uncanny valley. Yeah, no, absolutely Like these the imagine what you can do with cg if you can you can start getting gans to do this Just as well on full motion video. It's not perfect I had a few people that looked red and some asymmetries here and there I also truly believe the 10 years from now. We'll look at this and go Oh, these are obviously machine learning because we'll we'll learn What the hallmarks are and they'll start to be obvious in a way that they're not obvious to us right now But right now these these look dead on to me There's some implications to that folks Especially if it gets into video, I think with stills it's more just like well now we have a lot more clip art to draw from but Yeah, folks if you want to get all the tech headlines each day in about five minutes Be sure to subscribe to daily tech headlines Dot com and vidya announced its earnings 80 cents per share in q4 on revenue of 2.21 billion that beat analyst expectations Analysts had only expected 75 cents a share on 2.2 billion Although it's down 24 percent from last year in revenue operating income decreased 73 percent all while operating expenses increased 25 percent so basically the analyst just expected the quarter to be a little worse Uh, but nvidia is still doing okay. It's still still making uh money even if the revenue is declining An nvidia blamed excessive Post crypto boom channel inventory they're getting a lot more inventory piling up because people aren't buying them To do bitcoin anymore or other cryptocurrencies. There's also a pause in purchasing from public cloud providers That's happening. There's some china currency fluctuations that affected this nvidia also believes it's coming fiscal year revenue is going to be flat to down slightly They don't think they're going to bounce back right away. It's fiscal q1 However should see the bottom of excess inventory for gaming gpus and that's where it bears on us the consumer If we have a bunch of excess inventory patrick, does this mean that Prices are going to be good for video cards and is now the time to buy one um Man prices are as good as they've been uh in forever And it's it's really curious to watch what's going on right now One of the things that was rumored video cards with a zed dot com You know they they were they have been showing sneak peeks rumors of what they were calling a gtx 16 60 Which is like a 20 60 but with the ray tracing stripped out and that's going to be like the 200 250 dollar gpu You know sales are not as strong as nvidia expected on the rtx cards in part because you know it took a while for rtx to finally show up in video games And and then when it showed up the performance like you would turn on rtx and your frame rates dropped through the floor And then two weeks later there was a driver update and the frame where it's we're still much lower but not so bad you just wanted to stop playing the game and It's really subtle. I think because I look at it and i'm like that's different, but I don't know if it's particularly better um The demos make it look really spectacular real world gameplay. It's not quite as spectacular and it's all very very early in the technology Um 20 series cards the ones that just came out are really expensive when a 1080 ti came out everybody's like this is expensive It's 699 dollars, but it's amazing gpu The rtx 20 80 ti the msrp is a thousand dollars it's 999 dollars And it's even more for the founders edition and they're selling for like anywhere from over a thousand dollars to $1350 depending on how fancy the gpu is so, you know, that's a huge jump That's a 300 dollar jump from the previous flagship on the upside in terms of 3d games The the 20 80 ti is 30 or 40 faster than a 1080 ti um And then things kind of get weird because you know if you look around Um, there's almost no 1080 ti's out there.  That's that's driving down earnings The top cards are expensive and there aren't enough of them. So so where's the inventory? Where could I find the cheap cards? Uh, so the rtx 20 60s, uh, which is kind of the sweet spot for 1440. Uh, those started 350 dollars Um, that's pretty good. Uh, it's kind of like gtx 70 performance With occasional bumps to 1080p perform or so I should say gtx 1080 performance If you overclock it it gets really close to the to the rtx 20 70 on 3d games That's a 500 card. So I think for a lot of people the 20s the rtx 20 60 is the sweet spot 10 series cards. They're actually finally at or below msrp Like you can't find 1080 ti's 1080s are getting really really short But you know the the 10 60s and 10 70 ti's are all around the price of a 20 60 But you should just buy an rtx 20 60 You know if you have if you do 1080p gaming and you don't want to spend any money right now There's a glut of 6 gigabytes 10 60s and 3 gigabyte 10 60s Don't go near a 3 gigabyte 10 60 unless you like don't game But 6 gigabyte 10 60s are selling for as little as 200 dollars Nobody wants them anymore because they're all looking at the faster cards. Uh, the prices have dropped What makes it really crazy is at ces right? We got the announcement of the amd radion 7 Which caused nvidia to freak out and talk about you know, this is a ridiculous card It will never work. Do not pay attention to the man behind the curtain um And it's a really odd card because when you look at the gaming performance for $699 well, you know an rtx 2080 is better for gaming But it's got 16 gigabytes of you know hmb2 ram Which is doubling the ram bandwidth. So for certain professional workstation scientific applications It is incredibly fast and it's also incredibly less expensive than the traditional workstation GPUs like if you if you work in blender Just try to find an amd radion 7 you won't be able to find them because you know Their initial allotment is completely sold out as is the tradition with amd gpus and eventually hopefully more will show up Driver updates are kind of a mess for both of these like I talked about like battlefield 5 got ray tracing support And the frame rates were awful and a couple three weeks later. They released a driver update There was a huge bump in ray tracing performance Um dls s just came out. It's just finally coming in online We expect that to see performance improvements as they tweak the drivers radion 7 probably has some driver from from Some performance bumps that'll come out of the drivers And what really makes this messy is you've got these rtx cards that are expensive You've got this sort of professional slash gaming card from amd. That is kind of expensive At least until you look at a 2080 ti and that's not even the next generation Processing or the next generation processor from amd Which is the navi which is going to come out later this year because that that radion 7 is actually You know a 7 nanometer process a die shrink with the addition of of that faster memory on there So we have a whole another challenge from amd Which will probably deliver a big another big performance boost for them And then what makes it really crazy and part of the reason they can't sell cards Is because most gamers which we think of as being the primary consumers of these cards are playing on 1080p monitors And they don't need an expensive gpu because they don't have enough monitor to demand expensive gpu performance So, okay So to bottom line two questions navigating through all this If someone's like should i buy a video card right now if they if they don't absolutely need one Is this a good time to upgrade and if if they're like no i have to get one anyway Whether it's a good time or not which one would you point them towards for the average person? So okay, if you're going to spend all the money, uh the 2080 ti the performance is really kind of of mind boggling And the frame rates, you know in ray tracing are usable If you You know absolutely have to buy a gpu or i have to actually absolutely have to buy a gpu and you don't want to spend all the money The rtx 2060 looks really really good.  It's very early in that So as always wait as long as you can if you have to buy now I would probably go with a gtx 2060 any if you're if you're if your budget is anywhere around 350 dollars If you are a professional take a look at the benchmarks, uh for the amd Uh radion 7 uh to see if any of your applications are accelerated by that card And it's a giant block of memory and if not if you're a gamer i would go for the rtx 2080 Excellent. Thank you patrick. I think that's going to help a lot of people out There's too much information. Sorry No, it's it's great. Um speaking of helping people out. Thanks to everybody who participates in our subreddit You help us out every day by submitting stories and voting on others from your peers at daily tech news show dot reddit dot com Um, and we don't want to count out the folks at facebook facebook.com slash groups slash daily tech news show They promise they'll get better. All right. Let's check out the mail bag sarah Alison shared and my friend anior is weighed in on the apple subscription discussion that we've pretty much had all week Alison says peter kovka who writes for recode Obviously knows way more than me when he explains why the media companies would consider giving apple 50% of the revenue in their news offering There's one more consideration. I didn't hear mentioned Apple customers are also very high value customers willing to pay a grip for phones As rub doing what i would say and pay for photo storage when google gives it away for free And double or triple for computers versus their windows counterparts No, I like this I like partially because allison was very kind and said not that we missed anything But there's another consideration because this is another consideration Uh, if you're targeting advertising a lot of times it's not the numbers you need It's the kind of people who buy your products. And if you have an audience that's a little spendier You might attract some more advertisers willing to spend some more money because they know that they're advertising to an audience That's going to drop some dollars. So that could make a difference too. That's a really good point Thanks, allison Yeah, absolutely. Thank you allison. All right, let's check in with len peralta who has been illustrating today's show len What do you got for us? Yeah, you know, I I told you pre show that uh, I was going to do a mashup Yeah, I didn't know whether or not this was going to be funny or not But uh, I guess the audience will decide that I mashed up This person does not exist dot com along with the alfanzo rebaro story And it's a picture of him doing the carlton and it's sort of like they did the copyright office said Hey, you don't exist. The carlton is not distinctive enough to exist. Uh, yeah No, he's yeah, he's He does not exist. Yes. He does the other the other that's true. Uh, the other uh, interpretation I have of this len is That the a that the gan the the neural network has just created someone doing the carlton Oh, and who who proves that yeah, this isn't distinctive, right? Even that could be the yeah That could be the next the next step in this. Yeah, oh a step not choreographer. Oh, that's right, right Exactly, not choreographer. It was four steps. Well, then we'd have a case. Yeah, three not enough is four enough I don't know five six. Where do we go? Yeah Uh, good stuff len also thanks to patrick norton for being with us I think the last time we saw you was at ces So what's been going on and how can people keep up with with with that answer is between now and then Firing up, uh, a c ab excel robert and I finally we kind of had a break over january We started firing out episodes this month and uh, if you want to get your home theater and audio on And of course shannon morris and I do the whole tech thing each and every week and uh, we uh, we review products And answer questions and we would love to have your questions if you have a tech question email ask at tech thing dot com because We're listening Yeah, man I mean if you if you wonder where patrick has all this knowledge about video cards It comes from doing those two shows all the time, right and this week in computer hardware. Yeah, yeah Those three those three shows together. I keep them up to date So if you're like, wait a minute, I have another question about these graphics cards based on what you said Go check it out tech thing dot com avxl.com this week in computer hardware Our goal each month for this show is to get one more patron than last month. We need seven More people if you are not yet supporting the show not yet a member of dts And one of seven people Please right now go to patreon.com slash dts when you become a member You get access to an ad-free version of the rss feed special episodes from myself and sarah lane Special columns from roger chang It's all available right there And in fact, we're running a promotion right now where if you stay at your tier for three months At the top two levels you can get either a poster or a mug with len peralta's art on it It's the five-year anniversary art that he did back in december So go check that out at patreon.com slash dts slash merch Our email address is feedback at daily tech news show dot com keep it coming. We love to hear from you We're also live monarchy friday at 4 30 p.m. Eastern 21 30 utc Tune in if you can find out more at daily tech news show dot com slash live We're off monday for president's day, but back on tuesday with patrick bezia talk to you then This show is part of the frog pants network get more at frogpants.com My favorite president is franklin pierce and why is that? because No one appreciates him The underdog president Oh, goodness, that's funny. Um patrick, do you have a favorite president? It's not franklin pierce. Yeah, he was not a nice man Did you just pull that name? I'm like, I'm like, yeah, he Tom what were you thinking? You might want to change that tweet You might want to edit that tweet tom William Henry Harrison He died in 30 days He died in 30 days of being president. Uh, yeah Really the one that caught the flu? Yeah, something. Yeah. Oh, man. I didn't realize it was that quick. Yep The only reason I know that is because one month of being top dog Then you get the flu get a flu shot We are the lesson learned Occasionally re regrettable care take your presidents of the u.s. That's from the simpsons That's the only reason I know that um remember the band presidents of the united states. Oh, yes Loved them. They were they were they were hot apologies for a minute to the folks in the discord Oh, let's uh check out the show titles Also apologies anyone who heard my dog chirping like a bird which he was in his sleep I did not hear the doctor Okay Hope you can see the husky ears Uh, you can dance if you want to fortnight I don't know. I kind of like that the best fake people Are real people Reach out and touch I mean Video cards tmi too much information human learning sorry No, sorry. No. No. No. No. It wasn't tmi. It's information we need I like dancing with copyrights Oh, but it's really it's not really a copyright. It's a trademark Yeah, but it's all you know kevin costner movie reference dances with copyrights. Well, it's also it's it's with the the dancing carlum That sounds like a cigarette at the dancing carlum but uh Well, what say you Um, I like dancing with copyrights. Yeah, I either like that one or you can dance if you want to fortnight Go ahead and I actually have to log off because i'm going downtown to see a an exhibition that my son has Oh cool This is the artist's son. Yes. He has a piece of student Independent exhibition and he has some paintings or I believe one painting in there and he He wanted us to come down and see it. So oh, yeah, um ever since I started following him on instagram I'm like floored by his thoughts. Yeah, he's um he actually, um He sold one of his paintings for some like huge Like somebody in the art community brought bought one of his paintings recently. That's so cool I mean, he's so talented. I mean he gets it from somewhere. Obviously not for me But yeah, I mean I look at his art and I'm like wow, I mean I I it's it's it's remarkable Well more common. Hopefully. Yeah, that's so cool All right, I'm gonna go where did Tom go the Tom? um is I don't know He disappeared probably putting in another hat on but um putting out some fire and it was so great to have you as always Of course, and um and can't wait for next week. I will there he is. There's time Bye. Bye. Bye Patrick Take care Do-do-do-do-do-do Okay, sorry about that Hope you guys uh, uh new problem. We were just saying goodbye to Len Oh, I miss Len Yeah, for some reason he's kind of having a cool art exhibition in downtown Gleeville Yeah, for some reason my computer stopped, uh returning audio to me And that meant that it was not returning audio to the discord either so apologies to the discord We're all that's what you meant. I wasn't sure what you were apologizing for Earlier Well, yeah, and then I realized that you could hear me. Uh, even though I can hear you so I needed myself Got it Technology Who doesn't it's um Well, I can see that it's starting to drizzle outside in my neck of the woods la here we go again I don't think it's supposed to be drizzling and you're not looking out the window Because yesterday we had like an inch of rain and an hour and a half and it was kind of yeah No, yesterday it was it was um the window i'm looking out now yesterday it was It was the entire audience is like boo-hoo.  Oh, yeah started to leak a little bit So that's where you get scared. Yeah Did we pick a title? We did. Yeah. Okay. What'd we pick? Uh dancing with copyright. Love it. Great. Um Ace ace time For I will need to edit out the audio Yep, I'll need to edit out the audio. I think you're uh, you're a dTNS audio should be totally fine Should it yeah dTNS audio was not affected Okay It's a good day internet that you'll have to edit. Why would you have to edit dTNS? Because um, it didn't it's not in the folder unless it was 36 minutes ago. Um, hold on That would be a different problem if that's true That has nothing to do with me dropping out because I dropped out after the show was over Production because life's not complicated right Isn't snoozing like a bird over here I wish you was gonna do this Roger. It's still uploading for some reason. Oh because I because I restarted I had to restart my machine. Okay. Yeah, so it's still uploading. You'll get it in a second. What are you doing? apologies Oh Sinking files right now Sinking the wrong file sinking. I'm sinking. I wonder how the sausage is made. All right, Roger. You got the file now And We have cool plans for the weekend Oh, we're gonna paint the bathroom. Oh, that's cool Yeah That's a fine question, um, probably just standard interior semi-gloss I got it. I got to redo my own perhaps I actually really like either super bright color I like I like deep colors and I like non, you know a matte white A lot of the softer I've I think it's just because of this one office I worked in where the entire office was not exactly white Not exactly yellow and not exactly dirty, but a color that had the worst of all three of those kind of ruined So much the entire off-white universe for me. Yeah. Yeah No Well, all right, uh, look forward to hearing what color you chose But that's not gonna be like a latex paint or anything Uh Hey, I don't know I I prefer latex Oh, oh, sorry, uh, that's the music from matt white Oh, I see what you're saying That's a pink color Took us all a second. No, I may uh, I guess the people about that had the house before me when they painted the breakfast room They painted over wallpaper now. It's got curling up underneath the paint Yeah, that's the there was Move the wallpaper Yeah, it happens more than you'd think and I thought I thought I had a leak in the wall Right from the the storms right and trace. There's no there's nothing from the ceiling or the side That would indicate there's no, you know water damage. Usually it would You would have somewhere where it would travel, you know, but it just it's Yeah I mean, it's I've removed wallpaper from a room before it's not insignificant amount of work But it's also it's not that hard to do it's much worse to just paint over it Yeah, well it also means I mean some people are cheap and in a rush. Yeah Some people are so lazy. I mean we were we were in one room where Not here but in a house I read it with my parents where we found Mixed four layers of wallpaper mixed with like three layers of paint And the oldest wallpaper we figured was mid 19th century Pretty much ended having like, you know, you did all the wallpaper removal stuff and finally that by the end of it, we were just sanding This last layer of was was the mid 19th century wallpaper cool Was there anything salvageable from that because I'd loved it just like historical perspective Yeah, no, no, we made from the original manuscript of the Gettysburg address. Yeah Who was the president at the time? Um, yeah, that's a good question I mean that house was insane because the oldest section of the house like the house the first transaction on the house was 1766 um, wow And the oldest section of the house dated back to then and we found it had it had been a Working farm for the better part of 250 270 years And it had a big barn and there was stuff everywhere.  We realized that they had been dumping their garbage Over basically dumping their garbage over on the far side of the ramp at the back of the barn and then throwing dirt on it Uh, we found I found patent medicine bottles. I dated back to You know 100 100 plus years Um So it was crazy and then we would find stuff like tucked into barn rafters and and underneath floors and and it was You know, it was an insane and really cool place to grow up And also the barn was wrapped with asbestos and you know, I once found a bag of dbt basically and other things So there was exciting things about being in the old house too He makes literally like apples way cooler burn than the one I grew up in Well, it was much older and There's this whole sort of farmer mentality where you save everything because it might be useful So some of the stuff was like it would have been a poultry farm Oh the dbt that's where you get the thin eggshell. So it makes it easier for people to crack open I don't really think that's where they were going with that Well, that's why I think pan dbt because it made uh, yeah bird shells very Fragile like eagles and they became endangered. So it's not yeah We were not actually not because it was bad for people it was because it was bad for the entire of it Which you have spots on my apples, but leave me the birds and the bees please Is that jony michael? Yep, and then uh Counting crows to the cover. That's right. That's right. Very good. Oh Really, how do you guys know this? I know I know the song the jony michael song just because I know the song But when I asked the amazon echo to play it earlier today, they played the counting crows version and I was like, oh I don't know either of those songs. I don't think It's called big yellow taxi and it's uh, the one don't it always seem to go. You don't know what you got till it's gone Oh, yeah, the paradise put up a parking.  Oh, yeah. Okay. There you go. Yep. Yep We all have her we all have her lanes. That's right Ha and I'm a stand mine.  We started pulling in buzz out loud and stuff He said I could uh screen capture it and put it on reddit if I wanted. I don't know if I have time to do that, but Uh, let's see Oh, it's too bad as long as I'm the prettiest. It's all good It's fine with me. I made a pun on elon musk's name Uh, and darin said that's okay. I get snubbed at the office stuff And I said well, I just try to stay in my lane at work Uh, and then darin said have you really the jury's still out on that? And I wrote roger that This is so dad joke, but also so funny. Uh, I'd lend a hand with that, but I've been so busy V understand Veronica oh And then he wrote well, it's norton really my job, but I care about you man And I wrote thanks man after allison and dunn back at ya Wow That's true friendship. Oh it kept going I mean that's that's that that is real. That's not you could you could have a lot of acquaintances who would just not do that with you on signal Darin kitchen true friend Patriot a lot of acquaintances. I know who would and have in similar situations wrote stop in all caps It's probably me. Yeah I still to this day shameless makes puns and I'll be like you're not hanging out with tom anymore Like why are you not acknowledging my my linguistic talents and who is tom? God damnit merit Oh Lamar speaking of stop this lamar wilson is the king of writing in all caps on most of my instagram photos stop this I've got a few of those from him too. It's funny. It's always funny, you know Yeah, and like if I respond like I'll never get another response like that's where it Oh, no, that's it stop this and he's moved on.  I agree. Yeah No, no, it's just a thing. It's a bit It's fine. Yeah Oh my goodness. I have one of the great walks with him of all time Nice the great walks We were in new york to do a thing for amazon and we basically he was ordering takeout And I ran into him in the lobby because my flight arrived at like 11 o'clock at night And we ended up going to we're going to go walk down to a korean restaurant I used to go to because we were like a block from where I used to work in the city And we ended up walking all the way downtown to china town Yeah, it was a good walk. It's a pretty hysterical conversation too I mean funny, dude. Yeah, I'd walk in manhattan with lamar. No problem walking with lamar sounds like a podcast Yeah Right now video folks go search for that podcast. Yeah, that's that's gonna be your next thing audio folks stick around. There's more to come