Ben Laurie blathering

More Security Pie In The Sky

The Institute for Public Policy Research have a report called “A national security strategy for the UK”. They want money for it, though, so you might prefer the executive summary, even if you aren’t an executive.

Recommendation 60: The Government should also approach the European Commission and the incoming Swedish Presidency to sponsor a programme for the creation of a range of secure and reliable standard software modules (such as simple operating systems, database management systems and graphical user interfaces). These modules should be developed using formal methods and be made available free of charge through an open source licence to encourage their widespread use.

I’m with them on a range of secure and reliable standard software modules. I’m with them on the free/open source front. I’m even mostly with them on their example modules, though I would say that a secure GUI is less of a software engineering problem and more of an HCI problem. But formal methods? We have essentially zero examples of useful systems that have been shown to be secure using formal methods, so why make this recommendation? Are these things written entirely by people looking for funding? Clearly they’re not written by people who want to solve the problem, or they’d make suggestions that might actually lead to a solution.


  1. What about the Tokeneer project? Does that count?

    Comment by Michael — 7 Jul 2009 @ 13:37

  2. seL4 would be a counter-example to your assertion, depending on one’s interpretation of “useful” and “essentially”.

    I would argue that you’re underestimating what can be achieved in the formal methods space today. (I would be interested to know if the progress reported in the paper linked to above is above what you had expected could be reasonably achieved in this space when reading the exec summary you linked to.)

    Finally, if you’re still not convinced, 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?

    Comment by Toby — 7 Jul 2009 @ 13:59

  3. Well, it looks like the IPPR haven’t been reading their Knuth, for sure.

    Also, when did anyone last hear of someone running anything on a Viper CPU?

    Comment by Dave Walker — 7 Jul 2009 @ 18:37

  4. Ben – do you think a formally verified microkernel that enforces security controls within an OS is achievable/desirable?

    Comment by Ian Brown — 8 Jul 2009 @ 14:22

  5. Disparaging the entire field of ‘formal methods’ as being useless is a little harsh.

    Modern type systems spring from a solid formal footing, and mainstream languages are adopting functional features (e.g. C# and F#). Haskell is increasingly used for mission-critical applications. There’s a nice array of talks at CUFP 2009 this year on the commercial uses of functional programming (

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

    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.

    Comment by Anil Madhavapeddy — 7 Aug 2009 @ 17:00

  6. […] while back, I had a bash at formal methods. Reasonably enough, some people had a bash back. I feel I should […]

    Pingback by Links » Useful Security — 16 Aug 2009 @ 15:59

RSS feed for comments on this post.

Sorry, the comment form is closed at this time.

Powered by WordPress