Messages in this thread | | | Date | 06 Jan 2000 22:35:00 +0200 | From | (Kai Henningsen) | Subject | Re: Super Lint |
| |
vonbrand@sleipnir.valparaiso.cl (Horst von Brand) wrote on 02.01.00 in <200001021555.MAA01783@sleipnir.valparaiso.cl>:
> Jeff Dike <jdike@karaya.com> said: > > [ 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. > > One start in that direction (that I don't particularly like, BTW, as it > needs much assistance from the programmer, and seems to make certain legal > constructions like handling linked lists totally impossible) is lclint, > from somewhere on MIT AFAIR.
If it makes linked lists impossible, it's going about things the wrong way.
> For full generality you need a complete and sound formal semantic for > C. And that is _extremely_ hard, if indeed possible. In the end, you will
The really hard part is the stuff about sequence points and how they make for undefined behaviour. I gather the C0X draft currently has an appendix that has a somewhat formal for exactly this.
> hit the halting problem, so you will _always_ underestimate the "can't > happen", and that is exactly what irritates me the most of such tools.
I'm not quite sure if you think it's going to find too many or too few bugs.
Anyway, as anyone who's done mathematical proofs knows, you don't really need the fully general thing anyway. That's what you have a programmer for. You tell the thing what is supposed to happen, and the thing verifies that this is indeed what happens, or otherwise tells you that it can't figure this out and you'll have to look for yourself.
Currently, you have to control _everything_. With such a tool, you should be able to reduce this to very few parts of a program.
It's far easier to check a few small routines than to check all of a big program. Just as it's easier to verify that a call to snprintf gives the right buffer size, and that snprintf does the right thing with a buffer size, than that a call to sprintf will never overflow a buffer.
In fact, good advice for writing security-critical code is to design interfaces to avoid these problems in the first place.
If you absolutely must have variable-sized buffers, always have a buffer length in the parameter list. Better would be to only handle a buffer descriptor around that points to a buffer the called routine can adjust the size of as needed - has the added benefit of avoiding hardcoded maximum sizes.
> BTW, much of what you are describing is exactly what the compiler has to do > to discover optimization oportunities. I assume that is why lints fell > into disfavour, partly because of ANSI C prototypes (the original lint > served mostly to detect mismatches between declarations and uses) and stuff > like gcc's -Wall can be had almost for free in the compiler.
Also because, while there was a free gcc, there wasn't a free lint for quite a long time.
MfG Kai
- To unsubscribe from this list: send the line "unsubscribe linux-kernel" in the body of a message to majordomo@vger.rutgers.edu Please read the FAQ at http://www.tux.org/lkml/
| |