Re: Super Lint (was: Unexecutable Stack / Buffer Overflow

[Randall R Schulz]

Jeff,

You're exactly right. If you don't recognize the "knowledge-based" 
aspect of this problem and try to apply an ad-hoc approach, it's very 
unlikely you'll ever come up with a really useful tool.

Offhand, I'd say that to make this concept work one would need to 
apply conventional compiler construction techniques (lexical and 
syntax analysis, of course, but more importantly, as much data flow 
analysis as you can muster), plus an open-ended, declarative KB with 
a suitable inference engine.

Given all this and lots of work developing the KB representing the 
tests to apply (and that's got to be ongoing work, as the exploits 
and the understanding of them evolve), this concept would probably be 
feasible. It would require domain experts in information system 
security and processor architectures, knowledge engineers, people 
with in-depth compiler expertise and a good software engineering team 
if you wanted to support this.

I would not start from "scratch," naturally. Obviously one would use 
the available compiler construction tools and, if you add access to 
it, much of an optimizing compiler would be helpful, too (GCC / EGCS, 
is an obvious candidate). More importantly, I'd also employ a mature 
KB system such as Cyc for the knowledge-based aspects. Not to avail 
one's self of these tools would only add unnecessarily to the work 
required to realize this concept.

It's a lot of work, no doubt about it, but I certainly does sound fascinating.

Randy Schulz
Teknowledge Corp.
Palo Alto, CA USA

At 22:56 -0500 1/1/00, Jeff Dike wrote:
>[ Resend - accidentally sent it as a private reply instead of to the list...]
>
>  > Is this 'super-lint' something that could/should be implemented in
>  > something like 'cxref' and included in documentation?
>
>This super-lint is not something that you're going to toss into cxref.  It's a
>hard problem.
>
>I spent quite a while working on exactly this.  I got fed up with it about a
>year ago and decided to do something easier, like porting the kernel to
>user-space.
>
>What I have is essentially a theorem-prover, with the theorems to be proved
>generated from the code being analyzed.  E.g. "x[i] = 0" would generate the
>following theorems: "x is a valid pointer, the low bound of x is <= 0, and the
>high bound of x is >= i".  It would backtrack through the code along every
>path reaching the "x[i] = 0" proving in each case that the theorems are true
>or that the path is logically impossible.
>
>I believe that what I have now is on the right track to a workable tool (which
>is saying a lot considering the number of dead-ends I've gone down), but it
>still needs quite a lot of work.
>
>				Jeff
>
>
>
>-
>To unsubscribe from this list: send the line "unsubscribe linux-kernel" in
>the body of a message to [e-mail]
>Please read the FAQ at http://www.tux.org/lkml/