Re: Strategies for teaching secure coding practices

[Crispin Cowan <crispin () immunix com>]

Brian Chess wrote:


David Crocker wrote:
 


An alternative way is to *prove* that all inputs are within bounds ... This
approach is more or less impossible to apply if you are coding in C or C++.
It may be feasible if you are using Java (using tools such as ESC/Java) ...
   


Funny you should mention that.  My dissertation focused on showing that you
can apply Extended Static Checking to the problem of finding some common
types of security vulnerabilities in real C programs.  (Common types of
security vulnerabilities being things like buffer overflow, race conditions,
and format string vulnerabilities.)

In type-unsafe languages like C, where you can do arbitrary arithmetic 
on a void * pointer, proving type safety is semi-decidable. You can 
*sometimes* prove that a C program is type safe, a trivial example being 
to look for pointer arithmetic, and if the program doesn't use pointer 
arithmetic then it is much easier to prove type safety. Unfortunately, 
many C programs contain enough type-unsafe crap that it is impractical 
to prove type safety, in many cases because the program is type-unsafe :)


The difference between what David speaks of and what Brian speaks of is 
that David hopes to prove that a program is safe, while Brian can detect 
that a program is unsafe. This may sound like two sides of the same 
coin, but in practice there is a large gap between the two: undecidable 
C programs that don't have detectable vulnerabilities, but also cannot 
be proven to be safe. The main advantage of type safe languages like 
Java and ML is to close that gap.


Where you *cannot* close the gap (must run a large C application that 
cannot be proved safe) we provide run-time intrusion prevention tools in 
Immunix OS: StackGuard, FormatGuard, SubDomain, etc. Marketing crap 
deleted for your convenience, but you can read about it here 
http://www.immunix.com/shop/ and here http://www.immunix.org/


Crispin

--
Crispin Cowan, Ph.D.  http://immunix.com/~crispin/
CTO, Immunix          http://immunix.com
Immunix 7.3           http://www.immunix.com/shop/