Adam Wick on Security, Formal Methods, Types, Unikernels, HaLVM, DRM

1. We are here at QCon San Francisco 2015. I am sitting here with Adam Wick. Adam, who are you?

I am research lead at a company called Galois. We are a research and development firm out of Portland, Oregon. I lead our mobile security group as well as our system software group. So my particular role is to find interesting research projects in the area of mobile security, network security, operating system security. Find those projects, deliver interesting prototypes and results on those projects to our clients and then basically “wash, rinse, repeat”. I have been doing that for about 10 years.

2. Security is a big topic. Why isn’t our software secure by default? Do you have an opinion about this?

Software is not secure by default because it turns out security is actually very hard and it is hard for any number of reasons. It is hard because predicting what an adversary is going to do is very difficult. There is a lot of adversaries in the world with a lot of different motivations. I actually just came from a talk about attacker motivations and how you want to think about them and reason about them. It is a very complex field. The other problem is that software these days is just incredibly complex. The amount of layers that are in all of our software projects is huge and even the actual software we build is huge. So, if you think about a Java program or a C# program that is on the market today doing anything of any criticality, you have all the Java and the C# plus all the libraries, plus the virtual machine, all the libraries of the virtual machines requirements, plus all the operating system kernel. That is millions, and millions, and millions of lines of code, right? An attacker has to find one problem. Those of us doing defensive work have to solve all the problems. That is an asymmetry that is just very hard to deal with.

3. Are there are approaches for this that we could use, any tooling. Let’s say in a company where I do not use C, does it help or are all languages basically screwed?

Not using C helps, using higher level languages helps because they save you from a multitude of sins, right? You do not have to worry about accidentally having a buffer overrun that destroys the security of your entire project. You still have C underneath you somewhere, so you have to worry about that, right? But all security is a game of trading off what your risk is versus how much effort you are willing to put in to mitigate that risk. Different people have different levels of concern. If you are a media distribution company and all you are doing is distributing videos around the internet, then your level of risk is much lower than that of someone doing finance, which is in turn much lower than that of someone doing national security work. So you have to consider how much your secrets are worth versus how much you are willing to put into those secrets. So that is one tradeoff you make. Higher level languages help, unikernels, which I gave a talk about earlier, help by reducing your attack surface, there is a number of tips and techniques that you can just apply. Sometimes I wonder why people are not just using a TLS for all of their communications because, why not? It is pretty cheap. So these are some tools that you can use to help your security posture. But it is always a cost/benefit.

Werner: I guess one of the problems is of course C, one big offender, this portable buffer overflow generator, but as you mentioned, I can write in Java or your language of choice Haskell, I can write a SQL injection flaw in Haskell, unless you tell me otherwise.

You certainly can and, in fact, it might be easier in Haskell because fewer people write SQL stuff in Haskell and so there is fewer validators in the back-end, right? So that is sometimes the cost of going to a smaller language. But SQL injection is going to happen in any language you want. I mean that is just one problem with that attack.

4. Are there any other ways around that, like what about formal verification or are there any academic goodies that are promising us to make software correct? In your research, have you found any that helps now or that might help in the future?

With something like SQL injection attacks, there is basically three roads to helping yourself out. You can do formal verifications sometimes. Usually it is more in the nature of watching your information flows and using formal verification to ensure that data from a user never flows unedited or unobserved to the SQL backend. So you make sure that any way the user introduces data into your system, someone has looked at it, someone has processed it or appropriately handled it. We have seen some use of that at Galois, we have used that sometimes ourselves. It is a sort of technique of making sure that all information flows past through a guard, sort of a trick of ours, which leads me to the second approach. With a lot of security things, you can design your way out of security problems.

For example, one classic problem you have, you have a carefully designed system and then someone avoids it. There is this classic picture on the internet, if you have ever seen it, where there is a road with a gate in front of it and there is just lawn on either side and you see tire tracks going around the gate. So someone went to the forethought to think “Oh, there should be a gate here”, but they did not think “Oh, we need to make sure that they cannot just avoid the gate” Security is the same thing. We can put a lot of effort into making very cool gates, but a big part of security is looking at your design and going “OK, but is this the only way through the ones that we put the gate on?” So design is just a huge part of security sometimes: regardless of language, or implementation or tools, just making sure you know where your traffic is going and why. And then the final thing you can use: high level languages help with this sort of stuff, just sort of standard type systems, comments, all the stuff where you have to look down and someone has written down “We assume that everyone has to go through this gate”.

Because one of the biggest problems is not the initial version of the program, it is version three, because that is a different developer, even if it is the same physical person, right? They have changed over time and they have forgotten all the stuff they assumed before. So having documentation and rationales, hopefully reified in a type system or a formal model or some sort of something like that is great, but even just a comment or a design doc that says “By the way, anything that goes through here needs to be validated” is so helpful.

5. I like the example of sanitizing a string before it goes into any other query languages and so on. In different languages, how can I tell the language to do that for me? In Haskell, which we talked about, is there a monad for that or anything else, like tagged types?

There is always a monad for that, but actually, in Haskell, I would usually use a simpler methodology. So something you can do is: you have strings and just have them be strings, but you can make a new type, and I am actually using Haskell syntax as a I say this, but a new type which is user input. Then you can make sure that user input never directly flows into a SQL server, just by the type system, by saying the SQL server takes things of processed input and then your types missmatch. So you cannot just take user input and give it somewhere [that takes ]processed input. You have to go through a function that changes one into the other. So in Haskell we can play these games. In many high level languages you can play these games, just by wrapping things in one layer of types. That does have a performance hit sometimes, but again, we have to come back to “Is what you are doing right here really that performance critical? Is it so performance critical that you are willing to waive away the security benefit that you might get out of this?” I think there is a lot of cases where computers are pretty fast and we should let them be fast and we should use that fastness to make our things more secure.

Werner: It is interesting that you mentioned performance. I remember one of the recent hack cases. Someone found a user database and the password was hashed with BCrypt which is the right way, more or less, which is good. Except they found there was another column in the table where the password was hashed with MD5. I think some people discussed that this might have been a performance issue, “Logins are slow because someone is using the stupid BCrypt! Let’s MD5 it!”, which goes back to your point about version 3.

When situations like that pop up, I immediately leap to the fact that someone did not know that there was a BCrypt version and then they went “Oh, I need to get the password out, so I will just add an MD5 column here” So much of security sometimes is just documentation and knowledge transfer. It is that someone needs to solve a problem because their boss tells them they have 24 hours to solve this problem and they did not know to look somewhere else so they took a shortcut.

Werner: And they punched a hole in a wall

And they punched a hole in the wall and now there is a hole in the wall and anyone can look through it. Maybe MD5 was a performance thing, knowing absolutely nothing about this attack, just exactly what you told me right there. My guess, I bet there was some developer who was doing their best, who had a short deadline and said “I guess I need to make this right now. So, MD5 is a hash, I will use MD5 and see what happens”

Werner: It is interesting because I am wondering – you mentioned documentation and stuff like that. We all know what happens with documentation. It props open the door, right? I wonder what other approaches there could be.

As you said earlier, I am a Haskell person so types are always my solution. Types can be checked, they are automatically checked, they are checked every time I commit it, if I have any sort of continuous integration thing. The more types I can introduce to put barriers between shortcuts and actual security concerns, it is a huge win. So, if I can put a thing that says “This is unencrypted data” and “This is encrypted data”, then I can reason about where encrypted data goes and where unencrypted data goes, unprocessed strings and processed strings, all these sorts of things. Now, I will admit – I am not a perfect programmer. I talked about Tor yesterday and I put a Tor library online. There are some places in that where I really should have used types and I have not yet gotten around to doing that. But, I think it is a good discipline when there is really security critical data of “this is a password” – “this is a hashed password”. Let’s make sure that the only thing that goes on disk are hashed passwords and then we can just look and have one implementation of hashed passwords which is BCrypt. And everyone knows that and there are functions to deal with that and so you do not have to worry about any of this stuff getting cross-contaminated with other things. So, I like Haskell, I like high level languages like Haskell, I think types can save us from a lot of our problems. So that is where I would come from. I used to work in the Racket community and the Scheme community and there are voices at the back of my head from that community going “Types are not the answer!”. But they have things like contracts and tools that serve sort of the same purpose of being documentation that is checked as a program runs, before the program run, to make sure we do not make any of these accidental mistakes.

6. Going back to your example of the gate and the road and the grass next to it, I kind of wonder if that was done by a very law-abiding persons who said “Well, that is the road. I put a gate on it and no sane person would drive around it” So they just could not think it. That person was not, as I like to call it, a big enough jerk. On your development team you need a jerk who likes to break things. So what is your take on this?

I think it helps if you have some people of broader mind – let us put it that way – to look at these things. I mean the example of putting a gate on the road and then just having blank lawn all around it seems so obvious in hindsight. But if you are just thinking “OK. I have a road. The road is clearly the only way to drive a car from point A to point B. Let us put a gate on it” – that makes perfect sense as I am talking to you, but maybe you were imagining there were fences along the sides, maybe you were imagining there were buildings along the sides so that in order to go around the gate you would have to mow down pedestrians or something like that, which most people are not willing to do. So you have to be careful about your context sometimes. Sure that having someone with a broader mind is absolutely critical, if you can afford to have someone like that on your team, but also having the presence of mind to go to stop and look at the assumptions that you have about the world. So you need to revisit this assumption that cars can only drive on roads, right? And then think “Actually, cars can drive on lots of things that are flat. So, is it flat around here?” So, that is an interesting process. It actually goes back to my documentation point earlier. How much better would the situation have been if someone had said “Put a gate on the road, our assumption is that cars only drive on roads”. And if someone was taking that and applying it to this particular situation and had the presence of mind to look at that assumption and say “Actually, in this case, the cars can drive alongside the road”, then they might have thought “Maybe I need to think about something more advanced to do here” So again, to your earlier point, documentation is mostly useful at holding coffee cups and propping up doors, but having that documentation can also save you sometimes when you have something that worked here, whereas if you can list all the assumptions you made so that when someone tries to apply it in some other place, they can revisit those assumptions and make sure they are still true.

Werner: My favorite exploits are buffer overflows. I mean it is just data. That does not run. Oh, yes, it can, if you just poke it the right way.

Yes and it gets harder every day. I mean we had the simple buffer overflows that we love and respect and remember from school from 10-20 years ago, but the buffer overflows these days have gotten so complicated where they actually do not even inject code. They just change return addresses and then run through existing code to have some effect. I mean the whole return-oriented programming control flow attacks – we have been doing some research at Galois, trying to figure out how to stop this. And it is just an immense area. You know, protecting your computer programs is very hard. It is a hard problem. We can get so much leverage out of using high-level languages, about being pretty safe with the constructs we use, about throwing types every once in a while, having a design that makes sense, we can get so many low-hanging fruit by dealing with those. The nation states of the world – they are probably going to find a way around it. But for the class of attacks that, I think, most of us deal with on a regular basis, just having good processes, good languages, can save us from so many problems.

7. I love the classic buffer overflow. I used to think it was dead because of both the NX bits, the No-eXecute bits and also ASLR and stuff like that, but as you say, return oriented programming – that is amazing! The ROP gadgets are Turing complete, I think?

Yes. And it is becoming a race. So as I said, Galois has been doing some work in this area and it becomes a race. As you want to make gadgets harder to find, but they will always be here and so people advance the tools to find them and put them together. I have heard rumors of people using things like SAT solvers to combine gadgets to do something. So they basically just state what they want to do and solve for “How would I actually do this in this program?” which I think is kind of amazing. Now, I have not seen any evidence of this myself, but that sort of capability is potentially out there and it is a hard problem to solve. We have done some work with “Are there ways to recompile programs so that is harder to find gadgets?”, “Are there ways to insert instructions so that it is harder find gadgets?”, “Are there ways to change the operating system so that you can tell if someone has used a gadget?” But there are hard problems and in each case you are just raising the bar, which, do not get me wrong, I think it has great value, because it would be lovely if the only security threat we had to worry about was sort of nation state level actors and not organized crime or just script kiddies, right? But, we do just keep raising the bar and then attackers find a way to get over that bar and then we have to keep going.

Werner: Yes, it is astonishing. It should not be possible and just evading, getting around ASLR should be complicated. They find a way around it.

Yes, they do. At some point the attackers are not some sort of strange form of human, but they are human that are motivated by slightly different things. They have taken the problem and they have just deconstructed it. They say: “All right. You have the NX bit, you have the ASLR, you have all these things running. Step one: I am going to figure out how to undo your ASLR. Step two: I am going to add a ROP gadget that undoes the NX bit. Step three: I will then use a buffer overflow to inject some code into that and then I own your process”. It is a very methodical “Let’s do this, and then we will do this, and then we will do this, and then we will get through to the end” So you can see how they get around it, but at the same time, when people say “Oh, yes. I can get around XYZ, ABC” it is kind of mind-blowing to me.

8. And you think there is no end in sight for this? I mean, these attacks get much more difficult. There is so much thought and care involved. Is there nothing that will make it so hard that it is really a five year process of finding an exploit?

I think there is and I think we are just moving towards that over time. I think formal methods proving your programs correct. I mean if you prove your program is correct under some set of assumptions, as long as those assumptions hold, no one is going to be able to attack it. The trouble right now is that formal methods tend to be fairly expensive to use. We have used them at Galois for various pursuits, either to truly formally verify a component or to sort of spread some assurance through the thing and through your program. So, in one case, we took the core component of a secure architecture that we have built for basically doing multi-level file sharing. So you have “high” that wants to be able to read files at high, “low” that needs to be able to read files at low, but you also want to allow people at high to read the files at low. How do you do that without information transferring between the two levels? So we built a system to do that and we formally verified the very tiny core piece of that. But that was a pretty big effort and we are talking about, I think, somewhere around 100 lines of C. So that is expensive and does not really scale. So you have to think about formal methods in design and we can think about that. You can also use sort of light-weight formal methods. There is also some interesting tools out these days. Frama-C is one that we use a lot internally, where you can prove certain properties about your C program, make sure it does not have a buffer overflow or whatever. It increases your development time, but gets around a lot of these problems. I think as those tools get better and as we migrate to thinking about secure design and making sure our core security critical components are formally verified, we will get to the place where it is just very hard. We will get to a place where you will basically need to worry about supply chain attacks and you have to worry about just human factors of someone coming in and tricking you out of your password, right? That is always going to be problem. There will always be a human in the link. So we have to harden those too at some point. But computer security just the thing, I think we are moving towards around where that can be solved, but we are not there yet.

9. Going the other way from formal verification, which is very strict, locking everything down. If you look at something like ASLR, which is something else making things random, which kind of makes me think about polymorphic viruses and stuff like that. Is there research into this or just making things more random, as an approach?

I think there is a number of interesting things about randomness and I think it is a Darpa project. I know there is actually a couple of projects in this area where the idea is you actually can randomly modify programs so that they have the same behavior as the original program. But if you are in an attack that worked on the original program, it might not work on the new one. So basically you have this program which adds up these three numbers by adding A to B and then adding C.

We are going to randomly redo it so that now it adds B and C and then adds A, which is the same actual effect you want at the end, but if you are assuming that you get these instructions in this order in your attack, the new program does not match that attack. We have seen other things where there is the idea of making programs more brittle so that if you call a function from an unexpected context, it is much more likely to crash, which sort of breaks my brain a little bit because there was this whole session that we did in computer programming for a while which was all about resilience – let’s make every function resilient against even the most weird inputs.

The idea behind this is that maybe that was a bad idea because now an attacker can use that code, potentially in way that we did not mean it to be used. What if we make it more brittle on its input so that if you attack it, all of a sudden it crashes immediately? I think there is some really interesting ideas in randomly modifying programs as they run to make sure that we detect attacks as fast as possible. ASLR is sort of the base for this where you randomize the address system so that no one can predict where the code is. But there have been attacks against that that are, I have to say, fairly successful. So this is sort of the next step of “Can we randomize the runtime?” “Can we randomize the compilation that make it a little harder to predict not only where the code is, but what the code is fundamentally?” So it is a research program right now and we will see what it all comes up with. But it is interesting stuff.

10. I guess you have mentioned before, one way for making software more secure is to give attackers less of an attack surface. I guess that is the term. You are working on a project called HALVM, which is a unikernel. Maybe you can give our viewers just an overview of what makes a unikernel different from an operating system or other program?

Right. An operating system, a sort of traditional operating system when we think about it. They are designed to run a bunch of programs from a bunch of users on hardware. It is all about sharing resources amongst all these programs. One interesting thing that has sort of occurred is that now we have also moved to virtualization. Now we have multiple operating systems and now the hardware is actually being shared by the virtualization system below it, which has made us actually sort of revert, in some sense, so that a lot of deployments these days are running in an operating system that has one user and one program, right? And it is just doing one thing.

But the trouble is that of course, you still have all the other stuff there. You still have multi-user support, you still have schedulers waiting for other processes to start and you still have all the code and libraries and whatever to support stuff that you are not using. So the idea behind unikernels is that when we have this situation, can we just minimize all that away? Can we just take these small, tiny bits and pieces of the operating system that we are actually using and compile that into our program and then just run our program directly on virtual hardware. So it harkens back, there was a bunch of work on sort of early-mid 90’s onlibrary operating systems and exo-kernels, which was one of the terms that was used. We are sort of revisiting those notions again, but now in the context of virtual systems. So the idea is that instead of taking the operating system and taking it in its entirety a sort of a software package that we have to build on top of.

What if we treat it as a library? What if you just say I want this bit and this bit and this bit and I do not care about the scheduler and I do not care about the file system and I do not care about the disk drivers or wireless drivers or any of this other support that is in there. We just take the pieces that I need and then I will compile those into my application, which means that all the other stuff is not there anymore. So if there is a bug, you do not have to worry about it because you are not subject to that bug since that code is not there. We have seen attacks in the wild where people use things like clib or OpenSSL and it is not the part that they are using that gets cracked, it is some other feature. Some other function is reused in a bad way. So if they could just carve that out somehow, they could have gotten a big win. So that is part of what we are trying to do with unikernels, is how we can take these applications, compile them with enough library operating system support to make them run on virtual hardware or even physical hardware and then do that transformation. What that does is that it basically reduces our risk.

It reduces the number of places that things can go wrong. One of the ways to think about risk in a program is how many bugs per line of code do you have. Well, you can address that either by lowering the number of bugs per line of code or by removing the number of lines per code. So unikernels take that second approach: Let’s remove the amount of code in here and then even with the same defect rate, we will have much fewer defects because there is simply less code.

Werner: HALVM which it is using – you have to write your code in Haskell. Is that true?

Yes.

Werner: Haskell is obviously the best language out there.

Clearly.

Werner: But what if I do not want to use Haskell for some reason?

Unikernels are a concept really and there are many instantiations of that concept. So the HALVM is one, because I liked Haskell, because my company uses Haskell a lot, we chose Haskell for ours. There are a bunch of others. One of the sort of the bigger, better known unikernels out there is Mirage and they use OCaml. Now maybe you think OCaml is not much better than Haskell. Well, there is also these days a rump kernel which is just C, which, actually, a lot of us are starting to migrate to here and there because it is a substrate for us to play with. There is also Osv, there was at least one Erlang unikernel and there might be two now. Basically I tell people “If you want a funny unikernel through your language, search for your language on Xen, which is a hypervisor” Just do that Google search and you will probably find something. It might be a very early stages project, so you might want to rethink and go to one of the mainstream ones like Mirage, HALVM, rump kernel, OSv, one of those, but it is probably there. Interestingly, I keep expecting to see a Go or Rust unikernel. Both those languages seems like they are incredible targets for unikernels, but I have not been told of one yet. Possibly, as soon as this interview airs, I will get vast amounts of e-mail about why I did not know about this one. I apologize in advance. We'll crowd source it. I would donate to that Kickstarter campaign.

Werner: Oh, cool. So audience, you have your jobs.

I did not say how much. And I will donate.

11. So to wrap up – we were talking about security a lot. You have a project where you work on DRM. Does that make you evil?

Yes. We have been talking about security and when people talk about security, they tend to talk about whether the computer is secure. Then we try to make that computer as secure as possible. But the interesting thing about security is that if I, as a third party, am wondering around, how do I know that that computer is secure? I may trust you because I know you made the best effort to secure this computer, but if I am just a bank looking at a computer that is connected to me or a phone that is connected to me, why do I trust that that computer is secure? I think the next step in security is not just making things secure, but also proving to people that we are running in a secure way, right?

So we have been doing some work in a project in Galois, where we started investigating “I have a mobile phone, how do I prove to someone that the software running on that mobile phone is correct?” We end up starting to talk about things like roots of trust and measurement where we take scans of the phone and say “This is what I am running and you can trust that that is what I am running because I am running this software in my kernel and you can trust that I am running in that software in my kernel because I booted this kernel and you can trust that I booted this kernel because my root of trust says I booted that kernel” And then providing these arguments to third parties. So this has an interesting connection to DRM, because there is obviously some use for that in the DRM sense where you say “I will not give you content unless you can prove to me that you are running a unmodified player that I am OK with” That is an interesting way to do the DRM handshake. The reason why I bring all this up is because it is a different way of doing DRM than the way that people are doing things currently. So DRM today is frequently implemented by doing everything that they can to keep you from doing anything that might be bad in the future, because that is the only handle they have to turn – try to keep you from doing things that might be bad which means that my phone is locked and I cannot install whatever I want to unless I go through some sort of baroque unlocking procedure and I might want to install this, but I cannot do this because my upstream carrier will not install that thing, because one of their people does not want me to install it because maybe I could use it to send a movie to somewhere I should not send a movie. So that is one of the reasons why people hate DRM – because I bought this device and I should be able to do whatever I want with it. So the interesting thing about this measurement approach is that it says “OK. Go ahead. You can have your device. You can do anything you want with it. The only restriction is that as soon as you ask for content for someone, we want to know that you have not done anything on our bad list” So it is an inverted way to think about DRM and it is interesting both from a DRM case and from just a common enterprise security case. I might not want to deliver my sales list to a client or a salesman in the field if their phone has been compromised so it would be nice to be able to ensure that their phone has not been compromised. You could even be using any sort of MDM solution on their phone where supposedly they cannot open this application unless the MDM unlocks it appropriately. Of course, how do you know that the MDM is really running and that someone is not lying to you. So this ability to go back and prove that you are running exactly the software that people think you are running is actually very valuable. I just think it is very interesting in the DRM case as well because there was the huge DRM wars in the 90’s and so on and one of those main arguments was “They locked down my device”. What if I took that away and now it really is about “You can only run this player to play this software”. Does DRM bother you then? I am sure that there are people who go “Yes, absolutely” I think that this is a really interesting conversation that as we push forward in this proving security to other parties, that we are going to have to revisit and think about it.

Werner: It is definitely an interesting approach. I guess our audience can respond to the comments or e-mail you again.

Yes. I am sure I will get lots of email.

Werner: Excellent. To finish things off – you are a Haskell programmer.

Yes.

12. Adam Wick, if you had to be reborn as a monad, what would it be?

I think clearly the right choice is a continuation monad because no other monad allows you to go back in time or forward in time if you are in a really boring conference talk. So that sort of manipulation of “I went to this talk and now I regret it. Let’s just jump 40 minutes ahead” or “Oops. I totally wrote that Tor program wrong. I would like to jump back to the beginning and write it differently” I would definitely go with a continuation monad.

Werner: OK. Continuation monad it is. Thank you, Adam.

Thank you so much.