SF Scala: Meredith L. Patterson, Ambiguity Is Insecurity
Recording: SF Scala: Meredith L. Patterson, Ambiguity Is Insecurity
Tonight I'm going to be defending the claim that you see here. Um We hear a lot about the the epidemic of insecurity that is, you know, that is sweeping the the software that uh you know, exists in everything from our phones to our desktops to our critical infrastructure. Um you know, this is this is a multi-billion dollar problem. Um you know, especially with um you know, new regulations um making uh you know, like the GDPR making data uh you know, something that you actually have to protect now um otherwise, you know, pretty severe financial penalties. Um you know, this the stakes are finally starting to get raised on, you know, the cost of insecurity. Um So, what I want to talk about tonight is you know, well, we're going to we're going to talk about what language theoretic security is. But, in order to do that, come on. All right, maybe this does actually need to be closer
Thanks, Bluetooth. It was working before. There There we go. All right. Well, right. So, in order to as in order to answer the question like what is language theoretic security, first we have to ask and be able to answer what is language. So, let's talk about that. At its most basic, a language is a set of strings
Not that kind of string. More like these kinds of strings, you know, strings of text. The um a language can be a finite set. You know, those are the simplest kind to have to deal with. But, the set of strings in a language can also be infinite. Um and what generates a language that has the possibility to have an infinite number of strings in it is uh what we call a grammar. Just like, you know, in your in your English class when you're in school. Grammars uh describe, you know, the structure of expressions
Um you know, from the sentence level to the clause level to the phrasal level you know, all the way down to the to the vocabulary that's in the language. Um you know, and when it comes to um you know, when it when it comes to like network protocols, file formats, message formats you know the meanings of not just the, you know, not just what goes into the protocol, but how you talk about the protocol has to be pretty rigorously defined. You know, um there's an RFC that exists solely to define the meanings of words like must and should um in the context of other RFCs because, you know, in order for a person to implement a protocol correctly, they have to understand what, you know, what the implications of things like must and should are. Right? They have to they have to understand, you know what decisions though you know, about the about the implementation are obligatory and what decisions are optional. Um and you know, what happens if if they if they don't actually fulfill their obligations, right? And everybody has crucially, everybody you know, who works on you know, on on protocol implementations that use this kind of language you know, is supposed to at least, you know, come to a common understanding of it. You know, it's supposed to be the case that any one person's implementation and any other person's implementation of like the same RFC will be interoperable. In practice, does this necessarily already happen? Not really. So, I was sort of getting ahead of myself a little bit there
I mean, natural language is very, uh, you know, very underspecified, right? If I were If I were standing out on the street, you know, upstairs, and I saw a car speeding towards pedestrian, you know, I wouldn't have to show I wouldn't have to to get out the entire expression, "Look out for that car!" before, you know, before they had you know, before they jumped out of the way. I might just get, "Look out!" OR JUST, "AH!" AND BUT THAT WOULD STILL be enough information for them to to recognize, you know, even though the statement is incomplete, that something is going on that they should pay attention to. Formal languages, on the other hand, not so much. Um, you know, in HTML for instance, if you have an incomplete expression, like, you know, this body tag that's not correctly terminated, um, you know, that breaks the entire rendering. Now, we're also going to talk about processes, things going back and forth, you know, dialogue. You know, protocols are often interactive. You know, TCP, for instance, involves like, you know, two machines interacting with each other. Um, you know, I like I like using cars as, uh, as a metaphor for this, you know, because you know, you've you've got two parts of the you you've got two sides to it
You've got, you know, the human that's you know, that's sending the commands and the machine that's carrying them out. Um and you know, there's there's a there there's an idiom, right, for driving. You know, the the steering wheel is pretty much always going to be where you expect it to be. You know, the the there's always going to be, you know, the gas pedal on the right and the you know, the brake just to the left of that. Even you know, no matter what no matter whether you're you're driving like, you know, a US car or a UK car, right? Even even in a UK car, even even if the the steering wheel is on the opposite side, you know, the the pedals are still where you expect them to be. But sometimes you end up seeing you know, dialectal variations, right? You know, the the the indicator levers might be on the left side or the right side. Uh you might have paddle shifters or a you know, or a or a stick shift. Um you know, you if you might be driving a manual or an automatic, you know, an automatic is not going to have a clutch
Um and you know, you you have when you move from car to car, you have to learn a different dialect, right? It's the same it's the same process but executed ever so slightly differently. And this can mess you up, right? Like if if if something isn't where you expect it to be, um you're going to have you know, you're going to run into trouble carrying out the protocol of driving. And this is only more insidious and only more subtle when it comes to programs talking to each other. But before we get into that, let's talk about what language theory is because, you know, when we you know, it helps to understand what we you know, what language theoretic means. So, there's basically an entire subfield of discrete mathematics that's all about grammars and how they work. Um grammars are basically generative engines for for languages. You have some meaning that you want to that you want to express in a language. Um the grammar is the you know, the the structure that you hang that on
Um you know, basically taking the wood chipper analogy and you know, turning it into a simpler diagram. Automata, on the other hand, are um algorithms that interpret languages. Um so, this is a bowerbird. Um bowerbird bowerbirds um build complicated nests to attract their uh their mates. You know, so it's it's slowly build you know, building up bits of language into you know, a larger into a larger meaning. Um there are different kinds of automata for different classes of language. We will talk we'll talk about the different classes of language uh later on. Um but basically generation and interpretation are the the two important um you know, classes of process that we're talking about here
Uh generation is output and generation is what you do to make output and interpretation is what you do when you receive input. So, what do we mean when we say security? Personally, I like to put to Dan Geer on this one. He's the the CTO of In-Q-Tel. So, I I I like to think he knows what he's talking about. Um and he says it's the absence of unmitigatable surprise. Um basically you know ideally everything that happens doesn't come as a surprise. But if something does come as a surprise, you have some way to mitigate the bad effects of that surprise. And the biggest problem that you know that we see with you know with input handling um is that adversaries are able to come up with uh strings input strings that implementers didn't expect
You know, they never thought the implementer never thought that somebody would try to you know that that that somebody would try to you know to to pass something that you know didn't conform to what the you know what the developers were expecting. Let's talk about ambiguity. When there's more than one possible interpretation of a thing, um you know that's that's the you know that that's the dictionary definition of ambiguity. Um the most important ambiguity that uh ambiguities that we encounter I sort of alluded to them earlier. Um you know when an implementer um has a different understanding of what they're of what they're implementing than what they eventually end up instructing the machine to do. You know in other words, if the the implementer thinks they understand the specification, but uh the you know but they the but they've missed something or they've implemented something in in a haphazard way. Um That's you That's something that an an adversary can basically take advantage of. You know, the the the gap between developers' expectations and what they actually end up implementing
Um this is something that David Chapman has has written about somewhat extensively. Um from a from a more philosophical angle. Um You know, when when humans deal with ambiguity, you know, we we often try to you know to to resolve it one way or another. Um The thing is computers can only do that. You know, it's um it there's it's any you know, any input handling algorithm is going to be deterministic basically. Um what it's you know, how it's determined may also you know, be dependent on other layers in the system, right? Like you know, race conditions are a good example of this. You know, Spectre and Meltdown are another you know, another good case of this. And what's funny about those, you know, is that those were bugs where you know, under specification kind of came and bit us because you know, ti- timing timing sort of gets defined away um at at certain levels of of you know, of of of how we model like you know, processors for instance
Um and because nobody was taking that into account, but because time actually is a thing that exists in a physical system, um there was there was a deterministic effect that, you know, that could be exploited. Um we weren't reasoning about it because we assumed that we didn't have to think about time. Um but time does matter to the physical system. So, we're developers. We build things out of language, literally. Like that is what they pay us to do. You know, we we take we we take languages and we make stuff out of them. So, Claude Shannon, uh the father of information theory, um came up with a pretty nice model um that's that's survived uh you know, down to this day for describing, you know, the basic process of how we build a protocol, right? So, you start with some meaning, right? Some source of information
And that has to be transmitted by some entity. You know, could be a person, um could be a radio, could be uh could be a program. Um whatever that entity is, it's going to encode that information into some message. It will serialize it out into a message that it can transmit. And that message has to get transmitted over some channel. And that channel, of course, has properties. It might be lossy, you know, in which case the message encoding is going to need to be resilient to that. Um but that's kind of out of the scope of this talk
Um anyway, the message ends up at a receiver, which then has to decode it um into you know, the you know, whatever it whatever it's getting decoded into. So, ideally, the uh the the function that describes how the transmitter encodes the message in sorry, encodes the information into a message. You know, ideally that's the inverse of the function that the receiver uses to you know, to to turn the message back into the you know, back into the semantic content. Um but there's one thing that that this model is missing. And that's side effects. Um And you know, the incorporating side effects into the in into our mental model um is more accurate, but at the same time it also makes things a lot more difficult to reason about. Um I gave a keynote about this about five years ago. Um the uh the uh that the title is nearly everything that matters is a side effect, and there's a video on YouTube about that
Um okay, so one of the arguments that I have to make is that we need the simplest models that we can possibly you know, deal with reasoning about. Um in large part because you know, even when we have simple models, we end up composing them together into more and more and more and more complicated you know, models over time, right? There's no reason that the kernel should have like five ASN.1 parsers in it. It just does because that's accreted over time, right? So, we have like five different ways in kernel space of of interpreting um you know, of of interpreting ASN.1 objects. Um this is this is needless complexity. This is terrifyingly needless complexity. I mean, I don't I don't like to have to think about all this stuff. I I would really really really like for, you know, the for for the software that I'm using to interpret things the same way every time and, you know, not have this be like, you know, context-dependent, you know, depending on you know, depending on which library it happens to be calling that day, right? So, when there are ambiguities that um the persistent software um this can lead to exploitable conditions. Um I have a a small dramatization here
So, uh in this example, um uh Rick from Casablanca will be playing the role of an attacker. Um and Signor Ugarte will be playing the role of a certificate authority. So, the attacker goes to a certificate authority, right? And the attacker asks the certificate authority for a, you know, saying, you know, send the certificate signing request for a uh for the for a domain that uh you know, that that is a subdomain of a domain that he actually owns, right? You know, he owns rickscafe.com. Um deutschebank.de.nobite.rickscafe.com is at least in ASN.1 um a string that, you know, that that that is like, you know, that is a data domain name. Um and you know, so so this is actually this is this is actually taken from um an attack that uh Len Sassaman and Dan Kaminsky and I did back in 2009. Um it uh Moxie Marlinspike also uh discovered the same thing and gave a talk about it at uh Def Con that year. Uh it was called the null terminator attack. Because what happens, you see, is when the attacker goes ahead and presents the signed certificate to a web browser, the web browser treats that null byte as the end of the string and treats the certificate uh that you know, the the Rick obtained from the CA as if it were a certificate for just the just the substring that appeared before the null byte
You know, so you've got two different parsers. You know, the the CA and the web browser are using different parsers that treat that string differently. You know, the the first one treats it as like a four-level deep subdomain. The second one treats it as just you know, as as just a regular um you know, gTLD level domain. And because they disagree about this, um the attacker is able to make that make that cert look like it's a valid certificate for a bank where you know, when it's actually um a cert for um you know, um you know, for a for when it's actually a cert for a subdomain that uh you know, that nobody would actually visit because it's not like you know, it's not like the null byte's even going to work in the in in the URL to begin with, right? And you know, so so there you know, just to just to go into a little more detail about this, you know, there There are a bunch of different implementations of um X.509, which is the uh which is the uh kind of sub-language of ASN.1. The kind of the same way that like JSON-RPC is like you know a language built with JSON, X.509 is like a language built with ASN.1, right? Um So, you know, OpenSSL had its own implementation of X.509 parsing um CryptoAPI, which was what Microsoft used, had its own version. Um NSS, which is what Mozilla uses, had its own version. And, you know, because they were ever so slightly different, we were able to um you know, we we were able to leverage this to just forge SSL certificates
Um simply because the different implementations had a different syntactic interpretation of the uh of the certificate. And, this has played out over and over and over again in all different in all kinds of different areas. Um you know, Sergey and I gave uh a couple of talks at ShmooCon in 2012 and 2013 where we talked about um where we where we went into quite a lot of detail actually about like, you know, how uh you know, how how parsing of DNS packets went wrong in BIND, um how uh the Internet Explorer 8 uh cross-site scripting like protection filter actually introduced cross-site scripting bones uh because people were able to basically pass um fragments of malicious uh HTML or JavaScript in such a way that the uh the filter would rejoin them. Um PHP has had quite a few problems along those lines. Uh Ruby as well. Um like particularly with JSON. Um Uh yeah, I mean the list just goes on and on and on. Um And just in case you think this is just this is this is one of the application protocols, USB has the same problem
That doesn't surprise me. So the real the real shift in thinking that I that I hope you're able to take away from from my scattered jet-laggy ramblings, which I again apologize for, is that, you know, everybody likes to think of the program as the thing that's in charge. You know, the program chews up the data and, you know, and then it's done. It would be nice if it actually worked that way. Really, the program that you have written is a virtual machine. And the input that it processes is the bytecode that executes on it. Um and what this means is that you want that VM to be total. Um you want it to be able to have a definite you know, a definite response to any input it receives
You know, that that that response can be no. Um you know, it's it's not it's not only fine, but um you know, but savvy to, you know, to drop bad input on the floor before processing it because like, you know, if if it's never going to resolve to anything in the first place, why burn the cycles on it? But crucially, you don't want there to be like it you don't want the virtual machine that you have created to you know to have surprises. You know, when you when you trust your systems to behave in a predictable way, but you don't verify that your assumptions actually hold, um this is you know, this is when reality comes and bites you. So, what are we able to verify? Well, I talked a little bit about uh language classes earlier. So, let's let's delve a little farther into that. Um so, the simplest languages that um okay, well, I I actually left one off of this of this chart. I mentioned finite languages at the very beginning and finite languages are actually simpler than regular. Um but as far as infinite languages go, languages with uh you know, an an infinite number of possible strings in them
Um so, the regular languages are are the simplest um and those are just every uh every language that can be described by some regular expression. Um there then there are two classes of context-free languages, deterministic and non-deterministic. Um those are recognized by uh what are what are called the pushdown automata. Um on top of that or so sorry, more complex than that, um we've got the decidable languages, which are recognized by linear bounded automata. These are also known as the context-sensitive languages. Um and then you've got the the Turing recognizable languages, which are which are undecidable. So, the reason we've got the the zigzag boundary between decidable and Turing recognizable is if it's a Turing recognizable language, the only way that you can you know, tell what it's going to do is to evaluate it. You know, the the recognition and evaluation are the same thing at that point
Deterministic context free and regular however, what's nice about them is that those are the two classes of language for which grammar equivalence is decidable. What do I mean by that? Um So, if if I have two deterministic context free grammars it is possible not necessarily easy, but possible to prove whether they whether they generate the same language or not. Um past deterministic context free, it is an undecidable problem. Um So you know, the the one one way to to get around this right is you know if you use the same if if you use the same grammar and you know, generate your your input handling code from it, you know, you can you can you can sidestep the the question of you know, the the the the question of grammar equivalence um then it's really more a problem of you know, that then it's really more a question of okay, well, what assumptions are is your is like you know, your runtime making you know, if you're if you're talking about you know, implementations in two different languages, right? But you know, all other ceteris paribus if you're using the you know, if if you're if you're generating a parser from the same grammar um you should you know, you should get you should get equivalent results. Even if it's a tutor for languages. Come on, keyboard. All right. However, the you know, where this gets where this gets challenging is that um most of our um most of our network protocols are not in that uh in that nice little deterministic context-free or regular class
Um If I may jump in. Sure. So, what you just saw on that chart, right, is the doom of distributed systems. Right? What is a distributed system if not a bunch of parsers? I mean, probably like a horrifying example, right? Um there's a there's a SCADA protocol, like industrial control systems protocol, called DNP3. Um it's actually a three protocol stack. Like it's it's it's a three-layer stack of of formats. Um it's got like cross-layer data dependencies. Like you know, there there are fields in one layer that are dependent on on fields in previous layers
Like this thing was almost designed to be to be like hostile to to to parsing safely. Um and you know, this is what happens when critical infrastructure protocols get designed by committee. Everybody tries to cram in every you know, all the vendors want to cram in their preferred features, and you end up with a horrifying mess that you know, that we're stuck with. So, what happened? Well, I think that there are you know, I I think that there is hope. Um First of all, you know, I've I I I alluded So, I alluded to this point earlier. Um, you know, if you if you throw away bad input, um, before you you know before you devote a lot of cycles to processing it, you know, that's ultimately that's ultimately a cost savings for you. Um, so just, you know, treating input handling as a recognition problem in the first instance, recognize your recognize whether your input is a valid string in your input language before you process it. You know, that by itself, um, avoids, you know, an awful lot of sends
And why is this not advancing? Okay. Um, similarly, um, yeah, we suggested context for your regular earlier. The reason for this is the less power that you expose to an attacker, um, the less power the attacker has to you know to mess with you with. Um, because we you know because we deal with you know stacks and stacks and stacks of software on top of other software on top of other software on top of like several layers of firmware firmware into hardware, um, pretty much any kind of you know escape to another layer ends up, you know, providing attackers with power that you know that the developer wasn't even thinking about when you know when they developed the you know the application that they were developing. Um, but reducing the you know lowering the expectations, you know, on what input is supposed to look like, um, means that it's mean means that it's easier to verify that the input is what it's supposed to be. Again, reduce complexity, reduce complexity, reduce complexity. You know, we learned the lesson of a vowel, right? You know, well over a decade ago at this point, or so we thought. And yet it just keeps cropping up everywhere
Again, if it's if it's turn complete, you're not going to be able to recognize it without evaluating. Um, and endpoint equivalence, um, like I was talking about earlier, protocols protocol implementations have to agree on what they're talking to each other about. Um, and if they're not, then you can fool them into doing things that you don't want them to. Um, you know, there exist Unix tools for trying to for for working with grammars, but um, they're they're kind of deteriorating. Um, and it like maintenance has not been good on Flex and Bison. Like it's it's it's in kind of a sad state. But that said, we have better languages now. Like you know, it's it's not the C days anymore
Like we have Scala and Haskell, you know, we have robust parser combinator libraries for those. Uh, Hammer is a project of mine. It kind of started out as stunt programming. I wanted to prove that you could actually do parser combinators in C. Um, and it turns out that yes, you can if you're stubborn enough. Um, it's also it's also got bindings to like every other, well, not every other language, but about nine or 10 other languages. Um, it's also in the process of uh, it going to be undergoing a fairly major overhaul this year uh, because the memory model's kind of screwed up, but I can talk about that later if you want. Uh, let's see
Nom on the other hand, so Nom is a uh, parser combinator library written using the Rust macro system and it's kind of magical. Um, because the parsers that it produces are extremely fast. I mean, like you would expect, right? You know, you're if you're writing your if you're declaring your parser using macros then you know, that's going to get expanded to code and it'll get compiled. Um, yeah, there I mean, there code using Nom is going into VLC like as as VLC moves off of C and onto Rust. Um, so I'm I'm very sanguine about Nom. Um, and the JetBrains uh, meta programming system is uh, a particularly interesting uh, piece of kit. It's basically um, an IDE for developing for developing languages. Um, it's it's really cool for developing DSLs
Um, and actually this is probably a good place to plug the um, uh, the software language engineering conference um, which usual this year it's attached to uh, Splash which I think is in Boston this year. Um, but yeah, if you're if if you're interested in programming language engineering in general um, I strongly recommend checking out SLE. Um, it's in the fall. Um, yeah, that's that's where I learned about MPS. You know, but at the at the at the bottom of it all, this is you know, the the problem that we're dealing with is a a problem of you know, uh, it's it's a problem of pedagogy. How do we teach people how to build software that takes in untrusted input in a safe way. Um and that that starts out with figuring out, you know, how how people take problems apart. You know, you have to you have to decompose a problem into you know, into its individual pieces and solve them in the right order
Um like I was saying earlier in the talk, we have many many examples of trying to process data as we recognize it, like what I was talking about with DNS and IPv6 and bash and everything else. If you try to if if you try to you know, if if you try to process and recognize at the same time, you end up with a tangled mess. Whereas if you decompose the you know, where where whereas if you decompose the problem into first recognize, then process, you save yourself a lot of pain. You know, it's it's also a question about, you know, infrastructure and how we want it to last. Um you know, the the Rob Graham has a has a really fantastic talk on YouTube from BruCon. I believe it was 2013, but it might have been 2014. Um where he talks about it he basically draws a lot of parallels between um what civil engineering does right and what and what software engineering does wrong. You know, we're we're not The Verrazano-Narrows Bridge, right? Uh you know, the the this this particular this particular bridge has been studied like over and over and over again in in in civil engineering because you know, what people didn't realize when they were designing the bridge was that um you know physical effects from you know from from wind and the and the way that the bridge was was built would compound you know and you ended up with like you ended up with a with an incredibly unsafe surface
Right? And we don't really learn from those kinds of cascade failures in software. Um we've had lots of we we we've got a lot of examples to build on now though and we need to start learning. Um and crucially just not exposing power to to adversaries. So this is the this is my argument. Um let humans enjoy ambiguity and all of the all of the all of the fun and humor that it provides but you know let communication between software be unambiguous. And any questions? I am sorry if I was terribly confusing in my adult state. Not at all. So how do Scala and Haskell fit into this? Well first of all um gosh like three different things exploded into my head at the at the same time
Let me let me see which one I'm going to take first. Okay so first of all there's been a lot of really principled research and development into rigorous parsing. Um that's just you know that was just developed first in those languages right? Like I know the parser combinator library is not really batteries included in Scala anymore but it was for a really long time and I and and I don't know in my opinion it should still be. You know, partial combinators were first implemented in Haskell. And like pretty much most of the of the the cutting edge development in parsing happens these days either in Haskell or in Smalltalk. Yes. Is there a meaningful language or language security you write a difference between interpreted and compiled languages? That's an interesting question. So I mean most interpreted most interpreted languages don't really give you a lot to work with you know when it comes to type systems, right? And if you know if you think of the you know the problem of parsing as a problem of turning strings into well-typed objects, you know, well-typed is important there
You know you you want to you want your type system to be able to help you. I don't know whether that actually answers your question or not. Can I can I interject? Sure. If you think about it really hard, a compiled language is just an interpreted language in which the interpreter is a piece of silicon. That's a good way of putting it, yeah. Also if you have a chance to write a virtual machine, it doesn't have to be a real machine. Whereas your processor will be. It's somehow Sorry
So so JVM is is not is not a real machine or or is it? I'd I'd punt on that one. I don't know the detail. I mean it depends on which JVM, right? There there you know DOD has verified JVMs I'm given to understand. You know, does the same hold for Open JDK? Good question. The other thing is that the JVM was designed by someone who at least knew what he was doing. Yeah, Phil Wadler's no no slouch. Yeah. Phil was actually Guy Steele who did a lot of the uh Oh yeah, that's true
But yeah, I know I know I know type erasure was Phil's fault. I would possibly add to the answer. I would rather like you to think not of what you think of as programming language, but of the language of the data that that programming language language consumes. Because you get these results of ambiguity, and you get those results of input driving your implementation, either compiled or interpreted, into some sort of a weird inconsistent state, and thereby enabling essentially the reprogramming of your uh entire system by the incoming data. Um Um and this doesn't really need to depend on how you implement the processor. It could be an interpreter man, isn't an interpreter that suddenly springs an unexpected mode of programming. Uh it uh case in question, JavaScript has been found vulnerable to the language of its regexes. Regex
Uh uh a cheat uh compiled language was found vulnerable to the language of its format strings. Right? Uh on the other hand, you may have nothing that you think of a language as such, because the elf loader has been found vulnerable by Vex here. Vex, take the phone. Uh two metadata of the ELF executable. So long as you control the metadata of the ELF executable, the loader will execute the program while loading your code before running any of it. Uh If you wanted to talk that, then if you happen to control uh memory descriptor tables of the x86 MMU, uh such as the LDT, GDT, the page tables, and the TSS, the task switch segment, all baroque and from the point of view from the time when uh context switching was hardware based, which never really happened. Uh you can actually uh execute an arbitrary computation on the MMU itself without ever dispatching any instruction successfully. So, your uh your uh instruction pointer is always pointing at an invalid instruction at an invalid unmapped address
You cause a uh page fault. A page fault actually happens to read and write memory. Uh under certain conditions that they can fall to it can lead to a double fault, which also happens to read and write memory in the MMU logic. But it can actually fix up the handler for it and fix up You keep ticking between them. This is your processor. Uh the actual instruction decoding uh and execution and dispatching and the pipeline and all the fancy stuff that exists in the CPU need not apply. Um So, uh in that case, you're basically using what people Some people would say hardware, but this is really microcode, mostly. Uh and and and still your data is the input language that actually drives the computation, which happens to be Turing complete
So, any input is a program. Um uh whatever receives it can be of a very different nature. Compiled, interpreted, or uh baked into a chip. Um your conclusion was that uh computers should communicate only in unambiguous um program um format. Um I guess I have a kind of a uh counterargument or, you know, a a inflammatory statement, which is say I don't think it's ever possible to be completely unambiguous. In the sense that in order to describe one protocol, you have to use a language, whether it's a regular expression or whatever. And then you need to implement that in some programming language, which in turn is not specified 100% like Scala, for example. Maybe Haskell comes close
And so and then that language is then implemented by a compiler onto a machine, which has not been formally verified. Therefore, ultimately, there is always some ambiguity, right? Now, in practice, maybe we can get closer and closer, but Well, yeah, and I mean, this I I I sort of touched on this uh earlier when I mentioned Spectre and Meltdown, right? Um you know, time was you know, was not taken into account in the modeling. And it was in fact a timing channel um that was being exploited um because, you know, the there there is some physical system, right, that, you know, that ultimately, you know, this the yeah, that ultimately is performing here, and time matters for it. Um so, you know, what that what that means is that our models have to get better. You know, if if if we've under specified a model, we can fix that by correcting the specification, but we might not find out that we've under specified something until, you know, until it fails in practice. JSON is actually another example of this, right? Um you know, we've we've discovered the hard way that, you know, even though the the you know, even though it looks like a a nice little, you know, context-free language, um it's not immediately clear what's supposed to happen if uh a key is duplicated, for instance. And this has led to vulnerabilities in deployed software um because people assumed it would do one thing, and it actually did something else. Um so, yeah, I mean, I that's that's that that's absolutely a uh you know, a a a valid rejoinder, but really, you know, what it what it points to is that, you know, this is an ongoing process of elaboration
Um actually, if if you'll permit me to go on even more of a tangent, um you know, your your your remark earlier about how, you know, we have to, you know, how you know, how like the specification has to occur in some language, right? Uh so, the philosopher Robert Brandom, um you know, philosopher of language, um has has written about this um uh this sort of bootstrapping problem uh in a book called Between Saying and Doing. Um he he he actually uh develops a category theoretic treatment of how um an expressive vocabulary basically how a more expressive vocabulary can be elaborated from a less expressive one. And he he specifically points at like um you know, how like programming languages can be specified um using you know, using weaker uh weaker formalisms than than they actually are able to produce. So, we can talk about this rigorously. We have we just have to make sure that we're talking about everything we need to be talking about. Do you see a universal disambiguator product coming? No. We wish, right? I mean, somebody comes up with a specification and you just give it to this program and the program says, "Yeah, it's deterministic. No, it's not." So, try again
Question. So, why is it that us like computer scientists have all these problems, but mathematicians don't seem to have these problems? I don't know about that. Like, you know, I I I've I've run into plenty of I've run into plenty of disputes about notation in my time. That's space versus I I um I I disagree. Uh they had an enormous problem, an identity crisis in the beginning of the 20th century, right? And in fact, much of the so, the uh uh metatheory of mathematics uh which we now uh have at our fingertips with things like Coq, right? And Peano axioms. And that gives us total languages. Yeah, I'll I'll I'll open my notary program. Exactly
So, uh mathematics has had its moment, just like this. So, what are we going to do about it? Uh to survive, you mean? Well, we will survive, just like math did. It's just that we will need to take it seriously. Just like math did. That's why it survived. So, and and and this is a this is a a an extremely uh uh relevant question, right? Uh they've had a um uh a series of paradoxes that basically put lie to just about any claim of math being precise. Yes. What I'm really asking, of course, is like so the mathematicians confronted the failure of Cantor set theory and Dedekind set theory, Cauchy's calculus, Bolzano's calculus, like all these things failed and they didn't confront it
Russell's paradox was a big thing. It's the only one. And like in response to this, Hilbert kicked off this whole thing about formalism. And when Brouwer was like, "Nah, let's not do that." And like Hilbert's like, "Yeah, we're going to do that. We're going to." Right. And like they did. And like it took them like some period of time to recognize and get serious about the problem for later on and everything. But why is it that us in computing, like buffer overflows go back at least 1972? Um Why can't we do that? Perhaps we can't even stand badly
I like your style. Mathematics Mathematics wasn't being applied in a winner-take-all, first-to-market, multi-billion-dollar industry. I can interject actually. Excuse me? Um interestingly, uh one of the key precepts here of language theoretic security is the notion of type safety, which is where the language kind of comes uh comes in. It's not about the language in which you're programming, but the the notion of the mapping of that typing system uh to the language that you're trying to accept in first. place. so, really, if you think about it, the the dream that they tell you in in undergraduate school about proofs being mechanically verifiable, really, if you wanted to extend that concept into programming, the natural analog would be, when you write a specification, make sure that you define the typing system whereby you can mechanically verify the message in all your scripts. So, Andrew wanted to add something
Uh most of foundational issues in mathematics don't affect that much of how it is used in practice, which is a lot of why Hilbert encountered resistance. For I mean, you could have gone through that whole period working on on on any of a number of other of other topics in mathematics and never encountered any of those issues. You can't change the bottom of the software stack without affecting everything everyone does on top of it. Uh and you might say uh that uh math is still pursuing its own foundations, the homotopy type theory being the the Yeah, the whole univalent foundations program. Yeah. So, uh Voevodsky, who unfortunately passed away, um did have uh a personal brush uh with a proof that he wished he he wished he had verified. And then committed to that program of uh uh proving everything uh with mechanized means and checking the proofs with mechanized means. It was a huge loss
He did pass away. I think that that hot business is the exact same problem that we're looking at. It's the axiom of unique specification. If I I mean, I don't know that much about hot, but my understanding is that that we replace this issue of axiom of choice with a new issue of active unique specification which by the standard protocol speaks exactly what you're bringing up which is you cannot guarantee that star with eight things are indeed type in a isomorphic manner. Is that accurate? You can, but only if you constrain the language. That's what largely I think what Meredith was getting at when she said that the equivalence problem of grammars is solvable for deterministic context-free but no no more complex than this. Um and so certainly there is a need for further work. Um one of my own favorite things is to specify protocols in the BNF
Everybody hates to do this but you can make a clear mapping between the BNF grammar and something in any of any programming language that's complex enough to parse. Um so yes, you're absolutely right. But the idea here is to solve a more limited version of the problem at the very least when we're parsing. Um I know I'm on a very small very small tangent here. Um consider the notion of validity of public keys for authentication. Um I can't say where this bug exists but it does exist. If I specify a public key and my public key is just RSA, right? RSA has a trap in it in that you can say well this this BNF for this regex gives you an RSA key. Fine
If you don't constrain the problem domain and say our goal for this system is only to protect against keys that uh gaining a weird machine or general execution on on the thing in which we're processing. Um you might run up against deficiencies in the model and one such deficiency is that all fine here is my RSA key. It's 2 to the 17 bits long in the modulus. Uh every time you want to reject my authentication attempts you have to perform RSA of that length to figure out whether I'm telling you truth or false. But um and so I mean even again, you can specify all of these things in terms of of BNF if your goal is to determine whether it's a valid message or protocol and whether you should accept it or not. And if you're trying to avoid problems whereby your parser accepts things that it puts your processing into an undefined state, this works perfectly well. Um it's hardly a panacea for security if your security considerations include something um something beyond that. So, you really do have to tailor the approach to your exact purpose
Uh you might say that whatever uh I mean what people call parsing is a huge misnomer. It's actually a kind of evaluation. Yes. Uh in fact, so is um uh so is any kind of rendering as we have been uh so as we have been just shown by the Efail, right? And signal uh cross-site cross-site scripting. Well, serializer flaws, right? Uh And you just have to ask yourself, why did these nice people see fit to add more evaluation to uh a text message? Put that on my tombstone. Efail is just such a perfect example of why you would say there are problems with it so much because if our all of the general person is lower ability to detect, uh you unwrap the thing and then you get active content and the active content can do whatever it pleases, including disclose the contents of the message to the active adversary. Um you It's another example of suiting it to your purpose. You can't simply say, "Well, my part, the PGP part, is perfectly adequate and we can parse this and it's simple math." Um if you have a format that is as S-Mine, which is an ugly, nested thing, it can contain multiple different parts, the model for which parts can be what to other parts is completely implementation defined in the sense
Um, you can end up with these issues where you have a really technically valid message that has emergent semantics that nobody even thought of. I mean, how old was S-Mine? It was from the '80s. Um, until now, nobody had noticed that parts of the message could decrypt other parts, but it could view the parts of the message that You you cannot have things that are this broad because this emergent functionality comes from the fact that you cannot reason about. This is just uh this is really just Rice's theorem. We cannot non-trivially reason about things that are more complex than a certain class of complexity. Anybody else? Well, let's thank my host again.