Links

Ben Laurie blathering


Useful Security

A while back, I had a bash at formal methods. Reasonably enough, some people had a bash back. I feel I should respond.

Michael asked “what about Tokeneer?”

The description on that page makes some great points for me. Firstly, and I think most importantly

At each stage in the process verification activities were undertaken to ensure that no errors had been introduced. These activities included review and semi-formal verification techniques applicable to the entities being developed.

In other words: “we can’t actually apply formal methods to the entire process, so we did some ad hoc stuff, too”. Core to this problem is that you have to somehow describe what it is you are trying to do. In order to disguise the problem, formal methods folk like to call this a specification – but when you get down to it, it’s a program. Which can have bugs in it. Which you can only diagnose by thinking about it and testing.

Next, from the overview, section 5

Since release 7.4, SPARK has included an “accept” annotation that can be used to justify expected warnings and errors. These annotations have been added as appropriate.

In other words, verification fails, but these failures are “justified”. Hmmm.

Again from the overview (section 5.3) even after formal verification a bug was found, which was an elementary integer overflow bug. I would hope any competent programmer would have spotted this as they were writing the code, but apparently it was beyond all this expensive and painful infrastructure.

Finally (there’s more, but I have other things to write about, so I’ll stop here), again from the summary

# lines of code: 9939
# total effort (days): 260

Wow. That’s a lot of days for not very much code.

Toby asked “how would you feel about a proposal that asked for a range of standard software modules whose design had been subjected to formal analysis, at some semi-useful and reasonable level of abstraction, of some of its key functional/security properties?”

I guess I feel about this rather as Gandhi felt about Western civilisation: it would be a good idea.

More positively, I imagine there are actually some modules that are sufficiently small in scope that one could convince oneself that the specification was actually correct, and maybe even prove that the implementation matched the specification. For example, things like arrays, sets and maps might be implementable correctly. Where it all falls apart, in my view, is when you try to make a system that actually does something useful: then you get into the realm where debugging the specification is the hard problem.

Ian Brown asked “do you think a formally verified microkernel that enforces security controls within an OS is achievable/desirable?”

I think this actually might be achievable, and perhaps even desirable. But I’m not so sure it would be truly useful. A microkernel architecture inherently punts on all the interesting security questions and simply enforces whatever incorrect decisions you have made outside the kernel. So, you are still left with all the real-world security problems, but at least you have a place to stand when you claim you are enforcing whatever security properties you think your code implements (that is, you can discount the microkernel as a source of problems and only have to worry about the other 99% of the code).

I also strongly suspect that a team of skilled engineers could carefully write a secure microkernel that was just as robust without any need for formal verification. More quickly and with less swearing.

Finally, Anil Madhavapeddy writes “Modern type systems spring from a solid formal footing, and mainstream languages are adopting functional features”.

This is a great point, and I actually agree. I’m a big fan of type safety, as anyone who’s seen some of the hoops I jumped through in both the Apache module system and more recently in OpenSSL will know. I really like things to break at compile-time rather than run-time if at all possible, and type safety is one way to achieve this (this is one reason I prefer C++ to C, despite its many defects). I guess functional languages also have interesting properties from that point of view but I feel like I understand them less. I really must learn Erlang (or Haskell, I suppose, but I’ve tried and failed a few times already – it seems there are no good tutorials out there).

Anil also says “Even for C, static analysis is increasingly used to track down bugs (with products like Coverity which are very effective these days)”.

Sorry, but no. I thought for quite a while that there was a future in static analysis. But the more I am exposed to it, the less I think it is true. The false positive rate is still fantastically high, even in Coverity, which is probably the best system I’ve played with, and even correct hits tend to be on the “academically correct but not actually useful” side.

I do continue to suspect that static analysis combined with annotation might be useful, though (e.g. as in Deputy). But really, this is just trying to bolt on strong typing to weakly typed languages and isn’t truly static analysis is we hoped it might be.

Finally, he says “If things continue like they have been, then we’ll continue to cherry pick the practical developments from the formal methods community into mainstream languages, and reap the benefits.”

I certainly hope so, and I don’t want to discourage further research into formal methods. I just object to the notion that they are practical to the extent that we should be trying to use them wholesale to build real systems. They really aren’t.

I was intending to also talk a bit about things I think actually are useful for security, but I think I’ll leave that for a later post.

6 Comments

  1. I have had very good experiences with Coverity, and would recommend it strongly — if you can afford it! However, I suspect that for many users, the positive impact of Prevent comes from effectively upgrading C to be a type-safe language. Could all this have been avoided by starting with a type safe language in the first place?

    The more advanced aspects of Coverity’s product suite come in the form of semantic verification, such as lock verification, custom checkers, and so on. While the mechanisms involved may be easier to deal with than historic formal verification approaches, they do start to take on the the intellectual overhead of more traditional formal verification. In large part, this is because they require reasoning about the invariants of your program — something that many programmers (especially when working with products that have evolved incrementally over many years) have trouble doing. Often as not, invariants aren’t documented or don’t exist, and without invariants it’s hard to prove anything.

    Robert

    Comment by Robert Watson — 16 Aug 2009 @ 16:43

  2. Ben, I would love for you to read this paper to be presented at SOSP on seL4 and then to revise this post.

    I fear your knowledge of the state of the art in formal methods is incomplete.

    Comment by Toby — 16 Aug 2009 @ 21:07

  3. “I was intending to also talk a bit about things I think actually are useful for security, but I think I’ll leave that for a later post.”

    Oh pretty please do 🙂

    Comment by Carl — 17 Aug 2009 @ 9:00

  4. Thanks for the response Ben. To follow-up: would a verified security microkernel prevent a whole class of problems (eg buffer overflows), and therefore let coders turn their attention to the higher-level security issues that remain within strongly-isolated drivers/apps? Or would you claim those more systemic problems can also be dealt with effectively without the formal verification?

    Comment by Ian Brown — 21 Aug 2009 @ 11:17

  5. Regarding static analysis of C, it works great if you don’t expect miracles. In 2002, I wrote a super-simple GCC extension for OpenBSD to check that the actual declared size of static buffers was the same as that passed in to a function such as strlcpy(2). Over the years, it’s been run over the 5000+ apps in the ports tree and found ~100 bugs, some exploitable, with no false positives at all.

    After that, I got very enthusiastic about static analysis and ran into the false-positive brick wall when trying to do more complex things.

    However, using static analysis tools in order to enforce simple invariants such as not mixing up buffer sizes, or not messing up the order of memset, is incredibly useful, and let you run a smarter “grep” over an entire source tree (useful in OpenBSD where everything is in one place). Text processing doesn’t cut it when there are layers of cpp macros…

    Also, clang enables XCode in Snow Leopard to have the incredibly cool control-flow arrows. How can you argue with pretty graphics? 🙂

    Comment by Anil Madhavapeddy — 20 Sep 2009 @ 16:52

  6. […] response to my not-so-recent rants on formal methods I was told to go and read up on […]

    Pingback by Links » seL4 — 23 Sep 2009 @ 13:13

RSS feed for comments on this post.

Sorry, the comment form is closed at this time.

Powered by WordPress