When a security snafu happens on the Internet that's due to a design or coding error, there's always a scramble to issue a fix. Meanwhile, the public frets. Galois, Inc is one of several companies that is developing the process of writing provably correct and secure software. How do they do it?
______________________
The story started a few weeks ago (May 22nd) when I wrote my Friday column, Particle Debris, that referenced some frightening security lapses.
Not long after I refefrenced Logjam (and an infamous predecessor, Heartbleed), I ran across an article in the May, 2015 issue of Aerospace and Defense, page 40, that had a short article entitled "Anti-Hacking Software for UAVs." I was intrigued by this one sentence about the company, Galois, Inc.
Galois is part of a team that produced provably correct and secure software that runs on commercial UAVs.
The idea here is that if the OS of a commercial UAV could be hacked, the aircraft could be commandeered by an unauthorized person with unpleasant consequences. But, on the whole, it sound to me like the software development techniques could be more widely applied, and my guess was right. I decided to interview the CEO of Galois, Dr. Rob Wiltbank. Dr. Wiltbank was extraordinarily gracious and spent some time answering my questions via Skype. Here's an edited transcript. It's an eye opener.
Martellaro: I'd like to hear from you, at a high level, how this process you've developed works. Plus, is this a small scale thing for small hardware items, like a nine ounce UAV? Or whether this programming technique more widely applicable to companies like, say, Google and Apple.
Dr. Rob WIltbank, CEO Galois, Inc.
Wiltbank: That last question is very interesting. There's no doubt that more of these tools are being used by Google, perhaps less so, but by Facebook and Amazon. The use is expanding, and we're definitely seeing more use of verification tools. It's not pervasive by any stretch.
Back to the question before that, "... can it run on larger systems, or is it constrained?" My answer is that these techniques are definitely not constrained. We've seen people using these techniques at an enterprise level. We've seen it in medical devices. Writing provably correct code isn't constrained in any way.
TMO: How do you prove that software is secure? Do you have code that scans the source code?
Wiltbank. No. When we talk about provably correct, the fundamental basic approach consists of two steps. Number one, a thorough and complete logical model of the system. You ensure that the logical possibilities are coherent.
TMO: Is this something like UML? (Unified Modeling Language?)
Wiltbank: There are tools like that. Another is AADL. (Architecture Analysis & Design Language.) There are others. But after you have it all laid out, then the trick is a mathematical analysis of the code.
TMO: Tell me a little about the mathematical analysis.
Wiltbank: Sure. All that mathematics is done before you generate any code. These systems have massive numbers of possible states. You're basically running the math across the states of the system to check for logical consistency. [We didn't go into the exact mathematical functions in this high level discussion.]
Next page: Are some languages better than others for secure software?
Are Some Languages Better Than Others For Secure Software?
TMO: Are there any languages that are more amendable to secure code? Or are all languages equivalent in that respect?
Wiltbank: There are definitely better languages. We happen to use one called Haskell. The reason is that Haskell is a very strongly typed language that forces constraints, and it checks for things along the way that have to do with how you express your intentions to the system. [emphasis added.] As a result, there are certain expressions that you cannot communicate to Haskell in an unclear manner.
TMO: I read that Apple's Swift language has some of its roots in Haskell.
Wiltbank: Yes. And Apple is definitely doing more and more with this kind of stuff. That is, eliminating design bugs very, very early in the process. Before you've even written a single line of code.
TMO: I wanted to revisit briefly the idea of code that monitors code.
Wiltbank: What happens is that when you monitor runtime code, all you're doing is moving the trust from the original software to the monitor. The trick would be to design the monitor the same way as the original code. That might not be a bad idea, but it really is just relocating the trust. It doesn't substantively solve the core problem. You have to trust something, and if you put a monitor in place, do you need a monitor to monitor the monitor?
TMO: I see. Do you consult with Apple on any of this?
Wiltbank: We do some with work with large companies, but Apple isn't one of them. But because Apple does hardware work... people coming out of the hardware world, like Apple, are used to using CAD systems and mathematical modeling to validate the correctness of their physical design before manufacture. And when they get into the software world, they wonder: why aren't people doing any of this early design work before they write the code? They consider it to be patently irresponsible.
Going back to the second part of this process that I mentioned above, you don't hand write code. Preferably ever. Definitely not in the critical parts of the system. We use domain specific languages that actually generate the code. It's generated in such a way that it's correct because it's [unambiguously] based on the model that was built.
If you do it right, that computer written code is usually better than human written code. Now there may be programmers where that isn't true, but in the main, if you really want to trust code, you don't want to hand produce it.
TMO: I know from my own experience that the machine written code often looks complex and funky. The human programmer often has the feeling that he (she) can write cleaner code that they understand, but you just have to trust the machine written code.
Wiltbank: In fact, despite the temptation, you never tweak machine generated code. If there's a problem, you must go back to the generator and find the design problem.
TMO: But! The code generator is still written by humans!
Wiltbank: Yes, but because of the repeatability of the code generator, it's a better thing to trust than an individual programmer. There's a lot of work that goes into the refinement of the code generator.
Next page: A software fantasy.
A Software Fantasy
TMO: I have en enduring fantasy about an A.I. agent that sits over the shoulder of OS X (or Windows 10) and monitors the state of the system. It notes things that have changed, software that's been installed, looks for conflicts, analyzes spinning beach balls, and so on.
Wiltbank: We actually have a system like that that, but it's not A.I. It's an agent that works on cyber-physical systems that knows how the system should be performing and monitors it. [Examples are ADIDRUS and TrackOS.] Any variation ot the performance level gets flagged, and it can take remedial action.
TMO: Aha! My fantasy isn't a fantasy anymore.
Wiltbank: That's how we monitor the runtime of a drone. If someone or thing hacks in, we can detect the change in the state and figure out that something isn't working right. It may not know what, but it knows it shouldn't be happening. So it retreats into a safe mode and protects itself.
TMO: It seems to me that all we discussed has great application for autonomous cars, a subject that's become very popular lately.
Wiltbank: We're definitely doing a lot of work in autonomous systems.
TMO: In fact, this is all coming our way in terms of autonomous cars and family robots.
Wiltbank: It's already happening. You can buy a car today that controls your steering and brakes on the highway at 75 miles per hour. You're definitely trusting it to not crash.
TMO: This has been great, but it's time to wrap up. Do you have any final thoughts?
Wiltbank: I think you're working on an interesting topic: helping people understand the basics of formal verification, code generation, and that you can actually produce software you can trust. And the entire state of the Internet is going to remain as it is now until we decide to produce software in a different fashion.
TMO: Thanks Rob. This has been a fascinating discussion.
______________________
Computer languages teaser via Shutterstock.