NULL ptr dereferences found with Calysto static checker

[Ken Raeburn]

>> I played a bit with Splint some time
>> back, and one of its most glaring problems was the inability to
>> understand stuff like that -- in particular, realloc() success and
>> failure paths.
>
> Note that Calysto is a completely different beast. It's fully
> path-sensitive. For instance, Calysto easily proves (in 0.02 sec) that
> the following assertion is always satisfied:
>
> int f(int a, int b) {
>    int a1;
>    if (a%2) { a1 = a + 1; }
>    else { a1 = a; }
>    int c = a1 * a1;
>    assert(c % 4 == 0);
> }

If I felt like being picky, I'd point out that overflow in signed  
integer arithmetic in C produces undefined results according to the  
standard, so the assertion may not be met. :-)

> Currently, assertion-checking is not yet ready for mass- 
> consumption, but
> NULL-ptr dereference checking is very close. As Calysto evolves,
> projects that join Calysto Community will also get assertion checking.

That sounds great.

>> Is it possible to save the analyzed behavior of some functions or
>> their uses, maybe programmatically transform some subset of it into
>> some input format acceptable to Calysto (e.g., do you have an input
>> file that describes strncmp and gethostbyname to it?), and import the
>> result into an analysis of another module?
>
> It is doable, but IMHO, static checker should do checking not linking
> :-). So, I prefer to get a complete input, and specify only a few most
> important external functions through additional constraints.

Sure, that makes sense.  I'm just thinking about, down the road,  
being able to automatically generate descriptions of libraries, for  
use in checking applications in other packages where you don't  
generally pull together the sources of both library and application  
to build...  That's more about production use and friendly UIs, than  
getting the analysis portions well tuned.

> After spending a couple of hours analyzing your build process, I found
> the culprit: export-check.pl fails. After commenting lines 74 & 76,
> everything went through, producing 14 shared libraries and 65  
> binaries.

Interesting, though in hindsight, if you're intercepting compiler and  
linker commands, I'm not surprised that something's going on that  
export-check.pl doesn't like.  I wish I'd thought of that possibility  
before.

> I've run Calysto, and after 13.4 hours of computation got 784  
> warnings,
> which is quite a lot considering the size of the project. Roughly one
> third is in libkrb5.so.

Wow.  Much less impressive of us than you reported before. :-)  But,  
I'm not too surprised.

> I've attached the log. Please, check it out and sort binaries that  
> have
> unique_locations!=0 by priority, at least give me the top-ten most
> important ones. Note that since binaries share some code, some
> warnings are reported multiple times. After a quick analysis of the
> reports, it seems that there are 784 unique ones. Binaries are named
> source_path_binary_name.bc.

Okay.  I see from your listing that I forgot about several test  
programs we normally build but don't install.

At the top of the list, I think I'd put the main server programs:  
krb5kdc kadmind krb524d.

Next would probably be the setuid programs v4rcp and ksu, and kprop.

Perhaps then, some simple programs that exercise some key client-side  
functionality: kinit and kvno (though kvno was listed with 0 "unique  
locations").  While the programs themselves may not be the most  
critical from a security perspective, the functionality they exercise  
is crucial to most client-side Kerberos software.  Also ftpd, ftp,  
and kadmin, to exercise other parts of the GSSAPI code.

I guess that would be my top-ten list.

And then the other installed programs and the libraries would bring  
up the end of the list, I guess, probably libraries first.  Most of  
the interesting library routines should already be checked by  
analyzing the programs above, but there are undoubtedly some  
interfaces we don't directly use.

> As soon as I get the 'top-list', I'll start analyzing and  
> postprocessing
> the reports, and send them to krbcore-security at mit when done.

Thanks!

> Note that that script is quite a bit out of date, and I've changed
> it in the meantime. After I move to the new LLVM 2.0, I'll resend the
> new scripts so that people can compile their own code into bc files,
> saving my time. In the meantime, I'll have to explore the beauty of
> inventive build systems on my own :-)

I'm glad you're feeling adventurous. :-)

Ken