Secure Coding mailing list archives
Re: Theoretical question about vulnerabilities
From: Nash <nash () solace net>
Date: Tue, 12 Apr 2005 04:18:15 +0100
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?
By "bounded" I take you to mean "finite." In particular with reference to your taxonomy below. By "enumerate" I take you to mean list out in a finite way. Please note, these are not the standard mathematical meanings for these terms. Though, they may be standard for CS folks. If I interpreted you correctly, then the answer is, "no," as Crispin indicated. However, let's take "enumerate" to mean "list out, one by one" and allow ourselves to consider infinite enumerations as acceptable. In this case, the answer becomes, "yes." This proof is abbreviated, but should be recognizable as a pretty standard argument by those familiar with computable functions and/or recursive function theory. Thm. The set of exploits for a program is enumerable. Pf. Let P(x) be a program computing the n-ary, partially computable function F(x). Let an "exploit" be a natural number input, y, such that at some time, t, during the computation performed by P(y) the fixed memory address, Z, contains the number k.** Then, there exists a computable function G(x,t) such that: - G(x, t) = 1 if and only if P(x) gives value k to address Z at some time less than or equal to t. - G(x, t) = 0 otherwise. The values of x for which G(x,t) = 1 is effectively enumerable (in the infinite sense) because it is the domain of a computable function. Q.E.D. You can look up the relevent theory behind this proof in [Davis]. So, where does this leave us? Well, what we don't have is a computable predicate, "Exploit(p,y)", that always tells us if y is an exploit for the program p. That's what Crispin was saying about Turing. This predicate is equivalently hard to "Halt(p,y)", which is not computable.**** However, we can enumerate all the inputs that eventually result in the computer's state satisfying the (Z == k) condition. I suspect this is probably all you really need for a given program, as a practical matter. Since, for example, most attackers probably will not wait for hours and hours while an exploit develops.***** I think the real issue here is complexity, not computability. It takes a long time to come up with the exploits. Maybe the time it takes is too long for the amount of real economic value gained by the knowledge of what's in that set. That seems to be part of Crispin's objection (more or less).
I would think that what makes it possible to talk about design patterns and attack patterns is that they reflect intentional actions towards "desirable" (for the perpetrator) goals, and the set of desirable goals is bounded at any given time (assuming infinite time then perhaps it is not bounded).
I think this is a very reasonable working assumption. It seems consistent with my experience that given any actual system at any actual point in time there are only finitely many "desirable" objectives in play. There are many more theoretical objectives, though, so how you choose to pare down the list could determine whether you end up with a useful scheme, or not.
All we can hope is to come reasonably close and produce something useful, but not theoretically strong and closed.
I think that there's lots of work going on in proof theory and Semantics that makes me hopeful we'll eventually get tools that are both useful and strong. Model Checking is one approach and it seems to have alot of promise. It's relatively fast, e.g., and unlike deductive approaches it doesn't require a mathematician to drive it. See [Clarke] for details. [Clarke] is very interesting, I think. He explicitly argues that model checking beats other formal methods at dealing with the "state space explosion" problem. Those with a more practical mind-set are probably laughing that beating the other formal methods isn't really saying much because they are all pretty awful. ;-)
Is it enough to look for violations of some invariants (rules) without knowing how they happened?
In the static checking sense, I don't see how this could be done.
Any thoughts on this? Any references to relevant theories of failures and errors, or to explorations of this or similar ideas, would be welcome.
There are academics active in this field of research. Here's a few links: http://cm.bell-labs.com/cm/cs/what/spin2005/ http://www.google.com/search?q=international+SPIN+workshop&start=0&start=0&ie=utf-8&oe=utf-8&client=firefox-a&rls=org.mozilla:en-US:official ciao, -nash Notes: ** This definition of "exploit" is chosen more or less arbitrarily. It seems reasonable to me. It might not be. I would conjecture that any definition of "exploit" would be equivalent to this issue, though. **** Halt(x,y) is not computable, but it is enumerable. That is, I can list out, one by one, all the inputs y on which program x eventually halts. I just don't get them in any kind of useful order. And, there is no program to list out the inputs on which program x never halts. ****** It would be extremely interesting to know how many exploits could be expected after a reasonable period of execution time. It seems that as execution time went up we'd be less likely to have an exploit just "show up". My intuition could be completely wrong, though. References: [Davis] "Computability, Complexity, and Languages", 2nd Ed., Martin Davis, Ron Sigal, Elaine Weyuker, Elsevier Science, 1983, 1994. ISBN: 0-12-206382-1 [Clarke] "Model Checking", E.M. Clarke, MIT PRess, 1999. -- An ideal world is left as an exercise for the reader. - Paul Graham
Current thread:
- RE: Theoretical question about vulnerabilities, (continued)
- RE: Theoretical question about vulnerabilities David Crocker (Apr 11)
- Re: Theoretical question about vulnerabilities Crispin Cowan (Apr 12)
- Re: Theoretical question about vulnerabilities der Mouse (Apr 12)
- RE: Theoretical question about vulnerabilities David Crocker (Apr 12)
- Re: Theoretical question about vulnerabilities der Mouse (Apr 12)
- RE: Theoretical question about vulnerabilities David Crocker (Apr 13)
- Re: Theoretical question about vulnerabilities Crispin Cowan (Apr 13)
- RE: Theoretical question about vulnerabilities David Crocker (Apr 14)
- Re: Theoretical question about vulnerabilities Crispin Cowan (Apr 15)
- RE: Theoretical question about vulnerabilities David Crocker (Apr 17)
- RE: Theoretical question about vulnerabilities David Crocker (Apr 11)
- Re: Theoretical question about vulnerabilities Crispin Cowan (Apr 12)
- Re: Theoretical question about vulnerabilities der Mouse (Apr 13)
- Re: Theoretical question about vulnerabilities Nash (Apr 13)
- RE: Theoretical question about vulnerabilities David Crocker (Apr 13)
- Re: Theoretical question about vulnerabilities Crispin Cowan (Apr 13)
- RE: Theoretical question about vulnerabilities David Crocker (Apr 14)