Okay, okay great, we're talking about [UNKNOWN] [UNKNOWN] who is an expert in many things, software engineering, formal verification, he's done some work on a system called Flow Log, which allows for reasoning about [UNKNOWN] control programs and we're going to talk about formal verification of control as it pertains to [UNKNOWN] So, thanks for, for for the time [UNKNOWN]. >> Real pleasure Nick, thanks a lot. >> Cool. So so I guess Flow Log is actually one of the first things I think we've seen as far as like you know, looking at reasoning about SDN control programs and sort of looking at trying to basically design. A language or an interface that would allow us in control programs to be verified. I'm wondering how you, how you sort of designed this set of abstractions that Flow Long supports, like, it's based on data log, I think also people probably don't know too much about it, so you want to tell them, like give them. >> Yeah sure, I talked a little bit about that. >> How did you arrive the design for Flow Log Right. I think two different things came together. So one is, in the past we did a bunch of work on verifying and, reasoning about, like Cisco IOS programs, Cisco IOS policies, and access control policies, and things like that. We had a system called Margrave that we still used for doing this. So we were informed by thinking about rule based systems in general, and one, guideline for us was it looks like when you look at a lot of for real world policy languages, a lot of them tend to me, in some sense, rule-based, and people seem to work with these pretty well. Another example of something that's not a, a policy language but it's still kind of rule-based is sequel. So one set of inspiration for us was really these kinds of rule-based policy languages and sequel, and even some tactically we tried to draw some things like sequel, because we wanted to make this look familiar. So even though data log is the logic that's underneath. To me that's kind of like saying well underneath SQL is relationship logic. But there's a language on top of it that traced to provide a rule based interface that people can work with much more easily. So that was a major inspiration. But the other really interesting thing, I think the sort of the novelty in full log, is that it's what we call tierless. And, so this is kind of important to us because there's an analogy here tho the kind of, three tier architecture you use on the web, right? There's some backing store that's a database tier, then there's some control tier which is maybe your, you know, Java, servlet kind of thing. And then there's client code which is mainly in JavaScript. Right. And something analogous seems to happen in SDNs where you have some backing stored there's some persistent data you need to store. Then there's the control plane and then there's the data plane. And the data plane you have these, you know, these rules, these SDN open flow [INAUDIBLE] rules or whatever. It can whether or not you want to be writing JavaScript by hand. Right, so the analogy breaks down a little bit, but even more so then that you'd really like to not be writing these by hand. There's no UI involved. There's no analog to CSS. You'd really like to not look at this if you can help it except in some maybe, you know, performance tuning aspects or something. So Flow Log's goal is to be this tierless language so that we accommodate that as the back end as, you know, that's just, it even got a relational store, so that maps very nicely to what we want. And then the client side is basically we generate, we compile these rules down, so that the programmer thinks they're working in this one tier, and the other two tiers are generated by a compiler. So that's the other big design principle. So one big design principle is let's draw inspiration from rule based languages and sequel and so on. The other inspiration is let's be puralists and see how that works out. And, and you know the right way to think about that is an experiment and a few years from now, we might say it wasn't so great, but you know it's worth doing for now. >> Was the, was the decision to sort of focus on rule based like a rule based abstraction, was it like, we want to design something we can verify, or was it that like, oh, people kind of know sequel, or they're familiar with that, so let's kind of go. >> It was actually, so that's a great question because we were trying to find the sweet spot between those two things, right? The sweet spot between what can, what do we think people would be willing to program in and might familiar. But at the same time, what can verify and in particular, what can we incorporate a heavyweight verification at. You know, because people will also program in Python happily, but it's really hard to verify Python, especially if you want to do certain kinds of verification, and Flow Log is designed from the ground up. Again, that's another aspect of the experiment, is can we sort of co-design a language and its verification support together? And so, you know unlike other places where, other projects where you add as much expressiveness as possible and then try to claw back verification, we're trying to be a little more conservative and use verification, support as a, design principle to figure out when we can add things and how, and what form we should add things. So that's the other part of the Prolog experiment. >> Hm-mm, hm-mm. It's interesting actually, kind of, like, talked about [UNKNOWN] programming and familiarity. And I kind of imagine, like, network operators, I mean, I'm imagining now so, let's see, but that they're [COUGH], you know, perhaps more comfortable with something I guess QL than like a general purpose programming language. Like, I know, sort of as a, you know, as a matter of experience teaching this course, that there are many network operators who you know, certainly aren't programmers, many of them who've never seen programming languages. So, I think there's a real challenge in, in kind of like, designing something that an operator could use that you know, they could even understand without like a huge learning curve. It's that something that you're, you're concerned about? Is that, I mean, it seems like something we need to be concerned about but is that something you're considering as well? >> Yeah, yeah, I think very much. I think you hit the nail on the head. I mean, there are, and this isn't like, we're not trying to disparage net ops or anything right. They're perfectly capable of learning programming, but that's not, that's not what they wake up every morning thinking that's what I want to be doing right now. So, I think over time SDNs in particular are going to open up a new generation of net op people who are also programmers, software engineers, and so on. Because the, I mean, one of the beautiful things is that SDN has made possible for these people to come in and contribute. But we'll also have, we'll have all kinds of people and people with expertise more at the network level, at the hardware level, and figuring out what kinds of abstractions work well for them I think is a worthwhile activity. So, one approach is you could think about building domain-specific languages and say it's some more general thing, and Flow Log you can think of it's a different kind of domain specific language it's just not embedded in some bigger language. All right, now, one, one design decision of Flow Log is we really want to be able to reuse code that's already out there. You know, people have already written Python libraries and Java libraries and so on so we put a lot of effort, so far, not as much as we'd like when we'd like to do much more on building a good FFI, so that adjust, and, and again, the direct analogy is to SQL and calling out to external code from SQL, all right, store procedures. that's, that's directly inspire, inspirational to us, so we have this idea that you can call objects to external code and there's some signaling and so on. But yeah, it's very much, maybe this kind of rule based thing, and if it comes with good tool support as well, might be more attractive. >> When you when you talk about kind of calling out to different to different you know, procedures or, or, or other things too, it seems like there's a tension between and you sort of alluded to it already, like and you talk about it in the paper, like this tension between the wanting to express certain things and being able to verify them right. Like if you pop up to a general purpose programming language, like, all bets are off. In some sense or most bets are off. >> That's right. >> But but then you get sort of [INAUDIBLE] >> [INAUDIBLE] right. >> So, how do you figure out, like, okay, you talked about co design, as well, so, where do you kind of draw the line or, how do you figure out, like you know, what should go in a language versus like, okay well we'll, we'll use that as like a call out. >> Right, right, right. That's exactly. So that's, that's that's a really interesting design point. And like every one of those things is a, was a question of design. I think for us, we actually chose to start with a minimal core and stretch it out only as much as necessary based on the properties we were trying to verify. So you know, there's, there's very simple question like arithmetic, right, does arithmetic belong in the language? It sounds kind of a, you know, to a non-theoretician it sounds like a goofy question. but, you know, it actually has a real impact when you start thinking about decidability of things and so on, like, what kind of [INAUDIBLE] support? So, we've slowly been incorporating you know, we're doing some projects where we're actually using Flow Log as a target language, like, we are compiling chunks of IOS into Flow Log so that we can exploit the Flow Log [INAUDIBLE] so you could take this existing switch you got, you know, this IOS [UNKNOWN] and you can compile it down and now you have an SDN test spread on which you can try the same thing that you could do before. All right, so it's like a migration path sort of thing. So, there, like, clearly you need much richer support for some projects like that. So, I think the, the short version is, it's not like we have a hard design principle that always makes decisions for us. But verifica, verifiability is definitely the most important criteria and, not because it's sort of golden principle, but because it's the one, it's the hair shirt we've chosen to wear, right? That's our deal, and other people are going to make that decision differently. It seems to me like a really good thing to kind of try to focus on, I mean, certainly something I've always been interested in as well and it seems like certainly from [CROSSTALK], from like hard research problems, it seems not only very useful but also kind of like a holy grail. Wouldn't it be nice if you could do this. But actually like, I mean, one of the other things too that kind of comes up is, I mean you've kind of alluded to it already, you start with Cisco IOS, and you like, using Flow Log as a target and, now you gotta make some choices about, you know, do you represent everything, and actually that's another question I have is, like what kinds of things can you verify? What kind of things can't you verify? And then, do you think that there are things like are you finding that you made the right choices? Or are you thinking like actually it would be nice to verify these other kinds of properties? Like. >> Right right, that's a good question [CROSSTALK]. Yeah, you know one thing we've been weak on so far, and maybe that's just our own strengths and biasy showing, is we're not very good at these continuous properties. We've been mostly dealing with discreet properties, mostly dealing with logical properties, and it would be really interesting to start asking questions that have like, real numbers in them, for instance, right? Talking about volumes and bandwidths and so forth. And then going from there to even richer things like say, security properties. Actually, security is an interesting question that's on right as you well know, because some of it falls on under the, falls under the logic realm, some of it does not, and, you know, it's sort of, security touches on everything. So that's a separate matter, but just in general, there are a lot of continuous type properties that we would like to be able to talk about someday, but it's not been our priority. There's also a really interesting question about where does the network apology fit into all this? Because when you write this tierless program, you write this program that sort of taking all tiers into account and it only, if it talks about a particular element or particular switch, it has an identity for it and it talks about it, then that's relevant, otherwise it's not relevant, it doesn't care, that's a compilers job. But there are interesting questions you'd like to ask such as, you know, bandwidth allocation and so on where it is really useful to add, say hey, this is the specific topology against which I want to talk about this property, and that's something that Flow Log, as you know, we present this as a feature but it's also kind of a bug, right? Flow Log doesn't really talk about the typology at all. And there will be types of properties where we can only verify them once we can also get a network typology, a specific typology. So, right now the feature is its typology reasoning, but that's also a bug because you want to talk about typologies as well. So that and continuous properties, I think they actually kind of go hand in hand, because when you have a typology you can talk about flows, volumes, all sorts of things like that. >> It's really interesting, I mean, because I think like, this comes with a lot in, in, in, in other aspects of network management, probably also in software engineering as well, like, when you create abstractions, on the one hand, you kind of like create a convenience for the programmer, the operator, whoever. Like for example, the, the existence sort of virtual topology or, or just a network as one big [UNKNOWN] so you don't have to worry about the topology, but now, you want to make an assertion or a inducing debugging or something where you kind of like need to break the abstraction barrier. >> Absolutely, I think also one thing that would happen as we in, sort of the research version for the Full Log project is we're going to have these call outs right? For these equivalent moral equivalent store procedures, and some of the interesting logic will actually go in there, right, like constructing a route table. Maybe we dont want to be writing that in full auto, maybe that will come from something else, right? They'll be some, well, you know, somebody will have written an awesome thing to do that, and as you know there are already projects that do that, and we'd like to just copy those in and stick them in there and then some of that verification of those properties will actually end up being verification of that chunk of core that Flow Log was referring to and Flow Log is just going to passing through whatever it says and isn't getting involved in the middle. So there likely be a verification of the [xx] program saying you didn't mess up the verification you provided and then then it becomes a matter of verifying that plug in, basically. >> Mm-hm. Do you think like, actually this is a question I've, I've sort of grappled with myself. Like, because there are other kind of control frameworks like frenetic and pyretic that have these composition operators. >> Mm-hm. >> And you're sort of like talking about alternate composing modules and,. >> Yep. >> this is something that we've sort of thought of like, or run into as well, where a lot of these formal verification frameworks are well suited for like verifying a particular module. Like, I can verify this module and that module, now you’re going to plug them together. Are there good, formal verification frameworks for doing that? I mean, one that I’ve run into, for example, is with finite state machines, right? There’s really good, like. You know, logics for verifying the properties [UNKNOWN]. >> Now I want to compose them, and what happens then? >> Yep. So, in fact, that's in, that's interesting because this is, this is one of the really cool things, I think, about STNs is that they've opened up the possibility of using a lot of literature that we already have on these kinds of questions. So, there's actually a lot that we understand about compositional verification and what kinds of logics composed in what kinds of ways is, is actually a ton of really interesting literature on that. On some of which is made it into tool, some of which is still very much in the it's very understood in theory but maybe there haven't been as many domains that have called for it or the tools for it is not quite there, but I think we actually understand a lot more that is embodied in the, sort of popular tools that you can get right now. So as we learn more about this particular domain and the kinds of properties we want to verify, I think there will be a lot of people doing a deep dive into the literature and it's going to be one of these great things, right? There's a paper from 1984 and some conference you haven't heard of that actually solves the problem and, now you just have to implement or, 90% of the problem or 95%. That, I think this good, that stuff, that's going to do happen for sure. I, I think, you know, one interesting thing that's, that's almost certainly going to happen, I was just curious what you think, is there's going to be kind of this operating system level that's sitting on the, on the on the STN controller, or this virtualized controller anyway, and then there are going to be lots of people tryin' to plug in different features, right? I want to have control over routing, and I want to have control over intrusion detection and some other feature, and then we'll have to talk about how these things interact, because they're all going to want to say something about the packet, all right, they'll all want to read the packet, but they're also going to want to write the packet, and then we're going to have fun as they start clashing with each other. And, this is a problem we actually know a fair bit about from Telephony and other domains like that. You know, in a separate life I did work on module verification, these sort of feature-based systems, and, several other people have done really neat work in this area, and I think this now, this will become a problem, I'm pretty confident, and then we can bring a lot of this literature to bear and then find what's different in this particular domain. >> Yeah, it seems, I mean it seems analogous, I mean it seems like as you point out there's kind of like operating system analogies where you have applications that all want to sort of touch the same data or have access to it, to a particular resource like the disk or the network and you need something to. >> Exactly, exactly. >> In some sense, like, it seems similar, in other cases, it seems like there are going to be an entirely new set of conflicts that arise because you have, you know, these maybe are just applications but they're like, you know, operation's teams [CROSSTALK] or you can imagine different suborganizations in an enterprise or a campus, right? Each doing their own thing or each having their own set of control. >> That's right and I think we actually in our, again by analogy in certain domains like, you know, access control and so on, we've understood some things about how they should express even their decisions. Like we've learned that one useful thing is to think about even if there's a Boolean valued answer, just a yes no answer, it's really useful if you have a three valued answer that includes like I don't care, like I don't make decisions in this domain, and that makes it easier to compose and chain these things then if everybody is trying to make a decision about things they have no business, making decisions about, so I think we have some principles that will get us off the ground, that will then enable us to discover what really doesn't work in this domain. >> Yeah, on that, on that note, so you mentioned kind of continuous time properties, are there other kinds of things that you wish could be verified, that, that, that, like are just kind of tough to express, I mean, like it seems like, he's calling out to these general, general purpose programs seems kind of hard in general, but there are other properties, you think would be nice to, to be able to verify but just, you know, are hard for longer, or just, maybe hard in general. >> Right, I mean I think there's a real long standing challenge of how do you combine kind of rich temporal verification. Like, what's the long-term behavior of this program, with rich, properties about state, like, I've got these strong invariants about how this data relates, and, and, you know, as you, as you mentioned, you saw this, you may have seen this in our paper where we talk about if you've got a map-table, right, there's properties that's a table but it's actually a map, and it's a map with certain properties. It's like this injective function, and it has to be preserved, but it also has to be preserved across time. And so you have very rich statements about one particular point in time and it just, say, does some of that, too, right? But then you also have to talk about its evolution across time, and once you add both space and time, it's just, the stuff gets, it's sometimes easy to say, well it's not that hard to write down the property, but verifying it and actually building tool support and stuff and making it scalable can be really nasty. >> Yeah. This I feel is like, I mean, at least from my reading of the current literature, like you mentioned HSA like, and it seems really like there are a lot of these tools that will say like I can look at the data plan and tell you like this is going to happen like now. >> Right. Right. >> You know, for how long will this be true? As you point out, there are other things like, can my control program ever generate data plain state whistle. >> Absolutely. Absolutely. >> Doesn't seem like there's anything that can kind of solve that at the moment. >> Right. I would argue that at those kinds of properties at least expressible in Flow Log. >> Right. >> And I mean the thing is again we're going to [INAUDIBLE] our version of that property will be a little different because we're just not even talking about the low level data plan behavior, right. We're not talking about what rules are being generated or anything like that. We're just talking about some high level about the system state. So you can say that, now would you be able to trackedably verify that's not the question, I mean, you know, you used to, you did some work on like verifying BGP and using temporal logic and so on, right. So you know that there's that side of the world and we chose a slightly different tool suite for various reasons that may or may not be interesting. So, getting that combination together is difficult. So at least I would say, argue in Flow Log can express the property. Would I be able to verify it effectively? Maybe, maybe not. >> Yeah, actually that was another question I had for you, like, 'cause, like, I mean in some of the work we've been doing in STN Controller is like, which you may even not be familiar with, but like we've looked at, like, you know, CTL I guess, as they call it. >> Okay, okay. >> I'm told they never say computation tree logic, but it's just >> [LAUGH] Right, right. >> But I'm not an expert in this at all. Basically you know cold slashers are basically said hey, who's that? And were like, okay good idea. >> Good, good. >> But then you just serve an entire different set of things. I noticed like, you know, Veriflow uses sort of like sat solving card to, I mean, what’s this space here? I mean, how do you kind of reason about I want to verify this, these kind of sets of properties. Therefore I'm going to use this type of logic or this type of method. I mean, this is really basic. >> [CROSSTALK]. >> Right. [CROSSTALK]. >> I think most networking people [CROSSTALK] know it. >> Ok, so let me see, I'm going to condense about 30 hours of lecture into about 30 seconds. I mean, I think that high level question is, are you most interested in temporal properties, I mean, so the practical answer, okay, are you most interested in temporal properties or are you more interested in, like, which state in variance or state, state properties. All right and so, things like temporal logic like CTL, LTL and so on are very good at expressing properties about things that have happened over time. The thing that gives them that decidability properties is the fact that they tend to be pretty weak about what you can say about the structure of a state. In Flow Log, because we have this timelessness, the whole point is that this one program can talk about the entire state structure. I've got this table here, and I've got this other table. And these invariances they need to have hold between these tables like whenever this thing does this, this other thing should never do that. You know, just imagine you have like, N data, you have these lots of tables in your database and you've got these rich integrity constraints between them, right? And here you're writing a program and you want to essentially ask like, are these integrity constraints going to hold? Like, is it the case that I'll never end up in a state where this thing ends up saying this, but this other thing says that, and they're supposed to be consistent, and now they've become inconsistent. All right, so the trick ,we played a little bit of a technical trick in Flow Log which is we, we focused on the state, statements. And so that's why things like [UNKNOWN] solving end up being pretty good at that, because you can take these rich, logical specifications, compile them down to SAT, and then, you know, some magic happens under the hood, and it's all good, for the most part. And sometimes BDDs and things like that were also used for this purpose. But because of some properties this there's actually some pretty rich mathematics in the logic behind flow log that let us say, there's two different things. One is, when we want to talk about properties that are inductive, like I want to say, at no time does something happen, well the rules are actually pretty good because we don't have to talk about, we don't have to look at all of the paths, we can just talk about the induction step. Right, if it's true now, will it be true in the next step? And then by induction, it's always going to be true with some base case assumptions and so on. All right, and that lets us, sort of, break this triangle hold of like, how do we talk about long paths? Because if the induction works, then it works for overall time. Right? That's one trick and so that let us talk about temporal properties that were a certain set of temporal properties, pretty cheaply without having to go to temporal logic. Okay. The other thing that's happening, the sort of interesting mathematics under Flow Log is when you use things like [UNKNOWN], there's this problem that comes up that's always little brush that's always brushed under the rug a little bit, which is, you need to say something about what the SAT problem is, and there's a finite number of bits there. So you have to say like, well, I want three of these things and five of those things and two of those things. And what if you picked the wrong, you know, what if you picked the wrong number? And it turns out for the logic that sits under Flow Log in many cases we have a theorem that serves many cases. We can actually compute that bound automatically. So, you state the property and there's this, this sub routine that goes off and says can I compute the bound automatically and if it can it comes back to us and says I've computed the bound, this is a sufficient bound and if there's no counterexamples under this bound, there will be no counterexamples. All right, so there's this property called completeness, so we can do this in many cases, and especially in this kind of change-impact stuff we can talk about separately if you want. There we can really compute these bounds. So, now you can, so now it's this much nicer automated feel, right? It's got this automation that you want, but it's actually giving you a pretty powerful theorem but because we're in this when the space, that we sort of carefully navigated. >> That's, that seems it, I mean, I mean it's interesting that you're used to do, you're able to take these sort of things that allow for these, these things about states or a cheat and do some stuff. [CROSSTALK]. >> Right. >> This is exactly the kind of thing where I've noticed like, with CTL. Like we can say certain things like, you know, we could say that our, our controller is in a certain state, right? >> Mm-hm. >> Like, okay, we're in a state that says, like, you know, this host is not affected, and then. >> Uh-huh. >> Okay, well if this or that happens, then I want to basically transition to running this set of policies, right? >> Mm-hm. >> And now I can make exertions about. >> Hm. >> You know, when you can ever get in that state, or can you ever get out of it, or, you know. >> Yep. >> You know, will only reach this state if certain other things are true. But, we're at the level of talking about, like, you know, paretic policies or something. Right? Like, okay. >> Uh-huh. >> I can tell you that I'm, that I'm going to run a program called Drop. >> Right? >> But I can't tell you, like, what Drop actually does. Right? [LAUGH] >> [LAUGH] Right, right, right, right, right. >> You know what, what, what's in the tables at that point? So, I don't know. It seems to me like maybe Flow Log is closing some of this gap like, you know, but certainly as we did some of this work and then I looked at things like HSA I was like man there's this gap here, because like HSA kind of will tell you, you know, he, you know, here are the things that are true about forwarding like chronic data plank statement, and here's something like that will tell you like you know, what your control program like you know, what states it can get into, but what about like bridging the gap between- >> Right, right. >> Well, your control is doing, and that means like the state in your network is doing this. And then I can say like run this logic over here to tell me that I can be in this state and therefore that means I have a loop or not, like. >> Exactly. >> Is that the right way to think about bridging Opera? >> Yeah, yeah, yeah. So we, so as you rightly said, we've got these tricks that let us bridge the gap in certain cases. I think what HSA does is really neat. These are all great projects obviously, right? The thing with HSA is it's this very sort of instantaneous view of the world, and you'd like to think about how to make, stretch that into a temporal view. And one of the difficulties you're going to run into is if this data plane is being generated from some arbitrary program, well, now you've got all of arbitrary reasoning coming through the door because you left it open accidentally, right? and, you know, we know a lot more now about reasoning about programs in certain languages. But, you know, again we, my group's done some research on, you know, done a lot work on JavaScript and Python and things like that. So we also know what all the pitfalls there, right? We've got, we've got all the snake pits marked out nicely now. I think if you make certain restricted assumptions, if you say, look, I'm going to use this language, but I'm going to assume the following things never happened. And this is kind of the way the game's always played anyway, right? Most Java verification tools don't handle dynamic code loading, they don't handle reflection, they've implicitly already scoped the language down to the same version of the language or something. And we have some knowledge now how to create those sanitized versions of languages like Python as well, and so once we do that, then you could imagine building tools that generate, give you more information on what the step to step behavior is going to be. But I think that's one direction to go, that's sort of like working from the bottom up, and in Flow Log, we're sort of starting at the top and working our way down. And saying look you never want to actually see the open flow rules, that's obviously a stretch, but if you can be in a situation where you never want to see the actual rules except as generated by compiler, then hey, we can give you much better verification support. So this is the usual game, you sort of work from both ends, and at some point we'll hopefully meet up in the middle. >> That's interesting, and like as you mentioned you kind of like your, your, your experience applying verification, like to other languages and other settings, kind of like makes me wonder because, like coming from the networking side of things, I think, well, my bias is like, well, I've always kind of wanted to be able to do these types of things, and it's like, oh, here's SCNO, now suddenly, as you pointed out, okay now here's a whole bag of tricks that we can now go digging through and you know rummaging through old papers and maybe finding some cool ideas. From the perspective of someone who does formal verification types of things and testing and things like that, what's your view on SDM, like, is it basically like, oh, we know how to do this already and we're sort of like we're going to turn the crank on this new domain, or does SDM make it easier because it's a more limited domain, or is it...did it actually make it harder because it's some, you know, it's got a whole different set of. >> Yeah that's a great question. That's great, I mean, you know, like I was listening to a Nick McCuin's interview with you and, you know, he talked about how he wanted to, they wanted to bring software into the network and as somebody who used to wrestle with trying to deal with networking and verification, you know, ten years ago back when all you had was the, this, this language that some company owned and you didn't know entirely what it did. You know, we had a grad student go off on eBay and buy us this [UNKNOWN] and throw packets at it and try and understand what it does. We've all been there, right? So, from one point of view the great thing is that we've brought software into the network. The worst part of it is we've brought software into the network. Right, [LAUGH] we know a lot about software but we also know a lot about what goes wrong. So, it is absolutely the case that it's now fantastic that we have some control over what's going on, which, when it's no longer in some proprietary space we can throw tools like testing tools and verification tools at it. I worry a little bit that overtime people will discover exactly how little these tools do often achieve, right, and some of that promise will be discovered to be like more pain than promise and, you know, I think we'll see some sort of [INAUDIBLE] thing right, where eventually people say well, that was too hard so now let's go create some domain specific language that will make it easier to test, easier to verify. And you know Flow Log is arguably one of those and then you know then there'll be a backlash against that. So I think the usual sort of software cycle will play out. But it is the case that we know a lot more about testing and verification and so on. There's you know, great stuff like this, this wonderful project called Concolic Testing right which is combining symbolic and concrete testing and so on. All of these things are now techniques that were not there ten or 15 years ago, that we can now bring to bear. So, there's a lot innovation software world, lot of innovation networking world and STN definitely provides a place for both of those to stand together. And, and we'll discover you know, like from verification perspective, there are going to be things that will simply not work because the network is a different thing than a program running on an operating system traditional operating system, right. Where to get good decidability, we're going to have to figure out how to encode a theory of the network, a theory, and done some of this of course, theory of IP packets, theory of this, theory of that. But once we do that we'll discover that now we can bring all of this other cool stuff to bear and good things will happen. So I think the right thing is to be cautiously optimistic. I'm a little cautious because some of the stuff that never works quite as well as we'd like, but I'm definitely optimistic because there's a lot of stuff there to work with. Well, one thing that I wanted to ask you about to that we haven't quite touched on really, is like just this area of software testing. This came up a little bit, like even this week, like some stuff we built on [UNKNOWN]. [UNKNOWN] Has a regression test they made a change to the way packets were handled and then all of the sudden our app broke and they were like oops didn't have the right, you know, didn't have the right set of regression tests and it seems to me like okay, now we are in to this world of sort of like regression testing and, and, and just, also, just testing in general, what's kind of the state of affairs or kind of like the, this sort of I guess your sort of general opinion on software testing versus formal verification and, and specifically as it applies to like SDNs, I mean, it seems like, certainly like anyone who's looking at verification right now, maybe because of the, the people who are working on it, I don't know, but like, are really taking, taking more of sort of a formal verification approach more than like a testing approach. So, what's, what's your thought on that? >> Right. So I think now know a lot more about testing than we did 15 years ago. It used to be that 15 years ago, I mean obviously there were always people doing sophisticated things, but there was a lot of emphasis on thinking about different notions of coverage and so on, and that was good, that was important, it laid a good foundation, but now we have much more integration of the sort of formal, if you want to think of formal verification and testing as sort of two different camps. There's a much better understanding of how these two camps come together. There are concrete activities, you know like I said can call it testing is one. There's a lot more use now of writing specifications and generating tests from specifications. It's an old idea but it's made a serious revival in many ways. And how do we do this kind of random exploration to the search space and make it better and so on? We're doing a lot better job at this than we used to before. Obviously like with everything else having, having really powerful computers, [INAUDIBLE] and this you know, [INAUDIBLE] tools, machine running and so on. All of this really helps because we have great data structures, great representations, good optimization techniques, all of which are good because we're searching through a space and anything that makes representing spaces and searching through them better is good for us. So, I don't think of these things as at all being in conflict. I didn't, you're right, I think there's been some, to some extent. Maybe I'm a little guilty of this too. There's been some extent like the formal stuff has been emphasized more than the testing-oriented approaches. That may partly reflect the fact that the formal stuff, and I may be, may be a little mistaken on this but, tends to go with people who are building languages, and so they have more control over what is going on. In the software space, there's so much churn and there's so many different frameworks, and they're all kind of half-way there, and they're also building up, that investing and putting a lot of effort to testing one of them, if you're not one of the creators of them it's just not clear that that's where you want to put emphasis in just yet. Right? So there may be a little bit of that and once there's like more clear winners in the stream workspace then people who do testing might come in. But I want to actually talk about one thing that's really related which I alluded to, which is what this thing that we've been doing that we call change impact, right. Which is verification is great when you have a property you want to verify. I, I got something and I want this thing to be true. But often times that's not the real life of a programmer or of a developer. Right? We got a system that we have confidence in for some reason. sort of works for some reason. Right? Whatever, whatever reason we believe it works, it works. And then we change it and now, and we've had this conversation a lot with net ops and I'm sure you have too, where you say like, okay what is your standard technique when you change this thing and you want to know that'll still work, and invariably. [CROSSTALK] Break right, so, so can we do better than that? So, I'm really interested in this question of, so this is a kind of property free world, right? The property is how much is, it, is it the same, right? That's one kind of property. And so can we bring all this machinery of formal methods, all this representations and, you know, search space techniques and so on, to bear on this question of differencing. And that's where we, that's actually where we put most of our effort now in Flow Log and we did in the Margaret project as well, because that's something that a, that a developer and operator completely understands problem, right. You might say, well, I've got this tool and your first time to learn temporal logic, it's like, well, thank you and I'll get back to it in a year. [UNKNOWN] this is a problem they immediately understand. So, we're putting a lot of effort into that and I think that's another place that's, that's bridging the sort of, the sort of testing oriented [UNKNOWN] and technically that's exactly what you said right? It's a regression question. And, I made this mistake before do I still have this mistake [CROSSTALK]. >> [CROSSTALK] know what property it is that I want to express I just know that, it seems to work now and that's, I'd like it to continue. >> I'd like that to continue. Exactly. Exactly and, this actually goes back. I mean there's like, good human psychology [UNKNOWN] to be thinking about this, right? We're really bad about thinking about the things we don't think about, right? Sounds like a truism, but there's actually some content to that statement, like unknown unknowns, whatever, right? And so being able to say, hey, did you realize this was going to happen, and so this, this is the other thing is you have to think of this as an interactive process, right? You get some output and it says, here is lots of things that might have changed, and you say, well, okay, don't tell me about those things because I expected those. Now tell me about the things, you know, you want to apply a filter to it, you want to apply a view on it. Right. Tell me only the things that affect my egress filters because the rest I don't really care about. And then like, oh, that kind of. It is not going up. Well I didn't want that to happen, right? So we had to create opportunities for people to be surprised because the surprises are the ones that get them to reflect and what we, the really funny thing is then people start to build up properties. Like, you know what, I never really want that to happen, so now I'm going to state that as a property and that's a kind of way to trying to bootstrap the verification process as well, rather than just saying. Here's a tool, and if you don't have any properties it sits there and does nothing. Right. So, so that's another way, another approach to trying to bring these, the sort of the informal but coverage based testing world with the formal property world. >> That's interesting, yeah I guess another thing, that, that I mean. Probably could be highly frustrating for a programmer or an operator is like, you run a form, formal verification tool and it's like, okay that property failed. >> Yup. Yup. >> Okay, tell me how I fix it. >> Yeah. >> And even worse, like with the data plan right, like maybe if the [INAUDIBLE] fine and like, okay I have a loop or a black hole. Okay, tell me how I got into this state. >> That's right. >> What events led me here. >> That's right. >> Tell me what part of my control logic is messed up that got me into this state, like, do you think that like, I mean, the stuff that you're working on or, or other things like, in general, does verification help troubleshooting, or is it a related set of tools? I mean, where are [INAUDIBLE] troubleshooting. What kind of problems you know, are solvable, should be solved >> Yeah that's a great question, yeah. I think, I think these tools have a lot of potential, but one thing is also you have to think about what, even when the tool has the information I think you've got to put a lot of effort and think about how to present that information. Which I mean sounds kind of obvious. It's not surprising you have to put that effort in. You know, like in Flow Log for example we have taken as a founding principle, that people prefer concrete examples. So, and so even though we construct this, this mathematical object that represents all the possible things that can go wrong, what we do is actually we just spit out concrete examples, instances of that. And then people can say, oh, show me an instance of this form and then you know, do a, do a guarded exploration of the set of instances, and that's a way of understanding, that's a model, that's a, that's a belief we have about users and there's some you know, user studies and stuff that some people have done but [CROSSTALK]. >> I think that way. yeah, I'm not a mathematician, so I appreciate that a lot. [LAUGH]. >> [INAUDIBLE] You're pretty good at picking up being a mathematician. Let's put it that way. [LAUGH] But, but, it is the case. Even mathematicians [UNKNOWN] they work [UNKNOWN] examples. That's what they do, right? They don't prove a theorem, they go to the board and draw out an instance and say, wow, what about that? That should probably be over there. Like yeah, you're right, and then, that's how they generalize, right? They go from the, it's it's induction. Right? It's Baconian induction is what it is. So, so we've been giving people concrete examples, but then sometimes the examples can also be overwhelming. It's like oh my god, it's like, is there a more general structure? You're telling me that there are a thousand little examples, but there must be some more general structure. So then, how do you help for somebody to say, oh tell you what, I can generalize this part of this, I can generalize that part. I think there's actually a huge opportunity for HCI research here, right? We, there's been a little bit of work on understanding admins, some of it is anecdotal, some of it is more rigorous, but I think there's a huge opportunity if we can understand what, you know, the, a typical admin, you know, maybe two or three kinds of admins, what their accordances are, what kind of models, presentations work well for them, and then build our tools to cater to that. That would be so awesome. >> Yeah I know. Absolutely. I don't, I don't actually you know, another thing that, that certainly people have asked us. And, and maybe this hits like, right on your HTI point is that. You know we developed, we designed this for like, we think this is kind of easier to manage or easier to check. And then like, without actually trying it out, right, so you know, you tend to be like how do you know? Like, how do you know that's the right way to do it? I mean, is that something that you face as well in terms of like designing these systems? Is that something that you, you have to worry about it, those comments that you, say, get from reviewers, or [LAUGH] other things. >> Well, unless some reviewers, I think reviewers are kind of like us, so they won't believe you, [LAUGH] things a little more. but, but no, I think it reviewers would be, it would be good for everyone, all of us to be more skeptical about these things. And certainly, I mean I've read some of the chair literature I've done a little bit of non-network correlated to HCI and it's something that I really, I would love to do more of, but I'm just utterly unqualified so I just sort of bumble around in the space. But it will be really neat if more people and more HCI people and of course I know you've been involved in some of these projects as well, more of this sort of HCI networking interaction took place and we could do more to really understand what makes sense towards these operators because they're, you know, they're, they're really precious resources. Right? Every minute that an operator wastes we can measure in dollars and, you know, pick your favorite unit of currencies, so we can really measure these. And so, I think we would all be of benefit from being a bit more skeptical, not at the point of like. Cutting off research and saying no, no, don't do that. but, but at some point there's got to be, there's got to be that transition as well. It's like a different kind of technology transfer. >> No, absolutely, yeah I guess that actually taps on my last question which was. >> Uh-huh. You know, what were, you know, what do you think are, let's say you got a grad student walking in the door, or, anybody for that matter, who wants to work on verification, it's, you know, what would you, what would you have them focus on? What are the most important problems? I mean you just touched on a really important one which is sort of like how do you basically design an interface or a [UNKNOWN] to network operators because they don't want to write down math or these types of things but and I think we talked about some other things like you know, security being a challenge. I think another thing you mentioned was sort of coupling these temporal logic state based logics. A lot of interesting things I think came up, but anything else, like? >> No I think that's a great list. The thing that's really cool about the list you just gave me is it just shows how diverse this area is. Right? I can give a problem, depending on the student who came in, if they're an ACI student I can give them a hard ACI problem. If they're theory [UNKNOWN] student, some hard theory questions. If they're a PL student, a hard PL questions and every one of those areas makes progress, right? Progress in one area helps all the other areas. At least it doesn't hurt the other area, and maybe defines the area problem for that area a little bit better. And that's what's just so awesome about working in this field. It's like every one of these things, and you know, there's also the software engineering questions like testing and so on, and you know, and the interplay between these. Like how does the [INAUDIBLE] make the ver, it might even change the verification problem we work on. The verification changes the testing questions we need to ask. And, you know, it's just this beautiful interlinked area. That's what's so great about it. >> Yeah, I know. Lots of cool stuff [UNKNOWN] it's gotten me very excited as well. I, I sort of thought the whole thing was dead like ten years ago, as you pointed out, like when we were buying Cisco routers on Ebay. >> Yep. >> It's it's kind of like a whole new world now, so, it's cool. >> It totally is. Totally. >> Yeah. Well thanks a lot. Thanks for your time. >> A, a real pleasure, thanks, great talking to you Nick. Bye-bye. >> Okay, thanks.
