Pascal Meunier wrote:

Do you think it is possible to enumerate all the ways all vulnerabilities can be
created?  Is the set of all possible exploitable programming mistakes bounded?

No. It's not so much a programming problem, more a specification problem.

Tools now exist that make it possible to develop single-threaded programs that
are mathematically proven to meet their specifications. The problem is knowing
what should be included in the specifications. Let me give you some examples:

1. Buffer overflow. Even if nobody realised that buffer overflows could be used
to bypass security, it is an implied specification of any program that no array
should ever be accessed via an out-of-bounds index. All the tools out there for
proving software correctness take this as a given. So buffer overflows can
always be avoided, because if there is ANY input whatsoever that can produce a
buffer overflow, the proofs will fail and the problem will be identified. You
don't even need to write a specification for the software in this case - the
implied specification is enough.

2. SQL injection. If the required behaviour of the application is correctly
specified, and the behaviour of the SQL server involved is also correctly
specified (or at least the correct constraints are specified for SQL query
commands), then it will be impossible to prove the software is correct if it has
any SQL injection vulnerabilities. So again, this would be picked up by the
proof process, even if nobody knew that SQL injection can be used to breach

3. Cross-site scripting. This is a particular form of "HTML injection" and would
be caught by the proof process in a similar way to SQL injection, provided that
the specification included a notion of the generated HTML being well-formed. If
that was missing from the specification, then HTML injection would not be

4. Tricks to make the browser display an address in the address bar that is not
the address of the current HTML page. To catch these, you would need to include
in the specification, "the address bar shall always show the address of the
current page". This is easy to state once you know it is a requirement; but
until last year it would probably not have been an obvious requirement.

In summary: If you can state what you mean by "secure" in terms of what must
happen and what must not happen, then by using precise specifications and
automatic proof, you can achieve complete security for all possible inputs -
until the definition of "secure" needs to be expanded.

This should have consequences for source code vulnerability analysis software.
It should make it impossible to write software that detects all of the mistakes
themselves.  Is it enough to look for violations of some invariants (rules)
without knowing how they happened?

The problem is that while you can enumerate the set of invariants that you
currently know are important, you don't know how the set may need to be expanded
in the future.

David Crocker, Escher Technologies Ltd.
Consultancy, contracting and tools for dependable software development

Reply via email to