[LAUGH] All right, cool, we've got Nate Foster, Professor at Cornell. Super expert in programming languages, and all things in programming languages meets SDN. He's a well known for being one of the leaders in the Frenetic Project. Which also we're learning about in the class. So thanks Nate for, for hopping on to answer some questions and, and chat. >> Thank you. >> Cool, so so I'm curious what your, your background's certainly in, in programming languages but you, you definitely have been pretty, pretty deep into networking the past couple of years with the Frenetic Project, and I'm wondering, what led you to, to start working on it? You know, what, what kind of, made you jump the fence over to networking, what were the initial goals of the projects, you know, and, and more importantly, it's still going on, right? So, how's it, how's it changing and evolving as, as the project continues? >> Yeah, so I'll tell you a bit of personal history. As you alluded to my background was really in program languages. And, and somewhat towards the theoretical end of things in functional programming and type systems. And quite a bit away from systems and networking. But there were two things that kind of led me to start working this area. So one was that UPenn made a hire towards the end of my PhD. [UNKNOWN] so [INAUDIBLE] to this PhD at Berkeley I think it was [UNKNOWN] but he was working on this project called [INAUDIBLE] networking, where they were using a logical programming language called [UNKNOWN] to data log, to write, distribute writing protocols. And I thought this was just incredibly cool. The idea that you could take kind of the core pieces of these really complex things like, like BGP and, and encode them in a very beautiful way as a, a logic languag, and then you know, optimize it and analyze it, and prove things about it. I thought this was just a really cool connection. So I was already kind of. You know, intrigued by, by that kind of marriage of, of a very implied area, being treated by some quite formal techniques. And then, as I was finishing my PhD I was poking around for post-docs and and wrote to Dave Walker at Princeton and said, are you hiring post-docs? And he said. Well, I'm going away next year, but my college Jen Rexford is looking for someone in programming languages, to start working on developing languages for this new kind of network architecture, if you're interested in learning something new, this might be fun. And so that was that led me to sort of make a jump, and I think I guess that and, general advice for kind of grad students, and I think, whenever you can find areas where there's you know, maybe you have some training in and [UNKNOWN] can, can find a, another area of CS where your tools can apply. This can be a really powerful combination gives you really, you usually have a, a fresh perspective on things but also you, you learn a lot about stuff that you probably don't have much expertise in. And so you can really stretch in interesting ways. So that's the personal side of things. I think the [LAUGH] the, the vision, I mean, really I can. Jen Rexford who is my post-doc supervisor I think had the vision that, that there would be some interesting problems with SDN that some language techniques might. Might help with. And I can't take any credit for that, because that was completely her vision. As far as like our, our initial goals for the project we really started out just trying to write some programs. So, I, you know, initially I, I spent a few months just trying to. Take NOX, which was the first open source SDN controller. And just try to write some software in it. And sort of, you know, see what works well and what doesn't. And the thing that very quickly we discovered, was that NOX's programming model provided very little in the form of modularity. so, I don't know if you covered NOX in the class or not, but [CROSSTALK]. >> Yes. >> [INAUDIBLE] So NOX and, and many other controllers, basically would, you know, receive the network events, in the form of open flow messages, and then pass them up, a chain of event handlers. And so, if you were writing a network program, what you would do was write the code for those network handlers, and then choose, you know, for each element of the chain, whether or not to propagate the event up. so, already you kind of have these dependencies between different bits of code. Because, one handler installed below you, might obscure your visibility, if you're a module sitting higher up the chain, into events that you want to see. Another problem is that, each of these elements of these chains, these modules, are actually installing rules, in the flow tables of switches, and so, and, and they don't really have any protocol by which they can negotiate, you know, when it's okay to install a particular rule or not and so you can get this kind of interference between modules, where you know, one module might want to block traffic. And another module might want to forward it. And, if they both just installed rules, you know, whichever rule gets there last, is going to be the one that takes effect. And so, you know, some experience kind of trying to write programs and, and discovering that oh, it's actually tricky to kind of separate out the different concerns for different modules, and then turn that into running code. Led us to think about, well what if we, sort of, moved to a different programming model, where instead of responding to events and manipulating forwarding tables, we could describe at a higher level of abstraction, which functions we want the network to implement. And once we make that shift, we can then start to think about different ways of, combining functions that would correspond to sort of module composition operators. And that was kind of then, then we were kind of off to the races. >> Are the, are the, are these kind of abstractions in modules that you realized were ki, were appropriate for these kind of problems, are, are they, similar to, to the, you know, hammers that you'd use to solve other kinds of problems in programming languages? Or were there kind of specific things in networking, in, in these networking problems where you find some that you needed, you know, new, new types of, of of tools? In other words, like, were sort of new things that you had to put in the PL toolbox to, to solve these problems? >> Yeah, so, so two things I'd, I'd say here, so one. One thing I think has been exciting about the work that many different groups have been doing in this area, is actually discovering connections to other areas in programming languages, that existed before anyone thought about using them for networking. so, one example that, that we've done in our work is I think, we'll, we'll talk about this later, is there's a system called Kleene Algebra with Tests. Which was developed in the context of theoretical computer science. and, and we discovered that our, our functional language where we're using to write SDN programs, matched up quiet nicely with these Kleene Algebras with Tests. And that was really a, quiet surprising connection but it, it worked quiet precisely, and once you do that. You can then take advantage of all of the theorems, and program transformations, and optimization techniques, and, you know, all, all of the results that have been developed, really for decades, in this other area of CS, and start applying them to networking. so, that, that's one example of sort of, I think a ni, a nicely designed language that connects up to some existing theory can, can provide you other benefit. The other area where I think you see a lot of commonalities with, with other research is in the area of, kind of languages for distributed systems and program partitioning. So this is the, the domain is completely different but if you look at some work that Sam [UNKNOWN] at MIT, and my colleague Andrew Meyers have been doing they've been looking at how you could take a program running on a database, and that program might be expressed in a language like Java, and automatically partition it, into two programs. One that runs in the, in Java, and one that runs on the database. And the idea is that the database probably has some specialized code and data structures, and so on, to deal with massive data sets. And so it'll be much faster. But the Java code is, of course, much more flexible, because it provides, you know, general purpose language. And so this challenge of how you, kind of, write on description. And then split it into two or more pieces for efficiency often is, is something that's arisen a lot. Other examples are, are web programming. So people have written, developed languages where you can describe a web application. Sort of in one piece of code, and then, split it out into, you know, JavaScript code that runs in the browser, Java code that runs on the server, maybe some database code that runs in the back end. And some of the languages for SDN that have been developed, have the same kind of flavor, so you can write one program. And then, a compiler is going to partition it into a piece that runs on the controller. And then, hopefully a, larger piece that runs on the network devices. And the network devices, of course, are much more efficient at, at doing packet processing, and so they'll handle the majority of the work. But, some of the work that can't be compiled to the switches, will run on the controller. >> Well, I just had one, one question about the, the sort of Kleene Algebra with Tests. I don't know too much about the theory myself, but I'm, I'm wondering like do you think it was an accident that, that that, that construct mapped really well to, to networking and SDNs in particular? Or, or the types of problems that it was being used to solve before. Analogous to, to networking problems. Or was it an accident or, or, or why [CROSSTALK] why was the mapping so good? >> I think in hindsight it's, it's fairly obvious. And it's not an accident. and, and actually quite similar formalisms have come up in the networking community in the past. So of course there's lots of people who have used. You know, linear algebra types of techniques or [UNKNOWN] techniques to model a network and this kind of duality between matrices and graphs, is something that, you know, scientific computing people and linear algebras people have been doing for, for a long time. and, and Kleene Algebra with Tests is based on, it's, it's kind of, it's an algebraic presentation of of [UNKNOWN] from, from a language theory. And, and those are also a kind of graph, and, you can play the same games, transforming between an algebraic program type representation, of the thing you're trying to describe, and a [UNKNOWN] machine description, of the thing you're trying to describe. And perhaps, even a matrix representation of the thing you're trying to describe. And, these shifts of perspective, you know, reveal different aspects of the system but, but they're all precisely connected to each other. And I'd say, you know, once you realize that sort of, all of these different formalisms are ways of describing paths through graphs. At that high level it's completely unsurprising that, that this connection exists, and is so precise. Just to mention one other piece of work that is, is based on similar insights Tim Griffin at Cambridge, and others did some work on meta routing about ten years ago now and, and he's really playing in the same space. So looking at, you know, what are the algebraic operators that determine things like pass selection and so on. And how do, when you start combining paths and preferences on paths what, what structure arises from that, and it's, it's much of the same underlying formalism. >> Interesting, cool actually I, I know beyond the languages themselves that you've developed, you've also, you've, you've developed some some formalisms and, and compilers, and, and things that kind of relate to your languages. And,and there's sort of a whole family of stuff around, and frenetic there's there's, there's, the, the pyretics stuff, which actually, the, the students in the class will, will will use to actually you know there's, some people have had a super crash course in Python, but, >> Mm-hm. >> You know [LAUGH] they're, they're playing around with that. But, but, also, there's, there's frenetic. And then, there's also netCORE and Netcat. And I was just wondering. What are the relationship between all of them? and, and then how, how do you decide which, which tool or language to use or, or study? I imagine, of course, frenetic and pyretic are, are languages, and its, it'd be interesting to, to hear your thoughts on that. But, then there's also are these, are these theories things that, that people should, should appreciate and pay attention to as they're, as they're using the language and can you talk about kind of like, can you talk? This is not just a, and ordinary languages, this isn't sort of programming in open daylight, as it were. This is something else, right? So, can you, can you speak a little bit about this, this whole family? [LAUGH]. >> Yeah. So I think part of the, part of the reason for this question is, is our fault that we've kind of confusingly named things, at various times and reused names and so it's, it can be tricky to figure out exactly what name maps to which system. And they also all overlap with each other. So the, the way that we're trying to describe things right now is that frenetic is this umbrella term for a project that [INAUDIBLE] several different universities. Princeton, Cornell there's people at UMass now using this, this stuff, also in Belgium. And so, frenetic is kind of this umbrella term for, for all of these languages. Pyretic is a system that Josh [UNKNOWN] and [UNKNOWN] and Dave Walker have been leading at Princeton. Which is trying to realize sort of the, the general idea of kind of having high level languages for networking, in the context of Python. So in, in pyretic, you write a Python program that uses some of the languages that we've developed for describing packet forwarding, as a domain specific library, within Python. and, and then there's a bunch of run-time system functions and so on, that are packaged with that, to let you write effective dynamic programs. There's another implementation of frenetic up, you know, Camel that we've been developing here at Cornell in collaboration with folks at UMass and, and that's sort of a, of, a similar system, but it's done in a functional language and so, if, you know. I suspect for most, for most of your students, and for lots of people from the system's community, you know, Python is a, a thing they're familiar with. And so it, it's easy to get going with using some of the language construct in frenetic, in that environment. but, if you're brave and enjoy functional programming we have a, a versioning one as well netCORE and Netcat are, are sort of two points in an evolution of this, of sort of our core functional language for describing packet fowarding and querying so There are some differences and I don't want to kind of take you through the nitty gritty details of, sort of a, a intellectual history of kind of how these things evolved. But Netcore is an early version and then Netcat was a, a later version. I guess the precise difference between Netcore and Netcat. So, Netcore was a language trying to give you a functional interface to writing packet processing functions, in an entire network. So, really the model here is, instead of writing programs that produce rules, that get installed on switches, you write programs, that describe some mathematical function. And this function is what's applied to packets, everywhere in the network. so, so you write this function. You run it. And the compiler's going to take care of how to, of partitioning that into flow tables for all the switches in a way that implements that function. [COUGH] Netcore included, a few operators, for combining functions. Though the first was, what, what's sometimes called parallel composition, or union. And, this let's you basically take two functions, on packets, and, produce a bigger function, on packets. So and the idea is that these, these two programs. Sort of operate in parallel, on different copies of the packet. So, this kind of operator is useful if you want to do something like, take one function that implements some kind of monitoring function, and another function, that implements some kind of forwarding function. And you want your network to do both of those things. So if you use parallel composition, you can merge these two functions together, and you get a bigger function that does both of those things. The other operator in Netcore, is something called sequential composition, which is just like normal sequential composition from ordinary programming. And, instead of running two programs side by side, this operator feeds the outputs of the first function, into the inputs of the second. So this would be useful if you want to do something like, you have a firewall, and you want to make sure the firewall is always applied. Well, if you compose, the firewall, after the rest of your program. You'll be assured that the firewall program is always applied, and any packets that it drops, will not be forwarded. And there's other examples. So the Netcore had kind of, a little language for describing, you know, packet predicates, and modifications, and then these sequential and parallel composition operators. Netcat went a step further in adding a Kleene u-star operator. So if people have seen formal language theory, Kleene u-star is an, is a operator that lets you do things, zero or more times. You can think of it as kind of like a for loop but you do it, kind of, as many times as possible. And this this has two main uses. So one use is, if you want to model the behavior of an entire network, as a program, then you'd like to be able to encode the possibility of packets being processed, as many times as they need to be. So, for example, if your, if your network has a loop. And you want to model that in a language, you need some ability to express unbounded iteration. And with out Kleene u-star you can't do that. So Netcat adds that operator. Another use which I think, I believe you've, you looked in your work on software defined exchanges, is, you can imagine an exchange that's hosting programs from different parties, and you'd like to let them interact with each other. Sending traffic back and forth to each other zero more times, and although there's some upper bound that any given program will need, to send packets back and forth between those different tenants it's convenient to not have to do that enrolling by having just to say, you know, let customers a, b, and c forward packets to each other, until they're done. >> Right, right. >> Yes. >> So, I guess, one, one other difference with Netcat is it's, it's really I guess, as I started to allude to, you can use it both as a programming language. So you can write functions in it, and compile them to, to rules that run switches and, and we've done this. And you can also use it as a reasoning framework. So it, it kind of is this formalism that kind of blurs the line between a language, and, a, a reasoning framework. And so this, one of the exciting things about SDN from the PL perspective is people have started to get serious about things like network verification, and you, there's there's some really great work by [INAUDIBLE] out of Stanford, on [INAUDIBLE] analysis. Also George Fabrizi, and there's some. Also, also nice work out of the UIUC Matt [INAUDIBLE] and [INAUDIBLE] Godfrey, on Veriflow and Anteater. And so these are systems where you can automatically in a push button way, you know, check properties of, of a network program. And a lot of these tools work by translation into other representations, for which we have algorithms that can decide various properties. So for example, you could take your configuration, and encode it as a problem for a SAT solver, and SAT solvers are very fast these days, and so you, if you can do that kind of encoding. Then you can turn a question about a network, into a question about satisfiability. [COUGH] So Netcap, is designed to be the same thing. So it has it has a, a set of algorithms that can be used to decide, when two programs are equivalent. And so you can do a lot of this reasoning in the language as well. >> That's interesting, yeah, I mean I, I'd like to, to ask you a few more things about [CROSSTALK]. >> Yeah. >> About, about, verification I mean that, that's seems to be like a super hot topic, actually, the difference be, one of the main differences between the course this year, and last year, is that I've added a whole module on verification [CROSSTALK]. >> Okay. >> [INAUDIBLE] The things that you mentioned so that's, that's pretty cool. and, and I think that there's a lot of stuff, you know, that we can talk about there, as far as like. You know, to think maybe I, I'd like to ask a little bit about the types of things you can currently verify, the types fo things you'd like to verify, but you can't. I mean, what, what about that? It's like you mentioned, for example, certain types of things can be, translated into things like that a SAT solver could solve. You know, those tend to be, you know, things like data plane. You know, reachability in the data plane. [CROSSTALK] And things like data. And the header space analysis work, sort of is, you know, symbolic execution. You know, packets in the data plane. What are your thoughts on just, you know, what, what's the current state of things you can verify or not verify? And, and then, my follow up is like, what about control plane verification? Like, you know, it's, are there, do we have ways of verifying like, what the controller is going to do at a certain point in time? >> Yeah, so there's a bunch of questions there, and I think the, the overall like high bit is at least to me, it's super exciting that so many, people both on the PL side and verification side, and on the networking side, have gotten interested in this topic. There's you know, verification has been going on in networks for a long time. I know you, did some work, at MIT, during your grad school days on this. But it seems like there's really kind of a broad base of people who are interested from the very academic side, but also people trying to really deploy this in operational contexts, and,and that's super exciting. so, as far as the kind of lay of the land I think, one useful division is, is the one you said. So, there's a bunch of tools that are doing data plan verification and, you know? So they're, they're not modelling their controller but they're taking, you know, a snapshot of the network state. So, what is the topology and what are the configurations of all the switches? And then answering questions about what that snapshot does, in terms of packet processing. So, properties like reachability ,or with freedom, or isolation these tools, will often have, ways of encoding those properties and then, and then checking them automatically. And but, this is in, in some sense, you could call this [INAUDIBLE] I mean, it's kind of, these problems are, everything is, you know, [INAUDIBLE] state at this level, and there are great low level tools that can decide properties very efficiently, so things like SAT solvers and model checkers. but, there's still a lot of cleverness and, and research that goes into building a tool that can scale to the size of a campus, or data center, or enterprise network, and answer these questions. And so, you know work like Header Space, and, and Anteater and so on, and VeriFlow they have a bunch of really cool insights. To kind of take this problem, that if I just describe it from high-level sounds quite straightforward and, and make it, make it fast and effective. The other side of things is well, you know, you might ask the question, why start from a snapshot of, of the topology and the state of a network because, well, you know, even, even getting that snapshot in a consistent way is going to be hard. And, there's this controller that's doing things, and there's things happening in the network and so I think kind of the next major leap, is moving to doing both controller verification and modeling the chaotic state of the network with, with things like failures and congestion and, and so on. So the, on the controller verification side there's some really great work going on right now. So there was some early work by, by Jen Rexford and Marco Canini, and some others. Where they were using symbolic execution of the control program itself, to check that certain invariants were not violated. and, this is, sort of, hard for all of the usual reasons that software verification is hard. You know, taking, taking an arbitrary C++ or Python program, and trying to prove it does anything is, is incredibly difficult. And so there's there's, there's a sort of good bag of tricks now that you can start to use to throw at this problem. [COUGH] So things like starting to abstract away, from the from the actual program itself, and building a simpler model that's more attractable for analysis. This is a field that's kind of been developed over the past 30 years, and, and programming languages, and tools like [UNKNOWN] start to apply this to control programs. There's some other work. I'll just mention some names, and then we can go deeper depending on what you think is interesting. So there's a group led by Muli Sagid who's a professor in Israel. As well as a bunch of people at MSR so Tom Ball and [UNKNOWN] and others that are working on also controller verification and, they found some interesting some interesting constraints in the problem, so for example if you are trying to verify a control program. There's a certain class of properties, that are actually independent of the topology. So there are properties you can prove, other control program and the network state that it produces where, even if the topology is changing you know, that property can be proved or disproved. And that's a, important case to handle, because the controller may not have, you know, complete consistent visibility into the state of the topology. And so, that kind of verification result, although it limits the kind of properties you can talk about you know, does, does give you an answer that that you can believe with high confidence. Another group that's working on controller verification is is a group at Brown [INAUDIBLE] Christian Murphy and his students have been building a program, a language called flow log which is a language based on, on data log, like the work by [INAUDIBLE] I was talking about. So the idea is that you write a single, they call it, tierless program. Where you, you just write, you know, a staple program, it might, it might build up some tables with information learned from the network. It described the forwarding behavior of the network as well. And then you can verify that data log program to check certain invariance. And and so again it's you know, not just verifying the actual state of the network. But also, what happens dynamically over time in the control plane. Going further I think a really rich area, it is getting away from, from individual packet properties. [COUGH] So, a, a lot of these well, one interesting way to sort of classify a form of verification efforts is, if you're verifying something, you're probably verifying some kind of logical property. And that property, probably has the form, you know, for all something. [LAUGH] And then, some constraints on that thing. and, a lot of these tools that have been developed so far, can, can prove properties about, for all single packets, you know, something happens. So, for all single packets, if that packet is located at this switch, it will eventually be delivered to this switch. Or, you know, for all packets. And for any switch actually, you know, this packet cannot move back to the same switch. But if you want to talk about other properties, like fault tolerance, or various things that I'll lump under QoS, then, it's not enough to talk about a single packet. You may have to talk about. What happens with multiple packets, or also things about the, the network topology itself. And so, I think another kind of big step, in addition to kind of extending to control verifica, control point verification, is extending to these richer classes of the properties. [BLANK_AUDIO] >> Yeah, that, that, that, that definitely makes sense. You, you've done you've done a little bit of work on, on fault tolerance [INAUDIBLE] it seems like that's one kind of dynamic one kind of dynamic event that might occur is, is links going up and down. It seems like you know, there, there are, there are certainly big challenges there. I mean, you, you've sort of said a few times, like, okay, you want to have some, some notion that, that a particular property holds, you know, under a certain set of conditions. As far as fault tolerance is concerned, what can you say? Can you say. For example, when this link fails. Like I, I, you know, get certain security properties, or I get certain, you know, load balance properties, or are we not there yet? Like, what kind of things can you say with, with fault tolerance [CROSSTALK]. >> There, there, yeah, there's certainly some things you can do-. Sort of reducing the single packet properties. So the kind of thing that we proved before in, in our work which, which does concern these kind of single packet functions and properties, is you know, does this program behave a certain way? So does it provide connectivity? For example, in this typology even if up to. [UNKNOWN] fail. and, so, that, you know? You can ask a series of questions And basically, reduce that kind of question to Single packet properties. It's not a particularly efficient way to do things, but It, it at least gives you an algorithm My own opinion and, this is not an area I've really started to work in, yet, but I think it's a really exciting area. Is moving to probabilistic languages and probabilistic guarantees. I think, at a certain point, these models based around deterministic packet forwarding if you, if you continue kind of trying to sort of model every aspect of the network. As some kind of deterministic, operational model. It's just going to get too complicated to do that scale. And so, one way to abstract things is to basically align some of the de, details about how things like buffers and cues and maybe even failures behave, and replace them instead with. With some kind of probabilistic entity. So maybe, you know, maybe you model distributions on, on packets that arrive in your network. Maybe you model things like expected rates of failures. And then sort of replay the whole, the whole game of coming up with languages and formulas and algorithms. That can give you these kinds of probablistic guarantees. so, th, this also connects, there's, there's a lot of interest right now in the PL community in in languages whose semantics is based on probablistic foundations. A lot of this is driven by interest in machine learning. >> Mm-hm. >> But it seems like networking is, is another area where, where these kinds of structures would, would be quite useful. >> Yeah, that seems, that seems really interesting. It's, I guess that answered another one of my questions that which was sort of like [INAUDIBLE] we're working on this type of thing, what kinds of things are feeding back into the, into the programming language community. I guess that, that might be one. Sort of but are, are there others? I mean, things that basically, in working on, I mean is the programming language. [UNKNOWN] Is the programming language community, are they paying attention to this a lot? And sort of taking things back and, and developing, you know You know, new languages or, or, or techniques or, or models. >> I, I mean, [LAUGH] I hope that some people are getting interested in this stuff. I can point to specific individuals. Actually Gene Rexford was invited to give a, a keynote at the flagship Theoretical PL conference and I think that helped get a lot of people interested in. In, in my community and you know, oh yes that's an interesting kind of, of device to want to program and so I, I think that kind of, [UNKNOWN] people's appetite for this kind of work. There are a few people I've, I've already mentioned most of their names who actually have made the job considering research in this area and so, I think. Slowly, there's, there's some interest in, um-. >> Cool. >> ln, in people starting to do this. I will say there's, you know, some of the people that are doing this are the kinds of adventurous researchers who like looking for new areas to work in. >> Mm-hm. >> I can also point to a few, a few examples so, for example, our work on Kleene Algebras done, done here at Cornell, with, with colleagues in Princeton. Actually look, wrote in, my colleague Dexter Coats in, who's a theoretician. He's actually giving a talk tomorrow at the Mathematical Foundations of Program Semantics on, on that Cat. and, I, it's a little hard for me to quantify. But, like, this is an area of CS that's. So far away from [LAUGH] systems and networking and yet, you know, one of the invited talks will be on you know, a language approach study program, these things. so, I, I say I guess, in terms of like impact in PI, I don't think, you know, it's not like there's PL Conferences devoted to SDN popping up yet, but >> Not yet. [LAUGH]. >> So that, that, that's a yeah, that's a good, good point. Where I, I thought that I would ask some questions kind of in the other direction I mean. [INAUDIBLE] Do some work. That we did like way back in MIT. Actually, I was super excited when I started to see your work. Because, like, when we did some certain debugging and testing work way back. When I was like, you know, this is pretty hard, like really what we should do is just, like, start over. And have a language that, like, actually makes sense. And, and, and. I think the, the kind of the responses that I got at the time were sort of like, yeah, but, but operators are going to have to like learn this new language. And they already know, SISCO CLI and blah, blah, blah, like, you know, you shouldn't really work on this because like you know, you're going to be judged by adoption and things like that. Obviously like in your community you don't, actually. [LAUGH] >> You know there are other, they serve other, let me put that a different way, there, there are other ways that you can kind of like you know make meaningful contributions, like in systems and networking, I think we, we sort of like often measure ourselves by like you know. [CROSSTALK]. >> Is networking real world paying attention to us here? And, and one of the things that I noticed, like, in teaching a class here. Not only that but just, just sort of the, the vibe I get, like, you know, from, as, as this material gets out there is, like, for example. People, like, why are we programming in [UNKNOWN] and, like, why, you know, can't you put in more stuff on OpenDaylight and this and that. And, and you know, I th, and, and, and also, like There are a lot of people taking the class who basically never got, people who have basically been running networks for 20, 30 years who have not basically written a line of Python until they took a class here. And I think some of the, some of the comments I was getting, like ten years ago or more. Are pretty accurate. I don't, I, I don't know. I think probably you know, I may be biased. We're like, okay, it's probably inevitable, like, you know, this community's going to have to learn to program one day, one way or another but and, but that seems to be happening a little bit with, with things like OpenDaylight and stuff. But I guess [INAUDIBLE]. I've got a number of questions, sort of dates in there. One is like, is it inevitable like, you know, are, are network operators going to have to learn to program? I mean should we basically tell them to take their lunch here and, and, and do the assignments? Or or not and then and then I think the other question which is specific to, to your work is. There's this whole other juggernaut going on with, with OpenDaylight and a bunch of other stuff and, and they don't have this sort of you know, beautiful theory under, under the hood. And what do you, I mean, what do you make of that actually >> So a bunch of things. So, so first off, I'll say the line that you said. [LAUGH] Or that you didn't say, rather. >> [LAUGH] >> one, one can do PL research, and it can have no chance of adoption. And the community will still accept it, if there's some nice theory. [LAUGH]. >> And I think that's perhaps an extreme. And I sometimes wish that the program languages community would be a little, would pay a little bit more attention to things that. Practitioner's are doing you know, across our, you know, our field should be about programming. and, and what you described, where the you know, networking community can, can often push back in the other direction, that if something is not sort of, ready to be deployed on a short schedule, then it's probably not worth doing research in. You know, that's also not necessarily healthy. >> Mm-hm. >> The, part of that you just take a long time to get out there so just to, and I [INAUDIBLE] from the [INAUDIBLE]. But Apple announced this Swift programming language that, you know last week. Or a couple weeks ago. And there was a lot of, sort of discussion of this in, in various [INAUDIBLE] social networking and things. And a, a lot of the comments were of the form sort of you know, this is a really nice language based on technology from, from sort of 1980 or maybe 1985. And so there is this sense that kind of PL ideas take a long time to sort of get into practice. And I think you know, 30 years is, is probably too long. And I think there's, there's other reasons that in the context of general purpose languages like, like, you know, C++ and, and Swift and so on, Objective C, the basic things take so long to get into practice. Mostly because there's so much, you know, inertia, and sort of, friction, to getting new features in. I, I certainly hope that. At a time of transition there might be an opportunity to sort of help design some of the core abstractions in a way that that makes, you know, gets some good design in at the right time. so. that, that's sort of a rambling answer to sort of you know, what our thoughts about sort of how to, how people should think about different languages that are being proposed and when they might be useful. In terms of things like OpenDaylight and some of the commercial grade controllers that are starting to come down the pipe. I think there's two reasons that people might be interested in some of the more academic languages that have been proposed. So one is that languages like Netcat, we've actually carefully designed them. To try to allow sort of incremental adoption and I'll say what that means precisely. So Netcat actually includes open flow forwarding tables as a, as a special sort of sub-language within the language. So if you can strain yourself to only use certain operators in a certain constrained way. You can basically program tables. Now once you have those tables, you can also do things like combine them with parallel and sequential composition and the compiler will happily handle them. And you can, of course, also not write things in terms of tables. If you don't like writing tables, which are kind of perverse to write, you can write functions that describe tables. but, one of the things that. That we would like to do and, and some people are starting to do is to actually. You know, you can use a language like NetCat as a kind of intermediate language for other formalisms. So you may not be writing NetCat code yourself, but at some point, you know, a NetCat like language might be. Incorporating the tables that you're, you're code is producing and then doing further transformations on them and then spitting out, ultimately lower level configuration instructions. And so, you know, under, for, for someone who, you know, who just wants to be able to write operational code. certainly, you know, knowing a lot about things like OpenDaylight is important. But I, I think it may also be useful to understand some of the underlining sort of structure of, what are these objects that you're really working with when you write your code. so, you know? At the end of the day, if you're trying to get a network to perform some function, you know, understanding and having a, a kind of closed world view of, well here is a way of describing functions. You know? This language gives you a way to describe functions. And a sort of ready made very simple theory for how you can think about those functions, transform them, mutate them. That can be a useful mind set to have, whether you're programming in a language like Paretic or your programming in OpenDaylight. You know, if you're, if you're doing it OpenDaylight you won't, you won't have the, the syntax sitting in front of you, but you can use some of the insights in, in your code. And-. >> You'll still have the concepts. >> Yeah. >> Much like people know how to make lists. >> Yeah. >> And red back trees and things like that. Is that what you're saying? >> Yeah. I mean, I, I would certainly, we, we, you know, we would love to see some of the ideas in [UNKNOWN] get pushed into some of these commercial grade controllers and [LAUGH] if anyone wants to help make that happen, I would, I would love that. We're starting some some limited efforts in this, in this direction right now, so We have a goodwill somewhere of code, a student who's working on OpenStack integration but you know, this is a long engineering battle that researchers don't always have the resources to kind of carry out as, as first thing so >> Absolutely. >> Promises but >> Yeah I know, I think that's really valuable for, I mean for, for a lot of the people at least taking the course that you know, they're, they're coming from the operator perspective and certainly the industry perspective. >> Yeah. >> And I think that the insights are really important I think. I guess like. [CROSSTALK]. >> I was going to say, like also like lot of things are very simple. I mean Netcat is a language whose complete description fits on half a page. I'm not saying to go off on Netcat, but I'm saying, like the advantage of some of these academic formulas is, they're really quite lean. So, that's a weakness of course, because they don't model lots of things that are important to producing you know, operational networks that perform the way you want. But, for the things they are modeling, they do that in a very simple and lean way and so if you can internalize and, and learn those, those things. It can be a quite powerful tool that kind of cuts through a bunch of complexity of of kind of thinking about the whole level system all at once. >> Yeah, absolutely. I think personally it would be it would be great if, if operators often were able to think at that level of abstraction, so that's, that's really powerful. Actually maybe we should close with, with another area that's just a complete morass >> Right. >> Which is security. And I, I think this is something which we really won't cover this year in the course, but maybe in future years. It's certainly a personal interest of mine. It You know, to, you know, working in, in the area myself, I, I sort of have an appreciation for how messy it is. But I've also followed some of the work of ,of, of some of your colleagues, you know, even at, at Cornell, who've done pretty awesome work in, in using language constructs to do information flow control, and. And other things like that. I'm wondering if, I mean it just seems like there's a super, like, gap to be filled there as far as, you know, people stopped doing, like you know, nice, formal system security work a while ago. And, and, you know, when, when viruses and botnets came around, and I, I feel like, you know, the, it's, it's maybe time to go back to that. I mean, do, do you think that some of the, the language, the languages that you've developed and the constructs, do you think that they already have things that could help us [INAUDIBLE] about security? Or do you think that. That they should, that they could be extended in a certain way that would help us reason about certain properties >> Yeah, I think this is an exciting area that is pretty untapped, as you, as you said. So I don't know how much your class knows about this notion of information flow and, and non-interference kinds of properties so I'll give a short description. So in the, the light, the work that Andrew Myers and, and others have done in the languages community the, the whole idea is that you can design a language and a type system that can prove to you that if your program passes the type checker, then it will not leak secrets. So you can imagine a program that's guarding some database, and the database has, you know, high security and low security and possibly other levels of information. And then you're running some program, and that program's going to feed in some web page, so you want to make sure that the security side of it, sorry, the secret parts of the database are, are not published on the web. And so what these languages let you do is, is basically analyze the program and if it passes the type checker, then the, the, you're guaranteed that no secrets will be leaked. The way this turns into a, a theorem is that there's a property called. Non-interference which is the kind of main thing that you prove about these language views to show that they have the intended security property. And non-interference as if you have an input to some program, that consists of a mixture of high and low, or many other levels. But let's just do high and low. High and low security data. Then if the outputs can also be classified as being high and low security, then there's no way for high security inputs to affect low security outputs. And to put it another way, you know, you could completely delete the high security inputs, or you could replace them with garbage, or you could replace them with other different high security inputs. And the low security piece, the piece that you're going to publish, is not changed. So we did, in the, in the work we did on Netcap one piece of our paper actually used this kind of property in order to reason about isolation between programs. So, the motivation here is, you know? If you have a, a shared network. And, you have multiple parties that are providing programs, that are run on that shared network, you'd like to be sure that You have these kinds of non-interference properties between those programs. And you can actually talk about non-interference with respect to a couple of different properties And we use the kind of familiar terms from the security community of integrity and confidentiality. So in the domain of, kind of, network programming, one way to think about integrity is, if my program is running in a network alongside someone else. Integrity means that that other program can't somehow produce inputs, namely packets, that would cause my program to behave differently. And confidentiality means that my program won't leak packets to another program that might be snooping and you know observing what traffic is, is flowing through my program. And so you can, it turns out you can prove both of these kinds of properties as, as, sort of using this framework of non-interference. And you can actually do it in a language like Net Netcat by classifying certain kinds of packets as being high or low, or belonging, you know, Nick's packets or Nate's packets. And you can prove this kind of lack of interference between the two programs. So, this is one instance of this, for kind of, you know, deterministic packet forwarding, but there's a whole richer area which could extend to things like, you could connect this up with. With programs that are running on N hosts, for example, you might have a database server. And, it might have a notion of high and low security data, and if the network was aware of you know, that certain packets were high security packets, you could have a network that doesn't, you know, leak secret data. And this is a, I think a, a great area to work in, and. You know, kind of uniquely utilize the, the flexibility of SDN to start to explore these kinds of, you know, networks that provide richer properties that just best effort forwarding [SOUND]. >> Oh yeah, that seems like that it's a, it's a wide open area. Maybe, maybe in the future it will be Students will be hearing about that. [LAUGH]. But we got our work cut out for us, awesome. Well thanks thanks a lot for your time. I think I think people will really appreciate this. >> Yeah, thanks so much. >> Cool, all right. Thanks.
