[cap-talk] Security by safe language processing

[David-Sarah Hopwood]

John Carlson wrote:
> Can diverse double compiling disprove Godel's (sorry don't know how to  
> generate the umlaut) incompleteness theorems?

I don't see the relevance of either of Gödel's incompleteness theorems.
We do not need any complete formal system in order to build a secure
computing system -- the obstacles to building secure systems are a matter
of engineering difficulty and avoiding human mistakes and design errors;
not formal impossibility results.

In more detail, here's why I think that such impossibility results
(not just those of Gödel) are irrelevant. The gist of these results,
as they apply to security engineering, is that many systems (e.g.
logics, programming languages, models of computation, security policy
frameworks, etc.) have instances that are too difficult to analyse for
interesting safety properties. That is, a particular instance may have
some safety property, but there is no general method to prove whether it
does.

But such results do *not* say that it is impossible, or even difficult,
to recognise which instances might be in the difficult-to-analyse set.
So for the purpose of building a secure system, we implement a program
that checks whether an instance is easy-to-analyse *and* has the
desired safety properties. Instances that are too difficult are just
conservatively rejected. Provided that this does not limit the
expressiveness of the system too much, there's no problem with this
approach. In practice, the instances for which it is too difficult to
mechanically prove safety, are best avoided anyway because they are
also too hard for humans to understand and maintain.

-- 
David-Sarah Hopwood  ⚥  http://davidsarah.livejournal.com