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 security. 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 caught. 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 www.eschertech.com
